Arithmétique de Presburger ? — Les-mathematiques.net The most powerful custom community solution in the world

Arithmétique de Presburger ?

umrkumrk
dans Fondements et Logique
En me renseignant sur Thierry Coquand, et donc sur Coq, j’apprends que ce développement repose sur l’arithmétique de Presburger, dont je n’avais jamais entendu parler, et que celle-ci présente des propriétés sympathiques, à savoir qu’elle est complète et décidable. Mais alors pourquoi se torturer avec celle de Peano, qui ne l’est pas ?

Réponses

  • gerard0gerard0
    Modifié (16 May)
    En 10 secondes sur un moteur de recherche  : "arithmétique de Presburger".
    Et on voit dès la deuxième ligne pourquoi on ne s'en contente pas.
    Cordialement.
  • umrkumrk
    Oui, j’ai vu ça, mais ça n’empêche pas Coq d’être performant, visiblement
  • RescassolRescassol
    Bonjour,

    Je connais et ai pratiqué le presse-purée, mais là, c'est nouveau ...........  :)

    Cordialement,
    Rescassol

    OK, je sors.
  • @l@l
    Modifié (16 May)
    Bonjour,
    en écho à cette question, les arithmétiques dites faibles constituent un domaine de recherche en soi. Cf par exemple les JAF qui font le point régulièrement sur ces questions: http://lacl.univ-paris12.fr/jaf/
    Cf aussi les travaux de Jean-Pierre Ressayre sur ces questions.
    Par ailleurs, il y a énormément de connexion avec la théorie des corps réels clos: https://www.researchgate.net/publication/220315510_Real_closed_fields_and_models_of_Peano_arithmetic
    @l
  • gerard0gerard0
    Alors la bonne question n'est-elle pas : Coq se contente-t-il de l'addition ?
  • Médiat_SuprèmeMédiat_Suprème
    Je rajoute un point personnel : avant d'étudier l'arithmétique de Presburger, j'avais l'impression, l'intuition (cette mauvaise fille) que le schéma de récurrence était le responsable, si AP est essentiellement incomplète, on voit qu'il n'en est rien, le dernier clou du cercueil de cette idée est que l'arithmétique de Robinson est aussi essentiellement incomplète, 
    504, c'est trop !
  • FoysFoys
    Modifié (16 May)
    gerard0 a dit :
    Alors la bonne question n'est-elle pas : Coq se contente-t-il de l'addition ?
    Non. De plus coq prête le flanc aux théorèmes de Gödel et est donc indécidable ou contradictoire.
  • umrkumrk
    Merci à tous !
  • Médiat_SuprèmeMédiat_Suprème
    Modifié (16 May)
    Pour ceux qui voudraient en savoir un peu plus, sans fouiller le net : 
    504, c'est trop !
  • umrkumrk
    Merci !
  • Médiat_SuprèmeMédiat_Suprème
    Modifié (21 May)
    J'ai eu quelques échanges privés avec un lecteur de mon document sur l'arithmétique (cf supra), la question étant : comment $\mathbb{N} \, \biguplus \mathbb{Z}$  (union disjointe) peut vérifier l'axiome de récurrence (dans le cadre de la théorie PréA', (soit Peano sans addition ni multiplication).
    La gène venant de ce qu'intuitivement (dangereux en mathématique et plus encore en logique) la chaîne de récurrence est  "cassée" puisque l'on ne passe pas d'un élément de la partie $\mathbb N$ à un élément de la partie $\mathbb Z$ par l'application successeur.
    On peut même imaginer une formule $\varphi(x)$ vraie pour tous les éléments dans la partie $\mathbb N$ et fausse pour tous les éléments de la partie $\mathbb Z$ :
    $\varphi(0)$ est vraie par hypothèse
    Si $n$ est dans la partie $\mathbb N$ il en est de même de $s(n)$, donc $\varphi(n)$ et $\varphi(s(n))$ sont vraies et donc on a bien $\varphi(n) \Rightarrow \varphi(s(n))$.
    Si $n$ est dans la partie $\mathbb Z$ il en est de même de $s(n)$, donc $\varphi(n)$ et $\varphi(s(n))$ sont fausses et donc on a bien $\varphi(n) \Rightarrow \varphi(s(n))$. 
    L'axiome de récurrence permet de conclure : $\forall n \in \mathbb{N} \, \biguplus \mathbb{Z}\; (\varphi(n))$ ce qui est contradictoire avec sa définition.
    Mais on n'a pas démontré que cette structure ne vérifiait pas l'axiome de récurrence, mais juste que la formule $\varphi(x)$ n'existe pas.
    504, c'est trop !
  • FoysFoys
    Au sujet du texte en pdf ci-dessus, examinons ce petit texte

    Le Coran ne prouve pas la phrase obtenue en appliquant la procédure suivante:
    on écrit le texte entre guillemets ci-après une fois, puis on met un deux-points, puis on réécrit le même texte une deuxième fois en le mettant entre guillemets, et enfin on met un point final: "Le Coran ne prouve pas la phrase obtenue en appliquant la procédure suivante:
    on écrit le texte entre guillemets ci-après une fois, puis on met un deux-points, puis on réécrit le même texte une deuxième fois en le mettant entre guillemets, et enfin on met un point final".

    Le Coran ne peut prouver la phrase en italique ci-dessus que si elle est fausse.
    Même si l'effort de ne pas faire dire au théorème de Gödel ce qu'il n'a jamais dit est louable (et combien d'abus ont été commis dans ce sens), les parties réutilisables dudit théorème devraient (à mon avis) être beaucoup plus vulgarisées (c'est-à-dire les combinateurs de points fixes grosso modo). Peut-être que les élites ont peur que des gens fassent des bêtises avec leur ordinateur en sachant ça et préfèrent dissimuler ce savoir-faire mais de toute façon des hackers malveillants le possèdent déjà et il est trouvable sur le web lui aussi.
    Un livre qui démontre toutes les phrases vraies démontre aussi au moins une phrase fausse pour la seule raison que la langue courante permet de décrire les opérations de base d'un traitement de texte.

Connectez-vous ou Inscrivez-vous pour répondre.
Success message!