Lemme diagonal

(i) La fonction $n \mapsto \ulcorner \underline n \urcorner$ est primitive récursive, comme au point (i) de Vérité et incomplétude ; $\mathrm{Sb}$ l'est par le point (i) de Substitution, et $d$ l'est par composition. Si $\chi$ est une formule de code $n$, le mot $\underline n$ est un terme, de code $\ulcorner \underline n \urcorner$, et $x_0 = a_8$ : le point (i) de Substitution donne $d(n) = \ulcorner \chi[\underline n/x_0] \urcorner$.

(ii) Soit $y$ une variable qui ne figure pas dans $\psi$ et qui est distincte de $x_0$. La fonction $d$, primitive récursive, est récursive et totale (Fonctions récursives, (i)) ; par le point (iii) de Représentation des fonctions, elle est représentée dans $\mathsf Q$ par une formule $\delta$ de variables libres parmi $x_0$ et $y$ : pour tout entier $n$, $\mathsf Q \vdash \forall y\, (\delta_n \leftrightarrow y = \underline{d(n)})$, où $\delta_n = \delta[\underline n/x_0]$. Posons $\psi' = \psi[y/x]$ ; comme $y$ ne figure pas dans $\psi$, elle y est substituable à $x$, et les variables libres de $\psi'$ sont parmi $y$. Soit $$\begin{aligned} \chi &= \exists y\, \big(\delta \wedge \psi'\big), \quad n = \ulcorner \chi \urcorner, \\ G &= \chi[\underline n/x_0]. \end{aligned}$$ Les variables libres de $\chi$ sont parmi $x_0$. Comme $x_0$ n'est pas libre dans $\psi'$ et que $x_0 \neq y$, la substitution ne touche que $\delta$ : $G = \exists y\, (\delta_n \wedge \psi')$, et c'est un énoncé. Par (i), son code est $g = d(n)$.

L'axiome (2), avec le terme $y$, donne $\mathsf Q \vdash \delta_n \leftrightarrow y = \underline g$, et la règle des tautologies donne $\mathsf Q \vdash (\delta_n \wedge \psi') \to (y = \underline g \wedge \psi')$ et la réciproque. Or, pour deux formules $A$ et $B$ telles que $\mathsf Q \vdash A \to B$, l'introduction de l'existentiel avec le terme $y$, qui donne $\vdash B \to \exists y\, B$, puis l'élimination, permise puisque $y$ n'est pas libre dans $\exists y\, B$, donnent $\mathsf Q \vdash \exists y\, A \to \exists y\, B$ (point (iii) de Calcul à variables libres). Ainsi $\mathsf Q \vdash G \leftrightarrow \exists y\, (y = \underline g \wedge \psi')$.

Il reste à voir que $\vdash \exists y\, (y = \underline g \wedge \psi') \leftrightarrow \psi'[\underline g/y]$. Le remplacement d'un terme (point (v) du même nœud), appliqué à $\psi'$, à la variable $y$ et aux termes $y$ et $\underline g$, donne $\vdash y = \underline g \to (\psi' \to \psi'[\underline g/y])$, donc $\vdash (y = \underline g \wedge \psi') \to \psi'[\underline g/y]$ ; comme $\psi'[\underline g/y]$ est un énoncé, l'élimination donne $\vdash \exists y\, (y = \underline g \wedge \psi') \to \psi'[\underline g/y]$. Inversement, $(y = \underline g \wedge \psi')[\underline g/y]$ est la formule $\underline g = \underline g \wedge \psi'[\underline g/y]$, et l'introduction de l'existentiel avec le terme clos $\underline g$, avec $\vdash \underline g = \underline g$, donne $\vdash \psi'[\underline g/y] \to \exists y\, (y = \underline g \wedge \psi')$.

Enfin, $\psi'[\underline g/y] = \psi[\underline g/x]$ : comme $y$ ne figure pas dans $\psi$, les lettres $y$ de $\psi'$ sont exactement aux places des occurrences libres de $x$ dans $\psi$, et elles y sont libres. La règle des tautologies donne $\mathsf Q \vdash G \leftrightarrow \psi[\underline g/x]$, l'équivalence annoncée, puisque $g = \ulcorner G \urcorner$. Une théorie qui contient $\mathsf Q$ démontre tout ce que démontre $\mathsf Q$, par le lemme de remplacement de la preuve de Théorème de Craig.