Théorèmes d'incomplétude

Admis ici. Le point (i) est admis par anticipation : il est démontré plus loin, dans la théorie de la calculabilité, sous exactement ces hypothèses, une fois définis le codage des formules par des entiers et les ensembles récursivement énumérables. Voici le chemin suivi. On démontre dans le système formel que l'arithmétique de Robinson démontre tout énoncé vrai formé de quantificateurs existentiels placés devant une formule dont les quantificateurs sont bornés, et l'on montre que tout ensemble récursivement énumérable se définit par une telle formule. Si deux ensembles récursivement énumérables disjoints $A$ et $B$ sont définis par $\exists y\, \alpha(x, y)$ et $\exists y\, \beta(x, y)$, la formule de Rosser $$\exists y\, \big(\alpha(x, y) \wedge \forall z \leqslant y\ \neg\beta(x, z)\big)$$ est alors démontrée dans $T$ en $x = S \cdots S\, 0$ pour les entiers de $A$, et réfutée pour ceux de $B$ : c'est la représentation des relations récursives, obtenue sous la forme d'une séparation. Si $T$ était complète, ses théorèmes formeraient un ensemble récursif, puisqu'ils forment un ensemble récursivement énumérable dont le complémentaire l'est aussi, et l'ensemble des entiers où $T$ démontre la formule de Rosser séparerait $A$ et $B$ par un ensemble récursif. C'est impossible pour une paire récursivement inséparable, par exemple celle formée des indices des fonctions récursives qui valent $0$, et de ceux des fonctions qui valent $1$, en leur propre indice ; l'idée de raisonner sur une telle paire est de Kleene (1950). Ni le lemme diagonal ni l'astuce de Craig n'interviennent, et la cohérence simple suffit.

Le point (ii) est admis ici par anticipation. On représente d'abord dans l'arithmétique de Robinson les fonctions récursives, et non seulement les relations, par des formules dont elle démontre qu'elles définissent des fonctions ; on en tire le lemme diagonal, qui fournit, pour toute formule $\psi$ à une variable libre, un énoncé $G$ que $T$ démontre équivalent à $\psi$ appliquée au code de $G$. On écrit ensuite une formule $\mathrm{Pr}$, de la forme existentielle ci-dessus, qui définit dans $\mathbb N$ l'ensemble des codes des théorèmes de $T$ ; elle satisfait la première condition de dérivabilité, (D1) : si $T \vdash \varphi$, alors $T \vdash \mathrm{Pr}(\underline{\ulcorner \varphi \urcorner})$. Si elle satisfait aussi (D2), $T \vdash \mathrm{Pr}(\underline{\ulcorner \varphi \to \psi \urcorner}) \to (\mathrm{Pr}(\underline{\ulcorner \varphi \urcorner}) \to \mathrm{Pr}(\underline{\ulcorner \psi \urcorner}))$, et (D3), $T \vdash \mathrm{Pr}(\underline{\ulcorner \varphi \urcorner}) \to \mathrm{Pr}(\underline{\ulcorner \mathrm{Pr}(\underline{\ulcorner \varphi \urcorner}) \urcorner})$, pour tous énoncés $\varphi$ et $\psi$, le lemme diagonal, appliqué à $\mathrm{Pr} \to \varphi$, donne le théorème de Löb, et celui-ci, appliqué à $\varphi = \neg(0 = 0)$, montre que $T$, cohérente, ne démontre pas $\neg\mathrm{Pr}(\underline{\ulcorner \neg(0 = 0) \urcorner})$, qui est $\mathrm{Coh}(T)$. Tout cela est démontré plus loin, dans la théorie de la calculabilité.

La formule naturelle, qui transcrit dans l'arithmétique la définition des démonstrations formelles à partir d'une formule qui définit les axiomes de $T$, se met, par une équivalence démontrable dans l'arithmétique de Peano, sous la forme ci-dessus et définit l'ensemble des codes des théorèmes de $T$ ; l'arithmétique de Peano démontre pour elle (D2), puisqu'elle démontre que deux démonstrations mises bout à bout et suivies d'un modus ponens en forment une : c'est démontré plus loin, dans la théorie de la calculabilité, au nœud « Deuxième condition (D2) » ; $\mathrm{Coh}(T)$ est l'énoncé construit avec cette formule. La définition naturelle de l'ensemble des axiomes passe par le théorème de Craig : on remplace $T$ par une théorie $T'$ qui démontre les mêmes formules et dont l'ensemble des codes des axiomes est primitif récursif, ou par $T$ elle-même si c'est déjà le cas, comme pour l'arithmétique de Peano, et l'on transcrit la relation primitive récursive « $p$ code une démonstration à partir de $T'$ d'un énoncé de code $c$ ». L'arithmétique de Peano démontre aussi pour elle (D3), donc $T$ aussi : il faut qu'elle démontre, pour chaque énoncé $\sigma$ de la forme existentielle ci-dessus, que $\sigma$ entraîne sa propre démontrabilité, ce qui est, transportée à l'intérieur de l'arithmétique de Peano, la démontrabilité des énoncés existentiels vrais qu'emploie le point (i), appliquée à $\sigma = \mathrm{Pr}(\underline{\ulcorner \varphi \urcorner})$. C'est démontré plus loin, dans la théorie de la calculabilité, au nœud « Troisième condition (D3) », qui en tire le théorème de Löb et le point (ii).