Language

The language of the propositional logic BL consists of countably many propositional variables and the following primitive logical connectives:

• Implication ${\displaystyle \rightarrow }$ (binary)
• Strong conjunction ${\displaystyle \otimes }$ (binary). The sign & is a more traditional notation for strong conjunction in the literature on fuzzy logic, while the notation ${\displaystyle \otimes }$ follows the tradition of substructural logics.
• Bottom ${\displaystyle \bot }$ (nullary — a propositional constant); ${\displaystyle 0}$ or ${\displaystyle {\overline {0}}}$ are common alternative signs and zero a common alternative name for the propositional constant (as the constants bottom and zero of substructural logics coincide in MTL).

The following are the most common defined logical connectives:

• Weak conjunction ${\displaystyle \wedge }$ (binary), also called lattice conjunction (as it is always realized by the lattice operation of meet in algebraic semantics). Unlike MTL and weaker substructural logics, weak conjunction is definable in BL as

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

• Negation ${\displaystyle \neg }$ (unary), defined as

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

• Equivalence ${\displaystyle \leftrightarrow }$ (binary), defined as

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

As in MTL, the definition is equivalent to ${\displaystyle (A\rightarrow B)\otimes (B\rightarrow A).}$

• (Weak) disjunction ${\displaystyle \vee }$ (binary), also called lattice disjunction (as it is always realized by the lattice operation of join in algebraic semantics), defined as

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

• Top ${\displaystyle \top }$ (nullary), also called one and denoted by ${\displaystyle 1}$ or ${\displaystyle {\overline {1}}}$ (as the constants top and zero of substructural logics coincide in MTL), defined as

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

Well-formed formulae of BL are defined as usual in propositional logics. In order to save parentheses, it is common to use the following order of precedence:

• Unary connectives (bind most closely)
• Binary connectives other than implication and equivalence
• Implication and equivalence (bind most loosely)

Axioms

A Hilbert-style deduction system for BL has been introduced by Petr Hájek (1998). Its single derivation rule is modus ponens:

from ${\displaystyle A}$ and ${\displaystyle A\rightarrow B}$ derive ${\displaystyle B.}$

The following are its axiom schemata:

${\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}}}$

The axioms (BL2) and (BL3) of the original axiomatic system were shown to be redundant (Chvalovský, 2012) and (Cintula, 2005). All the other axioms were shown to be independent (Chvalovský, 2012).