Et donc tout ceci étant dit, pour vous répondre, à présent, je ne connais pas de théories ou de systèmes qui soit construit sur une sémantique spécifique au but de pouvoir formaliser l'indécidabilité de l'indécidabilité d'une formule F, afin de pouvoir en tirer des résultats formels.
Dernière modification par invite7863222222222 ; 26/07/2013 à 09h04.
Non, je n'ai aucune idée derrière la tête mais si on trouve une axiomatique quelconque où la réponse est OUI alors on pourra se tourner vers les théories classiques. Cela dit, je vois mal comment encoder dec(F) sans l'arithmétique, donc à mon avis c'est au moins dans Peano qu'on peut s'interroger.
C'est la formalisation de dec(F) qui importe il me semble.
ensuite, je n'ai pas répondu à votre remarque sur ma proposition sur la théorie des groupes, j'essaie :
Ainsi que Médiat le remarquait, il ne faut pas confondre la décidabilité logique et la decidabilité algorithmique :
Je pense qu'une formule F est logiquement décidable lorsqu'on a prouvé que F ou non F est dépendante de T, c'est à dire lorsque F est prouvable ou non F est prouvable dans T.
F est décidable algorithmiquement lorsqu'il existe un processus de décision de F (vraie ou fausse) qui termine dans le temps (machine de Turing qui s'arrête par exemple).
Je ne trouve pas, certes, dans la littérature, de théorème reliant ces deux notions (n'est-ce pas l'idée de la thèse de Church ?)
pour répondre à votre remarque : je suis d'accord, c'est bien dec(F) qui est décidable.
En revanche si il y a coïncidence entre les deux notions de décidabilité alors on rejoint ce que je dis : il y aurait un processus mécanique qui termine et qui dirait pour toute formule F si dec(F) est vraie ou pas, donc les ensembles des énoncés décidables et les énoncés indécidables seraient récursivement énumérables et donc récursifs, ce qui est contradictoire avec la théorie des groupes.
Si il n'y a pas coïncidence : quel contre exemple avons-nous svp ?
Je ne reviens sur le pc que ce soir ou demain,
merci,
à bientôt
S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une
La décidabilité de F n'a pas besoin de s'encoder pour se mettre en évidence (c.f. la commutativité dans la théorie des groupes est indécidable, nul besoin de l'encoder).Envoyé par ilelogique
Donc, le choix des théories qui encodent dec(F), n'est pas un choix qui s'impose.
Si ce choix est fait, je ne le comprends que par le fait que ces théories sont courantes.
Encore une fois, je pense que la formulation la plus correcte -- "et qui porte le moins d'interprétation sur vos propos" (même si je pense voir où nous mène votre question, je préfère que vous laissez la responsabilité de la formulation car il s'agit d'un domaine que je ne maitrise pas bien) -- la plus précise de votre question, est : existe-il un système construisant une sémantique spécifique au but de pouvoir formaliser l'indécidabilité de l'indécidabilité d'une formule F ?
Dernière modification par invite7863222222222 ; 26/07/2013 à 09h50.
Bonjour,
Concernant l'axiome de commutativité exprimé dans le langage de la théorie des groupes on peut lire : http://forums.futura-sciences.com/ma...ml#post1967634
Patrick
Jamais dit cela, moi.si la réponse est négative quelque soit l'axiomatique choisie (ce que semblent croire Médiat et ù100fil)
Par curiosité comment encodez-une formule dans la théorie des groupes ?
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Hé bien, "on sait/on ne sait pas" est orthogonal a "la machine s'arrête/ne s'arrête pas". Si la machine peut s'arrêter, la proposition est décidable qu'on le sache ou non. Si la machine ne peut s'arrêter, la proposition est indécidable qu'on le sache ou non.
Dans les premières pages
(ainsi que possiblement un ou deux message de Patrick)
Attention, ici tu sembles considérer que l’indécidabilité est une propriété des formules indépendamment des théories. Les indécidabilités dont tu parles ont elles étés prouvées à l'intérieur des théories pour lesquelles elles sont indécidables?
D'accord en gros, je suis du coté ilelogique, et vous du coté de Médiat et de Patrick.(ainsi que possiblement un ou deux message de Patrick)
Vous vous êtes de ceux qui ont raison, et moi, du coté de celui qui n'ont pas tout compris...
Merci mais gardez vos tendances de condamnations agressives (surement acquises à une autre époque...) et gratuites pour vous.
Dernière modification par invite7863222222222 ; 26/07/2013 à 15h10.
jreeman, je sais que c'est toujours difficile à évaluer par écrit, mais je n'ai attaqué personne sur ce fil et ce n'est pas du tout mon état d'esprit en ce moment. Je pars en vacance demain, il fait chaud, on est bien. Je me trompe sur Dec(F)? Très possible. Prenons une petite vodka et on en discute, ok?
Ceci étant dit.
Je vous suggère de ne dissimuler sous le tapis ou de découvrir ce message :
Pas de problèmes.
Peu importe en fait, c'est juste qu'il y a aussi un autre point de vue ici, qui n'a pas forcément été entendu.Je me trompe sur Dec(F)?
Donc je m'excuse pour mon emportement.
Dernière modification par invite7863222222222 ; 26/07/2013 à 15h29.
Tout ça me fait penser aux poupées russes. Si j'ouvre une poupée russe, est-ce que la suivante peut aussi être ouverte ? Si je n'essaie pas d'ouvrir une poupée russe, puis-je démontrer que son ouverture est indécidable ? Est-ce que je peux démontrer qu'on ne peut pas savoir si la n-ième poupée russe peut être ouverte ? Existe-t-il un n tel que l'ouverture de la n-ième poupée russe est indémontrable ?
Pardon, humilité, humour, hasard, tolérance, partage, curiosité et diversité => liberté et sérénité.
Restez-vous toujours dans ce cadre : logique du premier ordre tel que vous l'avez mentionné ou sortez vous maintenant de ce cadre ?
Patrick
On va attendre sa réponse, de que j'ai compris, la question d'ilelogique n'est pas forcément lié à une logique particulière, et est générale à l'indécidabilité.
Pourquoi concernant certaines conjectures on ne peut pas démontrer si elle sont décidable ou indécidable car on n'a pas trouvé la démonstration ? Vous semblez en déduire la démonstration que l'on se sera jamais le démontrer ? Si une formule est indépendante d'une théorie exprimée dans le langage de la logique d'une premier ordre elle peut être autre chose que indécidable ?
Patrick
Est-ce à moi que tu parlais? Je ne vois pas de contradiction: dire que "Dec(F) est indécidable dans T pour tout F indécidable dans T" implique nécessairement "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 vous suggère de ne dissimuler sous le tapis ou de découvrir ce message :
Par contre il est vrai que Médiat semble se contredire entre son message #35 et son message #95, mais j'imagine qu'il est assez grand pour s'expliquer tout seul.
Pourrais-tu exprimer ce point de vue de façon la plus claire et la plus simple possible, comme si tu parlais à un enfant de 5 ans?
Exemple:
"Pour un F indécidable dans T, Dec(F) peut être décidable dans T."
"Pour un F indécidable dans T, Dec(F) ne peut être décidable dans T."
Pas la peine d'attendre. Exemple:
"Pour tout F dans T avec T une théorie appartenant à une logique du premier ordre, alors (...). Par contre si T est une logique d'ordre (...), alors (...)".
(même question pour Patrick)
mmm je viens d'essayer avec un de 7 ans, la réponse est "Quoi?"
Au fait c'est une tentative de "démonstration par l'absurde" pour répondre à votre demande de démonstration.
Patrick
C'est surement un lapsus à force de lire ce fil
Patrick
Je comprends pas. Désolé.
Aucun intérêt c'est parti sur des mauvaises bases, il vaut mieux reprendre calmement.Pourrais-tu exprimer ce point de vue de façon la plus claire et la plus simple possible, comme si tu parlais à un enfant de 5 ans?
Par respect, que vous n'avez manifestement pas pour vos interlocuteurs, je préfère attendre la réponse d'ilelogique.Pas la peine d'attendre. Exemple:
"Pour tout F dans T avec T une théorie appartenant à une logique du premier ordre, alors (...). Par contre si T est une logique d'ordre (...), alors (...)".
Si son avis, ne vous intéresse pas ou si vous n'êtes qu'un "clone" d'ilelogique, je ne vois pas de but à votre message.
Dernière modification par invite7863222222222 ; 26/07/2013 à 18h49.
Bonjour
Je ne vois pas de contradiction, dans le message 35 je dis que, si une théorie ne démontre pas que dec(F) est décidable, cela ne dit rien sur la décidabilité proprement dite. Dans le message 95 je réfute avoir dit que la réponse soit la même pour toutes les théories.
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Je suis comme toi. C'est un domaine très difficile à appréhender qui nécessite beaucoup de pratique. Nous avons vite fait de faire des sophismes dans un semblant de formalisation sans même nous en rendre compte. C'est je que je cherche à dire à ilelogique qui semble campé sur ses positions.
Patrick
Correctif lexical.
Patrick
C'est ce que j'ai compris du message 95 effectivement. Pourrais-tu produire une réponse directe telle que "A mon avis, la réponse n'est pas la même pour toutes les théories"? Ce n'est pas tout-à-fait la même chose que de réfuter avoir dit le contraire, et cela répondrait à la question de idelogique (une démonstration serait un plus...).
Ce n'est pas ce que tu as dis dans le message 35. Après réflexion je suppose que tu veux dire en fait "Pour comprendre mon message #35 (...)"
(...) alors il faut savoir que, si une théorie ne démontre pas que dec(F) est décidable, cela ne dit rien sur la décidabilité proprement dite."
C'est bien cela? Je ne comprend pas cette dernière affirmation. Si dec(F) est décidable dans une théorie T, alors nécessairement il en existe une démonstration. Si une théorie T ne peut démontrer que dec(F) est décidable, alors nécessairement dec(F) est indécidable pour cette théorie. Non?
Je veux bien miser 3 haribos qu'ilelogique considérerait une réponse directe à sa question, quitte à ce que tu précises en quoi le degré de la logique change la réponse, comme plus respectueuse que 8 pages sans fournir de manière claire son opinion (ou son absence d'opinion).
Pas de problème, et je suis assez convaincu que ton message passe mieux par ce type de réponse directe que par une démarche "Socratique" qui pourrait apparaître comme de mauvaise foi aux yeux non habitués à ta maïeutique.
Dernière modification par Jiav ; 26/07/2013 à 22h06. Motif: (directe)
Ma compréhension si on est bien dans ce cadre de la logique classique :
Est que quelque soit l'énoncé/proposition/formule à condition qu'il soit formalisé dans le langage d'une théorie T alors on utilise le théorème de complétude pour parler de décidabilité/indécidabilité d'un énoncé dans le cadre de la théorie T :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. Un énoncé mathématique est donc indécidable dans une théorie s'il est impossible de le déduire, ou de déduire sa négation, à partir des axiomes de cette théorie. Pour distinguer cette notion d'indécidabilité de la notion d'indécidabilité algorithmique (voir ci-dessous), on dit aussi que l'énoncé est indépendant du système d'axiomes.
En logique classique, d'après le théorème de complétude, une proposition est indécidable dans une théorie s'il existe des modèles de la théorie où la proposition est fausse et des modèles où elle est vraie. On utilise souvent des modèles, pour montrer qu'un énoncé est indépendant d'un système d'axiomes (dans ce cadre on préfère employer indépendant plutôt qu'indécidable).
La réciproque du théorème de complétude est appelée théorème de fiabilité (en) (ou d'adéquation) Dixi wiki.https://fr.wikipedia.org/wiki/Th%C3%...ompl%C3%A9tude
Il affirme que si un énoncé est universellement valide, vrai dans toutes les structures où il peut être interprété, alors il peut être démontré. Plus généralement le théorème de complétude énonce que si un énoncé est conséquence sémantique d'une théorie, c'est-à-dire vérifié dans tous les modèles de cette théorie, alors cet énoncé est conséquence syntaxique de cette théorie, il peut être démontré à partir des axiomes de cette théorie en utilisant les règles d'un système de déduction comme la déduction naturelle, le calcul des séquents ou un système à la Hilbert.
Patrick
Sauf qu''en mathématiques, un avis n'à aucune valeur.
Ceci est manifestement faux (la théorie des groupes ne démontre pas que dec(commutativité ) est décidable et pourtant elle l'est.Si une théorie T ne peut démontrer que dec(F) est décidable, alors nécessairement dec(F) est indécidable pour cette théorie. Non?
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Pour cela arrivé au 116 ieme message il faudrait travailler sur un exemple pratique en le formalisant tel que par exemple :Pas de problème, et je suis assez convaincu que ton message passe mieux par ce type de réponse directe que par une démarche "Socratique" qui pourrait apparaître comme de mauvaise foi aux yeux non habitués à ta maïeutique.
F :=vise à exprimer la commutativité dans le langage de la théorie des groupes (il faudrait préciser la signature)
Il ma semble que par inférence sur des règles logiques une théorie est défini comme un ensemble clos et de ce fait il ne peut y avoir de proposition indécidable dans une théorie. Ce qui n'interdit pas, ne contredit pas qu'il peut très bien exister des propositions indécidables pour cette théorie.
Dans le cadre de la "théorie des groupes" la commutativité y est indécidable.
Maintenant comment coder dans ce cadre l'expression dec(F) := "Décidabilité de F" ? Pour ensuite parler dans le cadre de la théorie de la décidabilité de dec(F).
C'est le mieux que je puisse faire pour initier cet exemple.
Patrick
Désolé mais je ne comprends pas
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Pourquoi parlez vous de "coder" ?
Tentative d'aide sans prétention (à ne pas lire pour ceux qui trouvent mes messages n'ont pas assez de respect) :
Cliquez pour afficher
Dernière modification par invite7863222222222 ; 27/07/2013 à 12h05.
Si la définition générale d'une théorie := "ensemble clos par inférence", les propositions appartenant à cet ensemble clos ne peuvent être indécidable non ?
il peut très bien exister des propositions indécidables pour cette théorie : exemple l'axiome de commutativité pour la "théorie des groupes".
C'est la compréhension que je m'en suis faite elle est peut être effectivement erroné.
Patrick
