Théorème de la déduction

Par récurrence sur une démonstration de $\varphi$ à partir de $T \cup \{\psi\}$, montrons que $T \vdash \psi \to \alpha$ pour chacune de ses formules $\alpha$.

Si $\alpha$ est un axiome logique ou un élément de $T$, on a $T \vdash \alpha$, et $\alpha \to (\psi \to \alpha)$ est une tautologie : le modus ponens donne $T \vdash \psi \to \alpha$. Si $\alpha = \psi$, alors $\psi \to \psi$ est une tautologie.

Si $\alpha$ s'obtient par modus ponens à partir de $\beta$ et $\beta \to \alpha$, on a par hypothèse $T \vdash \psi \to \beta$ et $T \vdash \psi \to (\beta \to \alpha)$. La tautologie $$\begin{aligned} &(\psi \to (\beta \to \alpha)) \\ &\to ((\psi \to \beta) \to (\psi \to \alpha)) \end{aligned}$$ et deux modus ponens donnent $T \vdash \psi \to \alpha$.