Théorème de Gödel-Rosser

(i) Soit $A_0$ et $A_1$ les ensembles de Paire inséparable, et $\theta$ la formule que fournit le point (i) de Astuce de Rosser, avec $k = 1$ et une variable $v_1 = a_l$. Par la définition de $\theta(\underline n)$, le code de $\theta(\underline n)$ est $g(n) = \mathrm{Sb}\big(\ulcorner \theta \urcorner, \ulcorner \underline n \urcorner, l\big)$, avec la fonction $\mathrm{Sb}$ de Substitution ; comme au point (i) de Vérité et incomplétude, $n \mapsto \ulcorner \underline n \urcorner$ est primitive récursive, et $g$ l'est aussi.

Si $\mathrm{Th}(T)$ était récursif, $C = g^{-1}(\mathrm{Th}(T)) = \{n : T \vdash \theta(\underline n)\}$ le serait aussi (Récursif, r.e., (iii)). Si $n \in A_0$, alors $\mathsf Q \vdash \theta(\underline n)$, donc $T \vdash \theta(\underline n)$ : $A_0 \subset C$. Si $n \in A_1$, alors $T \vdash \neg\theta(\underline n)$, et, $T$ étant cohérente, $T \nvdash \theta(\underline n)$ : $C \cap A_1 = \varnothing$. L'ensemble récursif $C$ séparerait $A_0$ et $A_1$, ce que Paire inséparable exclut.

(ii) Par le point (iii) de Théorèmes r.e., $\mathrm{Th}(T)$ est récursivement énumérable. Supposons $T$ complète. Pour un entier $N$ qui code un énoncé $\sigma$, on a $N \notin \mathrm{Th}(T)$ si et seulement si $T \vdash \neg\sigma$ : par la complétude dans un sens, par la cohérence dans l'autre. Le code de $\neg\sigma$ est $\mathrm{conc}(\langle 1 \rangle, N)$ (Codage des mots). Ainsi le complémentaire de $\mathrm{Th}(T)$ est la réunion de l'ensemble des entiers qui ne codent pas un énoncé, récursif par le point (i) de Théorèmes r.e., et de l'ensemble des codes d'énoncés $N$ tels que $\mathrm{conc}(\langle 1 \rangle, N) \in \mathrm{Th}(T)$, intersection d'un ensemble récursif et d'une image réciproque d'un ensemble récursivement énumérable par une fonction primitive récursive. Il est récursivement énumérable (Récursif, r.e., (i) et (iii)), et $\mathrm{Th}(T)$ serait récursif par le point (ii) du même nœud, contrairement à (i).

(iii) Les axiomes de $\mathsf Q$ et de $\mathsf{PA}$ sont vrais dans $\mathcal N$ : pour $\mathsf{PA}$, c'est la preuve du point (iii) de Vérité et incomplétude, et $\mathrm Q_3$ l'est puisque tout entier non nul est un successeur (axiomes de Peano). Par le théorème de correction, ces théories sont donc cohérentes : tout ce qu'elles démontrent est satisfait dans $\mathcal N$, et une formule et sa négation ne le sont pas toutes deux. Elles ont un ensemble d'axiomes récursif, donc récursivement énumérable : pour $\mathsf Q$, sept énoncés fixés, comme les six premiers axiomes de $\mathsf{PA}$ au point (i) de Théorèmes r.e. ; pour $\mathsf{PA}$, par ce même point. Il reste à voir que $\mathsf{PA}$ contient $\mathsf Q$ ; seul $\mathrm Q_3$ n'est pas un axiome de $\mathsf{PA}$.

Soit $\varphi$ la formule $\neg(x = 0) \to \exists y\, (x = S\,y)$, avec $x = x_0$ et $y = x_1$. Comme $\vdash 0 = 0$, la règle des tautologies donne $\vdash \varphi[0/x]$. L'introduction de l'existentiel, avec le terme $x$ substitué à $y$ dans $S\,x = S\,y$, donne $\vdash S\,x = S\,x \to \exists y\, (S\,x = S\,y)$, d'où $\vdash \varphi[S\,x/x]$, puis $\vdash \forall x\, (\varphi \to \varphi[S\,x/x])$ par la règle des tautologies et la généralisation. L'axiome de récurrence pour $\varphi$ et $x$, dont la clôture universelle est la formule elle-même puisque $\varphi$ n'a que $x$ pour variable libre, donne alors $\mathsf{PA} \vdash \forall x\, \varphi$, c'est-à-dire $\mathrm Q_3$. Les points (i) et (ii) concluent.