L’arithmétique de Peano suffit, parce qu’elle peut encoder le calcul

• L’arithmétique de Peano (PA) peut exprimer des processus de calcul mécaniques, donc l’extinction de toute suite de Goodstein individuelle est démontrable dans PA
• Grâce à la forme normale de Cantor et à la notation héréditaire des ordinaux, on peut représenter les suites de Goodstein et leur décroissance, ce qui permet de construire des preuves de longueur finie
• Par induction (induction forte / induction transfinie), il est possible d’étendre séparément les preuves jusqu’à certains degrés d’ordinaux
• PA peut démontrer, pour tout entier naturel n, que « G(n) atteint 0 », mais une preuve globale du théorème de Goodstein (pour tout n) est impossible
• Avec PA, on peut suffisamment implémenter l’encodage du calcul, des structures de données (List, Pair, etc.), et même du langage de programmation (Lisp) lui-même, ainsi que l’encodage de son propre processus de preuve

---

Introduction et contexte du problème

• Cet article explique que l’arithmétique de Peano (PA) peut prouver que, pour chaque n, la suite de Goodstein « atteint 0 » (G(n) terminates)
• Cela peut sembler évident pour les logiciens, mais le texte l’explique du point de vue de l’encodage du calcul afin qu’un programmeur puisse le comprendre
• Pour chaque cas d’une suite de Goodstein, il est possible de construire une routine de preuve concrète à l’intérieur de PA

Ordinaux et suites de Goodstein

• Les ordinaux (Sets as Ordinals) sont construits à la manière de Von Neumann
  • 0 est l’ensemble vide, 1 est {0}, 2 est {0,1}, ω est {0,1,2,…}, ω+1 est {0,1,2,…,ω}, etc., avec un ordre bien défini
• Les suites de Goodstein sont décrites via une notation héréditaire en base utilisant la forme normale de Cantor
  • Exemple : ω^ω est ((1,ω)), c’est-à-dire ((1,(1,1)))
  • L’ordre < est déterminé par une comparaison lexicographique sur l’ordinal et le coefficient de chaque terme

Induction et induction transfinie

• Induction dans l’arithmétique de Peano : si c’est vrai pour 0, et vrai de n à n+1, alors c’est vrai pour tous les entiers naturels
• L’induction forte est elle aussi démontrable dans PA
• Induction transfinie : dans ZFC, etc., on peut l’étendre à des ordinaux infinis et l’appliquer aux nombres écrits en forme normale de Cantor
  • Théorème 1 : toute suite décroissante en forme normale de Cantor est nécessairement finie
  • Théorème 2 : on peut appliquer l’induction transfinie aux nombres en forme normale de Cantor

Induction transfinie dans PA et longueur des preuves pour les suites de Goodstein

• PA peut générer une preuve de l’extinction d’une suite de Goodstein pour un n arbitraire
  • On peut construire la preuve selon la hauteur de tour m=O(log* n) (logarithme itéré) de la forme normale de Cantor
  • En combinant m preuves à chaque étape, on obtient une longueur totale de preuve en O(m^2), ou en O(m log m) si l’on introduit une notation spéciale (ω[m])
• En revanche, une preuve du théorème complet de Goodstein (pour tout n) est impossible dans PA (pas d’induction transfinie jusqu’à ε0)
  • Si c’était possible, on pourrait aussi démontrer la cohérence de PA, ce qui entrerait en conflit avec le second théorème d’incomplétude de Gödel

Encodage des programmes et des structures de données dans PA

• PA permet d’encoder suffisamment le calcul / les programmes / les structures de données (nombres, paires, listes et toute autre structure)
• On peut ainsi implémenter diverses fonctionnalités, par exemple :
  • logique de base et opérations (+, *, pow, //, %, min, max, etc.)
  • pattern matching et branchements conditionnels (if, cond, etc.)
  • encodage d’un nombre en deux nombres (paire), puis extension répétée de paires vers des listes et d’autres structures plus complexes (listes récursives, arbres, texte, etc.)
• Grâce à cet encodage des structures de données, il est possible de construire jusqu’à un interpréteur de machine virtuelle / langage de programmation arbitraire (Lisp, etc.)

Bootstrap et encodage vers Lisp

• En prenant Lisp comme exemple, le texte explique comment implémenter des opérations numériques et logiques de base, des structures de données, ainsi qu’un interpréteur de langage de programmation
• Toute la structure de Lisp (mappage commandes/arguments, formes spéciales, macro, etc.) peut être implémentée dans PA au moyen de combinaisons appropriées de fonctions
• Plus encore, le processus de preuve de PA lui-même, les procédures de preuve logique et les structures auto-référentielles peuvent tous être encodés et implémentés symboliquement dans PA

Encodage de la logique elle-même dans PA

• En logique mathématique, il est possible d’encoder le processus de preuve de la logique du premier ordre comme des données numériques dans PA
• Chaque étape de preuve / proposition / règle d’inférence / vérification de validité d’une preuve peut être reconnue et traitée comme une série de fonctions numériques ou de traitements de listes
• Ce type d’encodage métathéorique et auto-référentiel mène jusqu’aux preuves de l’incomplétude de Gödel et du problème de l’arrêt

Conclusion

• Le calcul, les structures de données, les programmes et même les processus de preuve logique peuvent tous être suffisamment encodés, prouvés et interprétés dans PA
• Par conséquent, toute suite de Goodstein arbitraire (pour un n donné, extinction de G(n)) peut être prouvée concrètement à l’intérieur de PA
• En revanche, une preuve affirmant, pour le théorème complet de Goodstein (pour tout n), que « PA démontre le théorème de Goodstein dans PA » est impossible en raison des limites de la logique
• Du point de vue d’un programmeur, PA constitue une base logique complète capable d’encoder le calcul lui-même

[GN⁺]

Commentaire Hacker News

• Cet article est la version blog d’une question que j’avais posée sur Stack Overflow ; il explique les limites de ce qu’on peut prouver dans le système d’axiomes de Peano et comment bootstrapper Lisp à l’intérieur de l’arithmétique de Peano. Les blagues sont surtout dans la deuxième section. Les corrections et questions supplémentaires sont les bienvenues.
  • En lisant l’article, j’ai remarqué dans la section "Why Lisp?" un endroit où les parenthèses ne correspondent pas (voir l’exemple defun not (x) (if x false true)). Dès que quelqu’un commence à utiliser des parenthèses, j’ai le réflexe de vérifier qu’elles sont bien fermées. Puis j’ai éclaté de rire en voyant plus loin la remarque disant qu’"il est facile de programmer un ordinateur pour vérifier si les parenthèses sont équilibrées". Ce genre de blague m’a vraiment fait rire, et le commentaire ; After a while, you stop noticing that stack of closing parens. dans la section "Basic Number Theory" m’a aussi marqué. Cela faisait longtemps que je n’avais pas replongé dans Lisp, et j’ai trouvé l’article vraiment amusant.
  • Cet article est vraiment fascinant. Je n’ai encore lu que l’introduction, mais je trouve intéressant que, dans l’arithmétique de Peano (PA), on puisse prouver que tous les cas particuliers d’une suite de Goodstein finissent par atteindre 0, alors qu’on ne peut pas prouver que tous les cas atteignent 0 (même si, au fond, c’est un résultat attendu, cela reste passionnant). Et le fait qu’on puisse encoder le calcul avec la seule arithmétique de Peano est vraiment étrange à mes yeux (évident en principe, mais je n’avais jamais poussé la réflexion à ce niveau d’auto-référence). J’ai justement récemment essayé d’aller un peu plus loin en théorie des ensembles et j’ai étudié la partie sur les suites de Goodstein dans le manuel Intro to Set Theory. Si quelqu’un a des recommandations de manuels avancés sur la théorie des ensembles ou d’ouvrages qui creusent vraiment l’arithmétique de Peano, je suis preneur. Mon petit objectif est de comprendre pourquoi PA est insuffisant pour démontrer le théorème de Goodstein, mais je suis aussi ouvert à d’autres pistes.
  • À deux endroits dans l’article, l’auteur a oublié d’écrire les omégas sous la forme \omega.
• C’est très proche de la théorie de Boyer-Moore. Cette théorie construit les mathématiques au niveau de l’arithmétique de Peano. Boyer et Moore ont développé un démonstrateur automatique de théorèmes qui implémente cette théorie, et il en existe aussi une copie fonctionnant avec GNU Common LISP. Les liens vers l’article "A Computational Logic" et l’implémentation de nqthm valent le détour. Dans l’article, j’ai trouvé frappant l’exemple montrant que, si l’on part des axiomes de Peano, des théorèmes complexes comme la multiplication des nombres premiers sont difficiles, mais que la commutativité de l’addition, la distributivité de la multiplication ou encore des théorèmes liés à la fonction GCD restent tout à fait démontrables.
• J’ai une formation à la fois en mathématiques et en programmation, et personnellement je trouve encore plus intéressant le fait que la partie sur l’indépendance du théorème de Goodstein semble contournable d’une manière auto-référentielle. Je me demande si, en ajoutant à PA l’hypothèse "PA est oméga-cohérent" (omega-consistent), on pourrait démontrer le théorème de Goodstein, et peut-être aussi obtenir l’induction transfinie jusqu’à epsilon_0. EDIT : peut-être même que "PA est cohérent" suffirait ?
  • Malheureusement non. Et il se trouve que non seulement Con(PA) n’est pas suffisant, mais qu’aucune formule universellement quantifiée arbitraire ne suffit non plus. Voir cette réponse pertinente sur Math StackExchange. Concernant votre première question, je suis curieux de savoir comment on encode exactement l’oméga-cohérence comme formule de PA ; cela ne me vient pas immédiatement à l’esprit.
  • C’est moi qui ai posé la question sur Stack Overflow. J’y ai ajouté des liens vers quelques réponses supplémentaires. En substance, "PA est cohérent" ne suffit pas, mais une sorte de "principe de réflexion uniforme" disant que "si c’est démontrable dans PA, alors c’est vrai" suffit. Je ne peux pas affirmer avec certitude que ce principe est exactement équivalent à l’oméga-cohérence, mais c’est ainsi que je comprends l’explication sur Wikipédia. Si T est oméga-cohérent, cela signifie que "T + RFN_T + l’ensemble de toutes les formules vraies est cohérent", ce qui se lit comme équivalent à "T + RFN_T est vrai".
  • J’aime aussi cette structure d’induction (de récursion). Au bout du compte, on construit une méta-preuve sur ce que PA démontre, et si l’on fait confiance à PA, on peut aussi faire confiance à cette méta-preuve. En revanche, je ne comprends pas encore clairement en quoi le simple ajout de "PA est cohérent" suffirait. J’ai l’impression que PA + "PA est cohérent" permettrait qu’il existe un modèle dans lequel le théorème de Goodstein est vrai pour les entiers naturels standards, tout en autorisant aussi un modèle dans lequel il est faux pour un certain entier non standard N. Il me semble qu’un énoncé plus fort, comme l’oméga-cohérence, exclurait ce genre de cas.
  • Le billet sur Math StackExchange mentionne qu’une preuve de PA + induction transfinie jusqu’à epsilon_0 prouve PA lui-même. J’ai l’impression que PA + "PA est cohérent" devrait permettre de démontrer l’induction transfinie jusqu’à epsilon_0.
  • J’ai l’impression qu’on entre ici dans des détails au-delà de ce sur quoi je peux parler confortablement. D’après ChatGPT, PA + PA est cohérent ne suffit pas. Comme ChatGPT a sans doute ingurgité énormément d’ouvrages de logique, je suis tenté de lui faire confiance sur ce point.
• Le commentaire que j’ai écrit à JoJoModding sur Stack Overflow n’est pas correct. J’avais dit : "dans les modèles non standards de PA, il existe des entiers naturels infinis, donc même si PA prouve qu’il a produit une certaine preuve, il ne peut pas prouver que cette preuve est de longueur finie". Mais en réalité, si PA prouve que "PA a démontré X", alors PA démontre aussi X lui-même. Le point important n’est pas l’existence de modèles non standards, mais le fait que le modèle standard des entiers naturels est bien un modèle de PA. Donc si "PA prouve qu’il prouve X", cela produit effectivement une preuve correspondant à un entier standard fini, et on peut s’en servir pour construire dans PA une vraie preuve de X.
  • Je n’ai pas le temps d’examiner le raisonnement en détail, mais en langage naturel il me semble que la différence essentielle est entre "PA prouve forall n, G(n)" et "PA prouve forall n, Provable(G(n))". Je suis plutôt faible en logique, donc si quelqu’un peut m’expliquer concrètement pourquoi prouver forall n, Provable(P(n)) ne permet pas de prouver Provable(forall n, P(n)), je lui en serais reconnaissant.
  • L’énoncé "si PA prouve que ‘PA prouve X’, alors PA prouve X" n’est pas correct. On peut définir dans PA une fonction qui parcourt toutes les preuves possibles, et j’ai d’ailleurs esquissé cette approche à la fin de ma réponse. À partir de là, on peut aussi définir des fonctions comme will-return et opposite-return, ce qui rejoint la preuve standard du problème de l’arrêt. Si l’on considère le cas opposite-return(opposite-return, opposite-return), alors si PA prouve que opposite-return retourne, il prouve aussi qu’en fait il ne retourne pas ; et inversement, s’il prouve qu’il ne retourne pas, il prouve qu’il retourne. Si PA adoptait un principe plus fort du type "tout ce qui est démontrable est effectivement démontrable", on tomberait immédiatement sur le second théorème d’incomplétude de Gödel, ce qui signifierait que PA est contradictoire. Il faut donc absolument distinguer "PA prouve" de "PA prouve qu’il prouve".
• Le pur lambda-calcul suffit lui aussi, puisque le lambda-calcul encode déjà le calcul.
• En discutant des types de données inductifs avec quelqu’un, je lui ai montré la définition de Nat à base de zero/succ (comme on en voit dans Lean ou Rocq). La personne s’est demandé : "Est-ce que cela suffit à lui seul ?", "A-t-on vraiment besoin de l’arithmétique de Peano ?", "Existe-t-il quelque chose d’encore plus primitif que les types de données inductifs ?" Cela m’a rappelé qu’il est utile de ne pas considérer l’arithmétique de Peano comme une évidence essentielle, mais simplement comme un choix de conception parmi d’autres.
  • À la question "y a-t-il quelque chose de plus fondamental que les types de données inductifs ?", je répondrais que les entiers naturels eux-mêmes sont plus primitifs que les types de données inductifs. Tous les types de données inductifs peuvent être construits à partir des entiers naturels et de quelques autres constructeurs de types primitifs (Π, Σ, =, Ω).
• Voir aussi cette Q&R sur le théorème de Kirby-Paris.
• À propos de la cohérence de PA, voici une vidéo expliquant en quoi elle est démontrable à l’intérieur de PA : lien YouTube
  • C’est un point qu’il faut absolument expliquer aux non-logiciens. D’après le second théorème d’incomplétude de Gödel, si PA pouvait démontrer sa propre cohérence, alors PA serait contradictoire (et pourrait donc démontrer n’importe quoi, y compris des choses fausses). Cette vidéo ne montre pas que PA démontre qu’il est contradictoire ; elle montre qu’au sens plus faible, PA peut démontrer sa "propre cohérence". Sans bases solides en logique, il est difficile de comprendre cela précisément, mais c’est suffisamment intéressant pour mériter qu’on s’y attarde.
• Ce sujet a récolté 123 points ici, alors que le post original sur SO n’a reçu que 11 upvotes.
  • Sur Stack Overflow, il faut 15 points pour pouvoir upvoter. Entre la question de la réputation et cette limite des 15 points, cela décourage peut-être les gens de participer et empêche sans doute aussi davantage d’upvotes.
• Le calcul suffit-il à lui seul ? Les réels calculables ne sont qu’un sous-ensemble de l’ensemble des réels.
  • Je pense que le mot même de "réels" est un terme trompeur. On peut interpréter les réels comme représentant des rapports physiques réels. Par exemple, dire 180,255 livres signifie le rapport physique réel entre le poids réel de Jones et l’unité standard de la livre. Ces rapports existent aussi physiquement ; en ce sens, les réels peuvent être vus comme des rapports physiques. Aujourd’hui, on a plutôt tendance à considérer les nombres comme des concepts abstraits séparés du réel, dans une perspective typiquement platonicienne. Mais dans la pratique, il est impossible de mesurer ou de représenter quoi que ce soit avec une précision infinie. Par exemple, au-delà de 50 chiffres de précision, des limites quantiques rendent la mesure impossible. Si l’on voulait mesurer sans erreur l’orbite des corps du système solaire, au-delà de 50 chiffres il faudrait prendre en compte l’effet de masse des étoiles voisines ; au-delà de 100 chiffres, il faudrait modéliser la galaxie entière, et à la fin il faudrait intégrer des influences physiques impossibles à mesurer. Donc, dans le monde réel, seule une mathématique à précision finie est possible. Autrement dit, en principe tout est calculable, mais à mesure qu’on pousse vers l’infini, le modèle mathématique lui-même perd son sens.
  • Vraiment ? En fait, l’idée qu’"il y a davantage de non dénombrable" part d’un malentendu. Voir mon explication ici. Si l’on accepte qu’il y ait "plus" de non dénombrable, on est forcé d’adopter une position controversée sur ce que signifie "exister". Voir aussi cette discussion connexe. Enfin, même si l’on pousse le raisonnement logique jusqu’au bout, tout peut toujours être représenté sur un ordinateur. Même si l’on ajoute de grands ensembles à ZFC, on peut partir de PA et dériver n’importe quelle conclusion ; en pratique, j’en conclus donc que PA suffit. Si vous avez besoin d’être davantage convaincu, je recommande le livre Gödel, Escher, Bach.
  • Ma position est un peu différente. Les réels en général ne peuvent pas être manipulés, symbolisés ou enregistrés sous quelque forme que ce soit, mais les énoncés portant sur les réels peuvent souvent être exprimés et calculés de manière utile. J’aime beaucoup les tentatives, chez Harvey Friedman ou chez l’auteur de cet article, de produire des valeurs d’une complexité inimaginable à partir de systèmes simples. (À noter : le site audiomulch n’est pas accessible.)
  • Sans objectif précis attaché au mot "suffit", la question reste mal définie. Suffisant pour quoi ? C’est cela qui importe.
  • Je pense que la question "le calcul suffit-il à lui seul ?" est mal posée. Bien sûr que non. Si c’était le cas, cela donnerait raison à ceux qui voient la réalité comme une simple mécanique d’horlogerie. Le réel est bien plus intéressant et bien plus complexe que cela.