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 vérifiant de « bonnes hypothèses » est incomplet, c'est-à-dire qu'il existe une proposition telle que ne prouve ni ni .
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 les propositions de la forme « termine », où 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 , on construit l'énoncé = « termine », et on recherche en parallèle une preuve de , et une preuve de . 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 telle que ni ni 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 . Il construit un codage dans PA de la proposition = « 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 ou une preuve de , ce qui est possible grâce au fait que PA a un ensemble d'axiomes décidable. S'il rencontre une preuve de , il accepte, et inversement, s'il rencontre une preuve de , il rejette. Par l'hypothèse que PA est complète, il existe une démonstration de ou une démonstration de , 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 , 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 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 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 , donc il faut que soit décidablement0 axiomatisée, c'est-à-dire que l'ensemble des axiomes de doit être décidable. Par ailleurs, nous nous sommes servis d'un codage calculable de « 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 de manière raisonnable :
Définition : On dit qu'une théorie du premier ordre classique contient l'arithmétique s'il existe un encodage calculable des énoncés de PA vers les énoncés de tel que pour tout énoncé de PA, , et de plus, si est prouvable dans PA, alors est prouvable dans . 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é de PA, si prouve , alors est vrai (dans ℕ).
Remarque : Si est arithmétiquement vraie et est réfutable, alors est faux (car , 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 une telle théorie, soit l'encodage depuis PA, et supposons complète. Construisons l'algorithme qui prend , qui construit = « termine », calcule , puis cherche une preuve de ou (grâce au fait que est décidablement axiomatisée). Il termine par complétude de , et résout le problème de l'arrêt car 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 ou de , mais on peut accepter que la vérification ne termine pas si on n'a pas une démonstration de ou , à 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 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 semi-décidablement axiomatisée. Soit un semi-algorithme (mettons une machine de Turing) qui semi-décide l'ensemble des axiomes de . On forme une théorie en rajoutant à des symboles de fonction et ainsi qu'un symbole de prédicat , et en changeant chaque axiome en l'axiome , où est le temps de calcul de sur , avec le codage et . Clairement, est décidablement axiomatisée, et c'est une extension conservatrice de .
(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 plutôt que ? 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 complète, alors on peut construire un programme qui, via une recherche de preuve/réfutation dans de « 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 « 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é , à savoir « termine », tel que est équivalent à « 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 est équivalent à « est réfutable » revient à dire que est équivalent à « n'est pas prouvable ». Il se trouve que dans la présentation usuelle, est équivalent à « n'est pas prouvable », donc je vais inverser et pour avoir le bon sens (autrement dit, plutôt que « termine », je considère finalement « ne termine pas »).
Il devient un peu moins flagrant dans cette reformulation qu'il faut supposer que est décidablement axiomatisée et contient l'arithmétique, mais faire fonctionner l'autoréférence, il faut que puisse parler de ses propres preuves. Pour encoder la définition d'une preuve dans , il faut bien qu'elle contienne l'arithmétique, et pour que puisse vérifier ses propres axiomes, elle doit être décidablement axiomatisée.
La preuve simplifiée est donc : Soit 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 est vrai si et seulement s'il est prouvable. Mais par le lemme diagonal, il existe un énoncé arithmétique équivalent à « n'est pas prouvable dans », d'où une contradiction. ∎
Sous les mêmes hypothèses sur qu'à la section précédente, on peut imaginer une variante de la diagonalisation, où au lieu de construire équivalent à « n'est pas prouvable dans », on le construit équivalent à « 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 formalise « est faux » de manière uniforme : qu'on puisse définir dans un prédicat tel que pour tout entier , l'énoncé codé par est équivalent à . 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 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 est arithmétiquement vraie et cherchons par quoi la remplacer.
Reprenons équivalent à « n'est pas prouvable dans ». Supposons faux. Par définition, est prouvable dans . Cette fois, nous ne pouvons plus déduire immédiatement une contradiction : si n'est plus arithmétiquement vraie, elle peut parfaitement prouver même si est faux. Mais tout espoir n'est pas perdu.
Je vois les choses de cette façon : On a « est faux », qui par définition entraîne « est prouvable dans ». On veut provoquer une rencontre entre « est faux » et « est prouvable dans », et pour cela, il faut les avoir au même niveau, soit au niveau méta, soit au niveau de .
Pour remonter un énoncé , on est obligé de supposer que est arithmétiquement vraie, auquel cas on peut passer de « est prouvable dans » à « est vrai ».
Pour descendre un énoncé, l'outil est la réflexion des preuves. « est vrai » n'implique pas « est prouvable dans », mais en revanche, si on a « est prouvable dans », on peut prendre une preuve, l'écrire dans et l'accompagner d'une preuve triviale que toutes les règles ont été suivies à chaque étape, et cela permet de déduire « “ est prouvable dans ” est prouvable dans ».
Si est arithmétiquement vraie, on peut remonter « est prouvable dans » au niveau méta en déduisant qu'il est vrai. On fait donc une rencontre au niveau méta entre « est faux » et « est vrai », qui donne une absurdité.
Si on n'a plus cette hypothèse, on ne peut plus remonter « est prouvable dans » au niveau méta. Il va falloir utiliser la réflexion. On ne peut pas réfléchir « est faux », par contre on peut réfléchir « est prouvable dans », ce qui donne « “ est prouvable dans ” est prouvable dans », soit encore « est réfutable dans » (il faut pour cela refaire à l'intérieur de la preuve triviale de équivalent à « n'est pas prouvable »). On a donc à la fois « est prouvable dans » et « est réfutable dans », 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 est incohérente.
Pour résumer, si est faux, alors est prouvable dans , donc par définition, “ n'est pas prouvable dans ” est prouvable dans , mais par réflexion, “ est prouvable dans ” est prouvable dans , d'où l'incohérence de .
Par contraposition, si est cohérente, alors est vrai, donc par définition, ne prouve pas . Mais est-ce qu'elle peut réfuter ? Si c'est le cas, par définition, prouve qu'elle prouve . Et par réflexion, prouve qu'elle réfute . Donc, elle prouve qu'elle est elle-même incohérente. Mais nous sommes un niveau trop bas ! Nous avons prouvé que prouve qu'elle est incohérente, pas que 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 pourrait prouver « il existe une preuve de ⊥ dans », sans qu'il existe une telle preuve. Or, clairement, si un entier ne code pas une preuve de ⊥ dans , alors 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 contenant l'arithmétique via un encodage est ω-cohérente lorsqu'il n'existe pas de prédicat tel que prouve , mais pour tout , prouve .
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 équivalent à « pour toute preuve de dans codée par un entier , il existe une preuve de dans codée par un entier tel que ».
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 n'ait pas accès à sa propre cohérence rend la distinction utile.
Supposons que prouve . Par réflexion, prouve qu'elle prouve , par une preuve de code . En appliquant à ceci, prouve qu'elle réfute , par une preuve de code . Mais par ailleurs, comme est cohérente, elle ne réfute pas (puisqu'elle le prouve), c'est-à-dire qu'aucun ne peut coder une preuve de , et par réflexion, peut prouver pour que ne code pas une preuve de , et la disjonction de cas étant finie, ces preuves peuvent se rassembler. Ainsi, prouve à la fois qu'un tel existe et n'existe pas, donc est incohérente, absurde.
Maintenant, supposons que réfute . Soit le code minimal d'une preuve de . Par définition de , prouve qu'il existe une preuve de , codée par un entier , telle qu'aucun entier ne code une preuve de . On peut donc tenir à l'intérieur de le raisonnement suivant : soit un tel . On n'a pas (car on sait par réflexion que code une preuve de ), donc . Mais comme est une constante explicite, on peut, toujours à l'intérieur de , vérifier que chaque entier de 0 à ne code pas une preuve de , ce qui est le cas puisque est choisi minimal. Ainsi, prouve une contradiction, absurde.
Ainsi, n'est ni prouvable ni réfutable dans , donc 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.
On dit traditionnellement « récursivement axiomatisée », mais je n'aime pas cette terminologie.
C'est à dire image par φ d'un certain énoncé de PA.
Laisser un commentaire