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

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

T-нормы — это бинарные функции на интервале [0, 1], которые в нечёткой логике обычно используются для моделирования связки конъюнкции. Если ${\displaystyle a,b\in [0,1]}$ — степени уверенности в утверждениях ${\displaystyle A}$ и ${\displaystyle B}$, тогда для составного утверждения «${\displaystyle A}$ и ${\displaystyle B}$» степень уверенности ${\displaystyle a*b}$ вычисляется через t-норму ${\displaystyle *}$. T-норма ${\displaystyle *}$ должна удовлетворять свойствам:

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

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

монотонность: если ${\displaystyle a\leqslant b}$ и ${\displaystyle c\leqslant d}$, то ${\displaystyle a*c\leqslant b*d}$,

и обладает единицей ${\displaystyle 1*a=a}$.

Заметим, что в этом списке отсутствует свойство идемпотентности ${\displaystyle a*a=a}$; максимум, что можно получить — ${\displaystyle a*a\leqslant 1*a=a}$. На первый взгляд может показаться странным быть менее уверенным в «${\displaystyle A}$ и ${\displaystyle A}$», чем просто в ${\displaystyle A}$, однако жёсткое требование монотонности и естественное стремление допускать возможность того, что уверенность в «${\displaystyle A}$ и ${\displaystyle B}$» меньше, чем в каждом из ${\displaystyle A}$ и ${\displaystyle B}$, приводит к неравенству ${\displaystyle a*b<a\leqslant b}$, а значит ${\displaystyle a*a\leqslant a*b<a}$. Иными словами, t-норма учитывает только числовые значения уверенности, не различая «${\displaystyle A}$ и ${\displaystyle A}$» и «${\displaystyle A}$ и ${\displaystyle B}$», если уверенности одинаковы.

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

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

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

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

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

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

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

С алгебраической точки зрения, операция ${\displaystyle \Rightarrow }$ называется резидуумом t-нормы ${\displaystyle *}$, если для любых ${\displaystyle a}$, ${\displaystyle b}$ и ${\displaystyle c}$ выполняется

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

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

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

что связано с возможностью преобразовать доказательство ${\displaystyle C}$ из ${\displaystyle A\otimes B}$ в доказательство ${\displaystyle B\to C}$ из ${\displaystyle A}$ введением импликации, и обратно. Лево-непрерывность t-нормы — необходимое и достаточное условие существования такой связи между t-нормой как конъюнкцией и её резидуумом как импликацией.

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

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

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

Часто также используются следующие определяемые связки:

• Отрицание ${\displaystyle \neg }$ (унарная), определяется как

${\displaystyle \neg A\equiv A\rightarrow \bot }$

• Эквиваленция ${\displaystyle \leftrightarrow }$ (бинарная), определяется как

${\displaystyle A\leftrightarrow B\equiv (A\rightarrow B)\wedge (B\rightarrow A)}$

Для MTL это эквивалентно ${\displaystyle (A\rightarrow B)\otimes (B\rightarrow A)}$.

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

${\displaystyle A\vee B\equiv ((A\rightarrow B)\rightarrow B)\wedge ((B\rightarrow A)\rightarrow A)}$

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

${\displaystyle \top \equiv \bot \rightarrow \bot }$

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

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

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

из ${\displaystyle A}$ и ${\displaystyle A\rightarrow B}$ выводится ${\displaystyle B}$.

Аксиомы задаются следующими схемами:

${\displaystyle {\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)^[3]. Аксиомы (MTL4a)–(MTL4c) заменяют аксиому делимости (BL4) BL. Аксиомы (MTL5a) и (MTL5b) выражают закон резидуации, а аксиома (MTL6) соответствует условию прелинейности. Аксиомы (MTL2) и (MTL3) в оригинальной системе были позднее признаны избыточными (Хваловский, 2012; Чинтула, 2005). Все остальные аксиомы независимы (Хваловский, 2012).

Как и в других пропозициональных t-норма нечётких логиках, для MTL основное значение имеют алгебраические семантики. Рассматриваются три основные класса алгебраических структур, по отношению к которым эта логика полна:

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

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

• ${\displaystyle (L,\wedge ,\vee ,0,1)}$ — ограниченная решётка c нулём 0 и единицей 1,
• ${\displaystyle (L,\ast ,1)}$ — коммутативный моноид,
• ${\displaystyle \ast }$ и ${\displaystyle \Rightarrow }$ образуют галоисово соответствие, то есть ${\displaystyle z*x\leq y}$ тогда и только тогда, когда ${\displaystyle z\leq x\Rightarrow y}$, где ${\displaystyle \leq }$ — порядок решётки ${\displaystyle (L,\wedge ,\vee )}$ для любых ${\displaystyle z,x,y\in L}$ («условие резидуации»),
• ${\displaystyle (x\Rightarrow y)\vee (y\Rightarrow x)=1}$ для любых ${\displaystyle x}$, ${\displaystyle y}$ в ${\displaystyle L}$ («условие прелинейности»).

Важные примеры: стандартные MTL-алгебры на интервале [0, 1]; все булевы алгебры, линейные гейтинговы алгебры (обе с ${\displaystyle \ast =\wedge }$), все MV-алгебры, все BL-алгебры и др. Поскольку условие резидуации эквивалентно системе тождеств^[4], MTL-алгебры образуют разновидность.

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

• Сильная конъюнкция — операцией моноида ${\displaystyle \ast }$
• Импликация — операцией ${\displaystyle \Rightarrow }$ (резидуум ${\displaystyle \ast }$)
• Слабые «и»/«или» — операциями решётки ${\displaystyle \wedge }$ и ${\displaystyle \vee }$ соответственно
• Пропозициональные константы нуль и единица — константы 0 и 1
• Эквиваленция определяется операцией ${\displaystyle \Leftrightarrow }$ как

${\displaystyle x\Leftrightarrow y\equiv (x\Rightarrow y)\wedge (y\Rightarrow x)}$

Благодаря прелинейности это эквивалентно определению через ${\displaystyle \ast }$ вместо ${\displaystyle \wedge }$:

${\displaystyle x\Leftrightarrow y\equiv (x\Rightarrow y)\ast (y\Rightarrow x)}$

• Отрицание — определяемая операция ${\displaystyle -x\equiv x\Rightarrow 0}$

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

${\displaystyle {\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. Некоторые формулы (например, p → p) выполнимы в любой MTL-алгебре — это таутологии MTL.

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

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

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

MTL-алгебры — это все алгебры, в которых логика MTL корректна. Дополнительно справедлива теорема о сильной полноте:^[5]

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

Как и для других нечетких логик^[6], для MTL-алгебр справедливо свойство линейного субдиректного разложения:

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

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

Это свойство влечёт теорему полноты по линейным MTL-алгебрам (Esteva & Godo, 2001):

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

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

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

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

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