Моноидальная t-нормальная логика

В математической логике , моноидальная логика основанная на t-норме (или сокращенно MTL ), логика непрерывных слева t-норм , является одной из нечетких логик t-нормы . Она принадлежит к более широкому классу субструктурных логик или логик резидуальных решеток ; Хёле он расширяет логику коммутативных ограниченных целочисленных резидуированных решеток (известную как моноидальная логика Оно _{, FL ew} или интуиционистская логика без сжатия) с помощью аксиомы прелинейности.

Мотивация

В нечеткой логике вместо того, чтобы рассматривать утверждения как истинные или ложные, мы связываем каждое утверждение с числовой достоверностью этого утверждения. По соглашению доверительные интервалы варьируются в пределах единичного интервала. $[0,1]$, где максимальная достоверность $1$ соответствует классическому понятию истинной и минимальной достоверности $0$ соответствует классическому понятию ложного.

Т-нормы — это двоичные функции на действительном единичном интервале [0, 1], которые в нечеткой логике часто используются для представления соединительной связки ; если $a,b\in [0,1]$ это уверенность, которую мы приписываем утверждениям $A$ и $B$ соответственно, тогда используется t-норма $*$ рассчитать уверенность $a*b$ приписано составному высказыванию ' $A$ и $B$'. Т-норма $*$ должен удовлетворять свойствам

коммутативность $a*b=b*a$,

ассоциативность $(a*b)*c=a*(b*c)$,

монотонность — если $a\leqslant b$ и $c\leqslant d$ затем $a*c\leqslant b*d$,

и имеющий 1 в качестве идентификационного элемента $1*a=a$.

Примечательно, что в этом списке отсутствует свойство идемпотентности. $a*a=a$; самое близкое, что можно получить, это то, что $a*a\leqslant 1*a=a$. Быть менее уверенным в себе может показаться странным. $A$ и $A$', чем просто $A$, но обычно мы хотим, чтобы уверенность $a*b$ в комбинированном ' $A$ и $B$' быть меньше, чем уверенность $a$ в $A$ и уверенность $b$ в $B$, а затем порядок $a*b<a\leqslant b$ по монотонности требует $a*a\leqslant a*b<a$. Другими словами, t-норма может учитывать только доверительные отношения как числа, а не причины, которые могут лежать в основе приписывания этих доверительных отношений; таким образом, он не может лечить ' $A$ и $A$'в отличие от' $A$ и $B$, где мы одинаково уверены в обоих».

Потому что символ $\wedge$ поскольку его использование в теории решеток очень тесно связано со свойством идемпотентности, может быть полезно переключиться на другой символ для соединения, который не обязательно является идемпотентным. В традиции нечеткой логики иногда используют $\&$ для этого «сильного» союза, но эта статья следует традиции субструктурной логики использования $\otimes$ для сильного союза; таким образом $a*b$ это уверенность, которую мы приписываем утверждению $A\otimes B$ (все еще читаю ' $A$ и $B$', возможно, с «сильным» или «мультипликативным» в качестве уточнения «и»).

Формализовав союз $\otimes$, хочется продолжить с другими связками. Один из подходов к этому — представить отрицание как карту, меняющую порядок. $[0,1]\longrightarrow [0,1]$, затем определяя оставшиеся связки, используя законы Де Моргана , материальную импликацию и тому подобное. Проблема при этом заключается в том, что результирующая логика может иметь нежелательные свойства: она может быть слишком близка к классической логике или, если не наоборот, не поддерживать ожидаемые правила вывода . Альтернативой, которая делает последствия различных выборов более предсказуемыми, является продолжение импликации. $\to$ в качестве второй связки: в целом это наиболее распространенная связка в аксиоматизациях логики, и она имеет более тесную связь с дедуктивными аспектами логики, чем большинство других связок. Доверительный аналог $\Rightarrow$ импликационной связки фактически может быть определена непосредственно как остаток t-нормы.

Логическая связь между конъюнкцией и импликацией обеспечивается таким фундаментальным явлением, как правило вывода modus ponens. $A,A\to B\vdash B$: от $A$ и $A\to B$ следует $B$. В случае нечеткой логики это более строго записывается как $A\otimes (A\to B)\vdash B$, потому что это ясно показывает, что наша уверенность в предпосылках здесь заключается в том, что в $A\otimes (A\to B)$, а не те, что в $A$ и $A\to B$ отдельно. Итак, если $a$ и $b$ наша уверенность в $A$ и $B$ соответственно, тогда $a\Rightarrow b$ это искомая уверенность в $A\to B$, и $a*(a\Rightarrow b)$ это совокупная уверенность в $A\otimes (A\to B)$. Мы требуем, чтобы

$a*(a{\mathbin {\Rightarrow }}b)\leqslant b$

поскольку наша уверенность $b$ для $B$ не должно быть меньше нашего доверия $a*(a\Rightarrow b)$ в заявлении $A\otimes (A\to B)$ откуда $B$ логически следует. Это ограничивает искомую уверенность $a\Rightarrow b$, и один подход для поворота $\Rightarrow$ в бинарную операцию, например $*$ было бы сделать его как можно большим, соблюдая при этом эту границу:

$a{\mathbin {\Rightarrow }}b\equiv \sup \left\{x\in [0,1]\;{\big |}\;a*x\leqslant b\right\}$.

принимая $x=0$ дает $a*x=a*0\leqslant 1*0=0\leqslant b$, поэтому верхняя грань всегда принадлежит непустому ограниченному множеству и, следовательно, корректно определена. Для общей t-нормы остается возможность, что $f_{a}(x)=a*x$ имеет скачок при $x=a{\mathbin {\Rightarrow }}b$, в этом случае $a*(a{\mathbin {\Rightarrow }}b)$ может выйти строго больше, чем $b$ Несмотря на то $a{\mathbin {\Rightarrow }}b$ определяется как наименьшая верхняя граница $x$это удовлетворяет $a*x\leqslant b$; Чтобы предотвратить это и обеспечить ожидаемый результат строительных работ, мы требуем, чтобы t-норма $*$ является непрерывным слева . Таким образом, остаток непрерывной слева t-нормы можно охарактеризовать как самую слабую функцию, которая делает нечеткий modus ponens действительным, что делает его подходящей функцией истинности для применения в нечеткой логике.

Более алгебраически мы говорим, что операция $\Rightarrow$ является остатком t-нормы $*$ если для всех $a$, $b$, и $c$ это удовлетворяет

$a*b\leq c$ тогда и только тогда, когда $a\leq (b{\mathbin {\Rightarrow }}c)$.

Эта эквивалентность числовых сравнений отражает эквивалентность следствий.

$A\otimes B\vdash C$ тогда и только тогда, когда $A\vdash B\to C$

существует, потому что любое доказательство $C$ из помещения $A\otimes B$ может быть преобразовано в доказательство $B\to C$ из помещения $A$ делая дополнительный шаг введения импликации , и наоборот, любое доказательство $B\to C$ из помещения $A$ может быть преобразовано в доказательство $C$ из помещения $A\otimes B$ выполнив дополнительный шаг устранения последствий . Непрерывность слева t-нормы является необходимым и достаточным условием для сохранения этой связи между соединением t-нормы и ее остаточной импликацией.

Функции истинности дальнейших пропозициональных связок могут быть определены с помощью t-нормы и ее остатка, например, остаточного отрицания. $\neg x=(x{\mathbin {\Rightarrow }}0).$ Таким образом, непрерывная слева t-норма, ее остаток и функции истинности дополнительных пропозициональных связок (см. раздел «Стандартная семантика» ниже) определяют значения истинности сложных пропозициональных формул в [0, 1]. Формулы, результат которых всегда равен 1, тогда называются тавтологиями относительно данной непрерывной слева t-нормы. $*,$ или $*{\mbox{-}}$тавтологии. Набор всего $*{\mbox{-}}$тавтологии называется логикой t-нормы $*,$ поскольку эти формулы представляют собой законы нечеткой логики (определяемые t-нормой), которые выполняются (до степени 1) независимо от степеней истинности атомарных формул . Некоторые формулы являются тавтологиями относительно всех непрерывных слева t-норм: они представляют собой общие законы пропозициональной нечеткой логики, которые не зависят от выбора конкретной непрерывных слева t-норм. Эти формулы образуют логику MTL, которую, таким образом, можно охарактеризовать как логику непрерывных слева t-норм.

Синтаксис

Язык

Язык пропозициональной логики MTL состоит из счетного числа пропозициональных переменных и следующих примитивных логических связок :

• Импликация $\rightarrow$ ( двоичный )
• Сильное соединение $\otimes$ (двоичный). Знак & является более традиционным обозначением сильной связи в литературе по нечеткой логике, тогда как обозначение $\otimes$ следует традиции субструктурной логики.
• Слабое соединение $\wedge$ (двоичный), также называемый решеточной конъюнкцией (поскольку в алгебраической семантике он всегда реализуется решеточной операцией встречи ). В отличие от BL и более сильных нечетких логик, слабая конъюнкция не поддается определению в MTL и должна быть включена в число примитивных связок.
• Нижний $\bot$ ( нулевой — пропозициональная константа ; $0$ или ${\overline {0}}$ являются общими альтернативными токенами, а ноль - общим альтернативным именем для пропозициональной константы (поскольку константы дно и ноль субструктурной логики совпадают в MTL).

Ниже приведены наиболее распространенные определяемые логические связки:

• Отрицание $\neg$ ( унарный ), определяемый как

$\neg A\equiv A\rightarrow \bot$

• Эквивалентность $\leftrightarrow$ (двоичный), определяемый как

$A\leftrightarrow B\equiv (A\rightarrow B)\wedge (B\rightarrow A)$

В MTL определение эквивалентно $(A\rightarrow B)\otimes (B\rightarrow A).$

• (Слабая) дизъюнкция $\vee$ (двоичный), также называемый решеточной дизъюнкцией (поскольку он всегда реализуется решеточной операцией соединения в алгебраической семантике), определяемый как

$A\vee B\equiv ((A\rightarrow B)\rightarrow B)\wedge ((B\rightarrow A)\rightarrow A)$

• Вершина $\top$ (нулевой), также называемый единицей и обозначаемый $1$ или ${\overline {1}}$ (поскольку константы top и ноль субструктурной логики совпадают в MTL), определяемые как

$\top \equiv \bot \rightarrow \bot$

Правильно составленные формулы MTL определяются, как обычно, в логике высказываний . Чтобы сохранить круглые скобки, обычно используется следующий порядок приоритета:

• Унарные связки (связываются наиболее тесно)
• Бинарные связки, кроме импликации и эквивалентности
• Импликация и эквивалентность (наиболее слабая связь)

Аксиомы

Система вывода в стиле Гильберта для MTL была представлена ​​Эстевой и Годо (2001). Его единственное правило вывода — modus ponens :

от $A$ и $A\rightarrow B$ вывести $B.$

Ниже приведены схемы его аксиом :

${\begin{array}{ll}{\rm {(MTL1)}}\colon &(A\rightarrow B)\rightarrow ((B\rightarrow C)\rightarrow (A\rightarrow C))\\{\rm {(MTL2)}}\colon &A\otimes B\rightarrow A\\{\rm {(MTL3)}}\colon &A\otimes B\rightarrow B\otimes A\\{\rm {(MTL4a)}}\colon &A\wedge B\rightarrow A\\{\rm {(MTL4b)}}\colon &A\wedge B\rightarrow B\wedge A\\{\rm {(MTL4c)}}\colon &A\otimes (A\rightarrow B)\rightarrow A\wedge B\\{\rm {(MTL5a)}}\colon &(A\rightarrow (B\rightarrow C))\rightarrow (A\otimes B\rightarrow C)\\{\rm {(MTL5b)}}\colon &(A\otimes B\rightarrow C)\rightarrow (A\rightarrow (B\rightarrow C))\\{\rm {(MTL6)}}\colon &((A\rightarrow B)\rightarrow C)\rightarrow (((B\rightarrow A)\rightarrow C)\rightarrow C)\\{\rm {(MTL7)}}\colon &\bot \rightarrow A\end{array}}$

Традиционная нумерация аксиом, приведенная в левом столбце, получена из нумерации аксиом BL Гаека базовой нечеткой логики . Аксиомы (MTL4a)–(MTL4c) заменяют аксиому делимости (BL4) BL. Аксиомы (MTL5a) и (MTL5b) выражают закон невязки , а аксиома (MTL6) соответствует условию предлинейности . Показано, что аксиомы (MTL2) и (MTL3) исходной аксиоматической системы являются избыточными (Chvalovsky, 2012) и (Cintula, 2005). Показано, что все остальные аксиомы независимы (Хваловский, 2012).

Семантика

Как и в других пропозициональных нечетких логиках с t-нормой , алгебраическая семантика для MTL преимущественно используется с тремя основными классами алгебр , относительно которых логика является полной :

• Общая семантика , сформированная из всех MTL-алгебр — то есть всех алгебр, для которых логика верна.
• Линейная семантика , состоящая из всех линейных MTL-алгебр, то есть всех MTL-алгебр, решетки порядок которых линейный.
• Стандартная семантика , образованная из всех стандартных MTL-алгебр — то есть всех MTL-алгебр, редукцией решетки которых является действительный единичный интервал [0, 1] обычного порядка; они однозначно определяются функцией, интерпретирующей сильную конъюнкцию, которая может быть любой непрерывной слева t-нормой

Общая семантика

MTL-алгебры

Алгебры, для которых верна логика MTL, называются MTL-алгебрами. Их можно охарактеризовать как предлинейные коммутативные ограниченные целочисленные вычетные решетки. Более подробно, алгебраическая структура $(L,\wedge ,\vee ,\ast ,\Rightarrow ,0,1)$ является MTL-алгеброй, если

• $(L,\wedge ,\vee ,0,1)$ представляет собой ограниченную решетку с верхним элементом 0 и нижним элементом 1
• $(L,\ast ,1)$ является коммутативным моноидом
• $\ast$ и $\Rightarrow$ образуют сопряженную пару , т. е. $z*x\leq y$ тогда и только тогда, когда $z\leq x\Rightarrow y,$ где $\leq$ – порядок решетки $(L,\wedge ,\vee ),$ для всех x , y и z в $L$, ( условие невязки )
• $(x\Rightarrow y)\vee (y\Rightarrow x)=1$ выполняется для всех x и y в L ( условие предлинейности )

Важными примерами MTL-алгебр являются стандартные MTL-алгебры на вещественном единичном интервале [0, 1]. Дальнейшие примеры включают все булевы алгебры , все линейные алгебры Гейтинга (обе с $\ast =\wedge$), все MV-алгебры , все BL -алгебры и т. д. Поскольку условие вычетности эквивалентно выражается тождествами, MTL-алгебры образуют разновидность .

Интерпретация логики MTL в MTL-алгебрах

Связки MTL интерпретируются в MTL-алгебрах следующим образом:

• Сильная конъюнкция моноидальной операцией $\ast$
• Последствия операции $\Rightarrow$ называется остатком ( который $\ast$)
• Слабая конъюнкция и слабая дизъюнкция решеточными операциями. $\wedge$ и $\vee ,$ соответственно (обычно обозначаются теми же символами, что и связки, если не может возникнуть путаницы)
• Константы истинности ноль (вверху) и единица (внизу) константами 0 и 1.
• Связка эквивалентности интерпретируется операцией $\Leftrightarrow$ определяется как

$x\Leftrightarrow y\equiv (x\Rightarrow y)\wedge (y\Rightarrow x)$

В силу условия предлинейности это определение эквивалентно тому, которое использует $\ast$ вместо $\wedge ,$ таким образом

$x\Leftrightarrow y\equiv (x\Rightarrow y)\ast (y\Rightarrow x)$

• Отрицание интерпретируется определяемой операцией $-x\equiv x\Rightarrow 0$

При такой интерпретации связок любая оценка e _v пропозициональных переменных в L однозначно распространяется на оценку e всех правильно построенных формул MTL согласно следующему индуктивному определению (которое обобщает условия истинности Тарского ) для любых формул A , B , и любая пропозициональная переменная p :

${\begin{array}{rcl}e(p)&=&e_{\mathrm {v} }(p)\\e(\bot )&=&0\\e(\top )&=&1\\e(A\otimes B)&=&e(A)\ast e(B)\\e(A\rightarrow B)&=&e(A)\Rightarrow e(B)\\e(A\wedge B)&=&e(A)\wedge e(B)\\e(A\vee B)&=&e(A)\vee e(B)\\e(A\leftrightarrow B)&=&e(A)\Leftrightarrow e(B)\\e(\neg A)&=&e(A)\Rightarrow 0\end{array}}$

Неформально, значение истинности 1 представляет полную истину, а значение истинности 0 представляет полную ложность; промежуточные значения истинности представляют собой промежуточные степени истины. Таким образом, формула считается полностью истинной при вычислении e, если e ( A ) = 1. Формула A называется истинной в MTL-алгебре L , если она полностью истинна при всех оценках в L , то есть если e ( A ) = 1 для всех оценок e в L . Некоторые формулы (например, p → p ) справедливы в любой MTL-алгебре; они называются тавтологиями MTL.

Понятие глобального следствия (или: глобального следствия ) определяется для MTL следующим образом: набор формул Γ влечет за собой формулу A (или: A является глобальным следствием Γ) в символах $\Gamma \models A,$ если для любой оценки e в любой MTL-алгебре, когда e ( B ) = 1 для всех формул B в Γ, то также e ( A ) = 1. Неформально глобальное отношение следствий представляет собой передачу полной истины в любой MTL-алгебре. алгебра истинностных значений.

Общие теоремы о корректности и полноте

Логика MTL является корректной и полной по отношению к классу всех MTL-алгебр (Esteva & Godo, 2001):

Формула доказуема в MTL тогда и только тогда, когда она справедлива во всех MTL-алгебрах.

Понятие MTL-алгебры фактически определено таким образом, что MTL-алгебры образуют класс всех алгебр, для которых логика MTL верна. Кроме того, справедлива сильная теорема полноты :

Формула A является глобальным следствием в MTL набора формул Γ тогда и только тогда, когда A выводима из Γ в MTL.

Линейная семантика

Подобно алгебрам для других нечетких логик, MTL-алгебры обладают следующим свойством линейной подпрямой декомпозиции :

Любая MTL-алгебра является подпрямым произведением линейно упорядоченных MTL-алгебр.

( Подпрямое произведение — это подалгебра прямого произведения, что все проекционные отображения сюръективны такая , . MTL-алгебра линейно упорядочена, порядок ее решетки линейный если .)

Вследствие свойства линейной подпрямой декомпозиции всех MTL-алгебр справедлива теорема о полноте в отношении линейных MTL-алгебр (Esteva & Godo, 2001):

• Формула доказуема в MTL тогда и только тогда, когда она справедлива во всех линейных MTL-алгебрах.
• Формула A выводится в MTL из множества формул Γ тогда и только тогда, когда A является глобальным следствием во всех линейных MTL-алгебрах Γ.

Стандартная семантика

Стандартными называются те MTL-алгебры, редукцией решетки которых является действительный единичный интервал [0, 1]. Они однозначно определяются вещественной функцией, интерпретирующей сильную конъюнкцию, которая может быть любой непрерывной слева t-нормой. $\ast$. Стандартная MTL-алгебра, определяемая непрерывной слева t-нормой $\ast$ обычно обозначается $[0,1]_{\ast }.$ В $[0,1]_{\ast },$ представлена ​​остатком импликация $\ast ,$ слабая конъюнкция и дизъюнкция соответственно минимуму и максимуму, а константы истинности ноль и единица соответственно действительным числам 0 и 1.

Логика MTL полна относительно стандартных MTL-алгебр; этот факт выражается стандартной теоремой о полноте (Jenei & Montagna, 2002):

Формула доказуема в MTL тогда и только тогда, когда она справедлива во всех стандартных MTL-алгебрах.

Поскольку MTL полна относительно стандартных MTL-алгебр, определяемых непрерывными слева t-нормами, MTL часто называют логикой непрерывных слева t-норм (аналогично тому, как BL — логика непрерывных t-норм ).

Библиография

• Хайек П., 1998, Метаматематика нечеткой логики . Дордрехт: Клювер.
• Эстева Ф. и Годо Л., 2001, «Логика, основанная на моноидальной t-норме: к логике непрерывных слева t-норм». Нечеткие множества и системы 124 : 271–288.
• Дженей С. и Монтанья Ф., 2002, «Доказательство стандартной полноты моноидальной логики Эстевы и Годо MTL». Студия Логика 70 : ​​184–192.
• Оно, Х., 2003, «Субструктурная логика и остаточные решетки — введение». В Ф. В. Хендриксе, Дж. Малиновском (ред.): Тенденции в логике: 50 лет Studia Logica, Тенденции в логике 20 : 177–212.
• Синтула П., 2005, «Краткая заметка: Об избыточности аксиомы (A3) в BL и MTL». Мягкие вычисления 9 : 942.
• Синтула П., 2006, «Слабо импликативная (нечеткая) логика I: основные свойства». Архив математической логики 45 : 673–704.
• Хваловский К., 2012, « О независимости аксиом в BL и MTL ». Нечеткие множества и системы 197 : 123–129, дои : 10.1016/j.fss.2011.10.018 .