indécidabilité de la décidabilité

[ilelogique]

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.
-----

[ansset]

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.

moi j'en pense que ça sent bon la verdure.
Cdt

[ilelogique]

Ah bon ?
Et pouvez-vous me dire où ça ne va pas alors svp merci ?

[ansset]

je ne suis pas spécialiste de ces questions, mais deux points me sautent aux yeux.
une analogie ( même plus ) entre la notion de "décidabilité" logique (Godel ) et celle algorithmique (Turing ).
tu sembles prendre la seconde pour "retourner" la première.

sur le second point je suis moins sur, mais je pense que mettre Dec(A) ( en reprenant tes termes ) dans E , est un abus de logique. ( celle mathématique ).
d'où ton laius sur la récursivité, qui semble prendre appui sur la logique algorithmique pour faire dire à la logique mathématique ce qu'elle ne dit pas.

en attendant un logicien....
afin qu'il me corrige ou me complète.
Cdt

[A voir en vidéo sur Futura]

[ilelogique]

Bonjour,
la coïncidence entre les deux décidabilité j'en ai parlé plus haut
Sinon un "abus de logique" dont vous parlez je ne sais pas ce que c'est. En revanche dec(A) est un prédicat, il a donc vocation à aller dans E il me semble.
Aussi : le laïus sur la récursivité me parait logique, rien de mal là dedans : si dec(A) est indécidable on peut bien concevoir de faire le même raisonnement sur des formules du type dec(nondec(B)) je ne vois pas ce qui vous chiffonne.
Enfin, c'est quoi la verdure svp ?
merci.

[ansset]

un prédicat n'est pas un énoncé décidable.
la verdure se mange ou parfois est utilisée en infusion , voir se fume aussi.

[ilelogique]

dec(A) est un énoncé, il peut donc être décidable ou pas
je n'ai pas fumé...

[Deedee81]

Salut,

je n'ai pas fumé...

Inutile de le préciser. C'était du second degré

[ilelogique]

J'espère qu'un logicien va répondre car je voudrais bien être sûr de ma preuve
merci

[Matmat]

D'accord mais c'est un peu donner le bâton pour se faire battre d'utiliser " la coïncidence entre les décidabilités aux sens de Gödel et de Turing " alors qu'un argument diagonal doit faire l'affaire.

[gandhalf.legris]

J'espère qu'un logicien va répondre car je voudrais bien être sûr de ma preuve
merci

bonjour ,
j'apprécie beaucoup votre pseudo mais je trouve qu'un e est en trop
c'est comme si je demandais pouvez vous dire qu'un état d'un objet est vrai tout en étant faux sans utiliser la physique quantique ( superposition d'état à écarter ... ) .
certains répondraient , tu veux quelle couleur pour les matelas ...

[illusionoflogic]

C'est pour moi la différence entre arithmétique et algèbre ; l'un à donner l'algorithme et l'autre la logique. (je précise que ce sont des domaines fils, des ramifications).

[ilelogique]

je ne vois pas quel argument diagonal peut venir remplacer l'appel à cette coïncidence,
aussi première question :
- en supposant cette coïncidence ma preuve est-elle correcte ?
- Quid de cette coïncidence ?

[ilelogique]

Re bonjour,
je réponds d'abord à vos assertions qui, selon moi, ne sont pas en lien avec mon sujet :
- L'île logique est le nom de ma compagnie de théâtre burlesque et sciences théoriques, c'est bien sûr un jeu de mot, si bien que le "e" est indispensable.
- pour la couleur des matelas et le vrai et faux quantique ou pas dont vous parlez : no comment, aucun lien avec ma question (ou tout du moins non argumenté)
- Pour arithmétique et algèbre, notons que la construction de celles-ci, depuis au moins le XXe siècle, reposent toutes sur la logique, algorithmique comprise, et encore une fois, je ne vois pas le lien avec ma question.

Aussi, s'il vous plaît, si vous souhaitez commenter ce que je viens de dire et/ou dire à nouveau des choses hors sujet, merci d'ouvrir une autre discussion (à laquelle je me ferai un plaisir de me joindre !)

Et donc, revenons à mes moutons svp, je remets ici ma double question, je suis ici pour une question de logique :

1) peut-on raisonnablement supposer l'équivalence entre la décidabilité au sens de Gödel et celle au sens de Turing ? Et surtout : si non, quel argument logique l'infirme ?
2) Et c'est le but PRINCIPAL de ma question : en admettant l'équivalence entre les deux décidabilités, la démonstration suivante du fait qu'il existe des énoncés dont la décidabilité n'est pas décidable vous paraît-elle bonne ? Et si non : quel argument avancez-vous ?

Merci.

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…

[ilelogique]

j'oubliais, évidemment : je suis tout à fait preneur d'un autre argument dans ma preuve qui, du coup, éviterait de faire appel à cette "coïncidence" qui, semble-t-il, ne fait pas consensus....
merci

[ansset]

bjr, j'ai lu plusieurs articles sur les différences entre la décidabilité mathématique/algorithmique.
en première lecture, j'ai l'impression que l'une s'intéresse aux énoncés et l'autre à la prise décision et à la théorie elle-même.
la notion "d'arret" par exemple existe dans le second cas , pas dans le premier.
en tout cas, tous s'accordent à distinguer les deux.
je suis loin d'être assez informé pour avoir un avis argumenté, mais une démo partant d'un principe d'équivalence me semble douteux.

[Schrodies-cat]

Il y a me semble-t-il une confusion.
On peut définir, disons en arithmétique pour préciser les choses, la démontrabilité, et aussi, comme vous le faites, la décidabilité d'un énoncé.
Ce prédicat de décidabilité est il décidable ? (!!!), c'est à dire, si on se place dans le cadre de la théorie de Turing, existe-t-il un algorithme permettant de savoir à coup sur si un énoncé est décidable ou non ?
Il n'y a aucune raison de l' affirmer: en fait la réponse est non ! ce n'est pas parce que le terme décidabilité contient le mot décidable qu'on pourrait en déduire la décidabilité de la décidabilité !

[ilelogique]

Merci, donc :
1) en admettant cette coïncidence ma preuve vous semble-t-elle correcte ?

2) Pour la coïncidence, le théorème de complétude de Gödel affirme qu'un énoncé P qui est décidable dans une théorie T (donc vrai dans un modèle de T) si et seulement si il existe une suite finie d'énoncées partants de T qui, dans un système de déduction, prouve P (P est démontrable dans T) : or la correspondance de Curry-Howard ne permet-elle pas alors d'établir une correspondance bi-univoque entre les deux décidabilités ?

[c.bien.moi]

Bonsoir,

C'est dommage que tes questions soient restées sans réponse, pourtant il me semble qu'il y a des logiciens qui fréquentent ce forum...

En même temps ta question est peut-être une question qui est encore sans réponse, je pense en particulier aux liens entre indécidabilité logique et calculatoire, il me semble improbable qu'aucun logicien n'ait réfléchie à cette question, il donc fort probable que tu t'appuis sur une conjecture qui reste à démontrer ou à infirmer.

Bonne soirée.

[ilelogique]

Bonjour,
je suis bien d'accord que c'est dommage qu'aucun logicien ne vienne répondre à mes questions, quand bien même serait-ce pour dire ici qu'ils n'ont pas les réponses.
mais bon, ça viendra peut-être ?
Merci.

[Matmat]

Tout ce que vous demandez c'est est ce qu'on peut faire la démonstration d'un résultat connu et déjà démontré en partant d'une hypothèse qu'on peut contester . Si la démonstration est correcte mais l'hypothèse contestable , il n'y a pas besoin de logicien .. Tout repose sur l'admission ou pas de l'hypothèse contestable .

[ilelogique]

Bonjour,
si le résultat est connu et démontré en avez-vous une preuve logique svp ? Car je ne trouve rien là dessus (sur l'existence d'énoncés dont la décidabilité n'est pas décidable)
Ensuite je suis d'accord que l'hypothèse que je prends doit être discutée (c'est pourquoi je fais appel au théorème de complétude puis à la correspondance de Cury-howard), pensez-vous par exemple qu'il serait judicieux que j'ouvre une nouvelle discussion à cet égard ?
Enfin on peut aussi, il me semble, admettre temporairement cette hypothèse et voir si, en ce cas, ma preuve est valide ou non (c'est d'ailleurs ce que fait souvent la logique : on démontre des choses sous certaines hypothèses...) donc je veux bien savoir si ma preuve est correcte dès lors qu'on admet cette hypothèse (qui par ailleurs certes doit être discutée)
Il me semble que tout mon propos ici fait bien appel à des logiciens car, et je ne vous cache pas que je m'en navre, depuis 2 pages d'échanges nous n'avons pour ainsi dire pas encore parlé de logique !!
Merci.

[Matmat]

je ne trouve rien là dessus (sur l'existence d'énoncés dont la décidabilité n'est pas décidable).

Mais plus haut on vous a cité le "problème de l’Arrêt" pourtant.

[Schrodies-cat]

Il est vrai que j'ai répondu de façon peu formelle, préférant vous laisser réfléchir.
Notons qu'une preuve faisant appel à une coïncidence n'en est pas une.
Je précise la confusion que vous avez faite:
"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"
Le fait qu'une affirmation soit codable sous la forme d'un prédicat n'implique pas qu'elle soit codable sous la forme d'un algorithme terminant à coup sur. C'est précisément le principal enseignement des travaux de Gödel et Turing.
Que vous faut-il de plus ?
Je ne voulais pas vous aider plus qu'il ne me paraissait nécessaire et ai donc laissé un flou sur le terme "décidable" (je suis un peu comédien parfois).
Je n'entrerait pas dans les détails mais je donnerai les indications suivantes:
Décidable au sens de Gödel s'applique à des énoncés mathématique.
La théorie de Gödel permet de construire des énoncés indécidables particuliers dans toute théorie mathématique consistante contenant l'arithmétique.
Décidable au sens de Turing s'applique à des familles d'énoncés, par exemple du type la machine de Turing M s’arrête au bout d'un temps fini quand on la fait travailler sur la donnée n.
La théorie de Turing permet de construire des familles d'énoncés dans lesquels on trouve une infinité d'indécidables, quelque soit la théorie permettant de définir la calculabilité dans laquelle on se place, par exemple en prenant pour M une machine universelle dans l'exemple ci-dessus.

[Schrodies-cat]

Bien sur, il fallait entendre théorie mathématique définie par un ensemble récursif d'axiomes ...
Bref ce qu'on entend habituellement par théorie mathématique, dans laquelle la notion de démonstration est des plus claires.

[ilelogique]

Matmat : je ne vois pas le rapport entre le problème de l'arrêt et le fait qu'il existe des énoncés dont la décidabilité n'est pas décidable.
Schrodies-cat : je prétends que la formule Dec(A) est codable au sens de Gödel ici. je ne vois pas de quelle confusion vous parlez, entre quoi et quoi ?

[Schrodies-cat]

Je voulais illustrer les deux notions d'indécidabilité .Le théorème dont vous parlez est un autre théorème.
En fait, pour vous donner une idée de sa démonstration, si la décidabilité était décidable, on pourrait construire une théorie complète, non contradictoire et à l'axiomatique récursive par l'algorithme suivant: en énumérant les énoncés de cette théorie, en testant un par un si ces énoncés sont décidables, et en ajoutant au fur et à mesure comme axiome chaque énoncé indécidable pour poursuivre.

Votre confusion, je l'ai pointée précisément est sur "coder", ce n'est pas la même chose de coder comme prédicat et de coder comme algorithme.

[ilelogique]

De ce que je comprends de votre proposition c'est que vous ajoutez mon ensemble G à AP dans ma preuve, mais G n'est pas récursivement énumérable (sinon l'ensemble des énoncés décidables E serait récursif)
Ensuite je ne vois pas trop où je confonds les codages, je parle de codages au sens de Gödel et ensuite (on y revient encore) j'admets que la décidabilité au sens de Gödel implique celle au sens de turing et je déduis l'existence de la machine de turing qui s'arrête pour toute formule A sur la décision de dec(A), les deux codages sont donc distincts non ?

[Schrodies-cat]

Oui, bon, je n'ai peut être pas lu avec suffisamment de soin votre lancement de ce sujet. Il semble que nous soyons assez d'accord sur ce que vous avez proposé, dont j'aurais en fait proposé dans mon dernier message une démonstration alternative, et peut être mieux formalisable.
Il est vrai que pour ce genre de chose, il serait en principe nécessaire d'utiliser un formalisme rigoureux, mais cela rend souvent la compréhension laborieuse.
J'enfoncerais cependant mon clou en répétant que habituellement, la décidabilité au sens de Gödel porte sur des énoncés particuliers et la décidabilité au sens de Turing porte sur des familles d'énoncés (on rencontre cela aussi dans la notion de "théorie décidable en logique mathématique".
L'indécidabilité de Gödel est relative à une théorie donnée ; un énoncé pet être indécidable dans un théorie particulière mais décidable dans une théorie plus puissante (dans laquelle il restera bien entendu d'autres indécidables).
Dans une famille d'énoncés indécidable au sens de Turing, quelle que soit la théorie (raisonnable) dans laquelle on se place, il restera des indécidables.
On ne peut donc identifier les notions d'indécidables aux sens de Gödel et de Turing, même si ces deux notions sont profondément liées.

[ilelogique]

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.