indécidabilité de la décidabilité

[invite6754323456711]

Oui, et alors ?

Je cherche juste à montrer, me semble t-il, que le problème de la décidabilité de la décidabilité de F "dec (dec(F))" est de la même forme syntaxique que le problème de la décidabilité de F "dec (F)".

Patrick
-----

[invite6754323456711]

Je cherche juste à montrer, me semble t-il, que le problème de la décidabilité de la décidabilité de F "dec (dec(F))" est de la même forme syntaxique que le problème de la décidabilité de F "dec (F)".

Dit autrement. Vous semblez convaincu d'avoir découvert dans le cadre de la logique classique concernant les concepts mathématiques de décidabilité/indécidabilité d'énoncés, des propriétés qui ne seraient pas capturées par les théorèmes de complétude et d'incomplétude. D’où mes interrogations pour chercher d'éventuel biais.

Patrick

[ilelogique]

Je suis d'accord que dec(dec(F)) a la même forme syntaxique que dec(F).
Je n'ai pas spécialement eu l'impression de faire une découverte sensationnelle, juste que je demande si on peut concevoir ou pas un énoncé dont la décidabilité est indécidable (en ce sens qu'il existerait des énoncés dont on a prouvé, dans une théorie, qu'on ne pourrait jamais savoir si ils sont indécidables ou pas)
et, en parlant ici, je commence à trouver quelques réponses,
il semble que la réponse soit oui.

[Médiat]

Je n'ai pas spécialement eu l'impression de faire une découverte sensationnelle, juste que je demande si on peut concevoir ou pas un énoncé dont la décidabilité est indécidable (en ce sens qu'il existerait des énoncés dont on a prouvé, dans une théorie, qu'on ne pourrait jamais savoir si ils sont indécidables ou pas).

Il suffit de trouver les modèles qui vont bien pour avoir la réponse.
En fait je ne suis pas sûr de bien comprendre où vous voulez en venir, pourriez vous exprimer votre idée dans le cadre de la théorie des groupes.

[ilelogique]

Bonjour,
je ne cherche pas spécialement dans la théorie des groupes.
Je veux juste savoir si il est possible, dans un certain cadre, d'avoir une formule dont la décidabilité n'est elle même pas décidable.
Aussi en prenant une théorie pour laquelle l'ensemble des énoncés décidables est récursivement énumérable, comme c'est le cas des groupes (et je ne suis pas certain que ce soit le cas de l'arithmétique), ainsi que je l'ai proposé plus haut, il me semble qu'on arrive au fait qu'il y a forcément une formule F telle que dec(F) soit indécidable.
Il est vrai que je n'ai pas explicitement exprimé dec(F) dans le langage L, mais, en m'appuyant intuitivement sur le fait que Gödel a fait le même genre de truc dans son théorème, je me dis qu'il y a bien au moins une théorie et un langage pour lesquels c'est possible !

La conséquence est qu'alors on aura la même chose pour dec(dec(F)) et ainsi de suite.

Si bien qu'on ne peut pas, à coup sûr, affirmer qu'une proposition est soit décidable soit indécidable : il se peut que sa décidabilité ne soit pas décidable (et qu'on puisse donc choisir si on la veut décidable ou pas en ajoutant l'axiome ad'hoc à T)

Voilà.

Ensuite, je peux développer si ça vous intéresse, je pense que ce résultat agit sur une autre question de fond :
inventons-nous ou découvrons-nous les mathématiques ??

[Médiat]

C'est la troisième (et la dernière fois) que je vous le signale : qu'une théorie soit incapable de démontrer l'indécidabilité d'une de ses formules ne démontre pas qu'elle est effectivement indécidable.

[Médiat]

Voir le message 10 de la conversation "l'homme et les mathématiques", ou faites une recherche sur "inventées".

[ilelogique]

Re,
quand vous dites : "qu'une théorie soit incapable de démontrer l'indécidabilité d'une de ses formules ne démontre pas qu'elle est effectivement indécidable" je suis bien d'accord, mais je ne crois pas avoir dit ça ! (ou bien où svp ???) et je suppose bien sûr que le "elle" parle de la formule.

J'ai dit qu'il existe nécessairement une formule F telle que dec(F) soit indécidable, car si tel n'était pas le cas, alors dec(F) serait décidable pour toute formule F si bien qu'au bout d'un temps fini on saurait si oui ou non F est décidable, ce qui rendrait l'ensemble des énoncés décidables mais aussi celui des énoncés indécidables récursivement énumérables et donc récursifs, ce qui est en contradiction avec l'hypothèse que j'ai prise (comme la théorie des groupes ou de l'arithmétique (?)).

[invite7863222222222]

J'ai dit qu'il existe nécessairement une formule F telle que dec(F) soit indécidable, car si tel n'était pas le cas, alors dec(F) serait décidable pour toute formule F si bien qu'au bout d'un temps fini on saurait si oui ou non F est décidable,

Non, vous arrivez seulement à :

J'ai dit qu'il existe nécessairement une formule F telle que dec(F) soit indécidable, car si tel n'était pas le cas, alors dec(F) serait décidable pour toute formule F si bien qu'au bout d'un temps fini on saurait si oui ou non dec(F) est décidable.

Pour vous donner un exemple, sur IN, pour chaque élement e, je considère la question, est-ce 2e est pair (je prends un exemple basique exprès) ?

On peut répondre à la question pour chaque élément e (la réponse est oui), mais est-ce ca prouve que pour tout élément de IN, la réponse est la même (oui ils sont pairs) ? Non, puisque qu'en l'occurrence, évidemment tous les éléments de IN ne sont pas pairs.

[Médiat]

ne crois pas avoir dit ça ! (ou bien où svp ???)

Message #63.


J'ai de plus en plus l'impression que vous confondez décidabilité d'un énoncé dans une théorie et décidabilité d'une théorie.

[pelkin]

Message #63.


J'ai de plus en plus l'impression que vous confondez décidabilité d'un énoncé dans une théorie et décidabilité d'une théorie.

Bien d'accord,

Faudrait peut être demander à "ilelogique" dans quel ordre de logique il se situe pour poser sa question

[invite6754323456711]

juste que je demande si on peut concevoir ou pas un énoncé dont la décidabilité est indécidable (en ce sens qu'il existerait des énoncés dont on a prouvé, dans une théorie, qu'on ne pourrait jamais savoir si ils sont indécidables ou pas).

J'ai dit qu'il existe nécessairement {une formule F telle que dec(F) soit indécidable},

Il existe nécessairement -->

La prouvabilité d'un énoncé à partir des axiomes d'une théorie des ensembles cohérente, et plus généralement de toute théorie cohérente qui permet d'exprimer « suffisamment » d'arithmétique formelle est indécidable.


Décidabilité, indécidabilité d'un énoncé dans un système logique : Une proposition (on dit aussi énoncé) est dite décidable dans une théorie axiomatique, si on peut la démontrer ou démontrer sa négation dans le cadre de cette théorie.

Les deux notions de décidabilité (logique et algorithmique) interprètent chacune la notion intuitive de décision dans des sens clairement différents. Elles sont cependant liées.

L’indécidabilité est la négation de la décidabilité : Dans les deux cas il s'agit de formaliser l'idée qu'on ne peut pas toujours conclure lorsque l'on se pose une question, même si celle-ci est sous forme logique.

Une théorie axiomatique est décidable s'il existe un algorithme qui réponde toujours par oui ou non à la question de savoir si un énoncé donné est démontrable dans cette théorie.

Dans une théorie récursivement axiomatisable, « être une preuve » est décidable, mais cela ne permet pas de vérifier mécaniquement qu'un énoncé est un théorème. On peut bien lancer la machine, tant que l'on n'obtient pas l'énoncé que l'on cherche à démontrer, sans autre information, on ne sait pas si c'est parce que la machine le donnera plus tard ou ne le donnera jamais.

La problématique que vous posez (quand bien même elle fait apparaitre plusieurs niveau - problème du problème) ne relève t-elle pas plutôt du problème de la décision comme déjà fait remarqué ?

Patrick

[ilelogique]

Bonjour,
je ne comprends pas trop. je vous demandais en quoi ce que j'ai proposé ne va pas, à quel endroit je me trompe ?
Au lieu de cela vous dites que je confonds la décidabilité d'un énoncé avec celle d'un ensemble, mais je ne vois pas trop en quoi.
Pour moi un énoncé est décidable dans une théorie si il est prouvable ou réfutable alors qu'un ensemble est décidable, au fond, si il est récursif, c'est à dire si on peut mécaniquement tester l'appartenance à l' ensemble.
Aussi n'hésitez pas à me dire ce qui ne va pas dans ce que j'ai proposé et, si ça ne va pas, auriez-vous une idée de la question originale que j'ai posée :
Existe-il un langage et une théorie pour laquelle on peut trouver une formule F dont la décidabilité n'est pas décidable ?

Pour ce qui est de l'ordre, il me semble que tout ceci devrait pouvoir se formaliser au premier ordre.

[invite6754323456711]

Existe-il un langage et une théorie pour laquelle on peut trouver une formule F dont la décidabilité n'est pas décidable ?

Dans le cadre de la logique classique du premier ordre une porte ne peut être que soit ouverte ou soit fermée non ? Une formule exprimé dans un langage L d'une théorie T ne peut être que décidable ou indécidable (dans le cadre de cette théorie) non ? Maintenant le démontrer n'est pas toujours possible, il existe des cas ou on ne sait pas, mais cela ne démontre pas que c'est ni l'un ni l'autre non ?


Patrick

[invite7863222222222]

Existe-il un langage et une théorie pour laquelle on peut trouver une formule F dont la décidabilité n'est pas décidable ?

"Existe-il un langage et etc. [???]" ressemble beaucoup à un énoncé mathématique. D'où,

vous vous demandez :

1. s'il existe un système théorique qui exprime formellement votre question et qui en donne une réponse ?

ou

2. dans toutes les théories sur lesquelles les mathématiciens travaillent aujourd'hui, il en existe une théorie où une telle chose a été mise en évidence ?

?

C'est une des raisons pour laquelle je ne vous réponds pas, n'étant pas sûr que vous sachiez exactement vous-même exactement ce que vous recherchez.

[invite7863222222222]

n'étant pas sûr que vous sachiez exactement vous-même exactement ce que vous recherchez.

Après relecture, je me rends compte qu'involontairement, la forme de ce que j'ai dit est "connotée".

J'ai voulu dire, donc en reformulant :

"n'étant pas sûr que vous ayez formulé, exactement, la question correspondant, à ce sur quoi vous vous interrogez".

[ilelogique]

je ne comprends pas, ça fait 10 fois que je remets ma question !
Pour U100fil : vous dites qu'un énoncé est soit décidable soit indécidable, pouvez-vous le prouver svp car c'est justement là dessus que je doute.
Pour ma question :
Existe-t-il un langage L, une théorie T sur L, et un système de règles d'inférences de sorte que pour une formule F on puisse écrire une formule "Dec(F)" qui exprime le fait que F est décidable (l'existence d'une preuve de F ou de non F) et telle que, donc : Dec(F) serait indécidable ???????????

En gros donc : se peut-il que la décidabilité d'une formule soit indécidable ????

En fait j'ai un peu l'impression que personne n'en sait rien, pas de souci, mais dites le svp.

Car on me répond toujours par des questions et surtout ces questions me semblent souvent sans lien vraiment avec ma question. De la même façon j'ai tenté d'y répondre moi même (page 5 environ de cette discussion) en partant de la théorie des groupes, on m'a dit que je confondais des choses mais sans me dire à quel endroit et pourquoi.

J'avoue que je me lasse un peu !

[ilelogique]

J'ai personnellement l'impression que ma question est claire et que je sais ce que je cherche.
j'ajoute :
Si on parvient à prouver que dec(F) est indécidable alors dec(F) serait indépendante de T et on peut ajouter à T dec(F) ou nondec(F) sans perdre en cohérence, c'est à dire choisir si on veut ou pas que F soit décidable.

[invite73192618]

Pour U100fil : vous dites qu'un énoncé est soit décidable soit indécidable, pouvez-vous le prouver svp car c'est justement là dessus que je doute.

Oui. Si les axiomes sont assez puissants, par exemple s'ils incluent Peano, alors ils permettent de construire une machine de Turing qui s'arrête si et seulement si l'énoncé est décidable. Ou elle peut s'arrêter, ou elle ne peut pas.

[shokin]

Pour U100fil : vous dites qu'un énoncé est soit décidable soit indécidable, pouvez-vous le prouver svp car c'est justement là dessus que je doute.

N'y a-t-il pas simplement le tiers exclu ?

[Médiat]

J'avoue que je me lasse un peu !

Et je parie que vous n'êtes pas le seul !

Soit T une théorie et F une formule.

Soit F est démontrable dans T
Soit F n'est pas démontrable dans T

Soit non F est démontrable dans T
Soit non F n'est pas démontrable dans T

Je vous laisse étudier les 4 cas possibles et vous verrez que ù100fil a raison !

[ilelogique]

re, merci pour vos réponses.
d'abord je voudrais dire que si je pose cette question, personnellement ça m'arrangerait bien que la réponse soit négative (et qu'il n'existe pas de telle formule).
La réponse de Jiav est assez convaincante car une machine de Turing doit bien s'arrêter ou ne pas le faire, cependant nous savons tous que tant que la machine de Turing ne s'est pas arrêtée : on ne sait pas si elle s'arrête ou pas, si bien qu'on pourrait dire que ou bien elle s'arrête ou bien on ne sait pas...
Et ne pas savoir est une tierce réponse, quand Shokin parle de tiers exclu, bien qu'on ne se place pas là dans la mesure où le choix ou non de cet axiome importe peu ici je pense, on peut en effet faire un parallèle : une chose est-elle nécessairement vraie ou fausse ?
Si on prend par exemple la question de l'existence de Dieu, si, bien sûr, on peut dire que ou bien Dieu existe ou bien Dieu n'existe pas : le fait qu'il soit à peu près certain qu'on ne pourra jamais le prouver ou l'infirmer, on voit bien que la question est inepte, indécidable, trois possibilités : ou bien il existe, ou bien il n'existe pas, ou bien on ne pourra jamais le savoir.
Aussi, pour répondre à ù100fil et Médiat :
vous dites qu'il n'y a que deux possibilités pour un énoncé : il est décidable ou bien il ne l'est pas.
Pouvez vous prouver cela ? ou me l'expliquer ? Pourquoi ne se peut-il pas qu'on ne puisse pas savoir ??
Mediat dit qu'il me laisse étudier ces 4 cas possibles : je ne vois pas en quoi j'ai besoin de les étudier (d'autant que je pense bien les voir) mais surtout en quoi ce seraient les seuls "possibles" (et c'est bien ma question depuis le début) ?
à supposer que vous ayez raison (ce que je souhaite), aussi : en quoi ce que j'ai dit plus haut (avec les groupes) serait faux svp ?
- Ou bien il serait impossible, dans aucune théorie, d'écrire une telle formule dec(F) pour toute formule F (mais j'ai l'impression que c'est faisable de formaliser le fait qu'il existe une preuve de F ou de non F, et pas forcément au second ordre (en quantifiant sur les formules))
- Ou bien, et je pense que c'est ce que vous me dites : cette formule dec(F) serait donc toujours décidable ? (mais ça me menait à une contradiction sur le fait que la théorie des groupes deviendrait alors décidable, récursive (au sens algorithmique du terme))

aussi j'essaye à nouveau de poser la question :
Pensez-vous qu'une telle formule dec(F) n'est pas possible à écrire dans aucun langage d'aucune théorie ou bien, si vous ne le pensez pas, pensez-vous alors qu'une telle formule serait nécessairement décidable et pourquoi ???

[invite73192618]

La réponse de Jiav est assez convaincante car une machine de Turing doit bien s'arrêter ou ne pas le faire
(...)
vous dites qu'il n'y a que deux possibilités pour un énoncé : il est décidable ou bien il ne l'est pas.
Pouvez vous prouver cela ? ou me l'expliquer ?

Si ma réponse est convaincante, pourquoi reposes-tu la question?

- Ou bien il serait impossible, dans aucune théorie, d'écrire une telle formule dec(F) pour toute formule F (mais j'ai l'impression que c'est faisable de formaliser le fait qu'il existe une preuve de F ou de non F, et pas forcément au second ordre (en quantifiant sur les formules))

C'est bien entendu possible, sauf pour des théories trop faibles.

- Ou bien, et je pense que c'est ce que vous me dites : cette formule dec(F) serait donc toujours décidable ? (mais ça me menait à une contradiction sur le fait que la théorie des groupes deviendrait alors décidable, récursive (au sens algorithmique du terme))

Non la réponse que l'on t'a faite est que si F est indécidable pour une théorie alors dec(F) est également indécidable.

[invite7863222222222]

J'ai personnellement l'impression que ma question est claire et que je sais ce que je cherche.

Pourquoi ne répondez-vous pas alors à ma question, afin de savoir si j'ai bien saisis votre question ? :

vous vous demandez :

1. s'il existe un système théorique qui exprime formellement votre question et qui en donne une réponse ?

ou

2. dans toutes les théories sur lesquelles les mathématiciens travaillent aujourd'hui, il en existe une théorie où une telle chose a été mise en évidence ?

?

Donc est-ce 1. ou 2., les deux, ou ni l'un ni l'autre ?

[ilelogique]

Bonjour,
pour Jiav : vous ne citez qu'une partie de ma phrase, il y a un "cependant" juste après qui répond à la question que vous venez de poser.
Ravi d'apprendre que Dec(F) peut exister selon vous, vous êtes le premier à le dire ici.
Enfin vous dites : "la réponse que l'on t'a faite est que si F est indécidable pour une théorie alors dec(F) est également indécidable.", je veux bien savoir :
- où avez-vous fait une telle réponse svp ?
- Ce que vous dites signifie il me semble donc que si dec(F) est décidable alors F est décidable (par contraposée) or ceci me parait faux puisqu'on a déjà prouvé l'indécidabilité de Formules dans la plupart des théories élaborées.

Pour Jreeman :
Ainsi qu'il me semble l'avoir déjà dit, je cherche juste à savoir si il existe un langage, une théorie, un système de déduction et une formule F tels que la décidabilité de F dans T soit indécidable. donc, en soi, oui, peu importe le système (car si la réponse est NON alors ce sera non pour tous les systèmes et si c'est OUI on sera amené à se poser la question pour les théories usuelles des maths).
Non je ne ressens pas le besoin de formaliser et trouver un système qui explicitera lui même la question (car là ça irait bien loin !!) : il suffit juste que dec(F) soit formalisé dans le langage, pas ma question elle même !
Ensuite, bien sûr, si une telle réponse était positive sur une théorie comprenant Peano je serais bien ennuyé, mais au moins je serai fixé !
en espérant avoir été plus clair ??

[ilelogique]

je pense que ma question peut aussi se formuler ainsi :
est-il possible que la question de l'indépendance ou non d'une formule F d'une théorie T soit exprimable dans le langage et elle même indépendante de T ???

[invite7863222222222]

- Ou bien il serait impossible, dans aucune théorie, d'écrire une telle formule dec(F) pour toute formule F (mais j'ai l'impression que c'est faisable de formaliser le fait qu'il existe une preuve de F ou de non F, et pas forcément au second ordre (en quantifiant sur les formules))

Je ne peux tjrs pas répondre tant que vous ne précisez pas à quoi vous faîtes allusion par "aucune théorie" :

1. "théories mathématiques" sur lesquelles les mathématiciens travaillent à l'heure actuelle (arithmétique, théorie des ensembles, théories des groupes, théories de noeuds etc...),
ou
2. celles formalisées par un système théorisant formellement mathématiquement votre question (quantification sur l'ensemble des théories possibles/langages possible, et de la décidabilité de leur formule) afin d'y répondre ?

- Ou bien, et je pense que c'est ce que vous me dites : cette formule dec(F) serait donc toujours décidable ? (mais ça me menait à une contradiction sur le fait que la théorie des groupes deviendrait alors décidable, récursive (au sens algorithmique du terme))

Je vous ais expliqué que non, vous n'arrivez à aucune contradiction, juste que dec(F) est décidable pour toute formule F (tautologie), tout simplement.

Pensez-vous qu'une telle formule dec(F) n'est pas possible à écrire dans aucun langage d'aucune théorie ou bien, si vous ne le pensez pas, pensez-vous alors qu'une telle formule serait nécessairement décidable et pourquoi ???

Pour répondre, même question préalable à nouveau.

Non la réponse que l'on t'a faite est que si F est indécidable pour une théorie alors dec(F) est également indécidable.

Ha bon ? à quel message ?

[invite7863222222222]

Ok donc vous avez répondu à ma question.

Non je ne ressens pas le besoin de formaliser et trouver un système qui explicitera lui même la question

Pourtant, quand je lis ceci :

donc, en soi, oui, peu importe le système

Je me demande, comment vous pouvez penser être sûr d'avoir une réponse définitive et sûre, si vous ne formalisez pas mathématiquement le peu importe le système.

Car à priori, c'est bien une telle réponse (définitive et sûre) vous le demandez, et il est donc nécessaire de la formaliser dans un système, non ?

[ilelogique]

Ma question relève à la fois de vos 1) et 2) il me semble. En effet :
- A terme c'est bien la question de la formalisation de dec(F) puis de celle de sa décidabilité dans les théories classiques de maths (notamment celle contenant l'arithmétique et/ou théorie des ensembles, voire la théorie des groupes ainsi qu'explicité plus haut) qui m'intéresse.
- Au demeurant, si on trouve une réponse positive à la question dans une axiomatique quelque peu farfelue construite exprès (j'entends ici par axiomatique la donnée d'un langage, d'un ensemble de règles de déduction et d'une théorie) alors ça voudra dire que la question peut devenir légitime pour les théories conventionnelles (la théorie farfelue en question devra pourtant tout de même permettre d'exprimer dec(F)) et si la réponse est négative quelque soit l'axiomatique choisie (ce que semblent croire Médiat et ù100fil) elle le sera bien sûr aussi pour les théories usuelles.

Bien sûr quand je demande si il existe une axiomatique telle que dec(F) soit indécidable dans T, il faut pouvoir formaliser dec(F) mais pas besoin de formaliser ma question elle même il me semble (le théorème d'incomplétude s'écrit-il au premier ordre ?)

Enfin selon moi dire que "si F est indécidable pour une théorie alors dec(F) est également indécidable" est faux car on arrive à une contradiction par contraposée.

[invite7863222222222]

pas besoin de formaliser ma question elle même il me semble (le théorème d'incomplétude s'écrit-il au premier ordre ?)

C'est contradictoire avec le fait que ce soit 1. et 2. qui vous intéresse.

A moins que vous ayez en tête que dans les théories existantes habituelles (arithmétique, théorie des ensembles, théorie des groupes etc.), il y a déjà une réponse à votre question et que vos prévisions quant à l'axe que devrait prendre cette discussion sera une confirmation de cela.

Mais je continue à douter de cela, je pense que vous cherchez plus ou moins un système qui formalise votre question, pour y apporter une réponse définitive, de manière à ce que même si dans les théories existantes il n'y a pas de confirmation, on puisse quand même mettre en exergue un cas qui vous intéresse dans le sens où vous le dîtes.