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

Argument de la preuve du second théorème d'incomplétude

Pour démontrer le premier théorème d'incomplétude, on a eu besoin de formaliser la prouvabilité dans une théorie arithmétique. Il est donc possible (sous les hypothèses du premier théorème) de construire un énoncé qui signifie par exemple que 0 = 1 n'est pas prouvable (0 = 1 ou n'importe quelle proposition contradictoire dans la théorie), c'est-à-dire la cohérence de la théorie. Le second théorème d'incomplétude énonce, sous des hypothèses un peu plus fortes que pour le premier, que cet énoncé n'est pas démontrable.

On peut déjà observer que la formule G que l'on construit pour démontrer le premier théorème d'incomplétude, et qui dépend de la théorie considérée, affirme qu'un certain énoncé (lui-même, en l'occurrence) n'est pas prouvable dans cette théorie. C'est donc déjà dans une certaine mesure un énoncé de cohérence, puisque dans une théorie incohérente tout est démontrable ; en fait, G a pour conséquence la cohérence de la théorie. Pour le second théorème d'incomplétude, il suffit de montrer que la cohérence de la théorie entraîne G.

Le second théorème d'incomplétude se prouve essentiellement en formalisant la preuve du premier théorème d'incomplétude pour une théorie T dans cette même théorie T. En effet, on a montré ci-dessus que, si la théorie était cohérente la formule G de Gödel (qui dépend de T), n'est pas prouvable. Mais la formule de Gödel est équivalente à sa non prouvabilité. On a donc montré que la cohérence de la théorie T entraîne G. Si maintenant T permet de formaliser cette preuve, on montre dans la théorie T que la cohérence de la théorie T entraîne G. Mais justement, si T est cohérente, G n'est pas démontrable dans T. On ne peut donc démontrer la cohérence de T dans T si cette dernière théorie est cohérente.

Pour ce raisonnement, on utilise seulement la non-démontrabilité de G, donc la simple hypothèse de cohérence suffit. Par contre, pour formaliser le raisonnement, la théorie T doit être plus expressive que pour le premier théorème d'incomplétude. En particulier on a besoin de récurrence.

Les conditions que doivent vérifier la théorie T pour démontrer le second théorème d'incomplétude ont été précisées tout d'abord par Paul Bernays dans les Grundlagen der Mathematik (1939) co-écrit avec David Hilbert, puis par Martin Löb, pour la démonstration de son théorème, une variante du second théorème d'incomplétude. Les conditions de démontrabilité de Löb portent sur le prédicat de prouvabilité dans la théorie T, que l'on nommera comme ci-dessus Dem_T :

• D1. Si F est démontrable dans T, alors Dem_T(⌈F⌉) est démontrable dans T.

• D2. Dem_T(⌈F⌉) ⇒ Dem_T(Dem_T(⌈F⌉)) est démontrable dans T.

• D3. Dem_T(⌈F ⇒ G⌉) ⇒ (Dem_T(⌈F⌉) ⇒ Dem_T(⌈G⌉)) est démontrable dans T.

La condition D1 est apparue implicitement pour démontrer le premier théorème d'incomplétude. La seconde condition D2 est une formalisation dans la théorie de D1. Enfin la dernière, D3, est une formalisation de la règle logique primitive dite de modus ponens. Notons coh_T la formule qui exprime la cohérence de T, c’est-à-dire que l'absurde, que l'on note ⊥, n'est pas démontrable (la négation est notée maintenant ¬) :

coh_T ≡ ¬Dem_T(⌈⊥⌉)

Comme la négation d'une formule F, ¬F, équivaut à F entraîne l'absurde, F⇒⊥, on déduit de la condition D3 que

• D'3 Dem_T(⌈¬F⌉) ⇒ (Dem_T(⌈F⌉) ⇒ ¬coh_T.

Pour déduire le second théorème d'incomplétude des trois conditions de Löb, il suffit de reprendre le raisonnement déjà fait ci-dessus. Soit G la formule de Gödel construite pour la théorie T, qui, si cette dernière est cohérente, entraîne ¬Dem_T(⌈G⌉). D'après D1 et la cohérence de la théorie T, G n'est pas démontrable dans T (premier théorème). On formalise maintenant ce raisonnement dans T. Supposons que dans T, Dem_T(⌈G⌉). Comme, d'autre part, on démontre dans T que Dem_T(⌈G ⇒ ¬Dem_T(⌈G⌉)⌉), on déduit par D3 dans T, Dem_T(⌈¬Dem_T(⌈G⌉)⌉). Finalement, par D'3, on a montré ¬coh_T dans T. Récapitulons : on a montré dans T que Dem_T(⌈G⌉) ⇒ ¬coh_T, c’est-à-dire par définition de G, ¬G ⇒ ¬coh_T, et par contraposée coh_T ⇒ G. Or on a vu que G n'est pas démontrable dans T, donc coh_T n'est pas démontrable dans T.

La preuve de D1 a été déjà été esquissée à propos du premier théorème d'incomplétude : il s'agit de formaliser proprement la démontrabilité, et on utilise le fait que les formules closes Σ₁ vraies sont démontrables.

La condition D3 formalise la règle de modus ponens, une règle que l'on a tout intérêt à avoir dans le système que l'on a choisi pour formaliser les démonstrations. Il faudrait rentrer dans le détail du codage pour donner la preuve de D3, mais elle ne sera pas bien difficile. Il faut faire attention à bien formaliser le résultat indiqué dans la théorie choisie : les variables en jeu (par exemple, il existe un x qui est le code d'une preuve de F) sont les variables de la théorie. Il faudra quelques propriétés de l'ordre, et savoir démontrer quelques résultats élémentaires sur les preuves dans la théorie.

C'est la condition D2 qui s'avère la plus délicate a démontrer. C'est un cas particulier de la propriété

• Pour toute formule close F Σ₁, F ⇒ Dem_T(⌈F⌉) est démontrable dans T

qui formalise (dans T) que toute formule close Σ₁ vraie est démontrable dans T. On n'a donné ci-dessus aucun détail sur la preuve de ce dernier résultat, T étant par exemple l'arithmétique de Peano. Si on en donnait, on se rendrait compte que l'on n'a pas besoin de l'axiome de récurrence de la théorie, mais que, par contre, l'on raisonne par récurrence sur la longueur des termes, la complexité des formules ... Comme il faut maintenant formaliser cette preuve dans la théorie, il faut de la récurrence. Pour résumer la situation : quand on a démontré sérieusement le premier théorème d'incomplétude pour l'arithmétique de Peano, on a fait cette preuve, qui est un peu longue, mais ne présente pas de difficulté. Pour le second théorème, la seule chose à faire consiste maintenant à montrer que cette preuve se formalise dans l'arithmétique de Peano elle-même, ce qui est intuitivement relativement clair (quand on a fait la preuve), mais très pénible à expliciter complètement.

On peut en fait démontrer le second théorème d'incomplétude pour une théorie plus faible que l'arithmétique de Peano, l'arithmétique primitive récursive. On étend le langage de façon à avoir des symboles de fonction pour toutes les fonctions primitives récursives, et on ajoute à la théorie les axiomes qui définissent ces fonctions. On restreint la récurrence aux formules sans quantificateurs, ce qui fait que celles-ci sont "immédiates". L'arithmétique primitive récursive est souvent considérée comme la formalisation des mathématiques finitaires, avec lesquelles Hilbert espérait pouvoir prouver la cohérence des théories mathématiques.