indécidabilité de la décidabilité

[invite6754323456711]

Ok merci je comprend mieux ta question.

Fait nous en profiter car pour moi il n'y a pas de meta-langage. La seconde question revient en fait à la même question que la première. Hilbert pensait aussi parler de méta-mathématique :

Sur la question plus générale de la validité de la distinction mathématique / métamathématique, Wittgenstein avait fait remarquer : « Les «métamathématiques» de Hilbert se révéleront être des mathématiques sous un déguisement » [Ludwig Wittgenstein and the Vienna Circle : 136]. Car « Ce que fait Hilbert ce sont des mathématiques et non des méta-mathématiques. C'est un type de calcul différent, comme n'importe quel autre » [ibid. 121]. « Les preuves métamathématiques de Hilbert ne sont pas un type de calcul d'une essence plus élevée, mais plus simplement un type de calcul différent : « Je peux jouer avec les pièces du jeu d'échecs selon certaines règles. Mais je peux aussi bien inventer un jeu où je joue avec les règles elles-mêmes. Les pièces de mon jeu sont cette fois les règles du jeu d'échecs, et les règles du jeu sont, disons, les lois de la logique. Dans ce cas, j'ai affaire à un jeu supplémentaire, non pas à un métajeu » »

Patrick
-----

[invite6c250b59]

pour la première, oui, c'est trivial puisque tous les axiomes d'une théorie sont démontrés ipso-facto, si on rajoute l'énoncé dans la théorie, il devient un axiome et donc avec une démonstration de longueur 1.

Certes, mais c'est la transitivité de la consistance que je trouve non trivial à priori.

Fait nous en profiter

Soit une formule F indécidable dans un système d'axiome A. ilelogique veut savoir si la proposition (F indécidable dans A) peut être décidable dans A.

Pour la seconde pas d'accord, je ne vois pas pourquoi la décidabilité ne serait pas décidable si l'énoncé n'est pas décidable.

Ayé je pense:
-Prenons peano et définissions cons(peano) comme la formule codant "peano est consistent". cons(peano) est indécidable dans peano par le second théorème d'incomplétude. Rien de nouveau sous le soleil.
-Construisons peano+cons(peano) et définissons cons(peano+cons(peano)) comme la formule codant "(peano ajouté de l'affirmation de sa consistance) est consistent". cons(peano+cons(peano)) est indécidable dans peano+cons(peano) par le second théorème. Même truc sauf que:
-si cons(peano+cons(peano)) est indécidable dans peano+cons(peano), alors il est aussi indécidable dans peano tout court.

[invite6754323456711]

ilelogique veut savoir si la proposition (F indécidable dans A) peut être décidable dans A.

Je ne vois toujours pas la différence avec la démarche de Gödel dans la démonstration des théorèmes d’incomplétudes : AP |- (G <--> Non Theor(G)) http://www.di.ens.fr/users/longo/Pap...completude.pdf

Patrick

[Amanuensis]

je pense que personne ici n'a la réponse pour le moment,

On vous la donne, mais personne ne l'a???

attendons Médiat

Parce que la même réponse venant d'une autre source peut être plus valable?

---

La seule interprétation est que vous n'arrivez pas à voir la réponse valide comme valide. Mais alors pourquoi poser la question sur un forum, puisque cela vous amène à la discourtoisie consistant à dire "la réponse ne me va pas parce que vous n'êtes pas une source que j'accepte", et encore pire "personne ici n'a la réponse"? Pourquoi n'allez-vous pas directement demander à une "autorité" dont vous accepterez telle quelle la réponse?

[Médiat]

Bonjour,
Pour pouvoir parler de l'indécidabilité tel que vous le faite, il faudrait en parler dans le cadre d'une théorie capable de formaliser cette indécidabilité ; et cela ne montrerait qu'une seule chose : que la théorie ne peut pas démontrer cette indécidabilité (mais il y a d'autres méthodes).
L'exemple de Syracuse me paraît non pertinent, car ce n'est pas une conjecture qui porte sur AP, mais sur , dont la théorie n'est pas récursive ce qui rend la formalisation impossible.
Dans AP Syracuse est manifestement fausse.

[karlp]

HS C'est un immense plaisir que celui de vous revoir très cher Médiat !!fin du HS

[Amanuensis]

Je ne vois toujours pas la différence avec la démarche de Gödel dans la démonstration des théorèmes d’incomplétudes : AP |- (G <--> Non Theor(G)) http://www.di.ens.fr/users/longo/Pap...completude.pdf

Je le trouve très bien, ce texte; merci Patrick de le faire découvrir (et à son auteur de l'avoir écrit...). Il me semble qu'on y trouve pas mal de réponses...

[Médiat]

Bonjour Patrick

Je note avec joie que je ne suis pas le seul à trouver la phrase "énoncés vrais mais indémontrables", pas acceptable.

[Médiat]

Dans AP Syracuse est manifestement fausse.

Je corrige : dans AP Syracuse n'est manifestement pas démontrable.

[ilelogique]

Bonjour à tous,
oui le texte a l'air intéressant je vais le lire, merci.
Je ne cherche pas spécialement une autorité pour me répondre (j'ai d'ailleurs envoyé la question à un ancien prof), c'est juste que je ne comprends pas trop vos réponses.
je suis d'accord sur la première trivialité, ce n'en est pas une, il faut en effet s'assurer de la consistance.
je vais tacher de dire encore comment je vois la question :
Prenons un énoncé F écrit dans une théorie axiomatique T cohérente, dans un langage L avec un ensemble de règles de déduction R.
Puisqu'il semble que Godel dans sa preuve a pu formaliser dans la théorie de l'arithmétique la décidabilité d'un énoncé (celui de la complétude de l'arithmétique non ?), je rajoute donc dans mes hypothèses que la formule dec(F), qui affirme la décidabilité de F dans T, soit exprimable dans L.
Ma question est celle de la décidabilité de dec(F) ???
Si j'entends bien que la décidabilité de la décidabilité d'une formule n'est pas forcément exprimable dans la théorie dans laquelle cette formule est énoncée, je demande si on peut au moins imaginer qu'une telle théorie et une telle formule puisse exister ?
Voire que dans une telle théorie on puisse énoncer dec(dec(dec...F)...)) ???

Pour ce qui est de la conjecture de Syracuse, il me semble qu'on ne sait pas encore si elle est démontrable ou non dans l'arithmétique, et que certains pensent qu'elle est indécidable (comme celle de goodstein), la question est : prouverons-nous son indécidabilité et surtout peut-on prouver que c'est faisable ??

On a montré par exemple que la conjecture de goodstein est indécidable dans l'arithmétique mais on l'a prouvée avec les entiers non standards. La preuve de cette indécidabilité aurait-elle pu se faire au sein de l'arithmétique ?

[Médiat]

Pour ce qui est de la conjecture de Syracuse, il me semble qu'on ne sait pas encore si elle est démontrable ou non dans l'arithmétique, et que certains pensent qu'elle est indécidable (comme celle de goodstein),

On a montré par exemple que la conjecture de goodstein est indécidable dans l'arithmétique mais on l'a prouvée avec les entiers non standards. La preuve de cette indécidabilité aurait-elle pu se faire au sein de l'arithmétique ?

Syracuse n'est pas démontrable dans AP (il existe des contre exemples), elle est soit fausse soit indécidable.
L'indécidabilité de Goodstein est bien démontrée au sein de AP, je ne vois pas le problème

[ilelogique]

Oui pas de problème, je suis d'accord.
mais ma question reste :
Prenons un énoncé F écrit dans une théorie axiomatique T cohérente, dans un langage L avec un ensemble de règles de déduction R.
Puisqu'il semble que Godel dans sa preuve a pu formaliser dans la théorie de l'arithmétique la décidabilité d'un énoncé (celui de la complétude de l'arithmétique non ?), je rajoute donc dans mes hypothèses que la formule dec(F), qui affirme la décidabilité de F dans T, soit exprimable dans L.
Ma question est celle de la décidabilité de dec(F) ???
Si j'entends bien que la décidabilité de la décidabilité d'une formule n'est pas forcément exprimable dans la théorie dans laquelle cette formule est énoncée, je demande si on peut au moins imaginer qu'une telle théorie et une telle formule puisse exister ?
Voire que dans une telle théorie on puisse énoncer dec(dec(dec...F)...)) ???

[Médiat]

AP doit convenir, et je ne vois rien de choquant à ce qu'une théorie ne puisse démontrer lesquels de ses énoncés sont indécidables.
Il faudrait comme je vous l'ai suggéré dans mon premier message que vous formalisiez "f est indécidable", puis que vous trouviez un raisonnement montrant que ces énoncés sont toujours démontrables ou non (cf. Gödel).

[Médiat]

Je précise que la méthode la plus courante pour démontrer l'indécidabilité d'un énoncé est de passer par la théorie des modèles.

[ilelogique]

ben oui mais si je faisais ça il me semble que je ne viendrai pas demander ici non ? lol.
je demandais juste si on savait quelque chose sur la décidabilité de la décidabilité ???
Je dois malheureusement partir quelques jours, je risque de ne plus trop réagir mais vous lirai avec joie dès mon retour,
merci !

[invite6754323456711]

la décidabilité de la décidabilité ???

Dans la suite de peut ont définir définir, votre prochain post va t-il être la logique peut elle parler d'elle-même ?

Patrick

[invite6c250b59]

mais ma question reste

Comment cela elle reste? Tu as eu deux ou trois fois la même réponse, et c'est la deuxième fois que quelqu'un te fait remarquer que tu as eu une réponse.

[ilelogique]

Existe-t-il un langage L, une théorie cohérente T sur L non triviale (contenant l'arithmétique par exemple) et une formule F de L, tels qu'il existe une formule de L dec(F) exprimant la décidabilité de F dans T, de sorte que dec(F) soit elle même indécidable dans T ?

[invite7863222222222]

une théorie cohérente T sur L non triviale (contenant l'arithmétique par exemple

Le 2nd théorème de Gödel, nous dit, que pour toute théorie T contenant l'arithmétique, si elle est cohérente, cette cohérence n'est pas démontrable dans T.

[Médiat]

Bonjour,
Dans le fil "contributions des forumeurs", le document "arithmétique" donne l'exemple de la formule Preuve(n,m) qui exprime que n est une preuve de m (il y a l'équivalent dans toutes les démonstrations du th de Gödel). Je vous laisse écrire Dec (m) à partir de là

[ilelogique]

N'ayant pas pour but, et surtout ne me sentant pas les compétences, de rentrer dans un tel formalisme, je demande juste si il existe, selon vous, une telle situation ?
Il me semble, pour faire informel que dec(F) serait une formule exprimant l'existence d'un entier n et d'une suite finie de formules (Fn) qui seraient déduites les unes des autres par les règles de déduction depuis les axiomes de T telle que Fn=F ou Fn=non ; c'est à dire que dec(F) exprimerait dans T l'existence d'une preuve de F ou d'une preuve de nonF. Il me semble que Gödel a exprimé une formule du même genre dans l'arithmétique pour sa preuve.

Ma question touche alors la décidabilité de dec(F).

Avez-vous connaissance d'une telle situation (où l'indécidabilité de la décidabilité d'une formule serait prouvée dans une certaine théorie) ???

[ilelogique]

Si par exemple on sait que la théorie des groupes est indécidable (dans la mesure où les énoncés décidables sont récursivement énumérables alors que l'ensemble des énoncés indécidables ne l'est pas), ça ne change rien à ma question :
c'est bien pour ça que j'ai parlé de 3 situations (minimum !) pour un énoncé :
- Il est décidable (lui ou sa négation est prouvable)
- Il n'est pas décidable (on a prouvé que ni lui ni sa négation n'est prouvable, il est donc "indépendant", comme l'axiome du choix dans les ensembles par exemple ou le 5e postulat en géométrie, etc.)
- La question de sa décidabilité n'est pas décidable (on a prouvé que dec(F) est indécidable)

C'est bien sur cette dernière classe que porte ma question :
Existe-t-il selon vous un langage L, une théorie cohérente T sur L non triviale (contenant l'arithmétique par exemple) et une formule F de L, tels qu'il existe une formule de L dec(F) exprimant la décidabilité de F dans T, de sorte que dec(F) soit elle même indécidable dans T ?

[invite6754323456711]

Ma question touche alors la décidabilité de dec(F).

Si on répété la même réponse comme vous répétez la même question. On codifié "la décidabilité de dec(F)" pour la ramener au langage L .... Votre troisième cas ne se ramène t-il pas à ce qu'a déjà exprimé Gödel non ? Et ceci aussi bien pour la décidabilité de la décidabilité de la décidabilité ....

Patrick

[Médiat]

c'est bien pour ça que j'ai parlé de 3 situations (minimum !) pour un énoncé :
- Il est décidable (lui ou sa négation est prouvable)
- Il n'est pas décidable (on a prouvé que ni lui ni sa négation n'est prouvable, il est donc "indépendant", comme l'axiome du choix dans les ensembles par exemple ou le 5e postulat en géométrie, etc.)
- La question de sa décidabilité n'est pas décidable

Le cas 3 ne peut être une propriété intrinsèque d'une formule dans une théorie : il suffit de trouver les bons modèles pour répondre à la question.

[ilelogique]

Re bonjour,
je me suis réveillé d'une sieste avec ceci, je vous le soumets...
Soit T une théorie sur un langage L.
Soit E l'ensemble des énoncés de L qui sont décidables à partir de T et CE sont complémentaire dans l'ensemble des énoncés du langage L.
Je suppose que E est récursivement énumérable mais non récursif (c'est le cas de la théorie des groupes, et sans doute celui de l'arithmétique (?)).
Supposons enfin qu'à toute formule close F on puisse donc associer la formule dec(F) qui affirme la décidabilité de F dans T (dec(F) affirmerait donc l'existence d'une preuve de F ou de nonF, c'est à dire d'une suite finie de formules déduites de T par les règles de déduction dont la dernière formule serait F ou nonF)

Si dec(F) était dans E (donc si dec(F) était décidable) pour toute formule F, alors il serait possible pour toute formule F de dire en un temps fini (de façon récursive) si la formule F est décidable ou pas, dans ce cas CE serait lui aussi récursivement énumérable et donc E serait récursif, contradiction.

Donc il existe nécessairement une formule F telle que dec(F) n'est pas décidable (dec(F) est dans CE)

Ceci a pour conséquence que dec(F) est indépendante de T, c'est à dire qu'on peut la rajouter à T, elle ou sa négation, sans changer la cohérence éventuelle de T. En ce sens que :
Coh(T)=> coh(T U dec(F)) et que coh(T) => coh (T U nondec(F))

On peut ainsi décider que F est décidable ou pas (et cela sans la valider ou l'invalider).

Pas de raison qu'on ne puisse pas ensuite recommencer cela, non ?

La question se pose encore pour les théories récursives ou celles qui ne sont même pas récursivement énumérables...

bon, à suivre...

[invite6754323456711]

Supposons enfin qu'à toute formule close F on puisse donc associer la formule dec(F) qui affirme la décidabilité de F dans T (dec(F) affirmerait donc l'existence d'une preuve de F ou de nonF,

Qu'est-ce qui "interdirait" de continuer le processus sur dec (dec (F)) ?

Cette hypothèse

Je suppose que E est récursivement énumérable mais non récursif

?

Patrick

[invite6c250b59]

Je suppose que E est récursivement énumérable mais non récursif (c'est le cas de la théorie des groupes, et sans doute celui de l'arithmétique (?)).

Pourquoi ce point d'interrogation?

il existe nécessairement une formule F telle que dec(F) n'est pas décidable

Hilbert sera tout chose de l'apprendre.

On peut ainsi décider que F est décidable ou pas (et cela sans la valider ou l'invalider).

Pas de raison qu'on ne puisse pas ensuite recommencer cela, non ?

On peut même faire plus rigolo. La cohérence de Peano n'est pas démontrable dans Peano, donc on peut ajouter à Peano l'affirmation de sa non cohérence, et le résultat sera cohérent. (du moins, autant que Peano ou Peano ajouté de l'affirmation de sa cohérence)

[ilelogique]

Oui je pense qu'on peut continuer avec dec(dec(F)) etc.
Mais cela peut se faire, sans ajouter d'axiome à T et donc pas de nouvelles exigences quant- au côté récursivement énumérable il me semble.
Si on suppose en effet que pour toute formule close f alors dec(F) existe, on a dec(F) qui est close et donc dec(dec(F)) existe aussi, etc.
Donc il me semble que dans toute théorie pour laquelle l'ensemble des énoncés décidables est récursivement énumérable et non récursif on peut trouver une formule F dont la décidabilité n'est pas décidable etc.
Il y aura aussi une formule dont la décidabilité de la décidabilité ne sera pas décidable...

Pour le point d'interrogation c'est que je ne suis pas sûr que l'ensemble des énoncés décidables dans Peano soit récursivement énumérable sans être récursif (je suppose que c'est un résultat classique non ?)

Pour Peano et sa cohérence, marrant oui, suis ok.

Je commence à voir un peu ma réponse !
Merci

[invite6754323456711]

Mais cela peut se faire, sans ajouter d'axiome à T

Gödel n'a t-il pas construit grâce à un processus de codification des énoncés exprimés dans le langage de la théorie T afin d'utiliser la formalisation de la théorie dans elle-même sans ajout et tout en restant dans un cadre syntaxique ? En exemple le second théorème ne codifie t-il pas la "cohérence de la théorie" comme d'un énoncé (formule close) de celle-ci ?

Dans une théorie récursivement axiomatisable, « être une preuve » n'est-il pas décidable ?

Patrick

[ilelogique]

Oui, et alors ?
si "être une preuve" est sans doute décidable dans la mesure où une preuve est une suite finie (certes déduite grâce à des schémas de règles, en quantité dénombrable) ça n'empêche pas il me semble.
je ne vois pas, dans ce que j'ai mis, en quoi il y aurait besoin de modifier T.