Extension par témoins

(i) Une démonstration formelle de $\psi$ à partir de $T \cup H$ n'emploie qu'un nombre fini d'axiomes de Henkin ; montrons $T \vdash \psi$ par récurrence sur ce nombre $k$, pour toute démonstration.

Si $k = 0$, c'est une démonstration à partir de $T$, écrite dans $\mathcal L^+$, et le changement de langage en donne une écrite dans $\mathcal L$.

Si $k \geqslant 1$, prenons, parmi les axiomes de Henkin employés, un axiome $h_\sigma$, avec $\sigma = \exists x\, \varphi$ et $c = c_\sigma$, dont la constante est de niveau maximal, disons $n + 1$, et notons $H_0$ l'ensemble des $k - 1$ autres.

La constante $c$ ne figure ni dans $T$ ni dans $\psi$, écrits dans $\mathcal L$, ni dans $\varphi$, écrite dans $\mathcal L_n$. Elle ne figure pas non plus dans les éléments de $H_0$ : un axiome $h_{\sigma'}$ de $H_0$ a une constante $c_{\sigma'}$ de niveau $m + 1 \leqslant n + 1$, distincte de $c$, et l'énoncé $\sigma'$ est écrit dans $\mathcal L_m$, donc dans $\mathcal L_n$.

Le théorème de la déduction donne $T \cup H_0 \vdash h_\sigma \to \psi$. Posons $$\theta = ((\exists x\, \varphi \to \varphi) \to \psi) ;$$ comme $x$ n'est libre ni dans l'énoncé $\exists x\, \varphi$ ni dans l'énoncé $\psi$, on a $\theta[c/x] = (h_\sigma \to \psi)$, et $c$ ne figure pas dans $\theta$. La généralisation sur une constante donne $T \cup H_0 \vdash \forall x\, \theta$.

Par distribution (Règles dérivées, (iii)), avec les instances de tautologies $$((A \to B) \to C) \to (\neg A \to C)$$ et $$((A \to B) \to C) \to (B \to C),$$ il vient $T \cup H_0 \vdash \forall x\, (\neg\exists x\, \varphi \to \psi)$ et $T \cup H_0 \vdash \forall x\, (\varphi \to \psi)$.

La première donne $T \cup H_0 \vdash \neg\exists x\, \varphi \to \psi$ par instanciation ; la seconde donne $T \cup H_0 \vdash \exists x\, \varphi \to \psi$ par la règle (iv), puisque $x$ n'est pas libre dans $\psi$. L'instance $$(A \to C) \to ((\neg A \to C) \to C)$$ donne alors $T \cup H_0 \vdash \psi$, par une démonstration qui n'emploie que $k - 1$ axiomes de Henkin, et l'hypothèse de récurrence conclut.

Si $T \cup H$ était incohérente, elle démontrerait toutes les formules (Cohérence, (i)), en particulier l'énoncé $\forall x_0\, (x_0 = x_0)$ de $\mathcal L$ et sa négation ; par ce qui précède, $T$ les démontrerait aussi, et serait incohérente.

(ii) Un énoncé $\sigma = \exists x\, \varphi$ de $\mathcal L^+$ n'a qu'un nombre fini de symboles, donc est écrit dans l'un des $\mathcal L_n$ ; pour le plus petit tel $n$, il a reçu une constante $c_\sigma$ de $\mathcal L_{n+1}$, et $h_\sigma \in H$. Une théorie qui contient $H$ démontre donc $\exists x\, \varphi \to \varphi[c_\sigma/x]$.

(iii) Soit $a_0, a_1, \dots$ une énumération de l'alphabet de $\mathcal L$, variables et symboles logiques compris. On code les mots par récurrence sur leur longueur : le mot vide a pour code $0$ et, si le mot $w$ a pour code $n$, le mot $w\, a_k$ a pour code l'entier $$2^{n}\, (2k + 1).$$ Tout entier $N \geqslant 1$ s'écrit d'une seule façon $2^n (2k + 1)$, où $n$ est le nombre de fois que l'on peut diviser $N$ par $2$, et l'on a alors $n < 2^n \leqslant N$. Par récurrence forte sur $N$, chaque entier est donc le code d'au plus un mot : le code $0$ n'est que celui du mot vide, et un code $N \geqslant 1$ détermine la dernière lettre $a_k$ et le code $n < N$ du mot qui la précède. Deux mots distincts ont ainsi des codes distincts.

En rangeant les mots dans l'ordre de leurs codes, on énumère les mots, puis les énoncés de la forme $\exists x\, \varphi$, donc les nouvelles constantes de $\mathcal L_1$, et l'on obtient une énumération de l'alphabet de $\mathcal L_1$ en intercalant les nouvelles constantes entre les anciens symboles.

Par récurrence sur $n$, on définit ainsi une énumération de chaque $\mathcal L_n$, puis de $\mathcal L^+$, en rangeant le $k$-ième symbole de $\mathcal L_n$ au rang $2^n(2k + 1) - 1$ et en ne retenant que sa première apparition. Tout est défini par récurrence, rien n'est choisi.