# BL

The logic BL was introduced by Hájek [1], It has two basic binary connectives $\displaystyle \to, \And$ and one nullary connective $\displaystyle \bar 0$ . Other connectives are defined as:
 $\displaystyle \varphi \wedge \psi$ as $\displaystyle \varphi \And (\varphi \to \psi)$ $\displaystyle \varphi \vee \psi$ as $\displaystyle ((\varphi \to \psi) \to \psi)\wedge ((\psi \to \varphi) \to \varphi)$ $\displaystyle \varphi \equiv \psi$ as $\displaystyle (\varphi \to \psi) \wedge (\psi \to \varphi)$ $\displaystyle \neg\varphi$ as $\displaystyle \varphi \to \bar 0$ $\displaystyle \bar 1$ as $\displaystyle \neg \bar 0$
BL has one deduction rule Modus Ponens (from $\displaystyle \varphi$ and $\displaystyle \varphi\to\psi$ infer $\displaystyle \psi$ ) and the following axioms:
 (A1) $\displaystyle (\varphi \to \psi) \to ((\psi \to \chi) \to (\varphi \to \chi))$ (A2) $\displaystyle (\varphi \And \psi) \to \varphi$ (A3) $\displaystyle (\varphi \And \psi) \to (\psi \And \varphi)$ (A4) $\displaystyle \varphi \And (\varphi\to\psi)\to \psi\And(\psi\to \varphi)$ (A5a) $\displaystyle (\varphi \to (\psi \to \chi )) \to (\varphi \And \psi \to \chi)$ (A5b) $\displaystyle (\varphi \And \psi \to \chi) \to (\varphi\to (\psi \to \chi))$ (A6) $\displaystyle ((\varphi \to \psi) \to \chi) \to (((\psi \to \varphi ) \to \chi) \to \chi)$ (A7) $\displaystyle \bar 0 \to \varphi$