Arithmétique de Presburger ?

umrk · May 2022

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 ?

gerard0 · May 2022

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.

umrk · May 2022

Oui, j’ai vu ça, mais ça n’empêche pas Coq d’être performant, visiblement

Rescassol · May 2022

Bonjour,

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

Cordialement,
Rescassol

OK, je sors.

@l · May 2022

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

gerard0 · May 2022

Alors la bonne question n'est-elle pas : Coq se contente-t-il de l'addition ?

Médiat_Suprème · May 2022

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,

Foys · May 2022

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.

umrk · May 2022

Merci à tous !

Médiat_Suprème · May 2022

Pour ceux qui voudraient en savoir un peu plus, sans fouiller le net :

umrk · May 2022

Merci !

Médiat_Suprème · May 2022

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.

Foys · May 2022

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.

Arithmétique de Presburger ?

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 47