Vérité dans le modèle standard de l'arithmétique

[Sephi]

Bonjour,

J'ai une question à propos du théorème suivant, dont la formulation vient de [M. Margenstern, "Le théorème de Matiyassévitch et résultats connexes", dans C. Berline et al. (éditeurs), Model Theory and Arithmetic, Lecture Notes in Mathematics 890] :

Théorème. Soit A un système d'axiomes dans un langage contenant les symboles {0, S,+,·,<} tel que :
(a) A est cohérente,
(b) A est récursivement énumérable,
(c) A est capable de démontrer tout énoncé vrai de la forme :

p + q = r
p · q = r
p < q

où p, q, r sont des nombres naturels.
Alors on peut explicitement construire un polynôme à coefficients entiers n'ayant aucune racine dans les naturels, et tel que cette absence de racine n'est pas démontrable dans A.

Tout d'abord, le mot "vrai" qui apparaît là-dedans est probablement à prendre comme "vrai dans le modèle standard lN de l'arithmétique".

On aura compris que ce théorème fournit constructivement un énoncé indécidable dans la théorie A mais vrai dans lN. (En fait, ce théorème est un corollaire du théorème de Davis-Putnam-Robinson-Matiyassévitch (DPRM)).

J'ai deux questions :

(1) Comment peut-on (en principe) vérifier que cet énoncé est vrai dans lN, si ce n'est par une démonstration dans une autre théorie que je vais noter T ? T serait quelle théorie (ZF ou quoi) ?

(2) Prenons A = T dans le théorème. Celui-ci nous fournit alors un énoncé vrai dans lN mais indémontrable dans T. Mais du coup, comment vérifier que c'est vrai dans lN, sachant que cette fois on ne peut pas le démontrer dans T ?
-----

[Sephi]

Autrement dit, si "vrai dans lN" signifie "être démontrable dans une certaine théorie T", alors on a une contradiction car le théorème (appliqué à la théorie T) nous donnerait toujours un énoncé vrai dans lN, mais indécidable dans T !

[Médiat]

Bonjour (ravi de vous retrouver),

Est-ce que vous auriez un lien sur ce texte ?

Tout d'abord, le mot "vrai" qui apparaît là-dedans est probablement à prendre comme "vrai dans le modèle standard lN de l'arithmétique".

Il est bien précisé "p, q, r sont des nombres naturels", donc si ces propositions sont "vraies" dans le modèle standard, alors elles sont vraies dans tous les modèles de Peano, mais ce qui compte c'est qu'elles soient démontrables dans A. Il y a une vraie subtilité ici (différence entre "pour tout n démontrer p(n)" et '"démontrer, pour tout n, p(n)").

(1) Comment peut-on (en principe) vérifier que cet énoncé est vrai dans lN, si ce n'est par une démonstration dans une autre théorie que je vais noter T ? T serait quelle théorie (ZF ou quoi) ?

Attention IN est un modèle, par exemple, on peut démontrer que dans IN il n'existe pas d'élément n qui soit strictement plus grand que tous les entiers, par contre il en existe dans des modèles non-standard de Peano (c'est un bon moyen de montrer, par compacité, qu'il existe des modèles non-standard).

(2) Prenons A = T dans le théorème. Celui-ci nous fournit alors un énoncé vrai dans lN mais indémontrable dans T. Mais du coup, comment vérifier que c'est vrai dans lN, sachant que cette fois on ne peut pas le démontrer dans T ?

Ma réponse précédente devrait convenir, j'ajoute que dans un cas (IN) on manipule des entiers, dans l'autre (A ou T), on manipule des éléments d'une théorie arithmétique.

[Sephi]

J'ai joint à ce message une numérisation de l'article. L'énoncé du théorème se trouve à la page 231.

Ma question est : que signifie exactement le mot "vrai" utilisé dans cet énoncé ?



Par ailleurs, je n'ai pas vu de réponse à ma question (1) de mon premier message :

Considérons le modèle lN. Comment vérifie-t-on qu'un énoncé d'une théorie quelconque est vrai dans lN ? Est-ce en montrant qu'il est démontrable dans une certaine théorie T admettant lN comme modèle ?

[A voir en vidéo sur Futura]

[Médiat]

J'ai joint à ce message une numérisation de l'article. L'énoncé du théorème se trouve à la page 231.

J'attends la validation.

Ma question est : que signifie exactement le mot "vrai" utilisé dans cet énoncé ?

"Vrai" dans IN (le minimum demandé à une théorie de l'arithmétique).

Par ailleurs, je n'ai pas vu de réponse à ma question (1) de mon premier message

Il me semblait avoir répondu, et même donné un exemple.

[Sephi]

Il me semblait avoir répondu, et même donné un exemple.

Euh je n'ai pas compris en quoi ça répondait à la question, que j'ai reformulée dans mon précédent message...

[Médiat]

Euh je n'ai pas compris en quoi ça répondait à la question, que j'ai reformulée dans mon précédent message...

La démonstration se fait dans le modèle lui-même, c'est à dire dans l'ensemble des propositions "vraies" dans ce modèle (ensemble de propositions qui n'est pas récursivement énumérable d'après le 1er théorème d'incomplétude de Gödel).
Je ne connais pas la forme de ce polynome, donc je ne peux rien en dire, mais l'exemple sur l'existence d'un élément plus grand que tous les entiers me semble correspondre très exactement à votre problématique.

[Sephi]

Par exemple, je me donne l'énoncé 4+5=9. Nous savons qu'il est vrai dans lN de sorte qu'on peut exiger que cet énoncé soit démontrable par la théorie A que l'on se donne dans le théorème.

Mais au fond, comment savons-nous que cet énoncé est vrai dans lN ? J'ai envie de dire : parce qu'il est démontré dans une théorie autre que A, par exemple dans Peano qui satisfait aussi aux hypothèses du théorème.

Du coup, on peut prendre la plus grande théorie connue T qui satisfait aux hypothèses du théorème, et lui appliquer ce dernier. Il en ressortira un énoncé de la forme "le polynôme P n'a pas de racine" qui, selon le théorème est vrai dans lN mais est indécidable dans T. Mais comment sait-on que cet énoncé est vrai dans lN puisqu'il n'est démontrable dans aucune théorie actuellement connue (car T est la plus grande théorie connue) ?

Désolé si je ne comprends pas les réponses précédentes, mais je fais de mon mieux.

Je ne connais pas la forme de ce polynome

C'est simplement un polynôme à coefficients entiers. Dans le théorème, les hypothèses sur la théorie A sont suffisantes pour que A soit capable de démontrer qu'un polynôme a une racine quand ce fait est vrai dans lN.

[Médiat]

Par exemple, je me donne l'énoncé 4+5=9. Nous savons qu'il est vrai dans lN de sorte qu'on peut exiger que cet énoncé soit démontrable par la théorie A que l'on se donne dans le théorème.

Mais au fond, comment savons-nous que cet énoncé est vrai dans lN ? J'ai envie de dire : parce qu'il est démontré dans une théorie autre que A, par exemple dans Peano.

Il est "vrai" dans IN car la définition du symbole 4 dans IN, la définition du symbole 5 dans IN, la définition du symbole 9 dans IN et la définition du symbole + dans IN, font que 4+5=9, ce qui vous force à remonter à la définition de IN que vous vous donnez (à aucun moment je n'ai fait appel à Peano, mais on pourrait, puisque tout ce qui est démontrable dans Peano est vrai dans IN (l'un des définition de IN est d'être le modèle premier de PA), et que ce théorème est démontrable dans PA).

Le coup de l'élément plus grand que tous les entiers n'est pas démontrable dans PA, par contre dans IN, on peut dire quelque chose.

[Sephi]

Il est "vrai" dans IN car la définition du symbole 4 dans IN, la définition du symbole 5 dans IN, la définition du symbole 9 dans IN et la définition du symbole + dans IN, font que 4+5=9, ce qui vous force à remonter à la définition de IN que vous vous donnez (à aucun moment je n'ai fait appel à Peano

C'est peut-être ici que je ne comprends pas. Car pour moi, la définition de "4", "5", "9" et "+" se fait en fait dans un système formel M (défini par les axiomes de Peano sans le schéma de récurrence, avec les axiomes de l'addition). J'ai donc l'impression que si je peux dire "4+5=9 est vrai dans lN", c'est parce que j'ai pu dire "4+5=9 est démontré dans M".

En fait, si je laisse de côté ma compréhension "intuitive" de lN (qui ne permet pas de faire des démonstrations rigoureuses), je ne l'appréhende qu'à travers un système formel. C'est pour ça que je me demande comment savoir qu'un énoncé est vrai dans lN sans mentionner une démonstration dans une théorie.

Le document a été validé ?

[Médiat]

J'ai donc l'impression que si je peux dire "4+5=9 est vrai dans lN", c'est parce que j'ai pu dire "4+5=9 est démontré dans M".

Ou parce que dans votre modèle M (ou N ou Robert), il y a un élément baptisé 4, un autre baptisé 5, un autre baptisé 9, et que le sous-ensemble de M³ qui est la fonction +, contient le triplet (4, 5, 9).

[Sephi]

En attendant, voici un lien vers l'article que j'ai mis sur un espace web :

http://oasis-lln.be/wp-content/uploads/Margenstern.pdf

[Sephi]

Ou parce que dans votre modèle M (ou N ou Robert), il y a un élément baptisé 4, un autre baptisé 5, un autre baptisé 9, et que le sous-ensemble de M³ qui est la fonction +, contient le triplet (4, 5, 9).

Ok, je crois mieux voir. Es-tu d'accord pour dire que, suite à cet extrait, on a montré que "4+5=9" est vrai dans M sans l'avoir démontré dans une théorie quelconque ?

[Médiat]

Ok, je crois mieux voir. Es-tu d'accord pour dire que, suite à cet extrait, on a montré que "4+5=9" est vrai dans M sans l'avoir démontré dans une théorie quelconque ?

C'est "démontré" dans la théorie de IN (ensemble des propositions vraies dans IN) ; je reconnais que "démontré" dans ce cas est un bien grand mot.

[Sephi]

C'est "démontré" dans la théorie de IN (ensemble des propositions vraies dans IN) ; je reconnais que "démontré" dans ce cas est un bien grand mot.

Mais s'agit-il bien d'une démonstration dans un système formel (la "théorie de lN"), même si elle est triviale ?

Remarquons que dans l'article, les naturels sont définis comme étant de la forme "S..S(0)" dans un certain système formel avec ces symboles (ce qui est ma façon de définir lN). L'article est-il ambigu ?

[Médiat]

Mais s'agit-il bien d'une démonstration dans un système formel (la "théorie de lN"), même si elle est triviale ?

Je n'ai pas encore lu l'article, mais dans un premier temps je peux dire que jusqu'à présent j'ai parlé de la théorie du modèle, et dans ce cas, elle est loin d'être triviale, puisque elle n'est même pas récursivement énumérable.

Par contre je viens de me faire une remarque < est parfaitement définissable à partir de +, et donc l'intérêt de rajouter ce point dans le langage et la définition pourrait paraître inutile, sauf qu'en ajoutant ce symbole, le diagramme simple du modèle (propositions sans quantificateur) peut inclure <, ce qui ne serait pas le cas sinon.

Autrement dit, vous pouvez ne considérez que les formules atomiques (dans ce langage) et les composés des formules atomiques par un nombre fini d'opérations booléennes (et, ou, non), ce qui donne bien ici, un truc trivial, et largement suffisant pour ce que l'on veut en faire.

Remarquons que dans l'article, les naturels sont définis comme étant de la forme "S..S(0)" dans un certain système formel avec ces symboles (ce qui est ma façon de définir lN). L'article est-il ambigu ?

Pas sur ce point, nous sommes tous d'accord que s(s(0)) = s²(0) = 2 (attention le statut de ces trois écritures est à chaque fois différent).

Ouh-là 44 pages, je ne vous promets de tout lire rapidement.

[Médiat]

Je viens de jeter un rapide coup d'oeil sur la page 31, je ne connais pas toutes les notations utilisées, mais il me semble que la démonstration repose sur le fait qu'il existe une équation diophantienne dont on ne peut pas démontrer dans A qu'elle n'a pas de solution, donc il existe des modèles où elle en a et des modèles où elle n'en a pas.
Or si IN était un modèle où elle a des solutions, tous les modèles de A en auraient (par construction de A, tous ses modèles vérifient toutes les formules atomiques de IN et donc le diagramme simple de IN) , ce qui serait alors démontrable, donc IN ne vérifie pas cette équation.

C'est un résultat un peu similaire à "Si la conjecture de Golbach est indécidable dans PA, alors elle est fausse "vraie" dans IN".

[Sephi]

Si tu veux un "résumé" en 4 pages du thème abordé, voici un texte en cours de rédaction. Je dois encore travailler la formulation de certaines phrases (exercice particulièrement difficile dans ce genre de sujet, surtout quand on veut s'adresser aux matheux non-logiciens dont je fais partie). Je compte déjà bien préciser qu'il s'agit toujours de "vérité dans le modèle standard".

http://oasis-lln.be/wp-content/uploads/dprm.pdf

Je serais heureux si tu pouvais me donner ton avis. Le théorème dont il est question dans ce sujet est énoncé à la 4e page.

[Sephi]

Or si IN était un modèle où elle a des solutions, tous les modèles de A en auraient (par construction de A, tous ses modèles vérifient toutes les formules atomiques de IN et donc le diagramme simple de IN) , ce qui serait alors démontrable, donc IN ne vérifie pas cette équation.

En tout cas, ce n'est pas l'argument utilisé dans la preuve présentée dans les textes ci-dessus.

[Médiat]

http://oasis-lln.be/wp-content/uploads/dprm.pdf

Je regarderai demain si je peux, mais en tout état de cause, la première phrase :

Le but de ce texte est de décrire, de façon informelle, la construction d'un énoncé vrai et indémontrable dans l'arithmétique

Est pour moi (je sais que certains logiciens n'y voit pas d'inconvénient) une horreur, puisqu'un même énoncé est qualifié d'un point de vue sémantique ("vrai") de façon très très insatisfaisante (on sait que c'est dans un modèle, mais on ne sait pas lequel), et qualifié d'un point de vue syntaxique (indémontrable) de façon incorrecte puisque la théorie n'est pas précisé (de quel arithmétique s'agit-il ? J'en connais de complètes, donc ne contenant aucune proposition indécidable).

Je sais que certains me trouve maniaque, et que beaucoup ne verront peut-être pas l'intérêt de mes critiques, je me trouve rigoureux,et ne conçois les mathématiques que sous cet éclairage même si ma façon de dire les choses est moins médiatique).

Du coup, je ne sais pas si je suis le mieux placé pour relire votre document.

[Sephi]

d'un point de vue sémantique ("vrai") de façon très très insatisfaisante (on sait que c'est dans un modèle, mais on ne sait pas lequel)

J'ai dit ci-dessus que je comptais mentionner qu'il s'agit du modèle standard de l'arithmétique.

la théorie n'est pas précisé (de quel arithmétique s'agit-il ?

L'arithmétique usuelle, celle des opérations + et x sur les nombres naturels. Si cela ne désigne pas une théorie précise, ce n'est pas grave puisqu'en fait, le résultat est vrai pour toute théorie qui formalise au moins l'arithmétique usuelle avec ses 2 opérations. Mais je suppose que cela ne fera pas de mal de le préciser, merci.

[Sephi]

Que faut-il répondre à la question suivante ?

Soit A une théorie formalisant l'arithmétique, lN le modèle standard et P le polynôme sans racine dans lN tel que ce fait est indémontrable dans A. Quel mode de connaissance avons-nous utilisé pour savoir que l'énoncé "P n'a pas de racine" est vrai dans lN ?

Sachant que la démonstration dans une certaine théorie est un mode de connaissance possible.

[Médiat]

Mais je suppose que cela ne fera pas de mal de le préciser

Je suppose que vous pensez à l'arithmétique de Robinson (ou système Q), mais faites attention, il y a aussi l'arithmétique de Goodstein, certes très exotique, mais complète !

[Médiat]

Je viens de lire votre document de 4 pages, comme je vous l'ai dit le vocabulaire est pour moi une pure abomination, mais à part cela, la construction du document est solide.

Je regrette juste des raccourcis, comme la décidabilité de la théorie A, et il faudrait rappeler dans la démonstration du théorème 8 que U est la représentation universelle des ensembles diophantiens.

Le résumé et le théorème 8 annoncent un polynome explicitement constructible, donc on s'attend à le "voir" ce polynome, mais on ne le voit pas, il est basé sur U, qui n'est pas construit explicitement non plus.

Je sais que "constructible" et "effectivement construit" ne sont pas synonyme, mais l'expression "effectivement constructible" rend l'absence effective de l'expression de ce polynome frustrante.

[Sephi]

Le résumé et le théorème 8 annoncent un polynome explicitement constructible, donc on s'attend à le "voir" ce polynome, mais on ne le voit pas, il est basé sur U, qui n'est pas construit explicitement non plus.

Merci pour le temps que tu as mis, il est vrai qu'il faudrait modérer les ardeurs dans le texte, étant donné que U est déterminé seulement à travers le théorème DPRM qui associe à l'ensemble diophantien universel sa représentation diophantienne.

Par contre, le polynôme sans racine dont on annonce qu'il est constructible, il dépend de U mais aussi de la théorie A qui est quelconque. C'est donc normal de ne pas pouvoir l'écrire explicitement !

Un truc intéressant serait de prendre A = Peano par exemple, et de voir à quoi ressemble ce polynôme.



Sinon, une idée des réponses possibles aux questions des précédents messages ?

[Médiat]

Un truc intéressant serait de prendre A = Peano par exemple, et de voir à quoi ressemble ce polynôme.

A priori, je vous conseillerais plutôt l'arithmétique de Robinson, qui est finiment axiomatisable. Mais je ne suis pas certain que vous puissiez effectivement construire le polynome, mais j'aimerais bien ...

Sinon, une idée des réponses possibles aux questions des précédents messages ?

Si vous faites allusion à

Quel mode de connaissance avons-nous utilisé pour savoir que l'énoncé "P n'a pas de racine" est vrai dans lN ?

Je vous ai donné 2 exemples, et votre document de 4 pages en donne un 3ième, je ne vois vraiment pas ce que vous cherchez de plus.

[Sephi]

A priori, je vous conseillerais plutôt l'arithmétique de Robinson, qui est finiment axiomatisable. Mais je ne suis pas certain que vous puissiez effectivement construire le polynome, mais j'aimerais bien ...

Pour commencer, une représentation diophantienne explicite de tous les ensembles récursivement énumérables se trouve par exemple dans :

James P. Jones, Three Universal Representations of Recursively Enumerable Sets, The Journal of Symbolic Logic, Vol. 43, No. 2 (Jun., 1978), pp. 335-351.

C'est un polynôme à 67 variables de degré 76. La contemplation de ce polynôme n'est pas très passionnante, j'avoue Mais peut-être que l'intérêt est de le voir de ses propres yeux.

Quant à la construction du polynôme sans racines dans lN, je ferai bien quelques recherches pour voir s'il n'y a pas un article là-dessus...

je ne vois vraiment pas ce que vous cherchez de plus.

Je souhaite simplement savoir si l'énoncé "le polynôme P n'a pas de racines dans lN" a été démontré. Si oui, dans quelle théorie ? Je suis perplexe car même si le texte montre bien tout ce qu'il faut, je ne pense pas encore l'avoir compris en profondeur malgré l'avoir rédigé.

Tu as glissé auparavant qu'il a été démontré dans la "théorie de lN" à savoir le (brutal) ensemble de toutes les propositions vraies dans lN. Être démontré là-dedans, c'est exactement faire partie de cet ensemble, c'est donc par définition être vrai dans lN. Dans le meilleur des cas, c'est une démonstration en une ligne, dans le pire c'est un serpent qui se mord la queue :
- Pourquoi c'est vrai dans lN ?
- Parce que ça fait partie des propositions vraies dans lN...

[Médiat]

Pour commencer, une représentation diophantienne explicite de tous les ensembles récursivement énumérables se trouve par exemple dans :

James P. Jones, Three Universal Representations of Recursively Enumerable Sets, The Journal of Symbolic Logic, Vol. 43, No. 2 (Jun., 1978), pp. 335-351.

C'est un polynôme à 67 variables de degré 76. La contemplation de ce polynôme n'est pas très passionnante, j'avoue Mais peut-être que l'intérêt est de le voir de ses propres yeux.

L'intérêt, c'est surtout de voir comment on le construit explicitement.

Je souhaite simplement savoir si l'énoncé "le polynôme P n'a pas de racines dans lN" a été démontré. Si oui, dans quelle théorie ? Je suis perplexe car même si le texte montre bien tout ce qu'il faut, je ne pense pas encore l'avoir compris en profondeur malgré l'avoir rédigé.

Son existence est démontrée par l'existence de U qui elle-même est démontrée par le théorème 4 (DPRM).

Dans le meilleur des cas, c'est une démonstration en une ligne, dans le pire c'est un serpent qui se mord la queue :
- Pourquoi c'est vrai dans lN ?
- Parce que ça fait partie des propositions vraies dans lN...

D'où mon message #14.

[Médiat]

Je précise le point précédent :
La théorie de IN n'est pas récursivement énumérable, donc même si le fait qu'il existe un polynome avec tel ou tel propriété, existe bien dans cette théorie (est un théorème de cette théorie), ce n'est pas pour autant qu'on peut y accéder facilement, c'est justement toute l'artillerie des ensembles listables qui donne des outils pour accéder à ces théorèmes, et qui permet de démontrer le DPRM.

[Sephi]

Peut-on dire alors que le théorème (affirmant l'existence d'un polynôme sans racine) fournit un algorithme pour lister une classe d'éléments de l'ensemble des propositions vraies dans lN ? Ces éléments étant systématiquement de la forme "le polynôme P_A n'a pas de racines dans lN" où A est une théorie satisfaisant aux hypothèses du théorème.

Cet algorithme est-il une démonstration rigoureuse dans un système formel ?



Enfin, puis-je tirer de ton message #14 qu'on ne peut pas enlever les guillemets autour de "démonstration", donc qu'il ne s'agit pas d'une vraie démonstration ? Y a-t-il seulement un sens à travailler dans la théorie de lN, où démontrer se réduit à exhiber par des techniques très particulières des axiomes de la théorie de lN ?