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 calculablement 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.
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écidablement1 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 𝒯.
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 BudgetZéro et BudgetSucc ainsi qu'un symbole de prédicat Budget, et en changeant chaque axiome 𝐴 en l'axiome 𝐴 ∧ Budget(⟨𝑛⟩), où 𝑛 est le temps de calcul de 𝐷 sur 𝐴, avec le codage ⟨0⟩ := BudgetZéro et ⟨𝑛+1⟩ := BudgetSucc(⟨𝑛⟩). Clairement, 𝒯' est calculablement 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 très liées. 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.
Il devient un peu moins flagrant dans cette reformulation qu'il faut supposer 𝒯 est calculablement 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 calculablement 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. Par le lemme diagonal, il existe un énoncé arithmétique2 𝐺 que 𝒯 prouve équivalent à « 𝐺 est réfutable dans 𝒯 ». Si 𝐺 est vrai, alors par définition il est réfuté par 𝒯, impossible car 𝒯 est arithmétiquement vraie. Donc 𝐺 est faux, donc par définition il n'est pas réfutable. Mais comme il est faux, il n'est pas non plus prouvable (à nouveau car 𝒯 est arithmétiquement vraie). Donc 𝐺 est indécidable dans 𝒯. □
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 à « 𝐺 est réfutable 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.
Supposons 𝐺 vrai. Par définition, 𝐺 est réfutable dans 𝒯. Cette fois, nous ne pouvons plus déduire immédiatement une contradiction : si 𝒯 n'est plus arithmétiquement vraie, elle peut parfaitement réfuter 𝐺 même si 𝐺 est vrai. Mais tout espoir n'est pas perdu. On va raisonner différemment, en descendant encore d'un niveau pour regarder ce que 𝒯 prouve/réfute qu'elle prouve/réfute. Puisque 𝒯 réfute 𝐺, par définition de 𝐺, elle prouve qu'elle ne réfute pas 𝐺. Mais comme elle réfute 𝐺, elle peut aussi prouver qu'elle réfute 𝐺, par réflexion de la preuve : il existe une preuve que 𝒯 réfute 𝐺, et on peut encoder cette preuve arithmétiquement dans 𝒯, l'accompagner d'une preuve triviale que toutes les règles ont bien été suivies, et en déduire une preuve dans 𝒯 que 𝒯 réfute 𝐺. Donc, 𝒯 prouve à la fois qu'elle réfute et qu'elle ne réfute pas 𝐺, ce qui entraîne que 𝒯 est incohérente.
Par contraposition, si 𝒯 est cohérente, alors 𝐺 est faux, donc par définition, 𝒯 ne réfute pas 𝐺. Mais est-ce qu'elle peut prouver 𝐺 ? Si c'est le cas, 𝒯 prouve qu'elle réfute 𝐺, et pourtant ne réfute pas 𝐺… pas de contradiction en vue, car 𝒯 n'est pas supposée arithmétiquement vraie ! Ici, nous sommes coincés.
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 réfutation de 𝐺 dans 𝒯 », sans qu'il existe une telle réfutation. Or, clairement, si un entier 𝑛 ne code pas une réfutation 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.
Dans le troisième essai, nous avons fait une disjonction de cas entre « 𝐺 est vrai » et « 𝐺 est faux ». Et si nous essayions plutôt « 𝐺 est prouvable dans 𝒯 », « 𝐺 est réfutable dans 𝒯 » et « 𝐺 est indécidable dans 𝒯 » ?
Supposons 𝐺 prouvable dans 𝒯. Par définition, 𝒯 prouve qu'elle réfute 𝐺. Et par réflexion, elle prouve qu'elle prouve 𝒯. Donc, elle prouve qu'elle est incohérente. Mais nous ne somme toujours pas contents ! Ce que nous voulions, c'est prouver que 𝒯 est incohérente, pas qu'elle prouve elle-même qu'elle 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).
Donc, nous sommes à nouveau coincés. Et à nouveau, l'ω-cohérence dissout le problème, car si 𝒯 est ω-cohérente, elle ne peut pas prouver son incohérence. En effet, supposons par l'absurde que 𝒯 ω-cohérente prouve son incohérence. Elle est cohérente (toute théorie ω-cohérente est trivialement cohérente), donc en posant 𝑃(𝑛) := « 𝑛 code une preuve de ⊥ dans 𝒯 », on voit que 𝒯 prouve ∃ 𝑛, 𝑃(𝑛), mais pour tout 𝑛, 𝒯 prouve ¬𝑃(𝑛) (en vérifiant simplement que 𝑛 ne code pas une preuve de ⊥ dans 𝒯), d'où une contradiction avec l'ω-cohérence.
Ainsi, sous l'hypothèse d'ω-cohérence, nous pouvons prouver que 𝐺 n'est pas prouvable. De manière symétrique, on montre qu'il n'est pas réfutable. Donc 𝐺 est indécidable. Nous avons une preuve alternative, mais l'ω-cohérence n'a pas voulu nous lâcher.
Continuons à explorer les variantes de la diagonalisation. Nous avons essayé 𝐺 équivalent à « 𝐺 est réfutable dans 𝒯 », et aussi, pour le théorème d'indéfinissabilité de Tarski, 𝐺 équivalent à « 𝐺 est faux ». Quid de 𝐺 équivalent à « 𝐺 n'est pas prouvable dans 𝒯 » ? C'est la preuve d'origine par Gödel.
Si 𝐺 est prouvable dans 𝒯, alors 𝒯 prouve à la fois qu'elle prouve 𝐺 (par réflexion) et qu'elle ne le prouve pas (par définition), donc 𝒯 est incohérente.
En revanche, si 𝐺 est réfutable dans 𝒯, alors 𝒯 prouve qu'elle réfute 𝐺 (par réflexion), et qu'elle le prouve (par définition). Ici, on retrouve le même problème que précédemment, à savoir que 𝒯 prouve qu'elle est incohérente, mais pour passer de « 𝒯 prouve qu'elle est incohérente » à « 𝒯 est incohérente », il faut une hypothèse d'ω-cohérence.
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 : L'astuce très élégante de Rosser, c'est de faire la 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 𝑝 < 𝑛 ».
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 𝑝 = 0, …, 𝑛-1 que 𝑝 ne code pas une preuve de ¬𝐺, et la disjonction de cas étant finie, ces preuves peuvent se rassembler. Ainsi, 𝒯 prouve à la fois qu'il existe 𝑝 < 𝑛, et qu'un tel 𝑝 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.