Constantes nouvelles et changement de langage

(i) Le remplacement de $c$ par $y$ respecte le modus ponens, puisque $(\beta \to \gamma)\langle y/c\rangle = \beta\langle y/c\rangle \to \gamma\langle y/c\rangle$, et il laisse inchangés les éléments de $T$, où $c$ ne figure pas.

Il reste à voir qu'il transforme un axiome logique en un axiome logique. Comme $y$ ne figure pas dans l'axiome, toute variable $z$ qui y figure est distincte de $y$, et le remplacement ne touche ni aux variables ni aux quantificateurs : les occurrences libres de $z$ restent les mêmes. Une instance de tautologie devient une instance de la même tautologie ; une généralisation $\forall y_1 \cdots \forall y_k\, \beta$ devient $\forall y_1 \cdots \forall y_k\, \beta\langle y/c\rangle$.

Pour le groupe (2), $\forall z\, \beta \to \beta[t/z]$ devient $$\begin{aligned} &\forall z\, \beta\langle y/c\rangle \\ &\to \beta\langle y/c\rangle[t\langle y/c\rangle/z], \end{aligned}$$ et $t\langle y/c\rangle$ est substituable à $z$ dans $\beta\langle y/c\rangle$, car la seule variable qu'il peut avoir en plus de celles de $t$ est $y$, qui n'est quantifiée nulle part.

Les groupes (3) et (4) sont conservés, puisque $z$ est libre dans $\beta\langle y/c\rangle$ exactement quand elle l'est dans $\beta$.

Pour le groupe (5), $z = z$ ne contient pas $c$, et $z_1 = z_2 \to (\beta \to \beta')$, où $\beta'$ remplace certaines occurrences de $z_1$ par $z_2$ dans la formule atomique $\beta$, devient $$\begin{aligned} z_1 = z_2 \to (&\beta\langle y/c\rangle \\ &\to \beta'\langle y/c\rangle), \end{aligned}$$ où $\beta'\langle y/c\rangle$ s'obtient de la même façon à partir de la formule atomique $\beta\langle y/c\rangle$.

(ii) Soit une démonstration formelle de $\theta[c/x]$ à partir de $T$, et $T_0$ l'ensemble, fini, des éléments de $T$ qu'elle emploie. Choisissons une variable $y$, distincte de $x$, qui ne figure dans aucune de ses formules : il y en a, puisque ces formules sont en nombre fini et que les variables forment une suite infinie, et l'on peut prendre celle de plus petit indice, sans aucun choix arbitraire.

Par (i), $T_0 \vdash \theta[c/x]\langle y/c\rangle$. Comme $c$ ne figure pas dans $\theta$, ses occurrences dans $\theta[c/x]$ sont exactement les occurrences libres de $x$ dans $\theta$, si bien que $$\theta[c/x]\langle y/c\rangle = \theta[y/x].$$ Par la généralisation, $T_0 \vdash \forall y\, \theta[y/x]$.

Les occurrences libres de $y$ dans $\theta[y/x]$ occupent les places des occurrences libres de $x$ dans $\theta$, qui ne sont dans la portée d'aucun quantificateur $\forall x$ : $x$ est substituable à $y$ dans $\theta[y/x]$, et, $y$ ne figurant pas dans $\theta$, $$\theta[y/x][x/y] = \theta.$$ L'axiome (2) donne $T_0 \vdash \theta$, et une nouvelle généralisation, sur $x$ cette fois, donne $T_0 \vdash \forall x\, \theta$, donc $T \vdash \forall x\, \theta$.

(iii) Une démonstration formelle n'emploie qu'un nombre fini de nouvelles constantes $c_1, \dots, c_k$.

Prenons des variables distinctes $y_1, \dots, y_k$ qui n'y figurent pas, et appliquons (i) $k$ fois, en remplaçant $c_1$ par $y_1$, puis $c_2$ par $y_2$, et ainsi de suite ; les éléments de $T$ et la formule $\varphi$, écrits dans $\mathcal L$, ne sont pas modifiés.

On obtient une démonstration formelle de $\varphi$ à partir de $T$ dont toutes les formules sont écrites dans $\mathcal L$.

Si $T$ est incohérente sur $\mathcal L'$, elle démontre toutes les formules de $\mathcal L'$ (Cohérence, (i)), en particulier $x_0 = x_0$ et $\neg\, x_0 = x_0$, et ces deux démonstrations se récrivent dans $\mathcal L$. Réciproquement, une démonstration écrite dans $\mathcal L$ l'est aussi dans $\mathcal L'$ : si $T$ est incohérente sur $\mathcal L$, elle l'est sur $\mathcal L'$.