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 $T$ vérifiant de « bonnes hypothèses » est incomplet, c'est-à-dire qu'il existe une proposition $P$ telle que $T$ ne prouve ni $P$ ni $¬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.

Un premier essai : l'arithmétique de Peano

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 $T$ les propositions de la forme « $X$ termine », où $X$ 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 $X$, on construit l'énoncé $P$ = « $X$ termine », et on recherche en parallèle une preuve de $P$, et une preuve de $¬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 $P$ telle que ni $P$ ni $¬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 $X$. Il construit un codage dans PA de la proposition $P$ = « $X$ 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 $P$ ou une preuve de $¬P$, ce qui est possible grâce au fait que PA a un ensemble d'axiomes décidable. S'il rencontre une preuve de $P$, il accepte, et inversement, s'il rencontre une preuve de $¬P$, il rejette. Par l'hypothèse que PA est complète, il existe une démonstration de $P$ ou une démonstration de $¬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 $X$, 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 Σ₁, et bien sûr sa négation fonctionne aussi et est au niveau Π₁, alors qu'au niveau Σ₀ = Π₀, tout est évidemment décidé.

Deuxième essai : une théorie arithmétiquement vraie

Comment généraliser cette démonstration à un système logique $T$ 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 $T$ 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 $T$, donc il faut que $T$ soit décidablement⁰ axiomatisée, c'est-à-dire que l'ensemble des axiomes de $T$ doit être décidable. Par ailleurs, nous nous sommes servis d'un codage calculable de « $X$ 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 $T$ de manière raisonnable :

Définition : On dit qu'une théorie du premier ordre classique $T$ contient l'arithmétique s'il existe un encodage calculable $φ$ des énoncés de PA vers les énoncés de $T$ tel que pour tout énoncé $P$ de PA, $φ(¬P) = ¬φ(P)$, et de plus, si $P$ est prouvable dans PA, alors $φ(P)$ est prouvable dans $T$. 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é $P$ de PA, si $T$ prouve $φ(P)$, alors $P$ est vrai (dans $ℕ$).

Remarque : Si $T$ est arithmétiquement vraie et $φ(P)$ est réfutable, alors $P$ est faux (car $¬φ(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 $T$ une telle théorie, soit $φ$ l'encodage depuis PA, et supposons $T$ complète. Construisons l'algorithme qui prend $X$, qui construit $P$ = « $X$ termine », calcule $φ(P)$, puis cherche une preuve de $φ(P)$ ou $¬φ(P)$ (grâce au fait que $T$ est décidablement axiomatisée). Il termine par complétude de $T$, et résout le problème de l'arrêt car $T$ 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 Σ₁ indécidable dans ZFC).

Aparté : et si la théorie est semi-décidablement axiomatisée ?

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 $P$ ou de $¬P$, mais on peut accepter que la vérification ne termine pas si on n'a pas une démonstration de $P$ ou $¬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 $T$ 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 $T$ semi-décidablement axiomatisée. Soit $D$ un semi-algorithme (mettons une machine de Turing) qui semi-décide l'ensemble des axiomes de $T$. On forme une théorie $T'$ en rajoutant à $T$ des symboles de fonction $\text{BudgetZéro}$ et $\text{BudgetSucc}$ ainsi qu'un symbole de prédicat $\text{Budget}$, et en changeant chaque axiome $A$ en l'axiome $A ∧ \text{Budget}(⟨n⟩)$, où $n$ est le temps de calcul de $D$ sur $A$, avec le codage $⟨0⟩ := \text{BudgetZéro}$ et $⟨n+1⟩ := \text{BudgetSucc}(⟨n⟩)$. Clairement, $T'$ est décidablement axiomatisée, et c'est une extension conservatrice de $T$.

(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 $T$ plutôt que $T'$ ? 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.)

Reformulation du deuxième essai : éliminons les coupures

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 $T$ complète, alors on peut construire un programme $X$ qui, via une recherche de preuve/réfutation dans $T$ de « $X$ 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 « $X$ 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é $G$, à savoir « $X$ termine », tel que $G$ est équivalent à « $G$ 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 $G$ est équivalent à « $G$ est réfutable » revient à dire que $¬G$ est équivalent à « $¬G$ n'est pas prouvable ». Il se trouve que dans la présentation usuelle, $G$ est équivalent à « $G$ n'est pas prouvable », donc je vais inverser $G$ et $¬G$ pour avoir le bon sens (autrement dit, plutôt que « $X$ termine », je considère finalement « $X$ ne termine pas »).

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

La preuve simplifiée est donc : Soit $T$ 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étique¹ $G$ est vrai si et seulement s'il est prouvable. Mais par le lemme diagonal, il existe un énoncé arithmétique $G$ équivalent à « $G$ n'est pas prouvable dans $T$ », d'où une contradiction. ∎

Intermède : le théorème d'indéfinissabilité de Tarski

Sous les mêmes hypothèses sur $T$ qu'à la section précédente, on peut imaginer une variante de la diagonalisation, où au lieu de construire $G$ équivalent à « $G$ n'est pas prouvable dans $T$ », on le construit équivalent à « $G$ 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 $T$ formalise « $G$ est faux » de manière uniforme : qu'on puisse définir dans $T$ un prédicat $P(n)$ tel que pour tout entier $n$, l'énoncé codé par $n$ est équivalent à $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 ».

Troisième essai : une théorie ω-cohérente

Peut-on affaiblir l'hypothèse que $T$ 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 $T$ est arithmétiquement vraie et cherchons par quoi la remplacer.

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

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

• Pour remonter un énoncé $P$, on est obligé de supposer que $T$ est arithmétiquement vraie, auquel cas on peut passer de « $P$ est prouvable dans $T$ » à « $P$ est vrai ».

• Pour descendre un énoncé, l'outil est la réflexion des preuves. « $P$ est vrai » n'implique pas « $P$ est prouvable dans $T$ », mais en revanche, si on a « $P$ est prouvable dans $T$ », on peut prendre une preuve, l'écrire dans $T$ et l'accompagner d'une preuve triviale que toutes les règles ont été suivies à chaque étape, et cela permet de déduire « “$P$ est prouvable dans $T$” est prouvable dans $T$ ».

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

Si on n'a plus cette hypothèse, on ne peut plus remonter « $G$ est prouvable dans $T$ » au niveau méta. Il va falloir utiliser la réflexion. On ne peut pas réfléchir « $G$ est faux », par contre on peut réfléchir « $G$ est prouvable dans $T$ », ce qui donne « “$G$ est prouvable dans $T$” est prouvable dans $T$ », soit encore « $G$ est réfutable dans $T$ » (il faut pour cela refaire à l'intérieur de $T$ la preuve triviale de $G$ équivalent à « $G$ n'est pas prouvable »). On a donc à la fois « $G$ est prouvable dans $T$ » et « $G$ est réfutable dans $T$ », 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 $T$ est incohérente.

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

Par contraposition, si $T$ est cohérente, alors $G$ est vrai, donc par définition, $T$ ne prouve pas $G$. Mais est-ce qu'elle peut réfuter $G$ ? Si c'est le cas, par définition, $T$ prouve qu'elle prouve $G$. Et par réflexion, $T$ prouve qu'elle réfute $G$. Donc, elle prouve qu'elle est elle-même incohérente. Mais nous sommes un niveau trop bas ! Nous avons prouvé que $T$ prouve qu'elle est incohérente, pas que $T$ 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 $T$ pourrait prouver « il existe une preuve de ⊥ dans $T$ », sans qu'il existe une telle preuve. Or, clairement, si un entier $n$ ne code pas une preuve de ⊥ dans $T$, alors $T$ 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 $T$ contenant l'arithmétique via un encodage $φ$ est ω-cohérente lorsqu'il n'existe pas de prédicat $P(n)$ tel que $T$ prouve $φ(∃ n, P(n))$, mais pour tout $n$, $T$ prouve $φ(¬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.

Quatrième essai : Rosser, notre sauveur

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 $G$ équivalent à « pour toute preuve de $G$ dans $T$ codée par un entier $n$, il existe une preuve de $¬G$ dans $T$ codée par un entier $p$ tel que $p < 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 $T$ n'ait pas accès à sa propre cohérence rend la distinction utile.

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

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

Ainsi, $G$ n'est ni prouvable ni réfutable dans $T$, donc $T$ est incomplète. ∎

Épilogue

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.

Remerciements, pointeurs

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.

Commentaires