Règles dérivées pour les formules à variables libres

(i) La démonstration du théorème de la déduction est une récurrence sur une démonstration formelle, qui n'emploie que le modus ponens et des instances de tautologies ; elle n'utilise ni que $\psi$ soit un énoncé, ni que les éléments de l'ensemble d'hypothèses en soient, et vaut donc mot pour mot pour $\Gamma$. La règle des tautologies se démontre comme au point (i) de Règles dérivées : la formule $\alpha_1 \to (\cdots \to (\alpha_n \to \beta) \cdots)$ est un axiome du groupe (1), et $n$ modus ponens donnent $\Gamma \vdash \beta$. Enfin, une démonstration formelle à partir de $\Gamma$ en est une à partir de $\Gamma'$.

(ii) La généralisation (Règles dérivées, (ii)) donne $T \vdash \forall x\, \alpha$ ; l'axiome (2) $\forall x\, \alpha \to \alpha[t/x]$ et le modus ponens donnent $T \vdash \alpha[t/x]$.

Pour la substitution simultanée, choisissons des variables distinctes $w_1, \dots, w_k$, différentes des $x_i$, qui ne figurent ni dans $\alpha$ ni dans les $t_j$. Dans une formule sans quantificateur, toutes les occurrences sont libres et tout terme est substituable à toute variable. En substituant successivement $w_1$ à $x_1$, …, $w_k$ à $x_k$ par le premier point, on obtient que $T$ démontre la formule où chaque occurrence de $x_i$ est devenue $w_i$, puisque les $w_j$ ne figurent pas dans $\alpha$. En substituant ensuite successivement $t_1$ à $w_1$, …, $t_k$ à $w_k$, chaque étape remplace exactement les lettres $w_i$ venues des occurrences de $x_i$, puisque les $w_j$ ne figurent pas dans les termes $t_l$ déjà placés ; le résultat est $\alpha[t_1, \dots, t_k / x_1, \dots, x_k]$.

(iii) Les sous-formules $\forall y\, \psi$ de $\neg\alpha$ sont celles de $\alpha$ ; le terme $t$ est donc substituable à $x$ dans $\neg\alpha$, et $(\neg\alpha)[t/x] = \neg\, \alpha[t/x]$. L'axiome (2) donne $\vdash \forall x\, \neg\alpha \to \neg\, \alpha[t/x]$, et l'instance de tautologie $(P \to \neg Q) \to (Q \to \neg P)$ donne $\vdash \alpha[t/x] \to \neg\forall x\, \neg\alpha$, c'est-à-dire $\vdash \alpha[t/x] \to \exists x\, \alpha$ (Quantificateurs).

Pour l'élimination, la généralisation donne $T \vdash \forall x\, (\varphi \to \psi)$, et le point (iv) de Règles dérivées donne $T \vdash \exists x\, \varphi \to \psi$. Avec une hypothèse $\chi$, l'instance $(P \to (Q \to R)) \to (Q \to (P \to R))$ donne $T \vdash \varphi \to (\chi \to \psi)$ ; comme $x$ n'est pas libre dans $\chi \to \psi$, ce qui précède donne $T \vdash \exists x\, \varphi \to (\chi \to \psi)$, et la même instance remet les hypothèses dans l'ordre annoncé.

Pour le renommage, si $y = x$, la variable $x$ ne figure pas dans $\varphi$, $\varphi[y/x] = \varphi$, et la formule est une instance de tautologie. Sinon, posons $\varphi' = \varphi[y/x]$ : la variable $y$, absente de $\varphi$, y est substituable à $x$, et les occurrences libres de $y$ dans $\varphi'$ sont exactement aux places des occurrences libres de $x$ dans $\varphi$, dont aucune n'est dans une sous-formule $\forall x\, \psi$. Ainsi $x$ est substituable à $y$ dans $\varphi'$, et $\varphi'[x/y] = \varphi$. Le premier point donne $\vdash \varphi \to \exists y\, \varphi'$. La variable $x$ n'est pas libre dans $\exists y\, \varphi'$, puisque toutes ses occurrences libres ont été remplacées ; l'élimination donne $\vdash \exists x\, \varphi \to \exists y\, \varphi'$.

(iv) Montrons d'abord $\vdash x = y \to y = x$. L'axiome (5), appliqué à la formule atomique $x = x$ dont on remplace la première occurrence par $y$, donne $\vdash x = y \to (x = x \to y = x)$ ; avec l'axiome $x = x$ et l'instance $(P \to (Q \to R)) \to (Q \to (P \to R))$, la règle des tautologies conclut.

On raisonne ensuite par récurrence sur le nombre de symboles de $\alpha$, l'énoncé étant établi pour tous les couples de variables et tous les choix d'occurrences permis. Si aucune occurrence n'est remplacée, $\alpha' = \alpha$, et $x = y \to (\alpha \to \alpha)$ est une instance de tautologie ; on suppose désormais qu'il y en a au moins une. Si $\alpha$ est atomique, toutes ses occurrences sont libres, et $x = y \to (\alpha \to \alpha')$ est un axiome du groupe (5).

Observons que $\alpha$ s'obtient à son tour à partir de $\alpha'$ en remplaçant par $x$ les occurrences de $y$ qui ont pris la place des occurrences choisies, et que ce remplacement est permis. En effet, on n'a remplacé que des occurrences libres, si bien que les blocs $\forall w$ de $\alpha$ et de $\alpha'$ sont aux mêmes places ; ces occurrences ne sont dans la portée d'aucun $\forall y$, par hypothèse, ni d'aucun $\forall x$, puisque les occurrences de $x$ y étaient libres. Pour une sous-formule propre $\beta$ de $\alpha$ et la sous-formule $\beta'$ correspondante de $\alpha'$, l'hypothèse de récurrence, appliquée dans les deux sens, donne donc $\vdash x = y \to (\beta \to \beta')$ et $\vdash y = x \to (\beta' \to \beta)$, puis $\vdash x = y \to (\beta' \to \beta)$ avec la symétrie établie d'abord.

Si $\alpha = \neg\beta$, alors $\alpha' = \neg\beta'$, et l'instance $(A \to (B' \to B)) \to (A \to (\neg B \to \neg B'))$ conclut. Si $\alpha = (\beta \to \gamma)$, alors $\alpha' = (\beta' \to \gamma')$, et l'instance $$\begin{aligned} &(A \to (B' \to B)) \to \big((A \to (C \to C')) \\ &\quad \to (A \to ((B \to C) \to (B' \to C')))\big) \end{aligned}$$ conclut.

Si $\alpha = \forall z\, \beta$, les occurrences remplacées, libres dans $\alpha$, sont dans la portée de ce $\forall z$ : donc $z \neq x$, et $z \neq y$ par hypothèse. Elles sont libres dans $\beta$, et $\alpha' = \forall z\, \beta'$. L'hypothèse de récurrence et la généralisation donnent $\vdash \forall z\, (x = y \to (\beta \to \beta'))$, et l'axiome (3) donne $\vdash \forall z\, (x = y) \to \forall z\, (\beta \to \beta')$. Comme $z$ n'est pas libre dans $x = y$, l'axiome (4) donne $\vdash x = y \to \forall z\, (x = y)$, et l'axiome (3) donne encore $\vdash \forall z\, (\beta \to \beta') \to (\forall z\, \beta \to \forall z\, \beta')$. La règle des tautologies enchaîne ces trois implications.

(v) Choisissons deux variables distinctes $a$ et $b$, différentes de $v$, qui ne figurent ni dans $\varphi$, ni dans $t$, ni dans $u$. Comme $a$ ne figure pas dans $\varphi$, la formule $\varphi[a/v]$ porte la lettre $a$ exactement aux places des occurrences libres de $v$, et ces places ne sont dans la portée d'aucun $\forall a$ ni d'aucun $\forall b$ ; la formule $\varphi[b/v]$ s'obtient en y remplaçant toutes ces occurrences de $a$ par $b$. Par (iv), $\vdash a = b \to (\varphi[a/v] \to \varphi[b/v])$, et la généralisation, en $b$ puis en $a$, donne $$\vdash \forall a\, \forall b\, \big(a = b \to (\varphi[a/v] \to \varphi[b/v])\big).$$ Le terme $t$ est substituable à $a$ dans la formule qui suit $\forall a$ : les occurrences libres de $a$ y sont dans $a = b$ et aux places des occurrences libres de $v$ dans $\varphi$ ; la portée de $\forall b$ ne capture rien, puisque $b$ ne figure pas dans $t$, et les autres quantificateurs sont ceux de $\varphi$, où $t$ est substituable à $v$. Comme $a$ est différente de $b$ et ne figure pas dans $\varphi$, l'axiome (2) donne $\vdash \forall b\, \big(t = b \to (\varphi[t/v] \to \varphi[b/v])\big)$. De même, $u$ est substituable à $b$ dans la formule qui suit $\forall b$, où $b$ ne figure ni dans $t$ ni dans $\varphi[t/v]$, et l'axiome (2) donne la conclusion, puisque $(\varphi[b/v])[u/b] = \varphi[u/v]$.

(vi) L'axiome $x = x$, la généralisation et l'axiome (2) donnent $\vdash t = t$. Soit $w$ une variable qui ne figure ni dans $t$, ni dans $u$, ni dans $r$, et différente de $v$. Le point (v), avec la formule atomique $w = t$, donne $\vdash t = u \to (t = t \to u = t)$, d'où $\vdash t = u \to u = t$ par la règle des tautologies. Avec la formule $w = r$ et les termes $u$ et $t$, il donne $\vdash u = t \to (u = r \to t = r)$, qu'on enchaîne avec $\vdash t = u \to u = t$. Enfin, avec la formule $r[t/v] = r[w/v]$, où $w$ ne figure pas dans le premier membre, il donne $$\begin{aligned} \vdash t = u \to \big(&r[t/v] = r[t/v] \\ &\to r[t/v] = r[u/v]\big), \end{aligned}$$ puisque $r[w/v][t/w] = r[t/v]$ et $r[w/v][u/w] = r[u/v]$, et $\vdash r[t/v] = r[t/v]$ conclut.