Pourquoi l’arithmétique de Peano suffit : PA peut encoder le calcul

 (math.stackexchange.com)
1 points par GN⁺ 2025-06-15 | 1 commentaires | Partager sur WhatsApp
  • PA ne peut pas démontrer l’énoncé complet du théorème de Goodstein, ∀n G(n), mais pour chaque entier naturel standard n, il est possible de montrer à l’intérieur de PA qu’il existe une preuve dans PA de G(n)
  • L’idée centrale consiste à ne traiter que la tour finie de puissances de ω nécessaire pour n, et à construire mécaniquement, sur cet intervalle, une preuve par induction transfinie
  • La hauteur nécessaire m correspond à la hauteur de la hereditary base notation de n, vaut O(log*(n)), et en utilisant une notation abrégée comme ω^[m], la longueur de la preuve se réduit à O(m log m)
  • Ce résultat signifie qu’« on peut construire une preuve pour chaque cas », et non que PA démontre le théorème de Goodstein dans son ensemble
  • PA peut encoder dans un seul entier naturel des nombres, des paires, des listes, des états de programme et des preuves en logique formelle ; il est donc aussi possible, dans PA, de vérifier qu’une preuve générée est bien une véritable preuve dans PA

Formulation mathématique de la question

  • L’objet étudié est l’énoncé G(n) affirmant qu’une suite de Goodstein finit par atteindre 0

  • La distinction connue est la suivante

    • PA peut démontrer chaque cas concret sur les entiers naturels standard, comme G(15) ou G(268)
    • PA ne peut pas démontrer l’énoncé global ∀n ∈ N: G(n)

  • La question est de savoir si PA peut démontrer un énoncé de la forme suivante

    ∀n ∈ N: ∃p ∈ N: P_PA(p, ⌜G(n)⌝)

  • P_PA(p, ⌜φ⌝) signifie que p est le code d’une preuve de φ dans PA

  • La conclusion est qu’à ce niveau, PA seul suffit

Ce que PA doit démontrer

  • Pour chaque n, PA doit montrer les trois points suivants
    • on peut calculer la longueur de preuve nécessaire pour démontrer G(n)
    • la procédure qui construit cette preuve se termine
    • la dernière phrase de la preuve construite affirme bien la terminaison de G(n)
  • Pour chaque G(n), on peut construire une preuve dans PA de longueur O(log*(n) log(log*(n)))
  • log* est le logarithme itéré (iterated logarithm), une fonction à croissance très lente
  • Comme la preuve nécessaire s’allonge quand n grandit, cela ne suffit pas à montrer que PA peut démontrer le théorème de Goodstein dans son ensemble

Suites de Goodstein et notations ordinales

  • Les suites de Goodstein utilisent la hereditary base notation, qui se relie à la représentation des ordinaux en forme normale de Cantor

  • Dans la construction à la John von Neumann, les ordinaux sont construits comme des ensembles

    • 0 est l’ensemble vide
    • si ord est un ordinal, alors ord ∪ {ord} en est aussi un
    • si X est un ensemble d’ordinaux, alors l’union de X est aussi un ordinal

  • La forme normale de Cantor représente un ordinal sous la forme suivante

    ((n1, ord1), (n2, ord2), ..., (nk, ordk))
    • chaque ni est un entier naturel strictement positif
    • chaque ordi est un ordinal
    • ord1 > ord2 > ... > ordk

  • Cette notation représente l’ordinal suivant

    n1·ω^ord1 + n2·ω^ord2 + ... + nk·ω^ordk

  • La comparaison se traite par ordre lexicographique selon ord1, n1, ord2, n2, et si l’une des deux écritures s’arrête plus tôt, la plus courte est la plus petite

De l’induction à l’induction transfinie

  • Le cinquième axiome de PA fournit l’induction sur les entiers naturels
    • S(0) est vrai
    • si S(n) alors S(s n) est aussi vrai
    • donc S est vrai pour tous les entiers naturels
  • À partir de là, PA peut définir < récursivement et démontrer aussi l’induction forte
    • si l’on montre que, pour tout n, le fait que S soit vrai pour tous les nombres plus petits que n implique que S(n) est vrai, alors S est vrai pour tous les entiers naturels
  • Dans ZFC, on peut démontrer l’induction transfinie, qui est l’analogue de l’induction forte pour l’ensemble des ordinaux
  • Pour les objets écrits en forme normale de Cantor, on utilise deux propriétés
    • toute suite strictement décroissante écrite en forme normale de Cantor est nécessairement finie
    • on peut appliquer l’induction transfinie aux objets en forme normale de Cantor

Portée de l’induction transfinie possible dans PA

  • PA ne peut pas démontrer l’induction transfinie pour tous les ordinaux
  • En revanche, certains intervalles d’ordinaux de hauteur finie peuvent être traités dans PA
    • PA démontre l’induction forte, donc on peut y traiter l’induction transfinie jusqu’à ω
    • par le même raisonnement, on peut aussi démontrer l’induction transfinie sur ω^ω
    • puis, de la même façon, itérer vers ω^(ω^ω), ω^(ω^(ω^ω)), etc., pour des tours de hauteur finie
  • À chaque étape, seule la hauteur de la tour change, et la preuve est générée mécaniquement
  • Si l’on écrit directement la m-ième tour, la longueur totale de la preuve est O(m^2)
  • Si l’on utilise une notation abrégée comme ω^[m], écrire m ne coûte que O(log m), donc la preuve totale tombe à O(m log m)
  • Pour chaque ordinal strictement inférieur à ε₀, il existe une preuve dans PA de l’induction transfinie correspondante, mais les réunir en une seule nécessiterait une preuve de longueur infinie
  • Si PA pouvait démontrer l’induction transfinie jusqu’à ε₀, il pourrait démontrer sa propre cohérence, ce qui entrerait en conflit avec le second théorème d’incomplétude de Gödel

Procédure de génération d’une preuve pour chaque G(n)

  • Pour un n donné, seule la hauteur de tour requise par sa hereditary base notation est nécessaire
  • Cette hauteur est O(log*(n)) et se traite dans PA comme une fonction facile à calculer
  • Un programme peut, pour une entrée n, produire ce qui suit
    • des preuves de faits généraux sur PA
    • une preuve que G(n) suit une suite décroissante à l’intérieur de ω^[m] pour un certain m
    • le calcul de ce m et une preuve de la valeur obtenue
    • une preuve de l’induction transfinie sur ω^[0]
    • une preuve que l’induction transfinie sur ω^[i] implique l’induction transfinie sur ω^[i+1]
    • pour chaque étape de i = 0 à m-2, la preuve correspondante d’induction transfinie
    • une preuve que l’induction transfinie sur ω^[m-1] implique que toute suite décroissante dans ω^[m] est finie
    • la conclusion que G(n) se termine
  • PA peut démontrer à propos de cette procédure les points suivants
    • la procédure se termine
    • elle génère une liste de phrases
    • la liste commence par les axiomes de Peano
    • chaque phrase découle logiquement des précédentes
    • par induction, chaque phrase est démontrée
    • la dernière phrase est « G(n) se termine »
  • Par conséquent, PA démontre que, pour tout entier naturel n, PA démontre bien la terminaison de G(n)

Comment PA encode le calcul

  • « Encoder » signifie fixer une convention selon laquelle un entier naturel donné représente une certaine structure
  • Les briques de base de PA sont les suivantes
    • 0
    • la fonction successeur (s n)
    • l’égalité
    • le prédécesseur (p n) pour les nombres non nuls
    • les définitions récursives justifiées par l’induction
    • des conditionnelles qui bifurquent selon 0 ou 1
  • Dans PA, on peut définir récursivement des fonctions arithmétiques de base comme
    • <
    • min, max
    • +
    • *
    • l’exponentiation
    • le reste %
    • la division entière //
  • Les propriétés fondamentales de ces fonctions peuvent être démontrées dans PA par induction

Construire des structures de données avec un seul entier naturel

  • Pour encoder deux entiers naturels dans un seul, on peut entrelacer les bits de leur écriture binaire
    • les bits en position impaire représentent head
    • les bits en position paire représentent tail
  • À partir de cette paire, on peut ensuite récupérer head et tail
  • Une fois les paires disponibles, on peut aussi représenter des listes chaînées
    • utiliser 0 comme nil
    • liste vide
    • ajout d’un élément en tête
    • lecture de la tête et de la queue
    • calcul de la longueur
    • accès à une position arbitraire
    • insertion et suppression
  • Avec des nombres, des paires et des listes, on peut également représenter dans un seul entier des piles, des files, des arbres, des documents texte ou une machine virtuelle

Lisp et l’encodage des procédures de calcul

  • Lisp est utilisé ici comme langage commode pour expliquer le parsing et l’interprétation grâce à sa structure parenthésée et à sa forme command and arguments
  • Dans PA, un entier naturel peut être interprété comme une paire (type, value)
    • nombre
    • booléen
    • paire
    • liste
    • texte, etc.
  • Certains entiers naturels peuvent ne pas être des valeurs valides d’un type donné, mais les valeurs valides représentent chacune une structure de manière unique
  • Sur cette base d’encodage, on peut construire des structures de données Lisp, une machine virtuelle Lisp et un interpréteur Lisp
  • Comme Lisp est Turing complete, cette voie permet d’encoder dans PA n’importe quelle procédure calculable ainsi que l’état de cette procédure
  • Il est aussi possible, dans PA, de représenter et de suivre l’état d’un calcul après un nombre donné d’étapes

PA encode aussi les preuves de PA

  • Une preuve en logique du premier ordre peut être vue comme une liste de phrases
    • chaque phrase correspond à une étape d’inférence
    • on peut aussi écrire des phrases incorrectes ou des inférences invalides, mais une procédure de vérification peut les rejeter
  • Dans PA, on peut définir un type comme type-proof et encoder une preuve comme une liste de phrases
  • Les procédures de vérification suivantes peuvent elles aussi être encodées dans PA
    • vérifier qu’une preuve est bien formée
    • vérifier que chaque étape de preuve est valide
    • vérifier quels axiomes sont supposés
    • vérifier que la conclusion finale est bien la phrase voulue
  • S’il existe, à partir de certains axiomes, une preuve d’une certaine phrase, alors il existe aussi un entier naturel de PA qui représente cette preuve
  • Comme PA peut exprimer le calcul qui vérifie si cet entier est réellement un code de preuve valide, les « preuves dans PA » peuvent elles-mêmes être traitées à l’intérieur de PA
  • Gödel a encodé la logique dans PA sans passer par un encodage complet du calcul, mais du point de vue d’un programmeur, comprendre cela en passant par l’encodage du calcul est une voie plus naturelle

À lire aussi

1 commentaires

 
GN⁺ 2025-06-15
Commentaires sur Hacker News

  • Un article qui développe une question Stack Overflow en billet de blog
    Il traite des limites de ce que l’on peut prouver avec les axiomes de Peano, et de la manière de commencer à bootstrapper Lisp à l’intérieur de ce cadre
    Toutes les mauvaises blagues sont dans la deuxième section, et les corrections ou questions de suivi sont les bienvenues

    • Après avoir tout lu, j’ai remarqué dans la section « Why Lisp? » que l’exemple (defun not (x) ...) contient une parenthèse non appariée
      C’était assez drôle compte tenu du passage écrit plus loin, « faire trouver à un ordinateur des parenthèses équilibrées est vraiment facile », et j’ai aussi trouvé amusante la remarque de la section « Basic Number Theory » sur le fait que « le tas de parenthèses fermantes finit par devenir invisible »
      Même si je n’ai pas fait de Lisp depuis longtemps, l’article était bon : j’ai pu le suivre à nouveau et en saisir l’idée générale
    • Je n’ai pas encore beaucoup lu au-delà de l’introduction, mais je trouve intéressante l’hypothèse selon laquelle chaque cas concret d’une suite de Goodstein se termine à 0 et peut être prouvé dans PA, alors que l’énoncé disant que toutes les suites se terminent ne peut pas être prouvé
      Le fait qu’on puisse encoder le calcul avec les seuls axiomes de Peano est aussi étrangement fascinant, comme s’il y avait une couche supplémentaire d’autoréférence
      J’ai récemment commencé à approfondir la théorie des ensembles et je suis arrivé jusqu’aux suites de Goodstein ; je serais curieux d’avoir des recommandations pour l’étape suivante, soit des manuels avancés de théorie des ensembles, soit des ouvrages qui traitent en profondeur l’arithmétique de Peano
    • Le Lisp de secteur d’amorçage se bootstrappe lui aussi : https://justine.lol/sectorlisp2/
      Plusieurs Lisp de https://t3x.org implémentent aussi les nombres et le reste à partir de cellules cons et de apply/eval
      L’évaluateur méta-circulaire de John McCarthy est le code qu’Alan Kay a appelé les « équations de Maxwell du logiciel », et dans SectorLISP il est implémenté sous une forme du genre ASSOC EVAL EVCON APPLY EVLIS PAIRLIS
      Certains Forth sont similaires, et le Zenlisp de T3X l’explique autour de la récursion mutuelle entre eval et apply : http://t3x.org/zsp/index.html
    • Il y a deux endroits où « omega » est écrit ; il faudrait sans doute écrire \omega

  • En tant que personne ayant fait à la fois des maths et de la programmation, je trouve plus intéressant que le codage du calcul lui-même le fait de pouvoir contourner l’indépendance du théorème de Goodstein par ce type d’autoréférence
    Cela semble vouloir dire que PA + « PA est ω-cohérente » peut prouver le théorème de Goodstein, et peut-être que l’induction transfinie jusqu’à ε₀ est également possible en général
    Modification : je me demande si PA + « PA est cohérente » ne suffirait pas déjà

    • En tant qu’auteur de la question SO d’origine, j’ai ajouté à la question quelques liens vers des réponses pertinentes
      En substance, « PA est cohérente » ne suffit pas ; en revanche, le principe de réflexion uniforme selon lequel « si PA prouve quelque chose, alors c’est vrai » suffit
      Je ne suis pas absolument certain que ce principe soit équivalent à l’ω-cohérence, mais c’est ainsi que je lis ce qui suit : https://en.wikipedia.org/wiki/%CE%A9-consistent_theory#Relation_to_other_consistency_principles
      Wikipedia décrit le fait que T soit ω-cohérente comme « T + RFN_T + l’ensemble de toutes les phrases vraies est cohérent », ce qui me semble équivalent à dire que « T + RFN_T est vrai »
    • J’aime cette structure récursive
      Essentiellement, on construit une méta-preuve de ce que PA prouve, et si l’on fait confiance à PA, on finit aussi par faire confiance à cette méta-preuve
      Cela dit, je ne vois pas bien en quoi PA + « PA est cohérente » serait suffisant
      Ce système semble admettre des modèles où, dans les entiers naturels standards, le théorème de Goodstein est vrai, mais où il est faux pour un certain entier non standard N ; et c’est précisément ce cas que la ω-cohérence, plus forte, semble exclure
    • Malheureusement, ce n’est pas le cas, et il semble que rien d’autre ne fonctionne non plus avec de simples formules universelles
      Autrement dit, ce n’est pas un problème spécifique à Con(PA), mais un phénomène plus général : https://math.stackexchange.com/questions/5003237/can-goodsteins-theorem-be-proven-in-mathrmpa-conpa
      À propos de la première question, je me demande comment coder l’ω-cohérence sous forme de formule de PA
    • L’article de Math Exchange dit que PA + induction transfinie sur ε₀ prouve la cohérence de PA
      Il semble donc possible que PA + « PA est cohérente » puisse prouver l’induction transfinie sur ε₀
    • Les détails dépassent désormais un peu ce que je peux affirmer avec assurance
      ChatGPT a dit que PA + « PA est cohérente » ne suffit pas, et comme il a sans doute absorbé suffisamment de manuels de logique, j’ai tendance à croire cette affirmation

  • La première fois que j’ai utilisé l’arithmétique de Peano, son expressivité m’a pas mal surpris
    Au début, cela ressemble à un système élémentaire, mais une fois qu’on comprend qu’on peut y encoder le calcul lui-même et simuler plusieurs types de calcul, des choses qui paraissaient complexes commencent à s’emboîter
    Je serais curieux d’avoir des recommandations de ressources expliquant ces techniques de codage de manière accessible aux débutants

  • Cela ressemble beaucoup à la théorie de Boyer-Moore. Cette théorie aussi construit les mathématiques à partir du niveau des axiomes de Peano.
    Boyer et Moore ont également créé un démonstrateur automatique de théorèmes adapté à cette théorie, et en ont placé une copie fonctionnant avec GNU Common Lisp sur https://github.com/John-Nagle/nqthm/tree/master.
    D’après leur explication, il est utile de voir le programme comme un assez bon étudiant en mathématiques. Si on ne lui donne que les axiomes de Peano, il est difficile d’attendre de lui qu’il prouve ou découvre le théorème de factorisation en nombres premiers ; mais si, avec les axiomes de Peano, on lui fournit une liste de théorèmes comme « prouver la commutativité de l’addition », « prouver que la multiplication est distributive par rapport à l’addition », « prouver que le résultat de la fonction GCD divise ses deux arguments », alors il s’en sort bien.
    Article : https://www.cs.utexas.edu/~boyer/acl.pdf

  • Le commentaire adressé à JoJoModding sur Math StackExchange est faux.
    L’explication selon laquelle « PA peut prouver qu’il produit une preuve, mais pourrait ne pas pouvoir prouver que cette preuve est de longueur finie » passe à côté du point essentiel.
    Si PA prouve que « PA prouve X », alors PA peut prouver X.
    Le point important n’est pas l’existence de modèles non standard, mais le fait que le modèle standard des entiers naturels soit un modèle de PA.
    Donc, si PA prouve que « PA prouve X », il existe effectivement un entier naturel standard fini correspondant à la preuve encodée de « PA prouve X », et cet entier permet de construire une preuve de X dans PA.

    • La version en langage naturel proposée est ambiguë, il est donc important de distinguer les cas.
      Ce qui a été montré n’est pas « PA prouve Provable(forall n, G(n)) », mais plutôt « PA prouve forall n, Provable(G(n)) ».
      Dans le premier cas, il s’ensuivrait effectivement que « PA prouve forall n, G(n) », mais le second est différent.
      J’aimerais voir un argument, sans faire référence aux suites de Goodstein, montrant que, pour une proposition générale P, prouver forall n, Provable(P(n)) ne permet pas de prouver Provable(forall n, P(n)).
    • L’énoncé « si PA prouve “PA prouve X”, alors PA prouve X » n’est pas vrai.
      On peut construire dans PA une fonction qui recherche toutes les preuves que PA peut produire, puis, à partir de là, construire une fonction will-return qui analyse si une fonction donnée et une entrée donnée vont retourner.
      Cela ressemble à une tentative de résoudre le problème de l’arrêt : cela ne fonctionne pas toujours, mais fonctionne dans de nombreux cas.
      Si l’on construit alors opposite-return, on peut faire en sorte qu’elle tente de retourner lorsque la fonction et l’entrée données ne retournent pas, et qu’elle ne retourne pas lorsqu’elles retournent.
      En considérant (opposite-return opposite-return opposite-return) de la même manière que dans la preuve standard du problème de l’arrêt, PA peut prouver que « si PA peut prouver que opposite-return retourne, alors en réalité elle ne retourne pas », que « si PA peut prouver qu’elle ne retourne pas, alors en réalité elle retourne », que « si PA pouvait effectivement prouver tout ce dont il prouve lui-même la prouvabilité, il devrait posséder une preuve de l’une des deux propositions précédentes », et donc que « dans ce cas PA est incohérent ».
      C’est une forme du deuxième théorème d’incomplétude de Gödel, et c’est pourquoi il faut distinguer « PA prouve » de « PA prouve qu’il prouve ».
    • Le fait que le modèle standard soit un modèle de PA ne vaut que si PA est cohérent, et PA ne peut pas prouver sa propre cohérence. Sauf incohérence, c’est impossible à cause du théorème de Gödel.
      La preuve proposée ne fonctionne donc pas à l’intérieur de PA, et cela semble être précisément le point de ce commentaire.

  • https://math.stackexchange.com/questions/4408124/what-does-the-kirby-paris-theorem-mean

  • En discutant avec quelqu’un des types de données inductifs, je lui ai montré une définition zero/succ comme le Nat de Lean ou de Rocq.
    La personne a demandé : « C’est tout ? Et les axiomes de Peano ? Existe-t-il quelque chose de plus primitif que les types de données inductifs ? », ce qui était intéressant.
    Cela m’a rappelé qu’il vaut mieux voir les axiomes de Peano comme un choix de conception parmi d’autres, plutôt que comme quelque chose d’évidemment intrinsèque.

    • Je considère que les entiers naturels sont plus primitifs que les types de données inductifs.
      En effet, tous les types de données inductifs peuvent être construits à partir des entiers naturels et de constructeurs primitifs de types, comme Π, Σ, =, Ω, etc.

  • Le pur lambda-calcul suffit aussi. Parce que le lambda-calcul encode le calcul.

  • À propos de la cohérence de PA, on peut la prouver dans PA : https://youtu.be/6pjLmmkZnIA

    • Pour quelqu’un qui n’est pas logicien, le contexte est indispensable.
      Le deuxième théorème d’incomplétude de Gödel montre que si PA peut prouver sa propre cohérence, alors PA est incohérent et peut donc prouver n’importe quoi, y compris des faussetés.
      Le travail mis en lien ne montre pas l’incohérence de PA ; il définit un nouveau sens plus faible de l’expression « prouver sa propre cohérence », puis montre que PA peut accomplir cette tâche plus faible.
      C’est un travail intéressant, mais il n’a vraiment de sens que si l’on connaît déjà bien la logique.

  • Cet article a reçu 123 points, alors que le post SO lié n’a que 11 votes positifs.

    • Sur Stack Overflow, il faut avoir une réputation de 15 points pour pouvoir voter positivement.
      Avec la réputation de supprimer facilement les posts qui y sont publiés, à laquelle s’ajoute cette limite de 15 points, il semble que beaucoup de gens ne puissent pas voter positivement.