MTL

From Mathfuzzlog

The logic MTL was introduced by Esteva and Godo ^[1]. It has three basic binary connectives $\to, \And, \wedge$ and one nullary connective $\bar 0$ . Other connectives are defined as:

$\varphi \vee \psi$	as	$((\varphi \to \psi) \to \psi)\wedge ((\psi \to \varphi) \to \varphi)$
$\varphi \equiv \psi$	as	$(\varphi \to \psi) \wedge (\psi \to \varphi)$
$\neg\varphi$	as	$\varphi \to \bar 0$
$\bar 1$	as	$\neg \bar 0$

MTL has one deduction rule Modus Ponens (from $\varphi$ and $\varphi\to\psi$ infer $ψ$ ) and the following axioms:

(A1)	$(\varphi \to \psi) \to ((\psi \to \chi) \to (\varphi \to \chi))$
(A2)	$(\varphi \And \psi) \to \varphi$
(A3)	$(\varphi \And \psi) \to (\psi \And \varphi)$
(A4a)	$\varphi \And (\varphi\to\psi)\to \varphi\wedge \psi$
(A4b)	$(\varphi\wedge \psi) \to \varphi$
(A4c)	$(\varphi\wedge \psi) \to (\psi\wedge\varphi)$
(A5a)	$(\varphi \to (\psi \to \chi )) \to (\varphi \And \psi \to \chi)$
(A5b)	$(\varphi \And \psi \to \chi) \to (\varphi\to (\psi \to \chi))$
(A6)	$((\varphi \to \psi) \to \chi) \to (((\psi \to \varphi ) \to \chi) \to \chi)$
(A7)	$\bar 0 \to \varphi$