Théorème d'incomplétude de Gödel - Définition

Une preuve partielle du premier théorème d'incomplétude

La preuve par Gödel de son premier théorème d'incomplétude utilise essentiellement deux ingrédients :

• le codage par des nombres entiers du langage et des fonctions qui permettent de le manipuler, ce que l'on appelle l'arithmétisation de la syntaxe ;

• un argument diagonal qui, en utilisant l'arithmétisation de la syntaxe, fait apparaître un énoncé similaire au paradoxe du menteur : l'énoncé de Gödel est équivalent, via codage, à un énoncé affirmant sa propre non prouvabilité dans la théorie considérée.

Mais l'énoncé de Gödel n'est pas paradoxal. Il est vrai dans N, car s'il était faux, il serait prouvable. Or cet énoncé est de complexité logique suffisamment simple pour que sa prouvabilité dans une théorie cohérente capable de coder l'arithmétique entraîne sa vérité dans N (on n'a pas besoin de supposer que N est modèle de la théorie). Il est donc vrai dans N. Il n'est donc pas prouvable, par définition de l'énoncé.

Pour montrer que la négation de l'énoncé de Gödel n'est pas non plus prouvable, il faut une hypothèse de cohérence plus forte, comme celle qu'a faite Gödel. Rosser a modifié astucieusement l'énoncé pour pouvoir utiliser simplement la cohérence. En ce qui concerne la preuve de Gödel l'argument est le suivant : l'énoncé étant vrai, sa négation est fausse. Si on supposait que N est modèle de la théorie, cela suffirait pour qu'elle ne soit pas démontrable. Mais Gödel a construit un énoncé d'une complexité logique suffisamment faible pour qu'une hypothèse beaucoup moins forte suffise : il s'agit essentiellement de dire que de tels énoncés faux ne peuvent être démontrables, et il peut l'exprimer de façon syntaxique.

La preuve esquissée ci-dessus est reprise de façon plus précise dans le paragraphe « diagonalisation ».

Arithmétisation de la syntaxe

À l'époque actuelle, quiconque connait un peu d'informatique n'a aucun mal à imaginer que l'on puisse représenter les énoncés d'une théorie par des nombres. Cependant il faut également manipuler ces codages dans la théorie. La difficulté réside dans les restrictions du langage : une théorie du premier ordre avec essentiellement l'addition et la multiplication comme symboles de fonction. C'est la difficulté que Gödel résout pour montrer que la prouvabilité peut être représentée par une formule dans la théorie.

La suite est un peu technique. En première lecture, on peut simplifier l'argumentation en supposant que N est modèle de T, auquel cas on n'a pas besoin d'être attentif à la complexité logique de l'énoncé. La partie sur la fonction β et la représentation de la récurrence reste utile. On précise également des notions, et des résultats qui ont été évoqués ou rédigés de façon approximative ci-dessus.

Codes

Il peut être amusant d'écrire soi même les codages, il l'est certainement beaucoup moins de lire ceux des autres. On trouve donc beaucoup de variété dans la littérature. Le choix du codage n'a pas grande importance, en soi. Éventuellement certains se "manieront" plus facilement dans la théorie. Comme les formules et les démonstrations peuvent être vues comme des suites finies de caractères, lettres, espace, ponctuation, et ceux-ci en nombre fini, on peut les coder par un nombre, celui étant écrit dans une base de taille le nombre de caractères nécessaire, ou par tout autre moyen qui permet de coder des suites finies d'entiers (Gödel utilise les exposants de la décomposition d'un nombre en facteurs premiers). On peut également utiliser un codage des couples (voir ci-dessous) pour représenter, suites finies, arbres, et donc les structures syntaxiques utiles ...

Formules Σ₀

Un problème plus important est d'avoir des fonctions pour manipuler ces structures, l'équivalent des programmes en informatique : il est à peu près clair que l'on ne peut se contenter de compositions de fonctions constantes, d'additions et de multiplications, c’est-à-dire de polynômes à coefficients entiers positifs. On va représenter les fonctions utiles par des formules. Voyons un exemple, par ailleurs fort utile pour les codages. La bijection de Cantor entre N×N et N est bien connue et tout à fait calculable : on énumère les couples d'entiers diagonale par diagonale (somme constante), par exemple en faisant croître la seconde composante :

=[1+2+ … +(x+y)]+y=½(x+y)(x+y+1)+y

Cette fonction n'est déjà plus représentée par un terme du langage, à cause de la division par 2, mais elle est représentée par la formule (on utilise "≡" pour la relation d'équivalence) :

z= ≡ 2z=(x+y)(x+y+1)+2y

Passons maintenant aux fonctions de décodage, c’est-à-dire à un couple de fonctions inverses. On aura besoin de quantificateurs :

x=π₁(z) ≡ ∃y≤z 2z=(x+y)(x+y+1)+2y  ;         y=π₂(z) ≡ ∃x≤z 2z=(x+y)(x+y+1)+2y

On a donc représenté une fonction, plus exactement son graphe (la formule soulignée) par une formule du langage de l'arithmétique. Les formules ci-dessus sont bien particulières : la première est une égalité polynomiale, si on remplace les trois variables libres par des termes clos du langage, représentant des entiers (s…s0), elle devient décidable. Les deux suivantes utilisent un quantificateur borné : "∃x≤z A" signifie "il existe un x plus petit ou égal à z tel que A". Là encore si on remplace les deux variables libres par des entiers cette formule devient décidable : pour vérifier une quantification existentielle bornée, il suffit de chercher jusqu’à la borne, soit on a trouvé, et l'énoncé est vérifié, soit on n'a pas trouvé et il ne l'est pas. Ce n'est plus le cas (pour la seconde partie de l'assertion) si la quantification existentielle n'est pas bornée. On pourra conserver cette propriété de décidabilité en ajoutant des quantifications universelles bornées, notée "∀ x≤ p A" ("pour tout x plus petit ou égal à p, A"). Les formules construites à partir des égalités polynomiales en utilisant les connecteurs booléens usuels, et des quantifications uniquement bornées sont appelées formules Σ₀. Remarquez que la négation d'une formule Σ₀ est Σ₀.

On se convainc facilement, des arguments sont donnés juste ci-dessus et au paragraphe vérité et démontrabilité, que la vérité dans N des formules closes Σ₀ est décidable : on a un moyen mécanique de savoir si elles sont vraies ou fausses. Pour démontrer le premier théorème d'incomplétude de Gödel (il faut un peu plus pour Gödel-Rosser, de la récurrence pour le second), la condition minimale sur la théorie, en plus d'être récursivement axiomatisable et d'une hypothèse de cohérence, est de démontrer toutes les formules Σ₀ vraies dans N, et donc, par stabilité par négation des Σ₀ et cohérence, de n'en démontrer aucune fausse. C'est ce que l'on a entendu par "formaliser suffisamment d'arithmétique". Remarquez que c'est une hypothèse sur les axiomes de la théorie. Par exemple l'ensemble des formules Σ₀ vraies dans N étant décidable, on peut le choisir comme système d'axiomes pour une théorie qui sera bien récursivement axiomatisable (on peut évidemment le simplifier). En particulier on peut démontrer :

Dans l'arithmétique de Peano, les formules closes Σ₀ sont vraies dans N si et seulement si elles sont démontrables.

Résultat qui se démontre d'ailleurs sans véritablement utiliser les axiomes de récurrence de l'arithmétique de Peano (ce qui est naturel puisqu'il n'y a pas véritablement de quantification universelle dans ces énoncés).

Formules Σ₁

Il serait bien commode de se contenter de manipuler des fonctions représentables par des formules Σ₀ : vérité et démontrabilité sont confondues, ces formules sont décidables, donc les fonctions représentées par des formules Σ₀ sont calculables. Mais le « langage de programmation » induit n'est pas assez riche. On doit introduire les formules Σ₁, qui sont obtenues en plaçant un quantificateur existentiel en tête d'une formule Σ₀. En général, la négation d'une formule Σ₁ n'est pas équivalente à une formule Σ₁. On a la propriété suivante :

Dans une théorie qui prouve toutes les formules Σ₀ vraies dans N, les formules Σ₁ vraies dans N sont prouvables.

En effet une formule Σ₁ "∃ x A x" est vraie dans N signifie que pour un certain entier, que l'on peut écrire "s…s0", la formule "A s…s0" est vraie, or cette formule est Σ₀.

Il existe des théories arithmétiques cohérentes, qui démontrent des formules closes Σ₁ fausses, contrairement à ce qui se passe pour les Σ₀. Il faut préciser que de telles théories arithmétiques sont assez pathologiques, comme celles qui démontrent un énoncé exprimant leur propre contradiction (voir début de l'article). L'hypothèse de cohérence supplémentaire utile pour le premier théorème d'incomplétude, que l'on va appeler Σ-cohérence, c'est justement de supposer que la théorie ne démontre aucune formule close Σ₁ fausse. On suppose que certaines formules ne sont pas démontrables, donc la contradiction ne l'est pas : c'est bien une hypothèse de cohérence au moins aussi forte que la simple cohérence. Elle est vraiment plus forte : on peut exprimer la négation de la cohérence d'une théorie par une formule Σ₁.

Fonctions définissables, fonctions représentables

Un sous-ensemble E de N, ou plus généralement de N^p est définissable dans l'arithmétique s'il existe une formule F de l'arithmétique avec p variables libres telle que :

(n₁,…, n_p) ∈ E si et seulement si F(n₁,…, n_p) est vraie dans N

Un sous-ensemble E de N^p est représentable dans une théorie T s'il existe une formule F de l'arithmétique avec p variables libres telle que :

(n₁,…, n_p) ∈ E si et seulement si F(n₁,…, n_p) est démontrable dans T.

Une fonction f à plusieurs variables sur N est définissable dans N si son graphe est défini dans N, représentable dans une théorie T si son graphe est représentable dans T. Un ensemble, ou une fonction est définissable par une formule Σ₁ si et seulement si il, ou elle, est représentable par cette formule dans une théorie Σ-cohérente où tous les énoncés Σ₀ sont démontrables.

Il existe d'autres notions de représentabilité plus fortes, pour les ensembles comme pour les fonctions. Pour celle introduite ici, on dit souvent « faiblement représentable ».

On notera y=f(x) une formule Σ₁ définissant ou représentant f. Pour le théorème de Gödel c'est la notion de fonction ou d'ensemble représentable qui est utile, mais la notion de fonction ou d'ensemble définissable est plus simple à manipuler, et comme on s'intéresse aux cas où elles sont équivalentes, on va dans la suite parler de définissabilité par une formule Σ₁.

On peut remarquer que la conjonction, la disjonction de deux formules Σ₁, la quantification existentielle d'une formule Σ₁, la quantification universelle bornée d'une formule Σ₁, sont équivalentes dans N (on note ≡_N) à une formule Σ₁ :

∃x A ∨ ∃x B ≡ ∃x (A ∨ B)  ;   ∃x ∃y A(x, y) ≡_N ∃z ∃x≤z ∃y≤z A(x, y)  ;   ∃x A ∧ ∃y B ≡ ∃x ∃y (A ∧ B) ;  ∀x≤z ∃y A(x, y) ≡_N∃ u ∀x≤z ∃y≤u A(x, y).

L'ensemble de fonctions à notre disposition est donc stable par composition (on donne l'exemple pour une variable, on généralise sans peine à des fonctions de plusieurs variables) :

z=f o g (x) ≡ ∃ y [z=f(y) ∧ y = g (x)]

On définit également de façon naturelle :

f(x)=g(y) ≡ ∃ z [z=f(x) ∧ z = g (y)]

Cependant, pour pouvoir avoir un langage suffisamment expressif pour définir les fonctions utiles sur la syntaxe, il manque une notion très utile : la définition par récurrence. L'idée pour l'obtenir est d'utiliser un codage des suites finies (les listes de l'informatique). Supposons que nous ayons un tel codage, notons l=[n₀;…;n_p] l'entier qui code la suite finie n₀,…, n_p. Il faut pouvoir décoder : notons β(l, i)=n_i l'élément en place i de la suite codée par l (la valeur n'a pas d'importance si i est trop grand). Supposons que nous ayons une fonction g de N dans N (une suite infinie d'entiers) définie par :

g(0)=a ;  g(n+1)=f(g(n))

et que f soit définissable dans N. Alors on pourra définir la fonction g par :

y=g(x) ≡ ∃ l [β(l,0)=a ∧ ∀ i < x β(l, i+1)=f(β(l, i)) ∧ y = β(l, x)]

formule qui est équivalente dans N à une formule Σ₁ dès que le graphe de β est Σ₁. Ceci se généralise au schéma de récurrence utilisé pour les fonctions récursives primitives. Il suffit donc trouver une formule Σ₁ qui définit une fonction β : c'est la principale difficulté à résoudre pour le codage de la syntaxe.

La fonction β

Le nom de fonction β est repris de l'article original de Gödel. Pour la définir, il a eu l'idée d'utiliser le théorème des restes chinois : pour coder n₁,…, n_p on va donner p entiers premiers entre eux deux à deux, engendrés à partir d'un seul entier d, et un entier a dont les restes des divisions par chacun de ces entiers sont n₁,…, n_p. La suite n₁,…, n_p sera donc codée par les deux entiers a et d, l'entier si on en veut un seul. Plusieurs (une infinité !) entiers coderont la même suite, ce qui n'est pas gênant si on pense à l'objectif (coder les définitions par récurrence). Le principal est que l'on assure que toute suite finie a au moins un code.

Étant donnés les entiers n₁,…, n_p, on choisi un entier s, tel que s ≥ p et pour tout n_i, s≥n_i. Les entiers

d₀=1+s!, d₁=1+2s!, …, d_n=1+(n+1)s!

sont alors premiers entre eux deux à deux. De plus n_i < d_i. Par le théorème chinois on déduit l'existence d'un entier a tel que pour chaque entier n_i de la suite finie, le reste de la division de a par d_i soit n_i. On a donc, en posant d = s! :

β(d, a,i)=r(a,1+(i+1)d) ;  z=r(a, b) ≡ z

On a bien une fonction β définie par une formule Σ₀.

On en déduit que :

si une fonction se définit par récurrence primitive à partir de fonctions définissables par des formules Σ₁, elle est définissable par une formule Σ₁.

On peut calculer beaucoup de choses avec les fonctions récursives primitives. Une fois ce résultat obtenu, le reste n'est plus qu'affaire de soin. On peut utiliser des méthodes plus ou moins astucieuses pour gérer les problèmes de liaison de variables. On montre que la fonction qui code la substitution d'un terme à une variable dans une formule est récursive primitive, que l'ensemble des (codes de) preuves d'une théorie T récursivement axiomatisable est récursif primitif, et enfin que la fonction qui extrait d'une preuve la conclusion de celle-ci est récursive primitive. Dire qu'une formule est prouvable dans T, c'est dire qu'il existe une preuve de cette formule dans T, ce qui, codé dans la théorie, reste Σ₁, bien que le prédicat "être démontrable" ne soit pas lui récursif primitif, ni même récursif.

En conclusion, pour une théorie récursivement axiomatisable T, on a deux formules Σ₁, Dem_T(x) et z=sub(x, y), telles que :

• Dem_T(⌈F⌉) est vraie dans N si et seulement si F est prouvable dans T ;
• pour toute formule F(x), ⌈F(n)⌉ = sub(⌈F⌉, n), et la fonction sub est définie par la formule z=sub(x, y).

On a noté ⌈F⌉ l'entier qui code la formule F.

Du fait que les formules sont Σ₁, on peut remplacer "vrai" par "démontrable dans T" sous les hypothèses suffisantes.

Diagonalisation

La construction de l'énoncé de Gödel repose sur un argument diagonal. On construit tout d'abord la formule à une variable libre Δ(x) :

Δ(x) ≡ ∀z[z=sub(x, x) ⇒ ¬Dem_T(z)]

qui peut s'interpréter dans N par la formule de code x appliquée à son propre code n'est pas démontrable dans T, et on applique cette formule à l'entier ⌈Δ⌉. On obtient G=Δ(⌈Δ⌉), une formule qui dit bien d'elle même qu'elle n'est pas démontrable dans T. On reprend en la précisant l'argumentation déjà donnée au-dessus. On suppose que T est récursivement axiomatisable, démontre toutes les formules Σ₀ vraies dans N, donc toutes les formules Σ₁ vraies dans N, et qu'elle est Σ-cohérente.

• G=Δ(⌈Δ⌉) est une formule close, équivalente à la négation d'une formule Σ₁ ;

• si la formule G était démontrable, la négation de G étant Σ₁ ne pourrait être vraie car alors elle serait démontrable, et donc cela contredirait la cohérence de T. La formule G serait donc vraie dans N, ce qui voudrait dire, par construction de G, que la formule G ne serait pas démontrable, contradiction. Donc G n'est pas démontrable.

• si la négation de la formule G était démontrable dans T, par Σ-cohérence elle serait vraie, or elle est fausse d'après ce qui précède. Donc la négation de G n'est pas démontrable.

On voit donc bien, le dernier argument étant assez tautologique, que le véritable contenu du théorème est dans la non-démontrabilité de G. Le premier théorème d'incomplétude de Gödel s'énonce donc aussi bien par :

Si T est une théorie récursivement axiomatisable, cohérente, et qui démontre toutes les formules Σ₀ vraies dans N, alors il existe une formule G, négation d'une formule Σ₁, qui est vraie dans N, mais non démontrable dans T.

Remarquez que la formule G en question est équivalente à une formule universelle ∀x H(x), où H est Σ₀. Cette formule étant vraie, pour chaque entier n (représenté par s...s 0) H(n) est vraie, donc démontrable étant Σ₀. On a donc bien, comme annoncé dans le paragraphe « vérité et démontrabilité », un énoncé universel ∀x H(x) qui n'est pas démontrable dans T, alors que pour chaque entier n, H(n) est démontrable dans T.

Vérité et démontrabilité

Théorèmes d'incomplétude et calculabilité

- Introduction - Énoncés des deux théorèmes - Des exemples de systèmes incomplets et d'énoncés indécidables - Vérité et démontrabilité - Une preuve partielle du premier théorème d'incomplétude - Théorèmes d'incomplétude et calculabilité - Argument de la preuve du second théorème d'incomplétude