indécidabilité de la décidabilité

[pazuzen]

Bonjour,
je voudrais savoir ce que vous pensez du raisonnement suivant et, donc, de la validité de l'assertion suivante :
"Dans toute théorie suffisamment élaborée (par exemple contenant l'arithmétique de Peano) : il existe un énoncé dont la décidabilité n'est pas décidable".

Je viens douter ici de la validité de mon propos notamment parce que j'y suppose la coïncidence entre les décidabilités aux sens de Gödel et de Turing (quid de cette coïncidence ?)
Au demeurant, il me semble que Giuseppe Longo en a proposé une démonstration.

Et donc :
Nous savons grâce à Gödel que pour tout énoncé A de l'arithmétique (notée AP) il existe un prédicat Théo(A) qui code le fait que A soit un théorème de AP (on peut coder «*théo(A)=il existe une preuve Y de A*») donc le prédicat «*Dec(A)=théo(A) ou théo(nonA)*» est un prédicat affirmant que A est décidable dans AP, il devrait être codable aussi. Or si on appelle E l'ensemble des énoncés décidables et G celui des énoncés indécidables dans AP alors E étant récursivement énumérable mais non récursif, on a G qui n'est pas récursivement énumérable (sinon E serait récursif), donc si pour toute formule A on a Dec(A) qui est dans E alors, si la décidabilité au sens de Gödel implique celle au sens de Turing (ce qu'on peut raisonnablement croire...), il existe un algorithme (une machine de Turing) qui s'arrête à coup sûr et décide pour chaque formule A de la validité de Dec(A), si bien qu'on saurait pour toute formule A si elle est décidable ou non, ce qui est contradictoire avec le fait que E soit non récursif, donc on déduit qu'il existe une formule A telle que Dec(A) est dans G, c'est-à-dire l'existence d'une formule dont la décidabilité n'est pas décidable.

Ceci impliquerait bien sûr qu'il y aurait une formule dont la décidabilité de la décidabilité ne serait pas décidable et donc l'existence, par induction, d'une chaîne infinie…

Qu'en pensez-vous svp ?
merci.

J'ai des remarques à prendre où à laisser...

D'abord le fait que Godel a démontré qu'un système d'arithmétique suffisamment complexe, récursivement axiomatisable, intégrant la théorie des nombres cohérent (donc non contradictoire) contient toujours des énoncés mathématiques dont on ne sait dire s'ils sont vrais ou faux (indécidables)

En effet, il existe un pont entre les systèmes formels récursifs et les algorithmes type 'machines de Turing' à la base du développement de l'informatique : C'est la thèse de Church Turing qui démontre l'équivalence entre différents algorithmes dont l'algorithme 'machine de turing' qui formalise la notion intuitive de calculabilité entre système formel et 'machines mécanisées' (par extension du concept de la machine de Turing) via l'algorithme formel de résolution entre les deux systèmes

Si tu es sur une théorie incomplète ou donc un système algorithmique complexe contenant l'arithmétique de Peano, tu as donc des énoncés indécidables (c'est démontré) et en pratique informatique, c'est le fameux problème de l'arrêt exposé par Turing en informatique car ne sachant décider, la boucle peut durer un certain temps...

La décidabilité, c'est conclure par oui ou par non à une assertion.
Oui OU Non
Boucler cette question par une réponse

La notion d'indécidabilité de la décidabilité n'a donc selon moi pas de sens dans un système formel incomplet intégrant Peano :
Elle ne concerne pas les assertions du modèle dont on a vu qu'elles pouvaient être décidables et parfois indécidables (ce dont nous sommes certain par Godel) mais ta question concerne l'indécidabilité de la décidabilité
Donc qu'on ne pourrait pas répondre par Oui / Non au fait de pouvoir répondre Oui / Non a une assertion du modèle.
Or on le sait.
On sait que, parfois, on peut répondre Oui grace au système formel et que parfois, on ne peut pas répondre par Oui / Non à une assertion d'un modèle incomplet par démonstration de Godel

On ne peut donc avoir une situation d'indécidabilité de la décidabilité
On sait qu'il y a des assertions décidables et on sait qu'il y a des assertions indécidables.
Il n'y a pas d'indécidabilité dans cette question.
-----

[Schrodies-cat]

Allons, bon, je me suis efforcé de préciser ces (il y en a plusieurs)notions d'indécidabilité et de décidabilité, mentionnant quelques résultats au passage, ce qui permet de préciser le (les ?) sens précis à cette expression d' "indécidabilité de la décidabilité" . Il faudrait des objections pertinentes pour que je m'y remette.

[pazuzen]

Je ne connais que les notions de décidabilité logique et de décidabilité algorithmique et les deux notions sont isomorphes à savoir qu'elles consistent à ne pas pouvoir conclure logiquement à une assertion au sein d'un système formel ou algorithmique.

Je ne comprends pas ce que t'amène la distinction sur la définition de décidabilité et je ne comprends donc pas ton dernier propos.

Est ce que tu pourrais développer ?

[Schrodies-cat]

re,
Au sens de Gödel (avec le théorème de complétude) un énoncé P est indécidable dans une théorie T si il n'existe pas de démonstration de P ni de démonstration de NonP ou bien si il y a des modèles de T où P est vraie et d'autres modèles où P est fausse. un ensemble.
or au sens de Turing un énoncé P est indécidable dans une théorie s'il n'existe aucune machine de Turing qui s'arrête pour dire si P est vrai ou non.
Et donc il me semblait qu'avec Curry Howard on pouvait établir la correspondance.

Eh bien il en existe toujours une ! Étant donné un énoncé P on considère les deux machines de Turing suivantes: elles ne tiennent pas compte de la donnée, l'une d'entre elles répond systématiquement vrai (ce qui peut se faire en un temps fini) et l'autre répondra systématiquement faux (idem); l'une de ces deux machine dira si P est est indécidable ou non !
Comme je l'ai dit plus haut, l'indécidabilité au sens de Turing concerne des familles (infinies) d'énoncés.

[Schrodies-cat]

Allez, je vais faire un effort :
Étant donné une théorie T (au sens utilisé jusqu'à présent) et un énoncé P du langage de cette théorie, on peut concevoir un algorithme qui étudie toute démonstration de longueur n de cette théorie, passant ensuite aux démonstrations de longueur n+1 etc ... Et qui s'arrête dès qu'il trouve une démonstration de P ou de non P. Un tel algorithme s'arrêtera si et seulement si P est est décidable dans la théorie P; soit, ce qui permet de définir la démontrabilité dans la théorie de Turing ; mais n'en déduisez pas plus qu'il n'est légitime.

[pazuzen]

Personnellement, je le comprends différemment
Quelle que soit la machine ou quelle que soit 'la machine de Turing' qui répond à la même logique de résolution algorithmique, il n'y en a pas une qui pourra décider quand l'autre ne pourrait pas.
Si le formalisme de résolution algorithmique est le même, les deux machines auront exactement le même problème d'indécidabilité qui est d'ailleurs ce problème de l'arrêt.

Etre indécidable est intrinsèque au formalisme de l'algorithme et des assertions indécidables existent dans tout système incomplet intégrant la théorie des nombres
Si je formalise l'ensemble des axiomes et des algorithmes de résolution au sein d'un navire pour en décrire formellement le fonctionnement, il y aura toujours l'âge du capitaine qui restera indécidable pour n'importe quel ordinateur
Je rigole à peine sur mon exemple
En gros l'exposé en rouge n'est pas rigoureux au sens de la décidabilité Turing

[ansset]

Si le formalisme de résolution algorithmique est le même, les deux machines auront exactement le même problème d'indécidabilité qui est d'ailleurs ce problème de l'arrêt.

ben justement, sur ce point, la notion d'indécidabilité logique ne décide pas ainsi du caractère indécidable, si?

[Schrodies-cat]

(...)
Quelle que soit la machine ou quelle que soit 'la machine de Turing' qui répond à la même logique de résolution algorithmique, il n'y en a pas une qui pourra décider quand l'autre ne pourrait pas.
Si le formalisme de résolution algorithmique est le même, les deux machines auront exactement le même problème d'indécidabilité qui est d'ailleurs ce problème de l'arrêt.
(...)

Oui ! deux machines dans lesquelles est implémenté le même algorithme se comporteront de la même façon !
Je n' y aurai jamais pensé tout seul ! J'apprends tout les jours quelque chose ici !
Ou alors je n'ai pas compris ce que vous entendez par "logique de résolution algorithmique".
Si c'est le cas expliquez moi ce que cela veut dire ! En fait je ne comprends pas ...

[pazuzen]

Ne vous enervez pas,
J'évoquais dans mon propos la formulation d'ilelogique que vous avez quoté en rouge et qui me semble fausse au sens de la décidabilité définie par Turing

Ceci dit, comme je l'écrivais et à mon sens, la notion d'indecidabilité de la décidabilité me semble être une erreur conceptuelle et certaines notions me semblent approximees dans la démonstration

Je l'évoque sans aucune volonté de froisser il n'y a pas de souci, je laisse ici mes remarques à prendre ou à laisser comme je l'indiquais

[Schrodies-cat]

La notion d'indécidabilité de la décidabilité est tout à fait concevable si on utilise les bon concepts.
Je me suis efforcé de préciser ceci depuis un certain temps.
Je distingue l'indécidabilité d'un énoncé particulier, plutôt associée à Gödel, et qui est relative à une théorie particulière (si un énoncé est indécidable dans un théorie, on peut sans risque l'ajouter comme axiome à cette théorie et on obtient une nouvelle théorie ou cet énoncé est démontrable)
Et l'indécidabilité d'une famille (infinie, sinon ce n'est pas intéressant ), plutôt associée à Turing, qui implique en fait que quelle que soit la théorie (axiomatisable, non-contradictoire, etc) utilisée, il reste des énoncés indécidable dans cette famille d'énoncés pour ladite théorie.

Je considère donc une théorie (contenant l'arithmétique etc) et je considère la décidabilité des énoncés du langage de cette théorie dans ladite théorie (première définition).
J'obtiens une famille infinie d'énoncés , ceux qui sont décidables au sens précédents, et j'applique la deuxième définition de la décidabilité à cette famille d'énoncés.
On peut ainsi définir la décidabilité de la décidabilité et, en travaillant un peu, on obtient que décidabilité n'est en général pas décidable.

[pazuzen]

De mon point de vue, il y a plusieurs erreurs dans cet exposé

Le premier concerne l'indecidabilité des systemes formels recursivement axiomatisables au sens de Godel
Il ne suffit pas d'ajouter une infinité d'axiomes pour forcer la décidabilité
D'une part parce que quels que soient les axiomes, tout systeme formel integrant la theorie des nombres continuera d'avoir des énoncés indecidables
La completude n'est pas écartée par l'introduction d'une infinité d'axiomes
D'autre part parce qu'ajouter des axiomes pose souci sur la consistance de la theorie
En gros plus tu cherches a etre complet plus tu perds en consistance et donc ajouter des axiomes te sort sur un énoncé de la non décidabilité au prix d'une injection de nombreux nouveaux énoncés indecidables

Concernant la notion d'indecidabilite que tu associes aux machines de Turing je ne suis pas d'accord non plus
Church Turing a énoncé l'equivalence d'une résolution algorithmique machine isomorphe aux systemes formels des mathematiques
En gros, la notion de décidabilité si elle s'exprime différemment est en fait sur les memes limites

[pazuzen]

En gros si tu definis un groupe d'enoncés indecidables dans un systeme formel mathematique intégrant la theorie des nombres et que tu les etudies sur un ordinateur dans lequel tu as programmé un algorithme qui repond à ce systeme formel (ce que font les mathematiciens pour experimenter leurs théorèmes), ces énoncés indecidables dans ton systeme formel mathématique resteront indecidables car non calculables sur ordinateur (en dehors du spectre de la résolution algorithmique et non recursivement axiomatisable)
Si un énoncé est décidable par démonstration mathématique dans ton systeme formel, il restera tout aussi décidable sur ordinateur
Ta notion d'indecidabilité de la décidabilité n'a intrinsèquement pas de sens
Je ne sais pas si je suis clair mais je renvoie aux notions de calculabilité et à la thèse de Church Turing

[Schrodies-cat]

Si il s'agit bien des personnes auxquelles je pense, le prénom de Turing étai Alan, et Church était le patronyme d'une personne prénommée Alonzo.
Voila pour ce qui peut être facilement rectifié.
Donner un sens au reste serait plus laborieux et aléatoire.
Reconnaissons toute fois que ce n'est même pas faux .

[pazuzen]

Disons que cet argument est a priori réversible.
Une chose est certaine, je n'énonce pas ce que j'écris comme une vérité incontestable mais comme l'interprétation que je m'en suis faite avec mon parcours comme avec mes limites, c'est vrai.

Mais si le théorème d'indécidabilité de la décidabilité sort du paysage mathématique, je saurai que vous aviez raison.
Pour rester parfaitement rigoureux, ajouter deux prénoms n'est pas une rectification mais un complément, facilité et vérité allant souvent dans un sens contraire.

[ilelogique]

Bonjour !
Excusez moi de ne pas être intervenu depuis quelques temps, figurez vous que ça fait une semaine que je mets à jour la page courante de mon dernier post et que j'étais déçu que personne ne réponde... jusqu'à ce que je vois le petit 3 à droite m'indiquant qu'une 3e page venait de s'ouvrir.... pft désolé !
je vais donc, quand j'aurai le temps, au plus vite, lire vos échanges avec attention.
Au demeurant, une chose m'attire le regard quand je lis en diagonale : c'est ce que dit Pazuzen : le fait que la question de l'indécidabilité de la décidabilité n'aurait pas de sens !
Je dois réfléchir à ça car je n'y avais pas du tout pensé !
Pourtant, je pense par exemple à la conjecture de Syracuse dont on ne sait pas encore si elle est décidable ou non dans peano, je me demandais si la réponse existe ou pas (et donc vous semblez affirmer qu'elle existe nécessairement),
au fond, ne sommes nous pas dans de la méta-logique alors (au sens du langage choisi) ??
Ce que vous dites est-il bien qu'on ne peut pas formaliser dans le langage la question de la décidabilité d'un énoncé ?
Car pourtant, ce que j'ai appelé dec(A) = theo(A) ou théo(nonA) n'est-il pas un énoncé comme bien d'autres, et qui s'énonce au premier ordre ?

et qui est donc susceptible d'être décidable ou non (voire de décidabilité indécidable si ce que je propose a un sens...)

[Schrodies-cat]

Considérons un mathématicien qui travaillerait à démontrer la non contradiction de l'arithmétique, de Peano, voire de ZF , dans l'arithmétique de Peano .
Chacun dira qu'il perd son temps.
Sur quoi repose ce jugement ? Pour justifier ceci, il faut bien admettre que les théorèmes de Gödel parlent de quelque chose.
"en mathématiques, on ne sait pas de quoi on parle ..." , soit, mais on parle de quelque chose même si on ne sait pas précisément quoi .
C'était le coin du platonicien réformé.

[ilelogique]

Re,
en fait, du coup, je suis en train de douter d'une des assertions que j'affirme : c'est lorsque je considère l’énoncé theo(A).
En effet je dis que theo(A) est un énoncé affirmant que que A est un théorème de T, c'est à dire que A est conséquence sémantique et syntaxique de T (A vraie dans tout modèle de T et il existe une suite finie de formules terminant par A qui sont déduites les unes des autres à partir des formules de T par les règles de déductions / ces deux notions sont bien les mêmes par le théorème de complétude).
Or je ne sais pas si un tel énoncé est effectivement constructible ?
Ce sont mes souvenirs qui me font dire ça,
aussi, pensez-vous, pour commencer, qu'il y a bien, pour toute formule A, une formule (du premier ordre) theo(A) ??

[pelkin]

"en mathématiques, on ne sait pas de quoi on parle ..." , soit, mais on parle de quelque chose même si on ne sait pas précisément quoi .
C'était le coin du platonicien réformé.

J'apprécie beaucoup, je suis sur que Médiat va apprécier énormément aussi d'ailleurs ; apprendre que cela fait quarante ans que l'on ne sait pas précisément de quoi on parle fait toujours plaisir

Pour justifier ceci, il faut bien admettre que les théorèmes de Gödel parlent de quelque chose.

C'est la phrase la plus idiote que j'aie jamais entendu sur LES théorèmes de Gödel, on l'aura décidément mis à toutes les sauces ce pauvre Kurt, y compris pour ne rien dire.

[ilelogique]

Allons allons, restons dans le sujet, la logique, svp, la décidabilité de la décidabilité....
La réalité et/ou l'utilité des maths et des théorèmes de Kurt sont un autre sujet, même si certes passionnantes et propices à de fortes et justifiées oppositions d'idées...

[mike.p]

Nous savons grâce à Gödel que pour tout énoncé A de l'arithmétique (notée AP) il existe un prédicat Théo(A) qui code le fait que A soit un théorème de AP (on peut coder «*théo(A)=il existe une preuve Y de A*») donc le prédicat «*Dec(A)=théo(A) ou théo(nonA)*» est un prédicat affirmant que A est décidable dans AP, il devrait être codable aussi.

Salut,

ce code n'est il pas déjà "Dec(A)=théo(A) ou théo(nonA)" et donc décidabilité^n(A) = décidabilité(A) ?

n'a t on pas décidabilité(P ou Q) = décidabilité(P) et décidabilité(Q) ?

[mike.p]

je précise :
si on admet que
décidabilité(P ou Q) = décidabilité(P) et décidabilité(Q)
et
décidabilité(non P ) = décidabilité(P)
et que la notation suivante est valide
décidabilité(théo(P)) = décidabilité(P)

alors
décidabilité(décidabilité(A)) = décidabilité( théo(A) ou théo(nonA) )
= décidabilité( théo(A) ) et décidabilité(théo(nonA) )
= décidabilité(théo(A))
= décidabilité(A)

décidabilité^n(A) = décidabilité(A)

Ce n'est valable que si les 3 hypothèses n'en sont pas dans la théorie et son formalisme. Qu'en est il ?

[Schrodies-cat]

je précise :
si on admet que
décidabilité(P ou Q) = décidabilité(P) et décidabilité(Q)
et
(...)

Hum, hum cela commence mal ...
l'usage du signe = me fait un peu tiquer mais passons ...
si on remplace dans votre axiome ou schéma d'axiomes Q par (non P).
on obtient:
décidabilité(P ou non P) = décidabilité(P) et décidabilité(non P)
Or dans la logique classique (si vous vous placez dans un cadre, intuitionniste dites le mais je ne suis pas sur que cela va arranger les choses).
(P ou non P) est toujours démontrable (par simple application d'un axiome de la logique) donc décidable par définition de la décidabilité.
Donc (P est Décidable) ou (Non p est décidable), ce qui donne, sachant que ces deux propriétés sont équivalententes:
Toute énoncé est décidable ! ce qui fait que votre notion de décidabilité ne présente aucun intérêt .

Il ne suffit pas de jeter des axiomes au hasard pour faire une théorie intéressante.

[Schrodies-cat]

Diable ! Je viens de m'apercevoir que j'en était à 666 messages !
J'en reposte un immédiatement !

[Schrodies-cat]

Je referme la porte que j'avais à peine entr'ouverte:
Dans un cadre intuitionniste, si P est démontrable et Q indécidable, alors (P ou Q) est démontrable .

Quant à la définition de l'indécidabilité en intuitionnisme, il faudrait peut-être plusieurs degrés d'indécidabilité.

[mike.p]

Hum, hum cela commence mal ...
l'usage du signe = me fait un peu tiquer mais passons ....

je peux utiliser "=", la décidabilité étant une fonction ( binaire ). "et" et "ou" sont des opérations sur des bits.

si on remplace dans votre axiome ou schéma d'axiomes Q par (non P).
...
Il ne suffit pas de jeter des axiomes au hasard pour faire une théorie intéressante.

c'est votre théorie là ...

Pour ma part j'ai essayé d'inférer à partir du message auquel je réponds en utilisant 3 suppositions d'ignorant et en demandant si elles ne sont pas inutiles ou au contraire explicitement fausses. Sauriez vous une réponse ?

J'ai un soupçon sur la véracité de :

et que la notation suivante est valide
décidabilité(théo(P)) = décidabilité(P)

En fait, je ne sais plus 1) si on suppose que l'indécidabilité peut dans certains cas être démontrée ou si c'est toujours l'incapacité de montrer la décidabilité, 2) si on suppose qu'il existe un algorithme universel pour la décidabilité ( sans lequel on ne peut inférer sur la décidabilité du code de la décidabilité de A ) ...

[Schrodies-cat]

(...)
c'est votre théorie là ...
(...)

Je n'ai pas émis de théorie personnelle, simplement réfuté la Vôtre.
En conséquence ...

[mike.p]

Je n'ai pas émis de théorie personnelle, simplement réfuté la Vôtre.
En conséquence ...

je ne suis pas convaincu qu'il y ait eu quoi que ce soit à réfuter ou non ... Mais si ça vous fait plaisir, n'en parlons plus.