Généralisation et règles dérivées

(i) La formule $\alpha_1 \to (\alpha_2 \to \cdots \to (\alpha_n \to \beta) \cdots)$ est un axiome logique du groupe (1) ; $n$ modus ponens successifs donnent $T \vdash \beta$.

(ii) Soit $\alpha_0, \dots, \alpha_m = \alpha$ une démonstration formelle à partir de $T$. Montrons par récurrence sur $k$ que $T \vdash \forall x\, \alpha_k$.

Si $\alpha_k$ est un axiome logique, $\forall x\, \alpha_k$ en est un aussi, car les axiomes logiques sont toutes les généralisations des formules des groupes (1) à (5). Si $\alpha_k$ appartient à $T$, c'est un énoncé, où $x$ n'est pas libre : l'axiome (4) $\alpha_k \to \forall x\, \alpha_k$ et le modus ponens donnent $T \vdash \forall x\, \alpha_k$.

Si enfin $\alpha_k$ se déduit par modus ponens de $\alpha_i$ et de $\alpha_j = (\alpha_i \to \alpha_k)$, avec $i, j < k$, l'hypothèse de récurrence donne $T \vdash \forall x\, \alpha_i$ et $T \vdash \forall x\, (\alpha_i \to \alpha_k)$ ; l'axiome (3) $$\begin{aligned} &\forall x\, (\alpha_i \to \alpha_k) \\ &\to (\forall x\, \alpha_i \to \forall x\, \alpha_k) \end{aligned}$$ et deux modus ponens donnent $T \vdash \forall x\, \alpha_k$.

(iii) Un terme clos $t$ est substituable à $x$ dans $\alpha$, donc $\forall x\, \alpha \to \alpha[t/x]$ est un axiome (2), et le modus ponens donne $T \vdash \alpha[t/x]$. La variable $x$ est elle aussi substituable à $x$, et $\alpha[x/x] = \alpha$ : le même axiome donne $T \vdash \alpha$.

Si $\alpha \to \beta$ est une instance de tautologie, sa généralisation $\forall x\, (\alpha \to \beta)$ est un axiome, et l'axiome (3) donne $\forall x\, \alpha \to \forall x\, \beta$ par modus ponens ; un second modus ponens donne $T \vdash \forall x\, \beta$.

(iv) La formule $(\varphi \to \psi) \to (\neg\psi \to \neg\varphi)$ est une instance de tautologie ; par (iii), $T \vdash \forall x\, (\neg\psi \to \neg\varphi)$, et l'axiome (3) donne $T \vdash \forall x\, \neg\psi \to \forall x\, \neg\varphi$. Comme $x$ n'est pas libre dans $\neg\psi$, l'axiome (4) donne $\neg\psi \to \forall x\, \neg\psi$.

Par la règle des tautologies, appliquée à l'instance $$(P \to Q) \to ((Q \to R) \to (\neg R \to \neg P))$$ avec $P = \neg\psi$, $Q = \forall x\, \neg\psi$ et $R = \forall x\, \neg\varphi$, on obtient $$T \vdash \neg\forall x\, \neg\varphi \to \neg\neg\psi,$$ puis $T \vdash \neg\forall x\, \neg\varphi \to \psi$ par l'instance $(A \to \neg\neg B) \to (A \to B)$. Or $\neg\forall x\, \neg\varphi$ est, par définition, $\exists x\, \varphi$.

(v) La généralisation $\forall x\, (\neg\neg\varphi \to \varphi)$ d'une instance de tautologie est un axiome, et l'axiome (3) donne $\vdash \forall x\, \neg\neg\varphi \to \forall x\, \varphi$. L'instance $(P \to Q) \to (\neg Q \to \neg P)$ donne alors $\vdash \neg\forall x\, \varphi \to \neg\forall x\, \neg\neg\varphi$, et $\neg\forall x\, \neg\neg\varphi$ est, par définition, $\exists x\, \neg\varphi$.