# MTL

The logic MTL was introduced by Esteva and Godo . It has three basic binary connectives $\displaystyle \to, \And, \wedge$ and one nullary connective $\displaystyle \bar 0$ . Other connectives are defined as:
 $\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$
MTL 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)$ (A4a) $\displaystyle \varphi \And (\varphi\to\psi)\to \varphi\wedge \psi$ (A4b) $\displaystyle (\varphi\wedge \psi) \to \varphi$ (A4c) $\displaystyle (\varphi\wedge \psi) \to (\psi\wedge\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$