Théorème 3Lemme diagonal et démontrabilité

Premier théorème d'incomplétude sous la forme de Gödel

Une théorie $T$ sur la signature de l'arithmétique est ω-cohérente s'il n'existe aucune formule $\psi$ , de variables libres parmi une variable $y$ , telle que $T \vdash \exists y\, \psi$ et $T \vdash \neg\psi[\underline n/y]$ pour tout entier $n$ . Une théorie ω-cohérente est cohérente : une théorie incohérente démontre toutes les formules (Cohérence, (i)), en particulier $\exists y\, \neg(y = y)$ et chacun des énoncés $\neg\neg(\underline n = \underline n)$ .

Les notations $\mathrm{Pr}\,\ulcorner \sigma \urcorner$ sont celles de Démontrabilité (D1).

Énoncé

Soit $T$ une théorie cohérente, dont l'ensemble des codes des axiomes est récursivement énumérable et qui contient $\mathsf Q$ , et $\mathrm{Pr} = \exists y\, \delta$ une formule de démontrabilité pour $T$ . Soit $G$ un énoncé tel que $\mathsf Q \vdash G \leftrightarrow \neg\mathrm{Pr}\,\ulcorner G \urcorner ;$ il en existe par le lemme diagonal, appliqué à $\neg\mathrm{Pr}$ .

(i) $T \nvdash G$ .

(ii) L'énoncé $G$ est vrai dans $\mathcal N$ .

(iii) Si $T$ est ω-cohérente, $T \nvdash \neg G$ : l'énoncé $G$ n'est ni démontrable ni réfutable dans $T$ .

Démonstration

Notons $g = \ulcorner G \urcorner$ . Comme $T$ contient $\mathsf Q$ , elle démontre $G \leftrightarrow \neg\mathrm{Pr}\,\ulcorner G \urcorner$ .

(i) Si $T \vdash G$ , la première condition de dérivabilité (Démontrabilité (D1), (ii)) donne $T \vdash \mathrm{Pr}\,\ulcorner G \urcorner$ , et l'équivalence donne $T \vdash \neg\mathrm{Pr}\,\ulcorner G \urcorner$ : $T$ serait incohérente.

(ii) Par (i) et le point (ii) de Démontrabilité (D1), $\mathcal N \not\models \mathrm{Pr}\,\ulcorner G \urcorner$ . Les axiomes de $\mathsf Q$ sont vrais dans $\mathcal N$ (preuve du point (iii) de Gödel-Rosser), et le théorème de correction donne $\mathcal N \models G \leftrightarrow \neg\mathrm{Pr}\,\ulcorner G \urcorner$ ; par la table de $\leftrightarrow$ , $\mathcal N \models G$ .

(iii) Supposons $T \vdash \neg G$ . L'équivalence et la règle des tautologies donnent $T \vdash \mathrm{Pr}\,\ulcorner G \urcorner$ , c'est-à-dire $T \vdash \exists y\, \delta_g$ , où $\delta_g = \delta[\underline g/v]$ est une formule Δ₀, par le point (i) de Σ₁-complétude, de variables libres parmi $y$ . Pour tout entier $m$ , l'énoncé Δ₀ $\delta_g[\underline m/y]$ est faux dans $\mathcal N$ : sinon, par le lemme de substitution, $\delta$ serait satisfaite sous une valuation qui vaut $g$ en $v$ et $m$ en $y$ , et $T$ démontrerait $G$ , contrairement à (i). Par le point (ii) de Σ₁-complétude, $\mathsf Q \vdash \neg\delta_g[\underline m/y]$ , donc $T \vdash \neg\delta_g[\underline m/y]$ , pour tout $m$ . Avec $T \vdash \exists y\, \delta_g$ , la formule $\delta_g$ contredit l'ω-cohérence de $T$ .

□

Remarque

L'énoncé $G$ dit de lui-même qu'il n'est pas démontrable dans $T$ : par le point (ii) de Démontrabilité (D1), $\mathcal N \models G$ si et seulement si $T \nvdash G$ . C'est le contenu du premier théorème de Gödel (« Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I », Monatshefte für Mathematik und Physik 38, 1931, p. 173-198, théorème VI), énoncé pour le système P des Principia étendu par une classe récursive d'axiomes ω-cohérente, où l'énoncé indécidable est construit directement. Le point (i) n'emploie que la cohérence ; c'est l'irréfutabilité qui demande davantage, et l'hypothèse sert exactement à interdire qu'une théorie démontre $\exists y\, \delta_g$ tout en réfutant chacun des témoins possibles.

Remarque

Rosser (1936) a obtenu un énoncé indécidable sous la seule hypothèse de cohérence en changeant d'énoncé : le sien dit que toute démonstration de lui-même est précédée d'une démonstration de sa négation. Le nœud Gödel-Rosser obtient le même résultat sans lemme diagonal, par une paire récursivement inséparable ; ici, c'est la diagonale qui désigne l'énoncé.

Remarque

Le raisonnement du point (i), « si $T$ démontrait $G$ , elle serait incohérente », porte sur les démonstrations de $T$ . Le second théorème d'incomplétude naît de la remarque qu'une théorie assez forte peut mener ce raisonnement elle-même ; le nœud Löb et second théorème dit à quelles conditions.

Repose sur

Lemme diagonal Formule de démontrabilité et première condition de dérivabilité

Sert à

Théorème de Löb et second théorème d'incomplétude sous les conditions de dérivabilité