Quelles sont les hypothèses minimales du premier théorème de Gödel ?

14 avril 2024 ⋅ Retour à l'accueil du blog

Je rassemble ici un certain nombre de faits que j'ai compris depuis qu'on m'a expliqué pour la première fois ce théorème dont je croyais à l'époque avoir fait le tour — grave erreur vu le nombre incroyable de subtilités qui se cachent de partout. Le but principal est de mettre de l'ordre dans mes idées, mais j'en profite pour partager ce que j'ai appris.

Le premier théorème d'incomplétude de Gödel, énoncé de manière vague, affirme que tout système logique TT vérifiant de « bonnes hypothèses » est incomplet, c'est-à-dire qu'il existe une proposition PP telle que TT ne prouve ni PP ni ¬P¬P.

Mais qu'entend-on exactement par « système logique » et quelles sont ces « bonnes hypothèses » ? C'est un peu délicat. Le premier théorème de Gödel a un énoncé usuel, qui s'applique aux systèmes du premier ordre décidablement axiomatisés contenant l'arithmétique cohérents… et il a deux preuves usuelles, l'une qui remplace l'hypothèse « cohérent » par « arithmétiquement vrai » et l'autre par « ω-cohérent ». Autrement dit, aucune preuve usuelle du premier théorème de Gödel ne prouve le premier théorème usuel de Gödel, ce qui est tout de même un comble. Mon fil conducteur va être de passer en revue différentes preuves qui affaiblissent progressivement les hypothèses.

Modification (29 mai 2024) : Deux sections étaient tellement idiotes que je me suis permis de les supprimer, en adaptant largement le reste.

L'idée générale de la démonstration par Turing du premier théorème, dans son fameux article fondateur de l'informatique, est qu'on peut encoder dans le système logique TT les propositions de la forme « XX termine », où XX est un programme (disons par exemple une machine de Turing, mais on pourrait bien sûr prendre une fonction générale récursive, un λ-terme, un système de réécritures, …). Ceci nous donne une stratégie pour tenter de résoudre le problème de l'arrêt. Étant donné un programme XX, on construit l'énoncé PP = « XX termine », et on recherche en parallèle une preuve de PP, et une preuve de ¬P¬P. Si cette recherche termine, on peut conclure. Comme le problème de l'arrêt est indécidable, la recherche ne peut pas toujours terminer — c'est donc qu'il existe PP telle que ni PP ni ¬P¬P soient prouvables.

Il se trouve que l'arithmétique est un « bon » cadre logique pour formaliser un modèle de calcul Turing-complet. C'est une théorie très naturelle, et le calcul consiste en une manipulation de données finies, or quoi de plus simple comme données finies que les entiers naturels ? Prouvons donc le théorème pour PA, l'arithmétique de Peano, et observons au passage de quelles propriétés de PA nous avons besoin dans la démonstration.

Premier théorème d'incomplétude pour PA : PA est incomplète.

Preuve : Supposons que PA soit complète. On construit un algorithme qui prend une machine de Turing XX. Il construit un codage dans PA de la proposition PP = « XX termine » ; il est très fastidieux mais pas difficile de montrer que ce codage peut être réalisé, et de manière calculable. Puis, il énumère les arbres de preuve, et pour chacun d'eux, vérifie si c'est une preuve de PP ou une preuve de ¬P¬P, ce qui est possible grâce au fait que PA a un ensemble d'axiomes décidable. S'il rencontre une preuve de PP, il accepte, et inversement, s'il rencontre une preuve de ¬P¬P, il rejette. Par l'hypothèse que PA est complète, il existe une démonstration de PP ou une démonstration de ¬P¬P, donc l'algorithme termine. Puisque PA est vraie (au sens où elle admet ℕ comme modèle), la réponse de l'algorithme résout le problème de l'arrêt sur XX, contradiction. ∎

En fait, on a prouvé un énoncé légèrement plus fort, à savoir qu'il existe une machine de Turing dont PA ne prouve ni la terminaison ni la non-terminaison. D'ailleurs, une telle machine de Turing ne peut pas terminer, puisque si elle terminait, il en existerait trivialement une preuve dans PA consistant à lister les étapes. En termes logiques, non seulement il existe un énoncé indécidable dans PA, mais il en existe déjà un au niveau Σ1, et bien sûr sa négation fonctionne aussi et est au niveau Π1, alors qu'au niveau Σ0 = Π0, tout est évidemment décidé.

Comment généraliser cette démonstration à un système logique TT quelconque ? Il faut d'abord définir ce qu'on entend par « système logique ». Or le système dans lequel les mathématiciens prétendent travailler est ZFC, qui est une théorie du premier ordre classique, et il semblerait intéressant de pouvoir lui appliquer le théorème de Gödel. Mettons donc que TT est une théorie du premier ordre classique.

Ensuite, listons les propriétés de PA dont nous avons eu besoin. Il faut pouvoir décider si un arbre de preuve donné est une démonstration dans TT, donc il faut que TT soit décidablement0 axiomatisée, c'est-à-dire que l'ensemble des axiomes de TT doit être décidable. Par ailleurs, nous nous sommes servis d'un codage calculable de « XX termine » dans PA. Pour s'assurer qu'un tel codage reste possible, postulons qu'on peut traduire les énoncés de PA en énoncés de TT de manière raisonnable :

Définition : On dit qu'une théorie du premier ordre classique TT contient l'arithmétique s'il existe un encodage calculable φφ des énoncés de PA vers les énoncés de TT tel que pour tout énoncé PP de PA, φ(¬P)=¬φ(P)φ(¬P) = ¬φ(P), et de plus, si PP est prouvable dans PA, alors φ(P)φ(P) est prouvable dans TT. Les images par φφ d'énoncés de PA seront appelées énoncés arithmétiques (cette définition est implicitement relative à un certain encodage φφ, qui n'est pas unique).

Une théorie contenant l'arithmétique est dite arithmétiquement vraie lorsque pour tout énoncé PP de PA, si TT prouve φ(P)φ(P), alors PP est vrai (dans ℕ).

Remarque : Si TT est arithmétiquement vraie et φ(P)φ(P) est réfutable, alors PP est faux (car ¬φ(P)=φ(¬P)¬φ(P) = φ(¬P), c'est à ça que sert la condition raisonnable sur la négation).

Premier théorème d'incomplétude pour une théorie arithmétiquement vraie : Toute théorie du premier ordre classique décidablement axiomatisée, contenant l'arithmétique et arithmétiquement vraie est incomplète.

Preuve : Soit TT une telle théorie, soit φφ l'encodage depuis PA, et supposons TT complète. Construisons l'algorithme qui prend XX, qui construit PP = « XX termine », calcule φ(P)φ(P), puis cherche une preuve de φ(P)φ(P) ou ¬φ(P)¬φ(P) (grâce au fait que TT est décidablement axiomatisée). Il termine par complétude de TT, et résout le problème de l'arrêt car TT est arithmétiquement vraie, contradiction. ∎

Ce théorème s'applique en particulier à ZFC (et à nouveau, on obtient un peu mieux : il existe un énoncé arithmétique Σ1 indécidable dans ZFC).

Traditionnellement, on énonce le théorème de Gödel sur une théorie décidablement axiomatisée. Mais si on observe la preuve, on se rend compte que cette hypothèse est plus forte que ce qu'il nous faut. Nous avons simplement besoin de pouvoir reconnaître à coup sûr une démonstration de PP ou de ¬P¬P, mais on peut accepter que la vérification ne termine pas si on n'a pas une démonstration de PP ou ¬P¬P, à condition de lancer toutes ces vérifications en parallèle, ce qui peut se faire de manière tout à fait standard. Ainsi, nous obtenons un théorème plus fort où la théorie TT est seulement supposée semi-décidablement axiomatisée.

À vrai dire, je trouve cette expérience de pensée intéressante : si on découvrait demain une théorie logique miraculeuse qui soit à la fois simple, manifestement vraie, puissante et élégante, mais dont l'ensemble des démonstrations ne serait que semi-décidable et pas décidable, pourrait-elle être acceptée comme fondement des mathématiques ? Si on est chargé de relire un article mathématique, même si la complexité des démonstrations fait qu'elles seraient affreuses à lire de manière complètement formalisée, on doit en principe pouvoir vérifier ce qui est écrit, ligne à ligne, de façon presque mécanique, et rendre cette vérification complètement mécanique est le but des assistants de preuve. Mais si la démonstration est fausse, doit-on pouvoir s'en rendre compte en temps fini ?

Cela dit, il y a une bonne raison pour ne pas s'embarrasser du cas semi-décidable, à savoir qu'on peut le ramener au cas décidable via une astuce standard de fuel / budget. Partons d'une théorie TT semi-décidablement axiomatisée. Soit DD un semi-algorithme (mettons une machine de Turing) qui semi-décide l'ensemble des axiomes de TT. On forme une théorie TT' en rajoutant à TT des symboles de fonction BudgetZeˊro\text{BudgetZéro} et BudgetSucc\text{BudgetSucc} ainsi qu'un symbole de prédicat Budget\text{Budget}, et en changeant chaque axiome AA en l'axiome ABudget(n)A ∧ \text{Budget}(⟨n⟩), où nn est le temps de calcul de DD sur AA, avec le codage 0:=BudgetZeˊro⟨0⟩ := \text{BudgetZéro} et n+1:=BudgetSucc(n)⟨n+1⟩ := \text{BudgetSucc}(⟨n⟩). Clairement, TT' est décidablement axiomatisée, et c'est une extension conservatrice de TT.

(Je ne suis pas sûr que cette astuce épuise complètement la question. Est-ce qu'il serait acceptable d'écrire un article mathématique dans TT plutôt que TT' ? D'ailleurs, il paraît que les preuves de Coq ne sont que semi-décidables, à cause des classes de type dont la résolution peut ne pas terminer.)

Il y a deux preuves usuelles du théorème de Gödel, celle de Turing via le problème de l'arrêt, et la preuve d'origine de Gödel, via une astuce d'auto-référence. J'ai mis un temps embarrassant à réaliser que ces deux preuves sont en fait la même. L'indécidabilité du problème de l'arrêt se prouve en raisonnant par l'absurde et en construisant un programme qui contredit l'oracle de l'arrêt sur lui-même. En éliminant les coupures à l'intérieur de la preuve précédente, elle se reformule en : supposons TT complète, alors on peut construire un programme XX qui, via une recherche de preuve/réfutation dans TT de « XX termine », décide s'il est censé terminer ou non, puis se comporte de manière à contredire la prédiction de la théorie. S'il trouve une réfutation de « XX termine », il termine, sinon (y compris s'il ne trouve jamais rien), il ne termine pas.

En pensant ceci en termes logiques plutôt qu'en termes de programmes, on a construit un énoncé GG, à savoir « XX termine », tel que GG est équivalent à « GG est réfutable ». En calculabilité, l'autoréférence dans la preuve d'indécidabilité du problème de l'arrêt est permise par le (second) théorème de récursion de Kleene, et du côté logique on appelle plutôt cela le lemme diagonal, mais c'est essentiellement la même idée.

Dire que GG est équivalent à « GG est réfutable » revient à dire que ¬G¬G est équivalent à « ¬G¬G n'est pas prouvable ». Il se trouve que dans la présentation usuelle, GG est équivalent à « GG n'est pas prouvable », donc je vais inverser GG et ¬G¬G pour avoir le bon sens (autrement dit, plutôt que « XX termine », je considère finalement « XX ne termine pas »).

Il devient un peu moins flagrant dans cette reformulation qu'il faut supposer que TT est décidablement axiomatisée et contient l'arithmétique, mais faire fonctionner l'autoréférence, il faut que TT puisse parler de ses propres preuves. Pour encoder la définition d'une preuve dans TT, il faut bien qu'elle contienne l'arithmétique, et pour que TT puisse vérifier ses propres axiomes, elle doit être décidablement axiomatisée.

La preuve simplifiée est donc : Soit TT une théorie du premier ordre classique, décidablement axiomatisée, contenant l'arithmétique via un encodage noté φφ, arithmétiquement vraie. Supposons-la complète. Alors, comme elle est aussi arithmétiquement vraie, un énoncé arithmétique1 GG est vrai si et seulement s'il est prouvable. Mais par le lemme diagonal, il existe un énoncé arithmétique GG équivalent à « GG n'est pas prouvable dans TT », d'où une contradiction. ∎

Sous les mêmes hypothèses sur TT qu'à la section précédente, on peut imaginer une variante de la diagonalisation, où au lieu de construire GG équivalent à « GG n'est pas prouvable dans TT », on le construit équivalent à « GG est faux ». Ceci donne le paradoxe du menteur, qui aboutit automatiquement à l'incohérence de la théorie… L'arnaque est que pour faire fonctionner le lemme diagonal, il faut que TT formalise « GG est faux » de manière uniforme : qu'on puisse définir dans TT un prédicat P(n)P(n) tel que pour tout entier nn, l'énoncé codé par nn est équivalent à P(n)P(n). L'argument précédent montre précisément, par l'absurde, que ce n'est pas possible, ce qui s'appelle le théorème d'indéfinissabilité de Tarski, et qui s'énonce sous la forme raccourcie « la vérité arithmétique n'est pas uniformément définissable dans l'arithmétique ».

Peut-on affaiblir l'hypothèse que TT est arithmétiquement vraie ? Par exemple, il serait amusant, à défaut d'être follement utile, d'appliquer le théorème à la théorie PA + ¬Coh(PA) formée en ajoutant à PA l'axiome que PA est incohérente. Cette théorie est fausse, mais en admettant le second théorème d'incomplétude, on voit qu'elle est cohérente, car une preuve de ⊥ dans PA + ¬Coh(PA) se traduirait en une preuve de Coh(PA) dans PA.

Oublions donc l'hypothèse que TT est arithmétiquement vraie et cherchons par quoi la remplacer.

Reprenons GG équivalent à « GG n'est pas prouvable dans TT ». Supposons GG faux. Par définition, GG est prouvable dans TT. Cette fois, nous ne pouvons plus déduire immédiatement une contradiction : si TT n'est plus arithmétiquement vraie, elle peut parfaitement prouver GG même si GG est faux. Mais tout espoir n'est pas perdu.

Je vois les choses de cette façon : On a « GG est faux », qui par définition entraîne « GG est prouvable dans TT ». On veut provoquer une rencontre entre « GG est faux » et « GG est prouvable dans TT », et pour cela, il faut les avoir au même niveau, soit au niveau méta, soit au niveau de TT.

Si TT est arithmétiquement vraie, on peut remonter « GG est prouvable dans TT » au niveau méta en déduisant qu'il est vrai. On fait donc une rencontre au niveau méta entre « GG est faux » et « GG est vrai », qui donne une absurdité.

Si on n'a plus cette hypothèse, on ne peut plus remonter « GG est prouvable dans TT » au niveau méta. Il va falloir utiliser la réflexion. On ne peut pas réfléchir « GG est faux », par contre on peut réfléchir « GG est prouvable dans TT », ce qui donne « “GG est prouvable dans TT” est prouvable dans TT », soit encore « GG est réfutable dans TT » (il faut pour cela refaire à l'intérieur de TT la preuve triviale de GG équivalent à « GG n'est pas prouvable »). On a donc à la fois « GG est prouvable dans TT » et « GG est réfutable dans TT », ce qui donne une contradiction, mais cette fois-ci, ce n'est plus une contradiction au niveau méta, mais une contradiction un niveau plus bas : on n'aboutit pas à une absurdité, mais seulement à la conclusion que TT est incohérente.

Pour résumer, si GG est faux, alors GG est prouvable dans TT, donc par définition, “GG n'est pas prouvable dans TT” est prouvable dans TT, mais par réflexion, “GG est prouvable dans TT” est prouvable dans TT, d'où l'incohérence de TT.

Par contraposition, si TT est cohérente, alors GG est vrai, donc par définition, TT ne prouve pas GG. Mais est-ce qu'elle peut réfuter GG ? Si c'est le cas, par définition, TT prouve qu'elle prouve GG. Et par réflexion, TT prouve qu'elle réfute GG. Donc, elle prouve qu'elle est elle-même incohérente. Mais nous sommes un niveau trop bas ! Nous avons prouvé que TT prouve qu'elle est incohérente, pas que TT est incohérente.

Or une théorie peut tout à fait prouver qu'elle est incohérente… tout en étant cohérente ! La première remarque à faire, c'est qu'on peut construire, toujours par les mêmes techniques de point fixe, une théorie PA+ := PA + Coh(PA+), autrement dit PA+ est formée en ajoutant à PA l'axiome que PA+ elle-même est cohérente (pas que PA est cohérente, c'est très différent). Sauf que cette théorie est incohérente, par le second théorème d'incomplétude, car elle prouve sa propre cohérence, un axiome étant bien une démonstration. Tout ceci, David Madore l'a écrit plus en détails. Mais que dire de la théorie PA- := PA + ¬Coh(PA-), qui postule sa propre incohérence ? Supposons qu'elle soit incohérente. La preuve de ⊥ dans PA- se traduit par une preuve de Coh(PA-) dans PA. Or Coh(PA-) est plus fort que Coh(PA), et PA ne montre pas Coh(PA), toujours par le second théorème d'incomplétude, contradiction. Donc, PA- est cohérente ! La même chose s'appliquerait à ZFC. Franchement, la logique nous nargue. Nous ne pouvons pas postuler la cohérence de notre système, sans quoi il s'effondre, en revanche nous pouvons postuler impunément son incohérence et il reste cohérent (bien que, on l'espère, faux).

Nous pouvons tout de même sauver quelque chose de légèrement mieux que ce que nous avions. Notre problème est que TT pourrait prouver « il existe une preuve de ⊥ dans TT », sans qu'il existe une telle preuve. Or, clairement, si un entier nn ne code pas une preuve de ⊥ dans TT, alors TT peut le prouver, en constatant simplement que ce n'est pas une preuve valable. Débarrassons-nous de ce problème… en ajoutant une hypothèse ad-hoc.

Définition : On dit qu'un théorie du premier ordre classique TT contenant l'arithmétique via un encodage φφ est ω-cohérente lorsqu'il n'existe pas de prédicat P(n)P(n) tel que TT prouve φ(n,P(n))φ(∃ n, P(n)), mais pour tout nn, TT prouve φ(¬P(n))φ(¬P(n)).

Premier théorème d'incomplétude pour une théorie ω-cohérente : Toute théorie du premier ordre classique décidablement axiomatisée contenant l'arithmétique et ω-cohérente est incomplète.

Qu'avons-nous gagné ? D'après mon impression… pas grand-chose. Les théories intéressantes arithmétiquement fausses et pourtant ω-cohérentes n'ont pas l'air de courir les rues. Certes, je trouve ici sur Wikipédia un exemple : de même que PA + ¬Coh(PA) est fausse mais cohérente, PA + ¬ω-Coh(PA) est fausse mais ω-cohérente (où ω-Coh(PA) exprime que PA est ω-cohérente). Mais c'est un peu décevant de ne pas trouver d'exemple dont la définition ne fasse pas elle-même intervenir l'ω-cohérence. (Comme l'a écrit quelqu'un, « Une notion mathématique est intéressante si elle permet de répondre à une question que l’on peut se poser sans connaitre la notion. ».) Si vous connaissez un meilleur exemple, dites-le moi.

Si j'ai bien compris l'histoire, le théorème de Gödel est resté établi seulement sous l'hypothèse d'ω-cohérence de 1931, date de sa première preuve par Gödel, à 1936, date où Rosser (le même que celui du célèbre théorème de Church-Rosser) a proposé « l'astuce de Rosser » pour se passer de cette hypothèse en la remplaçant simplement par une hypothèse de cohérence. C'est évidemment le mieux qu'on puisse espérer, puisqu'une théorie incohérente est trivialement complète.

Premier théorème d'incomplétude pour une théorie cohérente : Toute théorie du premier ordre classique décidablement axiomatisée, contenant l'arithmétique et cohérente est incomplète.

Preuve : Rosser nous propose de faire diagonalisation avec GG équivalent à « pour toute preuve de GG dans TT codée par un entier nn, il existe une preuve de ¬G¬G dans TT codée par un entier pp tel que p<np < n ».

J'ai mis longtemps à réaliser qu'on pouvait le voir non pas comme une astuce tombée du ciel, mais comme une extension naturelle de la preuve via les machines de Turing. Dans cette preuve, on construit une machine de Turing qui énumère les entiers à la recherche d'une preuve de « je termine » ou « je ne termine pas ». Comme nous pensons à la théorie comme cohérente, il nous paraît évident que si la machine trouve une preuve de « je termine », alors il n'existe pas de preuve de « je ne termine pas » : les deux cas sont mutuellement exclusifs. Mais à y regarder de plus près, au départ, l'énoncé « la machine ne termine pas » est équivalent à « il n'existe pas de preuve que la machine ne termine pas, ou alors il en existe une mais la machine trouve avant elle une preuve qu'elle termine ». Le fait que TT n'ait pas accès à sa propre cohérence rend la distinction utile.

Supposons que TT prouve GG. Par réflexion, TT prouve qu'elle prouve GG, par une preuve de code nn. En appliquant GG à ceci, TT prouve qu'elle réfute GG, par une preuve de code p<np < n. Mais par ailleurs, comme TT est cohérente, elle ne réfute pas GG (puisqu'elle le prouve), c'est-à-dire qu'aucun pp ne peut coder une preuve de ¬G¬G, et par réflexion, TT peut prouver pour p=0,,n1p = 0, …, n-1 que pp ne code pas une preuve de ¬G¬G, et la disjonction de cas étant finie, ces preuves peuvent se rassembler. Ainsi, TT prouve à la fois qu'un tel pp existe et n'existe pas, donc TT est incohérente, absurde.

Maintenant, supposons que TT réfute GG. Soit qq le code minimal d'une preuve de ¬G¬G. Par définition de GG, TT prouve qu'il existe une preuve de GG, codée par un entier nn, telle qu'aucun entier p<np < n ne code une preuve de ¬G¬G. On peut donc tenir à l'intérieur de TT le raisonnement suivant : soit un tel nn. On n'a pas q<nq < n (car on sait par réflexion que qq code une preuve de GG), donc nqn ≤ q. Mais comme qq est une constante explicite, on peut, toujours à l'intérieur de TT, vérifier que chaque entier de 0 à qq ne code pas une preuve de ¬G¬G, ce qui est le cas puisque qq est choisi minimal. Ainsi, TT prouve une contradiction, absurde.

Ainsi, GG n'est ni prouvable ni réfutable dans TT, donc TT est incomplète. ∎

Et maintenant ? Je devrais discuter de la manière dont on traite des logiques qui ne sont pas du premier ordre. Je suis sûr que des gens ont défini ce qu'est une logique en général, via les adjonctions monoïdales antisymétriques de Stone-Yoneda dans des catégories de préfaisceaux de je-ne-sais-quoi. Comme je n'y connais rien, je vais éviter de me rendre encore plus ridicule en essayant d'en parler. Il me semble toutefois qu'on peut donner un énoncé très général du premier théorème d'incomplétude en ne supposant presque rien sur la forme de la théorie et en compensant par des hypothèses qui n'utilisent que la forme de PA. Je devrais aussi parler du second théorème d'incomplétude, du théorème de Löb et autres joyeusetés. Mais comme je commence à fatiguer, je vais laisser cette entrée incomplète quitte à la reprendre peut-être plus tard.

Merci à Jean Goubault-Larrecq de m'avoir accidentellement poussé à réfléchir par une des fameuses anecdotes dont il a le secret.

David Madore a écrit sur son blog un nombre appréciable d'entrées toutes passionnantes sur le théorème de Gödel : 1 2 3 4 5 6.

Je mentionne aussi ce texte amusant pondu par le célèbre logicien Jean-Yves Girard dans son style d'humour très particulier.


0.

On dit traditionnellement « récursivement axiomatisée », mais je n'aime pas cette terminologie.

1.

C'est à dire image par φ d'un certain énoncé de PA.


Commentaires

Laisser un commentaire