C'est justement la ma question. En quoi la logique utiliser pour démonter que non (P ou nonP) est faux est différente de celle qui démontre que P ou (non P) est vrai.Envoyé par leon1789
J'ai l'impression que depuis le début du fil que tu appliques une logique hétérogène leon1789 inconnu (par moi j'en convient car je ne suis pas un expert du domaine) jusqu'alors
Patrick
Tu commences ta preuve par dire : <<Deux cas possible (en logique de boole) ...>>
Là, tu es exactement en train de dire << j'accepte le tiers exclus. >> car le tiers exclus, c'est ça : pas de tiers possibilité.
Ensuite ton raisonnement est correct et tu retrouves le tiers exclus.
Mon raisonnement ne fait pas appel à la validité du tiers exclus.
Il y a deux points points clés dans la preuve que j'ai rappelée
-1- la double négation (non non P) du tiers exclus est vrai (sans faire appel à la validité du tiers exclus).
-2- la triple négation (non non non P) est équivalente à la simple négation (non P), quel que soit P.
Ce sont deux théorèmes en logique.
Attention : (non non P) n'implique pas (P), donc le -1- ne montre pas que le tiers exclus est vrai.
Que veux-tu dire par logique hétérogène ?J'ai l'impression que depuis le début du fil que tu appliques une logique hétérogène leon1789 inconnu (par moi j'en convient car je ne suis pas un expert du domaine) jusqu'alors
Patrick
Je cherche juste à te répondre quand tu dis que (P ou Non P) est indécidable mais je démontre non (P ou Non P) est décidable.
Si j'utilise la même logique que toi (P ou non P) est décidable.
Que veux-tu dire par logique hétérogène ?Patrick
Oui, tu retrouves le tiers exclus, mais ce n'est pas étonnant car tu l'utilises au tout début de ta preuve : tu es d'accord ?
Non, tu n'utilises pas la même logique que moi car, dans la preuve que j'ai rappelée, on ne suppose jamais que le tiers exclus est vrai. Tu es d'accord ?
Le problème de fond est qu'on ne s'occupe pas ici d'algèbre de Boole, mais du principe du tiers exclu.
Ce que j'en comprends:
Il y a une distinction à faire entre une démonstration et l'algèbre de Boole.
La question du principe du tiers exclu n'est pas une question qui peut se traiter avec l'algèbre de Boole (en algèbre de Boole (A ou (non A)) est une tautologie, toujours vrai, suffit d'en faire la table de vérité). C'est une question de démonstration, de l'inclure ou non dans les principes qui peuvent être évoqués dans la succession des étapes qui forment une démonstration. D'autres exemples de tels principes sont le modus ponens, modus tollens, etc.
Il est naturel que ces principes respectent l'algèbre de Boole au sens où si on remplace les énoncés par des "vrai" ou "faux" booléen et qu'on applique les tables logiques correspondant aux principes évoqués alors cela "marche bien". Mais cela ne s'applique qu'aux valeurs booléennes, pas de manière totalement intuitive à la notion de "prouvé" pour un énoncé.
En bref, le principe du tiers exclu est lié à la notion de démonstration, le respect de l'algèbre de Boole est une nécessité, mais on ne peut pas aller sans danger dans l'autre sens, i.e., prendre une propriété algébrique et l'appliquer à la notion de démonstration. (Et un principe n'est ni "vrai" ni "faux", il est admis ou pas admis...)
Cordialement,
Dernière modification par invité576543 ; 29/01/2009 à 21h01.
PS : à u100fil. Un conseil est de bien lire, relire et comprendre le papier cité par Skydancer. Discuter du sujet sur ce fil ne semble pas amener quoi que ce soit d'autre que de la confusion. Si Médiat et God's Breath on arrêté d'intervenir, il y a une raison.
Cordialement,
Une assertion démontrable est-elle "vraie" ou "fausse" ?
La double négation d'un principe "admis ou pas admis" peut-elle être "vraie" ou "fausse" ou ni l'un ni l'autre ?
PS : La double négation du principe du tiers exclus est démontrable.
(http://people.math.jussieu.fr/~alp/philomatique.pdf , ligne 1 de la page 6)
tout à fait, et il est clair que les choses vont mieux quand les insultes ne fusent pas... Insultes venant d'incompréhensions, systématiquement.
Le doute est le début de la sagesse
merci du conseil
Patrick
Oui, c'est un bon document. Mais celui que je citais à l'avantage de présenter bcp d'exemples "concrets", celui de Skydancer aucun n'exemple si ce n'est l'algorithmique théorique en dernière section.
C'est marrant de reprocher aux forumeurs d'apporter des réponses prouvées aux questions qu'on se pose. J'ai rarement vu ça...
Je n'étais pas focalisé sur l'algèbre de boole mais sur :
l'ambiguïté : dans quel logique on se place ? peut on dire de même en logique classique ? peut on raisonner en mélangeant les logiques (sans rajout d'axiomes à une logique pour être équivalente à une autre) ?Ce qu’il se passe en réalité est que le tiers exclu est indécidable (et non pas faux) en mathématiques constructives.
Patrick
La phrase que tu cites n'a de sens que dans une logique où le tiers exclus n'est pas validé. Par exemple en logique intuitionniste (ou constructive).
En logique classique, celle que pratiquent 99% des matheux, le tiers exclus est valide : (P ou non P) est vrai.
Il y a quand un truc qui me dérange dans tout ça...
Page 6 de http://people.math.jussieu.fr/~alp/philomatique.pdf
Sur http://fr.wikipedia.org/wiki/D%C3%A9...idabilit%C3%A9le tiers exclu est indécidable (et non pas faux) en mathématiques constructives.
Ainsi, comme le tiers exclus est indécidable (en logique constructive), c'est que ni le tiers exclus, ni sa négation ne sont démontrables (en logique constructive). (*)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.
Or page 92 de http://www.reunion.iufm.fr/Recherche...cleJambon3.pdf
en logique constructive , on a
Si on applique cela à P = (Q v ¬Q) , on obtient ¬(Q v ¬Q) <=> ¬¬¬(Q v ¬Q) = ¬vrai = faux¬P <=> ¬¬¬P .
¬¬(Q v ¬Q) .
Donc ¬(Q v ¬Q) est décidable (puisque faux), mais cela est contradictoire avec (*)
......... message supprimé
non, ceci est faux.
En fait,
un énoncé mathématique est indécidable dans une théorie s'il est impossible de le déduire, ou de déduire sa négation, à partir des axiomes.
Donc le tiers exclus est indécidable (car on ne peut pas le déduire), mais sa négation est bien décidable (car fausse) . Michel m'a fait douter
Dernière modification par leon1789 ; 29/01/2009 à 23h59.
Cela est contradictoire avec la définition usuelle de "décidable", celle que tu as citée juste avant (dans le contexte d'une notion de démonstration bien définie, par exemple un langage, un ensemble d'axiomes et des principes de démonstration).
Maintenant, libre à toi de choisir un vocabulaire différent.
Cordialement,
Je me répète : ce n'est pas une question de logique, c'est une question de démonstration. Exemple de nuance : si on considère que "démontré" est équivalent au booléen "vrai", quelle peut être la valeur en booléen de P dans les cas respectifs "(non P) est démontré", et "P n'est pas démontré"?
On voit que parler de démonstration va plus loin que de parler de "logique" au sens algébrique.
C'est pour cela que le début de l'article cité parle de pré-ordre et de foncteurs, et non pas de "logique". La confusion est facile, puisque les deux langages sont très proches.
Cordialement,
Un dernier essai : àmha, le dérangement vient de la confusion entre la notion de décidable (ce qui demande un langage, des axiomes et des principes de démonstration) et un principe de démonstration.
Ma compréhension est que le tiers exclu est un principe de démonstration, qu'on admet ou pas, donc hors du champ de la décidabilité (qui demande des principes de démonstration comme préalable).
Cordialement,
Je ne choisis pas les définitions, je les lis !
Es-tu d'accord avec ces définitions ? (qui, encore une fois, ne sont pas les miennes !) On peut en changer si tu veux.Une proposition (on dit aussi énoncé) est dite décidable dans une théorie axiomatique, lorsqu'on peut la démontrer ou démontrer sa négation dans le cadre de cette théorie.
Un énoncé mathématique est indécidable dans une théorie lorsqu'il est impossible de le déduire, ou de déduire sa négation, à partir des axiomes.
Par ailleurs, démontrer une proposition, c'est prouvé qu'elle est vraie. Tu es d'accord ?
On sait qu'il est impossible de prouver le tiers exclu (en logique intuitionniste) donc , par définition, les tiers exclu est indécidable. Es-tu d'accord ?
La négation du tiers exclu est fausse car sa négation (ie. la double négation du tiers exclu, que l'on appelle aussi tiers exclu affaibli) est vraie. Es-tu d'accord ?
Dans la référence de skydancer, il est pourtant bien écrit (page 6) que le tiers exclu est indécidable ... non ?
Alors pourquoi dis-tu que le tiers exclu est hors du champ de la décidabilité ?
Si tu réfères à la phrase
je la comprends comme suit (et c'est une répétition de quelque chose que j'ai déjà indiqué):Ce qu’il se passe en réalité est que le tiers exclu est indécidable (et non pas faux) en mathématiques constructives.
En mathématiques constructives, un énoncé de la forme "P ou (non P)" a par défaut le statut "indécidable". Il est prouvé si et seulement si P est prouvé ou (non P) est prouvé; dans tout autre cas l'énoncé est indécidable.
Avec cette réécriture il n'y a pas de confusion entre ce qui est principe de démonstration (le tiers exclus, qui s'applique à des démonstrations) et la notion de décidabilité (qui s'applique à des énoncés).
Cordialement,
Si tu as lu mes messages, tu saurais déjà que je ne peux pas être d'accord. Comment expliquer que tu poses ces questions?
Cordialement,
C'est un peu confus pour un néophyte car cela n'apparait pas clairement dans la littérature internet.
Si on fait le parcours wikipédia :
La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l'anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du XXe siècle.
Aujourd'hui, une partie de la théorie de la démonstration se confond avec la sémantique des langages de programmation et interagit avec de nombreuses autres disciplines de la logique ou de l'informatique théorique.
La logique mathématique est née à la fin du XIXe siècle de la logique au sens philosophique du terme.
Au cours du XXe siècle, la logique mathématique s'est ramifiée en de nombreux sous-domaines :
* la théorie des ensembles ;
* la théorie de la démonstration ;
* la théorie des modèles ;
* la théorie de la calculabilité.
En logiques classique et intuitionniste, on distingue deux types d'axiomes : les axiomes logiques qui expriment des propriétés purement logiques comme par exemple A or not A (principe du tiers exclu, valide en logique classique mais pas en logique intuitionniste) et les axiomes extra-logiques qui définissent des objets mathématiques, par exemple les axiomes de Peano qui définissent l'arithmétique ou les axiomes de Zermelo-Fraenkel qui définissent la théorie des ensembles. Quand le système possède des axiomes extra-logiques, on parle de théorie axiomatique.
Pour Wikipédia le principe du tiers exclu est un axiome logique. Mais la notion de logique revêt plusieurs définitions.
En est il de même pour le concept de démonstration ? à t'il plusieurs définition ? comment se formalise t'il ? par des règles d'inférences ?
On comprend intuitivement qu'une démonstration par l'absurde utilise "les règles" (je ne sais pas comment le nommé) : si non P conduit à une contradiction alors c'est non (non P) qui est "non contradictoire/valide/vrai ?". Puis d'après le tiers exclu comme il ne peut y avoir que P ou Non P et que en logique classique non (non P) = P donc on déduit P.
Faut il comprendre le tiers exclu comme un axiome "logique" qui sert à la démonstration ?
Patrick
Ok, disons qu'on est d'accord sur ça.
Pour une proposition P quelconque, on a bien "non non (P ou non(P))" (c'est le tiers exclu affaibli).
Ainsi, par définition du "non", on a non (P ou non(P)) => faux
C'est cela que j'entends quand je dis que la négation du tiers exclu est fausse.
Es-tu d'accord avec non (P ou non(P)) => faux ?
Oui, au sens où pour tout énoncé P, l'énoncé "non (P ou non(P)) => faux" est démontrable avec les principes de démonstration acceptés par les constructivistes.
Non. Parce que tu emploies là un terme (tiers exclu) qui dénote un principe de démonstration, et la notion de "faux" ne s'applique pas plus à cette catégorie de termes, pas plus que "bleu" ou "fluide" ou "sale".la négation du tiers exclu est fausse.
Cordialement,
Bien d'accord. Et je me considère comme un néophyte, et j'ai bien peur que beaucoup de textes que l'on trouve sur la toile, dont Wikipédia, soit écrits par des néophytes.
Dans les textes sérieux que je lis, la distinction entre la logique (au sens algébrique, genre algèbre de Boole) et la démonstration est toujours soigneusement faite. Le texte cité par Skydancer rentre dans cette catégorie : tout le début introduit un formalisme concernant la démonstration, et cela ne parle pas de logique au sens "logique bivalente suivant l'algèbre de Boole", même si le mot "logique" apparaît.
C'est comme cela que je le comprends. Ou comme une règle de démonstration. Quelque chose qui permet de passer d'un énoncé à un autre dans la séquence d'une démonstration.Faut il comprendre le tiers exclu comme un axiome "logique" qui sert à la démonstration ?
En évitant d'utiliser le mot "axiome", on évite une confusion avec les théories axiomatiques, comme l'algèbre de Boole par exemple.
Cordialement,
ok !
Ainsi on a un exemple de proposition indécidable dont la négation est décidable (car fausse) :
il s'agit de (P ou non(P)) lorsque (P ou non(P)) est indécidable.
Ok ?
si Q est vrai alors non(Q) est faux
si Q est faux alors non(Q) est vrai
si Q est indécidable alors non(Q) est faux ou indécidable
ok ?
Tant que tu mélanges "décidable" et "vrai" ou "faux", il est difficile de répondre sans ergoter sur les termes.
décidable est lié à "prouvé", pas à vrai ou faux.
Plein de discussions sur les "fondements de mathématiques" sont pourries par le mauvais usage des termes "vrai" et "faux".
----
Sinon, au-delà de la forme qui n'aide pas, je pense comprendre ce que tu cherches à dire. Il se peut que l'approche intuitionniste amène à une autre définition des mots "décidable" et "indécidable". Je ne sais pas; faudrait trouver quelqu'un ou des textes permettant d'obtenir plus de détails sur les approches constructivites et intuitionnistes.
Cordialement,
Ok d'accord.
Dernière modification par leon1789 ; 30/01/2009 à 12h03.
