Pour éviter justement de parler dans le vide et confondre la notion de groupe qui est un modelé de cette theorie des groupes avec la théorie des groupes.Envoyé par jreeman
Ce qui permet d'enlever les sens ambigus artifice d'un discours dans le langage naturel.
Patrick
C'est exact ; j'aurais mieux compris si dans la deuxième partie de votre phrase vous aviez parlé de formule du langage n'appartenant pas à la théorie.
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
D'accord, alors, ca veut dire que j'ai essayé de coder de votre formule pour éviter les ambiguités du langage naturel.
Dernière modification par invite7863222222222 ; 27/07/2013 à 14h30.
Voila qui est manifestement faux, ou tautologiquement sans valeur.
Dec(communatitativit) est indemontrable dans la theorie des groupe, mais est decidable dans la theorie des groupes. Ah bon.
Merci. Je m'arrete la pour les vacances. A+
Bonjour,
de la Dordogne aux Pyrénées, à Arcachon également en vacances, je suis ok pour boire un verre ensemble, bienvenue en Bretagne...
C'est vrai que je pensais qu'on répondrait rapidement oui, non ou je ne sais pas à ma question, loin de moi l'idée qu'il faudrait toutes ces pages.
Or force est de constater que si celles-ci sont là c'est que quelque part ma question est mal posée, je m'exprime mal, quelque chose doit m'échapper et je ne sais pas encore quoi...
Au départ je me suis juste demandé s'il il existait des propositions dont la décidabilité n'est pas décidable.
Puis il a fallu préciser ce que j'entends par là...
Quelques remarques préliminaires :
a) J'ai fait mes études avec l'équipe de logique de Jussieu et le vocabulaire que j'utilise est donc le leur, particulièrement le livre en deux tomes de Cori et Lascar, mais il me semble qu'il n'est pas loin de celui qu'on retrouve sous wikipédia.
b) On m'a plusieurs fois demandé ici de "formaliser" ma question. Personnellement j'emploie plutôt le mot "formaliser" dans un sens proche de "écrire la question dans le langage du premier ordre", si bien que je n'en vois pas l'intérêt. Il me semble en effet qu'il n'est pas forcément nécessaire ni même toujours possible d'écrire l'énoncé des théorèmes de logique dans le langage considéré. ça commencerait à être particulièrement tordu si il fallait que la question que je pose soit elle même un énoncé du premier ordre...
c) Ainsi que je l'ai dit, je cherche à savoir si il existe ou non un énoncé dont la décidabilité ne serait pas décidable, aussi si quelqu'un exhibe n'importe quel langage, même du second ordre, une théorie farfelue et un tel énoncé ça répondrait à ma question. Cependant je vais tâcher ici d'être le plus près possible des théories standards.
Des hypothèses...
1) Une formule close F du premier ordre sera dite logiquement décidable dans une théorie T si F ou bien sa négation sont conséquences syntaxique de T, c'est à dire que F ou nonF sont démontrables à partir de T (et pas les deux bien sûr), c'est à dire qu'il existe une suite finie de formules déduites les unes des autres grâce aux règles de déductions et à partir des axiomes de T. On pourra aussi dire que F est dépendante de T. Dans le cas contraire, on dira que F est indécidable (ou indépendante). Une formule close F sera dite décidable algorithmiquement à partir de T si il existe une machine de Turing qui s'arrête en disant si F est vraie ou fausse dans T.
2) Soit L un langage et T une théorie contenant l'arithmétique. Sachant que Gödel a codé les formules du premier ordre avec les entiers avant d'utiliser son argument diagonal, je suppose qu'il est possible d'écrire dans L une formule Dec(F) exprimant la décidabilité logique de F dans T : en passant par un codage ad'hoc des règles de déduction, Dec(F) serait donc une formule close exprimant l'existence d'une suite finie de formules déduites les unes des autres à partir de T et par le biais des règles de déduction.
Une question préalable :
Si il me semble que la décidabilité au sens de Turing implique celle au sens de Gödel, la réciproque n'est pas certaine : si on sait qu'il existe une preuve de F ou de nonF à partir de T, cela implique-t-il qu'il existe un algorithme, une machine de Turing, qui décide de F en un temps fini, qui dit si F est vraie ou fausse dans T ??
Par exemple on sait que la conjecture de Riemann est logiquement décidable, il existe une preuve qui la valide ou la réfute ; peut-on en déduire qu'il existe une machine de Turing qui s'arrête en disant si elle est vraie ou fausse ?
Une proposition :
L'arithmétique, et donc T, est indécidable : l'ensemble E des énoncés décidables de T est récursivement énumérable mais non récursif. Il n'y a pas d'algorithme qui s'arrête à coup sûr à la donnée d'une formule F pour dire si elle est décidable ou pas, on a juste qu'un tel algorithme s'arrête seulement si F est décidable.
Si il y a coïncidence entre les deux décidabilités on aurait alors qu'il existe F telle que Dec(F) est indécidable. Car si tel n'était pas le cas alors Dec(F) serait logiquement décidable pour toute formule F et donc : pour toute formule F on pourrait dire si Dec(F) est vraie ou fausse avec une machine de Turing qui s'arrête si bien que le complément de E serait récursivement énumérable lui aussi et donc E serait récursif, l'arithmétique serait décidable.
Donc :
J'ai l'impression que : si Dec(F) peut s'écrire dans L et que les deux notions de décidabilité coïncident, alors la réponse à ma question est OUI.
A moins de me tromper encore et d'oublier un truc, je pense donc que ces deux hypothèses sont à étudier.
- La question de la possibilité de formaliser Dec(F) : j'y crois et ne me sens pas capable de le faire. Cependant si c'est possible, alors Dec(Dec(F)) est possible aussi, etc. N'y a-t-il pas un problème qui fait que c'est impossible ???
- Si les deux notions de décidabilité ne coïncident pas : quelqu'un connait-il un énoncé F dans une théorie T tel qu'il existe une preuve de F mais qu'aucun algorithme ne termine en validant ou niant F ???
Et bien sûr, si ces deux questions ne sont pas vraies, ça ne résout pas pour autant la question de départ !
Enfin, sur l'argument qui a été apporté ici : le fait que nécessairement une machine de Turing s'arrête ou pas, même si on ne le sait pas toujours.
Dans ce cas ça aurait pour conséquence que la décidabilité de toute formule est décidable et que la réponse à ma question est NON (ce qui m'arrangerait bien, soit dit en passant). Et donc ou bien Dec(F) n'existe pas ou bien dec(F) est décidable pour toute formule F et les décidabilités logiques et algorithmiques ne coïncident pas (sinon l'arithmétique serait décidable).
Je vois cet argument comme une sorte de méta-tiers exclu. Mais même si je le trouve intéressant, je ne parviens pas encore à me convaincre...
Pourquoi serait-il évident que tout énoncé soit décidable ou indécidable ? Un peu comme si on disait que Dieu existe ou n'existe pas...
Ne se peut-il pas, du fait qu'on sait qu'on ne peut pas le prouver (tant que la machine de Turing n'est pas arrêtée on ne sait pas si elle s'arrête ou non) qu'il y ait une tierce possibilité : celle que la décidabilité ne soit elle même pas décidable ???
S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une
En mathématiques on donne des démonstrations, pas des avis !
La formule dec(commutativité) ne peut même pas se formaliser dans le langage des groupes, par contre on connaît des modèles qui montrent que la commutativité est indécidable.Dec(communatitativit) est indemontrable dans la theorie des groupe, mais est decidable dans la theorie des groupes. Ah bon.
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Une formule F est indécidable dans une théorie T, si T ne démontre ni F ni non F.
Si on a montré l'indécidabilité et si cette indécidabilité devient une formule G. Si on a démontré l'indécidabilité de G, alors G n'est pas indécidable. Comme G = decidabilite(F), on a decidabilite(F) est décidable.
Si on veut sortir de ce schéma, il faut changer les concepts habituels que l'on a de théorie au sens classique, mais vous semblez vouloir vous y restreindre alors dans ce cas, on ne peut que vous répéter la phrase qu'il y a au dessus.
Correction
Si on reste dans la décidabilité logique d'un énoncé. Vous posez la condition que l'énoncé quel qu'il soit F, dec(F), dec(dec(F)) soit formalisable dans le langane L de la théorie T.
Dans ce cas cet énoncé appartient à l’ensemble clos par inférence (décidable) sur les axiomes de T ou n'appartient pas à cet ensemble clos par inférence (indécidable) non ?
Maintenant, pour tout énoncé exprimé dans le langage L d'une théorie fixé T que l'on ne puisse toujours trouver une démonstration pour son appartenance ou non à l'ensemble clos ne démontre pas qu'il peut y avoir indécidabilité de la décidabilité d'une formule close non ?
Patrick
Ce qu'a écrit Jean-Paul Delahaye
Simultanément aux recherches faites à propos du calcul, les logiciens découvrirent la notion d'énoncés indécidables, on précise parfois énoncés indécidables de Gödel, car c'est Gödel qui en 1931 démontra le premier théorème important à leur sujet.
Par définition ce sont des énoncés impossibles à démontrer ainsi que leurs négations. Mais cette notion est toujours relative à un système de démonstrations (ou système formel), et il ne faut pas la confondre avec celle de problèmes indécidables qui elle, est absolue.
Notre dernier paragraphe précisera les liens qu'entretiennent ces deux notions.
D'abord il faut bien voir qu'un problème indécidable est indécidable une fois pour toutes : l'indécidabilité d'un problème ne dépend pas d'un système de démonstrations particulier, l'indécidabilité d'un problème se réfère à la notion d'algorithme qui est unique, ce sur quoi tout le monde s'accorde.
Par contre un énoncé indécidable de Gödel est indécidable relativement à un système de démonstrations donné.
L'indécidabilité d'un énoncé est relative, et aucun indécidable de Gödel n'est absolu (c'est-à-dire indécidable dans tout système de démonstrations).
A l'indécidabilité de l'arrêt des machine de Turing correspond une infinité d'énoncés, celui disant par exemple que la machine numéro 1 s'arrête, celui disant par exemple que la machine numéro 2 ne s'arrête pas etc.
Par contre un indécidable de Gödel est un énoncé unique.
Ceci étant bien précisé, le rapport entre les problèmes indécidables et les énoncés indécidables de Gödel est assez simple :
si S est un système de démonstrations fixé. Et si P est un problème indécidable alors parmi tous les énoncés vrais correspondant au problème P il y en a un au moins qui est un indécidable de Gödel relativement à S.
Patrick
Bonjour,
deux choses
1) De façon semi-formelle : il me semble, vu que Gödel lui même l'a fait pour les formules, qu'on peut :
- Associer un entier distinct à chaque formule close et à chaque règle de déduction du système.
- Définir les prédicats : Ax(a) exprimant que a est le code d'un axiome, c'est à dire d'une formule de T et ded(a,b,c,d) exprimant que a est le code d'une règle de déduction R qui permet de déduire la formule dont le code est b depuis les deux formules dont les codes sont c et d (quitte à supposer que toutes les règles partent de deux formules pour en déduire une). On pourra alors créer le prédicat dem(a) exprimant que a est le code d'une formule close démontrable dans T (c'est à dire, par induction, qu'il existe x1...Xn qui sont les codes de formules de T ou bien de formules déjà déduites.
- Dec(F) serait sera une formule close exprimant "dem(a) ou dem(b)" avec a étant le code de F et b celui de nonF
il me parait donc normal de pouvoir exprimer cette formule dec(F) dans le langage L de T.
Si tel est le cas, alors (à moins que la réponse à ma question soit positive) Dec(F) serait décidable pour toute formule F ???
2) C'est l'histoire de la coïncidence entre décidabilité logique et décidabilité algorithmique : si, certes, on ne les définit pas pareil et qu'il semble que la seconde implique la première : décidabilité logique implique-t-elle décidabilité algorithmique ? Ou bien existe-t-il un énoncé dont on sache qu'il est décidable au sens de Gödel et qu'il n'y a pourtant pas d'algorithme finissant et permettant de le décider ?
La thèse de Chruch n'affirme-t-elle pas cette coïncidence ?
Merci.
S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une
Qu'on dise que dans ce système logique et dans telle théorie fixée une bonne fois pour toute, soit on peut démontrer, soit on ne peut pas démontrer une formule, ca fait partie du bon sens, il me semble.
Si on veut qu'il y ait une autre possibilité, ca veut dire, qu'on accepte que la théorie soit à frontière mouvante, c'est à dire soit qu'on accepte de rajouter des axiomes, soit carrément de passer à un autre système logique/théorie en définissant un lien avec l'ancien/ne.
Mais encore une fois, vous vous cantonnez toujours à un cadre classique à une discussion purement mathématique et c'est bien, mais ca me parait pas compatible avec le fond de votre question.
Dernière modification par invite7863222222222 ; 01/08/2013 à 10h49.
je ne comprends pas votre réponse :
personne ne semble trop, ici, nier que la formule Dec(F) puisse s'écrire dans le langage L de la théorie T contenant l'arithmétique (il faut coder les formules et les règles de déduction). Donc dec(F) est une formule close du langage comme les autres.
N'est-il pas légitime de s'interroger sur sa décidabilité ? Vous dites que dec(F) est toujours décidable ?
S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une
Je ne connais pas les détails, mais il faudrait s'assurer avant que que pour faire ce codage, ca ne nécessite pas de nouveaux symboles de langage. Je sais pas si vous êtes en mesure d'être certains sur ce point.
Mais alors, ca voudrait dire que coder la décidabilité de dec(F) devrait se faire en considérant ces nouveaux éléments.
Je ne sais pas bien ce que ca signifie, mais il me semble qu'on a pas besoin d'aller aussi loin que cela, dans une théorie et un langage fixés, convainquez vous peut-être plutôt qu'une formule est soit décidable ou pas.
Il me semble qu'on peut lister dans un tel contexte, sur papier toutes les démonstrations possibles e inimaginables. Et alors, soit la démonstration de F, y est, soit elle n'y est pas. Tout "simplement".
Dernière modification par invite7863222222222 ; 01/08/2013 à 12h07.
Au point ou nous en sommes pour sortir de cette impasse il me semble qu'il ne vous reste plus qu'a nous fournir une démonstration formelle qu'un énoncé exprimé dans le langage L d'une théorie T, peut être autre "chose" que décidable (appartient à l'ensemble clos par inférence) ou indécidable (n'appartient pas à l'ensemble clos par inférence) et ceci dans le langage L de la théorie T.
Patrick
Dernière modification par invite6754323456711 ; 01/08/2013 à 20h54.
Dit autrement, vous semblez penser que pour certain énoncé exprimé dans le langage L d'une théorie T nous pouvons démontrer, en restant dans le même cadre, qui ne sont ni décidable, ni indécidable. Et ceci sans être un problème de décidabilité algorithmique.
Patrick
Re,
C'est un peu agaçant : je ne parviens pas, comme vous, à citer les messages des autres...
vous dites :
"Je ne connais pas les détails, mais il faudrait s'assurer avant que que pour faire ce codage, ca ne nécessite pas de nouveaux symboles de langage. Je sais pas si vous êtes en mesure d'être certains sur ce point."
je suis bien d'accord mais je pense en effet que c'est possible...
Il me semble même que c'est là le nœud de ma question.
1) Si c'est possible de coder dec(F) dans le langage L, alors dec(F) devient une formule et il est légitime de s'interroger sur sa décidabilité (et si on suppose la coïncidence de la décidabilité logique et de la décidabilité algorithmique alors il existe une formule dont la décidabilité n'est pas décidable et la réponse à ma question est oui).
2) Si ce n'est pas possible, alors je conviens qu'on peut alors douter de la pertinence de ma question. On en arrive alors à : "convainquez vous peut-être plutôt qu'une formule est soit décidable ou pas."... je veux bien : mais comment cela ??
Enfin :
"Il me semble qu'on peut lister dans un tel contexte, sur papier toutes les démonstrations possibles e inimaginables. Et alors, soit la démonstration de F, y est, soit elle n'y est pas. Tout "simplement".
Il me semble que, vu que l'ensemble des énoncés décidables est déjà récursivement énumérable et non récursif, que l'ensemble des démonstrations sera lui aussi récursivement énumérable et non récursif (si bien que votre liste papier ne finira pas et, même si la preuve de F est ou non dans la liste, vous ne serez pour autant capable de le savoir !!)
S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une
Je ne vois pas pourquoi, il y a juste à cliquer sur "Répondre avec citation". Le message cité est alors dans la balise QUOTE dans la réponse.
Mais en tout cas, sommes nous bien d'accord ou pas que la condition nécessaire à votre entreprise, et que la codification de godel ne nécessite pas d'autres éléments de langage que celle de l'arithmétique ?"Je ne connais pas les détails, mais il faudrait s'assurer avant que que pour faire ce codage, ca ne nécessite pas de nouveaux symboles de langage. Je sais pas si vous êtes en mesure d'être certains sur ce point."
je suis bien d'accord mais je pense en effet que c'est possible...)
Il y a moyen d'être sûr de cela, c'est de "maîtriser" la démonstration de Gödel, non ?
Ce qui suivait dans mon message était une une proposition !je veux bien : mais comment cela ??
Je me suis peut-être trop avancé sur ce point.Il me semble que, vu que l'ensemble des énoncés décidables est déjà récursivement énumérable et non récursif
Toujours est-il que j'en reste à ma première impression qu'il faut nécessaire maîtriser la démonstration de l'indécidabilité de Gödel pour être tout simplement savoir si la décidabilité d'une formule F d'une théorie T nécessite ou pas d'autres éléments de langage que la théorie T.
Cliquez pour afficher
Dernière modification par invite7863222222222 ; 02/08/2013 à 12h26.
Cependant, je reviens sur cela :
Auriez vous une référence ?
Je dirai au contraire qu'on peut écrire un algorithme listant toutes les formules de longueur inférieure à n, cela forme un ensemble nécessairement fini.
Ainsi, on commence avec n=0, puis n= 1 etc. et on dénombre ainsi l'ensemble de toutes les formules de longueur finie.
Dernière modification par invite7863222222222 ; 02/08/2013 à 12h45.
J'essaye la citation mais :
1) Je dois me connecter avant
2) l'écran est alors tout petit (je ne vois que 5 lignes)
3) ça cite tout le message, il faut donc effacer le reste et recommencer si on veut re-citer.
4)On ne me propose plus de visualiser mon message avant de le poster !!
Bon, peu importe.
Oui, je pense que vous avez raison.
Cependant (selon mes souvenirs un peu éloignés de l'époque où j'ai lu et travaillé la preuve de Gödel...) il ne me semble pas que Gödel ait dû élargir le langage pour faire sa preuve, je crois bien qu'il fait ça dans le langage de l'arithmétique.
Ici, certes, il faut non seulement coder les formules mais aussi coder les preuves (donc coder les schémas d'inférence, c'est à dire les règles de déduction) puis les suites finies de formules déduites les unes des autres. Mais j'ai l'impression (rien de prouvé à ce jour) que ce codage est faisable sans élargir L (car les schémas de preuves sont dénombrables et qu'on peut utiliser la bijection de NxN vers N)
S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une
Pourtant rien que le signe "démontre que", n'existe pas dans l'arithmétique. La question est même en amont, quels sont ces éléments du langage nécessaire pour parler de décidabilité, peut-on formaliser cette "théorie", en est-elle vraiment une, d'ailleurs (n'est-ce pas plutôt un "système" ?) ? Cette "théorie" est-elle récursivement énumérable ?
Il me semble que le bon sens, par rapport à ces questions et de douter d'un sens possible à donner à la décidabilité de la décidabilité. Surtout qu'il me semble qu'il est possible de lister par un algorithme toutes les formules et démonstrations dans les théories dont il est en question, et donc qu'une formule possèdera forcément une démonstration ou pas. Donc que comme la démonstration soit y est, soit n'y est pas, une formule est définitivement soit décidable, soit indécidable.
Bonjour,
l'indécidabilité telle que formulée par Gödel doit se comprendre selon un certain point de vue ontologique des mathématiques, mais ne constitue pas une "preuve" en dehors de son domaine.
Cette notion ne s'applique pas au "réel", et donc aux phénomènes physiques tels qu'ils peuvent être connus d'un individu.
http://stl.recherche.univ-lille3.fr/...sou141101.html
Voir ce passage pour mieux en comprendre les fondements.
http://stl.recherche.univ-lille3.fr/...sou141101.html
En bon vivant, rien ne vaut un bonne logique ternaire.
1) normal mais c'est pas propre au fait de citer un message
2) je ne vois pas ce que vous voulez dire (appuyer sur CTRL + 0 peut-être, pour voir si ca résout votre problème ?). Peut-être que vous pourriez aller à cette section, pour expliquer ce problème et mettre une impression écran.
3) oui c'est normal, une solution un peu mieux serait de reprendre dans le message cité que ce qui est "sélectionné" avec la souris, mais c'est limité car avec la souris on ne peut pas selectionner plusieurs paragraphes.
4) oui il faut cliquer sur "Aller en mode avancé", après quoi vous pourrez prévisualiser le message.
Oui.
mais ce que vous dites suggère que la formule dec(F) ne peut pas exister. c'est à dire qu'on ne peut pas formaliser au premier ordre et dans l'arithmétique, le fait, pour une formule, d'être décidable.
Or je ne vois pas pourquoi on ne peut pas faire ce codage. Une preuve n'est qu'une suite finie de formules déduites les unes des autres par un ensemble dénombrable, voire fini, de règles.
Pour le signe "démontre que" on peut :
- ou bien l'ajouter au langage (et je pense qu'on peut le faire, dans la construction de formules, sans affecter l'arithmétique elle même)
- ou bien ajouter un symbole de relation : R (abcd) = a est le code d'une règle permettant de déduire la formule de code b à partir des formules codées par c et d)
- Si on ne veut pas enrichir le langage (quoi que je ne vois pas en quoi ça gène, le théorème d'incomplétude étant vrai dans tellement de théories) je ne suis même pas sûr que ce codage ne soit pas faisable.
Enfin, c'est sûr (et il y a peut-être moyen par là de prouver, par argument diagonal, que cette formule Dec(F) n'existe pas !!) : si dec(F) est une formule, alors dec(dec(F)) doit aussi en être une etc !
Pour les remarques de Xoxopixo : je ne vois pas le rapport avec le sujet.
S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une
Je n'ai jamais dit cela.
Dans le langage de l'arithmétique, ben non, je vous l'ai montré, c'est une évidence flagrante, il ne devrait même plus y avoir de questions sur le sujet.c'est à dire qu'on ne peut pas formaliser au premier ordre et dans l'arithmétique, le fait, pour une formule, d'être décidable.
Ca ne suffit pas 1 ne démontre pas 2, mais un ensemble de formule démontre une autre formule.Pour le signe "démontre que" on peut :
- ou bien l'ajouter au langage (et je pense qu'on peut le faire, dans la construction de formules, sans affecter l'arithmétique elle même)
Il faut aussi ajouter un nouvel ensemble de terme qui sont les formules de la théorie en question, non ?
Dans la nouvelle théorie, on a que 2 formules :
Soit F appartenant à l'ensemble des formules de T, alors T ne démontre pas F et T ne démontre pas non F.
Quelle autre formule voulez vous coder ?
Comme il est certain que la dec(F) ne s'exprime pas dans le langage de l'arithmétique, comme je vous le disais au début de ce message.Enfin, c'est sûr (et il y a peut-être moyen par là de prouver, par argument diagonal, que cette formule Dec(F) n'existe pas !!) : si dec(F) est une formule, alors dec(dec(F)) doit aussi en être une etc !
---
Vous n'avez pas réagi au fait qu'une formule est forcément soit décidable, soit indécidable.
Ca devrait clore le débat.
Sinon, pour le clore, voici ce que je vous propose :
définissez comme pour l'arithmétique, le langage, l'ensemble de terme de la théorie, les symboles de fonction, les symboles de relation, les axiomes de la théorie où se démontre la décidabilité.
Ensuite nous verrons bien, ce que ca donnera et si cela a un sens de parler de codage ?
Dernière modification par invite7863222222222 ; 02/08/2013 à 18h25.
Aussi juste pour dire, que par manque de temps, que je répondrais surement plus que si effectivement le travail qu'y auras été fait (s'il est fait), sur la formalisation précise de la théorie où se formalise la décidabilité, afin de voir si on peut en coder les formules comme pour les formules de l'arithmétique, me parait convainquant.
Dernière modification par invite7863222222222 ; 02/08/2013 à 18h44.
re,
Je n'ai pas dit que vous aviez dit ça mais que ça le suggérait : si toute formule est soit décidable soit indécidable dans une théorie alors dec(F) ne peut pas se formuler dans L (car sinon on aboutit à une contradiction ainsi que je crois l'avoir dit plus haut).
Enfin, oui, je dois bien me rendre à l'évidence :
Afin de savoir si il est possible que la décidabilité d'une formule soit indécidable (puisqu'on me répond souvent que ça tombe sous le sens que c'est faux...) je dois le prouver... Pour ne rien vous cacher, je pensais que la réponse viendrait simplement ici (ou bien que c'était évident ou bien que la preuve fût connue...).
Donc, oui, on en est là :
Je dois (ou nous devons...) trouver un langage L, une théorie T, les termes, les constantes et les règles de déduction de sorte que -sans doute par le biais d'un codage donc en prenant l'arithmétique- on puisse exprimer formellement dans L la décidabilité de toute formule de L (la formule dec(F) sera donc elle aussi une formule) et afin de répondre à ma question il faudra alors savoir s'il existe F telle que dec(F) soit indécidable.
êtes-vous d'accord ?
Pour ce qui est de réfléchir à cela, je vais y penser, mais étant pas mal pris, pas dit que je puisse avant longtemps !!
Mais l'espoir fait vivre...
Il faut que je reprenne mon "Cori Lascar"...
S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une
Ok, je l'ai fait de mon coté (rapidement, on va dire, voir message du dessus), mais je ne vois rien qui soit à peu près semblable à l'arithmétique (je n'obtiens notamment que 2 formules G=[il existe F décidable] et non G...).
A mon avis, on ne peut arriver à rien d'autres. Mais effectivement l'espoir fait vivre, je vous souhaite du courage...
Dernière modification par invite7863222222222 ; 02/08/2013 à 18h52.
Je ne vois pas pourquoi vous n'avez que deux formules. Gödel n'a-t-il pas lui même codé les formules mais aussi les preuves ? (afin de trouver une formule vraie non démontrable)
je vais y réfléchir et reviendrai vers vous si des fois j'avance (je veux relire d'abord la preuve des deux théorèmes de Gödel mais je n'ai pas mes livres avec moi et je ne la trouve pas sur le net !! (si des fois vous avez un lien ou un document ?)).
Par ailleurs, vu qu'il me semble que c'est lié, je vais ouvrir une autre question car je n'ai pas eu de réponse sur les deux décidabilités...
Merci en tous les cas...
S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une
2 formules car je suis allé dans votre sens, en essayant de parler de décidabilité dans le cadre d'une théorie qui se modélise comme l'arithmétique puisque c'était là votre condition pour pouvoir coder les formules... Si ca "marche" pas, la conclusion à en tirer est, il me semble, que c'est parcequ'il faut sortir de l'arithmétique pour parler de décidabilité d'une formule de l'arithmétique.
Dernière modification par invite7863222222222 ; 03/08/2013 à 11h37.
