BL (логика)

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

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

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

• Слабая конъюнкция ${\displaystyle \wedge }$ (двуместная), также «решетчатая конъюнкция» (так как всегда реализуется операцией пересечения в алгебраической семантике). В отличие от логики моноидной t-нормы и более слабых субструктурных логик, в BL слабая конъюнкция определяется так:

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

• Отрицание ${\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}}}$ (как константы верх и нуль в субструктурных логиках совпадают в MTL), определяется как

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

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

• Унарные связки (связывают ближе всего)
• Все двуместные связки, кроме импликации и эквиваленции
• Импликация и эквиваленция (связывают наиболее слабо)

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

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

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

${\displaystyle {\begin{array}{ll}{\rm {(BL1)}}\colon &(A\rightarrow B)\rightarrow ((B\rightarrow C)\rightarrow (A\rightarrow C))\\{\rm {(BL2)}}\colon &A\otimes B\rightarrow A\\{\rm {(BL3)}}\colon &A\otimes B\rightarrow B\otimes A\\{\rm {(BL4)}}\colon &A\otimes (A\rightarrow B)\rightarrow B\otimes (B\rightarrow A)\\{\rm {(BL5a)}}\colon &(A\rightarrow (B\rightarrow C))\rightarrow (A\otimes B\rightarrow C)\\{\rm {(BL5b)}}\colon &(A\otimes B\rightarrow C)\rightarrow (A\rightarrow (B\rightarrow C))\\{\rm {(BL6)}}\colon &((A\rightarrow B)\rightarrow C)\rightarrow (((B\rightarrow A)\rightarrow C)\rightarrow C)\\{\rm {(BL7)}}\colon &\bot \rightarrow A\end{array}}}$

Аксиомы (BL2) и (BL3) изначальной системы аксиом были показаны избыточными^[2][3]. Остальные аксиомы показаны независимыми^[2].

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

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