Non P est une notion première. Comme on PEUT PROUVER même avec que de l'intuitionisme qu'elle équivaut à P=>tout , bien des gens présentent ensuite ça comme une abréviation.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Ha ! Voilà une réponse plus précise.
J’ai l’impression que les échanges avec Ltav cachent de temps en temps ce genre de quiproquo. Chacun part de sa propre construction de la LC et du coup ça s’étend en échanges interminables alors que les présupposés ne sont peut-être pas les mêmes.
Bien étendu, ce ne doit pas être que ça. L’enfumage dénoncé par GaBuZoMeu relève d’autre chose.
C’est dramatique, mais c’est moi qui vais demander que chacun expose sa façon de définir la LC et la LI.
On pourrait alors travailler sur les équivalences entre les partis pris (RPA, TE, etc.).
Ça va faire répéter chacun une 48274722738e fois quelque chose, j’en conviens.
@Dom : il n'y a aucune contradiction et la réponse de Martial répond parfaitement à ton questionnement. Aucun ensorcellement non plus (ce genre de propos devient lassant). A partir du moment où tu démontres qu'une proposition est équivalente à une autre, tu peux la prendre sans problème comme définition. Encore faut-il que l'autre soit bien définie. Tout le problème est là.
Je vais répondre précisément et aussi brièvement que possible aux autres "arguments" de nos amis.
Ok.
J'avais relevé : (j'ai remanié les dialogues dans la manières que je les ai comprises, ainsi les propos ne sont pas exactement les mêmes). Au lieu de dire "on définit", j'utilise le symbole :=.
---début du dialogue Moi, en gros : En L.I. et en L.C., pour tout P, non(P):=(P=>Tout).
Ltav, en gros : Non,
En LC, non(P) := la proposition qui a une table de vérité opposée à celle de P.
On en déduit alors que non P <=> (P => tout).
En LI, non(P) := (P => tout).
Moi :
Ainsi tu nies qu’on a : non(P) := (P=>Tout) en LC ?
Sans s’occuper des tables de vérité ?
Ltav :
En LC, il est tout à fait possible de prendre cette définition.
---fin du dialogue---
Bon, ok, je comprends donc que quand tu parlais de table de vérité, ce n'était pas obligatoire pour définir ce "non".
On obtient toutefois un truc équivalent.
Je rebondis sur le propos de Christophe : "non" est une notion première.
Bon, c'est quoi alors ?
Oui, je ne comprends rien. J'ai l'impression que tantôt c'est ceci qu'on choisit (j'ai lu ça dans un message), tantôt c'est autre chose. D'où mes tergiversations.
@Dom : "Oui, je ne comprends rien. J'ai l'impression que tantôt c'est ceci qu'on choisit (j'ai lu ça dans un message), tantôt c'est autre chose. D'où mes tergiversations".
En fait ton dernier post montre que tu as tout compris.
C'est juste qu'il faut que tu prennes une bonne douche pour te désenfumer, lol.
Je ne donnerai pas ma définition de la LI, car je ne suis pas suffisamment expert dans ce domaine, et je n'ai pas envie de raconter des conneries, on en a suffisamment lu comme ça.
Le problème grave que je dénonçais est je l'espère plus visible, maintenant que Cc et Gbzm ont répondu sur leurs (non)définitions et leurs réponses montrent qu'ils ne comprennent toujours strictement rien à ce que j'ai dit (mon for intérieur est ébahi de leur manque de subtilité - sans parler du manque de politesse. [Oui, ce débat purement intellectuel doit rester cordial. Merci. Ltav]. Fermons cette parenthèse).
Dans la logique classique ou intuitionniste, je l'ai déjà précisé, non P n'est pas définie explicitement mais doit obéir à certains axiomes bien précis. Il y a donc quelque part la définition des propriétés que doit vérifier une éventuelle non P : en LC ou LI, non P c'est toute proposition d'un ensemble S vérifiant ces axiomes. A partir de là, on peut démontrer, comme l'ont fait Cc et Gbzm que non P <=> (P => tout). Autrement dit, si non P appartient à S, alors ces démonstrations sont correctes. Oui ou non ?
Mais existe t-il une seule proposition réalisant ces propriétés ? Que se passerait-il si S était l'ensemble vide ? S'il était vide (en ce cas, aucune non P ne peut appartenir à S : ma condition soulignée n'est plus vérifiée) alors leurs "démonstrations" prouveraient tout et son contraire, plus rien ne garantirait leur validité.
Bien, à ce problème grave et très précis de logique, voici le genre de réponse à la Cc/Gbzm qui se dégage en substance : "il n'y a pas besoin de définir non P, c'est une notion première, nos démonstrations sur non P sont correctes sans avoir besoin de définir non P, etc.". Eh bien, dois-je le répéter : c'est totalement faux et je viens de le prouver.
Heureusement les logiciens de la LC et de la LI ont très bien compris ce problème et défini des propositions consistantes vérifiant les axiomes de non P. Ils ont "rempli" de matière logique ce qui n'était peut-être qu'un pur symbole vide (je sais, je poétise là). En LC, cette définition de non P (tables de vérité opposée à P) se base obligatoirement sur le tiers-exclu puisque par définition non P doit le vérifier en LC. En LI, non P ne vérifie plus le tiers-exclu, il fallait donc trouver autre chose : on a alors proposé non P := (P => tout), pas pour faire joli ou aller vite mais parce que cette définition réussissait à vérifier les axiomes liés à "non P" en LI (LC moins tiers-exclu), sans avoir besoin du tiers-exclu.
J'ai encore été trop long...! Pour résumer grossièrement, en LC et LI, on ne démontre pas tout seul :
non P <=> (P => tout)
Mais avec au moins une condition devant (j'ai défini S plus haut) :
(non P $\in $ S) => (non P <=> (P => tout))
Sans définition de non P par une proposition consistante, rien ne garantit que S ne soit pas vide, et la condition n'est plus vérifiée. Bien sûr ça ne va pas gêner certains logiciens vides. Mais des mathématiciens, si. Il ne suffit plus d'utiliser des symboles "étiquettes" quand on veut appliquer une axiomatique à nos raisonnements de tous les jours (comme avec "$\sqrt2$ irrationnelle, etc.), on ne veut pas parler dans le vide. Il faut des propositions réelles vérifiant ces axiomes.
Le tiers-exclu est inévitable en LC dès le moment où l'on veut légitimement définir un non P vérifiant les axiomes de LC dont le tiers-exclu. C'est une évidence. Et il est a fortiori inévitable dans la démonstration de non P <=> (P => tout) avec un non P bien défini, "non vide". En LI, on ne doit plus utiliser le tiers-exclu : il est donc inévitable de devoir changer la définition classique de non P.
Cc et Gbzm n'ont simplement jamais réfléchi à ces considérations.
N.b. ah, Cc : restons sur notre sujet et évitons de discuter AO ici. Nos derniers débats, où j'avais démontré que tu avais attaqué à tort la validité logique de l'AO (et où tu changeais poétiquement à ta guise le sens d'un même mot), ont été assez éloquents. Les lecteurs intéressés pourront juger par eux-mêmes.
Merci Martial.
Bigre, ce fil me plaît : pas trop de bazar, quelques chagrinades dues aux écrits et donc aux quiproquos.
Allez ! On se concentre, moi le premier.
Édit : je n’avais pas ton dernier message, Ltav.
Édit : Dis-moi Martial, as-tu un document référence ?
Un site, un pdf, un bouquin ?
Je suis très très novice d’une part et en ce moment, c’est davantage pour ma culture générale et du loisir.
J’entends un document qui définit proprement le début du début en LC et/ou en LI.
Là, c’est difficile de retracer les liens adjacents. Je suis certain qu’en recoupant tout on aurait un truc extra mais c’est fastidieux.
Je me demande même si je ne vais pas (quand ?) taper un truc quitte à le modifier pour que ce soit propre, succinct et exhaustif. Tout ça grâce aux échanges.
@dom, tu n'as jamais assisté à la choses suivante:
1/ Soit blabla une structure (un quadruplet $(a,b,c,d)$ ) vérifiant blabla
2/ Théorème: dans ces conditions $a=c$
3/ Dorénavant, on donnera ce nom à $(a,b,c)$ et, au besoin, on se réfèrera à l'ancienne définition en parlant de $(a,b,a,c)$
? :-D
Par exemple:
1/ On appelle bidule un triplet $(E,\leq, non)$ où
1.1/ $\leq$ est un ordre sur $E$ tel que toute partie a une borne sup (donc un plus grand élément $1$ et un plus petit éléments $0$.
1.2/ Pour tout $a,b$ la borne supérieure de $A:=\{x\in E \mid inf(a,x) \leq b\}$ est un élément de $A$, noté $(a\to b)$
1.3/ non est une application décroissante de $E$ dans $E$ vérifiant: blabla.
2/ Théorème: pour tout $x\in E: (non(x) = (x\to 0))$
Dorénavant, on appellera "algèbre de Heyting complète" un couple $(E,\leq)$ tel que $(E,\leq , [x\mapsto (x\mapsto 0)])$ est un bidule.
La logique intuitionniste est le produit de toutes les algèbres de Heyting, ou, si tu préfères l'ensemble des expressions dont toute interprétation dans toute algèbre de Heyting vaut $1$.
Ensuite tu as le théorème suivant:
Soit $(E,\leq)$ une algèbre de Heyting. Alors elle est une algèbre de Boole si et seulement si $non$ est injective. Ce qui a entre pour conséquence que $\forall x\in E: [x = (non(non(x)))]$
Je pense que tu avais très bien compris en fait, mais bon...
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
@Ltav: il y a une manière de te trouver sympathique, c'est de te lire et de se demander (sans trouver) le plaisir que tu trouves à te ridiculiser comme ça. En tout cas, c'est courageux.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Merci Christophe.
En fait, je comprends des choses mais je ne « fixe » pas, faute de les récrire, de les travailler, de me les approprier.
Ça en devient pénible pour mes interlocuteurs (ça ne t’épargne pas ;-)).
Mea Culpa chers intervenants, merci de votre gratitude et patience.
Et il (le tiers-exlus) est a fortiori inévitable dans la démonstration de non P <=> (P => tout) avec un non P bien défini, "non vide".
En LI, on ne doit plus utiliser le tiers-exclu : il est donc inévitable de devoir changer la définition classique de non P.
Cc et Gbzm n'ont simplement jamais réfléchi à ces considérations.
C'est moi qui ai mis en rouge les passages.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
@Dom, pour préciser, je n'ai jamais inventé ces définitions : la LC définit bien de façon première non P par une table de vérité opposée à P. Elle procède ainsi car il lui est obligatoire de vérifier le tiers-exclu. C'est lui qui est obligatoire, plus que les tables de vérité. Si la LC décide de prendre une autre définition secondaire elle devra toujours vérifier le tiers-exclu. Comprends que le tiers-exclu fait partie des axiomes à vérifier par toute définition de non P dans LC. C'est aussi simple. La LI doit, elle, opter obligatoirement pour une définition première de non P qui ne vérifie pas le tiers-exclu (ce qui ne veut pas dire le réfuter), c'est encore ses axiomes qui l'imposent...Cette définition première est donc nécessairement différente de la LC, même si elles peuvent se "rejoindre" par le jeu des équivalences.
Peut-être peux-tu voir plus facilement les choses en termes de définitions premières et secondaires (à distinguer des notions premières de Cc qu'il semble voir comme non définissables).
la logique intuitionniste est juste l'ensemble des propositions obtenues comme suit:
1/ j'abrège la phrase $Q:=A_1\to (A_2\to (\dot (A_n\to x) )\dots )$ par $A_1;A_2;\dots \vdash x$. Les $A_i$ sont appelées hypothèses de la phrase $Q$.
2/ Les axiomes sont les phrases où la conclusion $x$ figure parmi les hypothèses.
3/ partant d'une phrase déjà prouvée, tu peux:
3.1/ permuter ses hypothèses
3.2/ Contracter quand répétition. Autrement dit considérer comme théorème $..;A;..\vdash x$ quand $..;A;A;..\vdash x$ en est un.
3.3/ virer une hypothèse si par ailleurs tu sais que c'est un théorème que tu as déjà prouvé.
3.4/ Remplacer $A_1;A_2;\dots ; ..;U;V;..\vdash x$ par $A_1;A_2;\dots ; ..;(U\wedge V);.. \vdash x$ et réciproquement)
3.5/ Considérer $L+M\vdash (A\wedge $ théorème quand tu as déjà prouvé $L\vdash A$ ainsi que $M\vdash B$ (L,M sont des lites, $+$ est la concaténation).
4/ Je te laisse ajouter des règles pour "ou" et "non".
Mais le plus important, ne cherche pas à retenir par coeur. Tout passage au "cas particulier" génère un théorème intuitionniste et réciproquement à ceci près que :
4.1/ le "A =>(A et A)" va générer des choses non triviales (mais qui le deviennent si tu gardes "A et A" à la place de A
4.2/ Tu t'autorises à considérer que A=>B est un cas particulier de B (ou si tu préfères que A et un cas particulier de A et .
5/ En fait à (4.1) près la logique intuitionniste dit qu'un énoncé est un théorème ssi il est pseudo-trivial.
6/ "P est pseudo-trivialé veut dire il existe une application $f$ et une trivialité pure $Q$ tel que $P$ s'obtient en remplaçant chaque lettre $x$ (variable) dans $Q$ par $f(x)$.
7/ Je pense que tu vois bien que le raisonnement par l'absurde "ajoute quelque chose", non? Tu vois bien qu'il n'y a aucun moyen de l'obtenir comme ça?
Je te donne une autre description si tu veux :
On part des évidences pures (phrase où la conclusion figure parmi ses hypothèses) et on les conjoncte au sens large:
1/ On peut s'autoriser une conjonction des $(A_i\to B_i)$ comme suit: $(\bigwedge_i A_i)\to (\bigwedge_i B_i)$
2/ Et on considère $(A\to (B\to C)=((A\wedge \to C)$ comme une pure égalité (qu'on peut faire comme on veut
3/ On considère que $A=(A\wedge A)$
ET RIEN DE PLUS
Autre remarque: tu sera peut-être frustré que je ne parle pas de "ou" (ni avec bcp d'estime de $\wedge$ (et)). Cela provient de la polarité logique:
1/ pour savoir si $R(a\vee b)$ est un théorème et que l’occurrence de $(a\vee b)$ est positive, il suffit de se demander si
$[(a\to x) \wedge (b\to x)]\to R(x)$ en est un (avec $x$ fresh variable of course)
2/ pour savoir si $R(a\vee b)$ est un théorème et que l’occurrence de $(a\vee b)$ est négative, il suffit de se demander si $R(a)$ ainsi que $R(b)$ en sont, etc
Tout ceci, tu peux le faire tout seul. En gros, la seule chose qui manque à la logique intuitionniste pour être classique, c'est juste l'injectivité de la fonction qui à $X$ associe $X\to tout$.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Je te le dis pour la 32687436ième fois Ltav: tu es courageux ou inconscient, je ne sais pas. Tu as l'air de penser que ce que tu es sur ce forum ne se voit pas.
Et il semble trop difficile de t'expliquer comment les parcours de débutants sont toujours un peu les mêmes, avec les mêmes pièges, les mêmes "inspirations" et les mêmes bisounourseries. Tu es attendrissant en apprenant (très doucement***), te plantant sans arrêt, rebifurquant sans cesse pour cacher ces plantes, etc
*** Le problème étant que PERSONNE, je dis bien PERSONNE ne comprend pourquoi, vu que tu es anonyme, tu n'avoue tout simplement pas que tu es béotien et que tu aimerais progresser. Du coup, tu passes 90% de tes posts à patauger pour planquer (sans aucun succès) que tu n'y connais rien, mais en plus que tu comprends très mal (et il n'y a pas de honte) et 10% à "améliorer" ta connaissance de telle ou telle petite information sans trop savoir si elle est importante. C'est vraiment du gâchis.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Cc, tu démontres une fois de plus ton incapacité à comprendre les phrases d'autrui (de là à interpréter leurs pensées)...
Je réécris mes phrases pour toi :
Et il (le tiers-exclu) est a fortiori inévitable dans la démonstration de (non P)$_{LC}$ <=> (P => tout) avec un non P bien défini [comme le veulent les axiomes LC], "non vide".
En LI, on ne doit plus utiliser le tiers-exclu [dans (non P)$_{LI}$ <=> (P => tout)]
Toute ta carrière de logicien t'a mené à ne plus comprendre des subtilités aussi basiques et à voir des contradictions imaginaires. C'est encore plus dommage.
@dom: il y a par chance UN TRUC GRAVEMENT FAUX dans ce que je t'ai dit. Mais je ne corrigerai que demain** Je mettrai la correction en blanc. Un excellent moyen pour toi de "fixer" est de le trouver.
** Étant sur mon téléphone
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
@Dom : merci, je dois avouer aussi que nous sommes contents de t'avoir comme fidèle compagnon à tous ces débats, dans ce rôle difficile - et ingrat - d'observateur, voire d'arbitre, scientifique, mais qui te plaît et que tu réussis malgré tout avec un certain talent.
@Cc (*) : tu sors "l'artillerie lourde" (si lourde qu'elle s'enraye...) pour expliquer comment tu définis la négation d'une proposition...? Tu as parlé de travailler avec des "notions premières", peux-tu préciser ce que tu entends personnellement par là ? A partir de quel moment as-tu besoin de les définir ? Est-il possible qu'elles ne correspondent à rien d'existant mathématiquement et invalident tes démonstrations en LC ou LI ?
non P et (P => tout) sont parfaitement équivalentes mais elles le sont grâce au tiers-exclu
C'est factuellement faux.
J'espère que tu as compris que tout mon discours se plaçait en aval de l'acte de définition explicite de non P en LC. L'amont ne m'intéresse pas mais doit surtout être évité par les mathématiciens, puisque non P n'y est qu'une étiquette vide pouvant cacher un concept contradictoire invalidant tous les raisonnements. Cette définition explicite doit par principe vérifier le tiers-exclu.
- Une fois (non P)$_{LI}$ définie en LC, on a bien grâce au T-E (je te précise l'indice pour éviter tes risques de confusion) le théorème qui avait été "démontré en sursis" avec l'étiquette vide non P (en attendant de lui donner une "âme" consistante) :
(non P)$_{LC}$ <=> (P => tout)
Dès qu'il y a définition de non P, il y a tiers-exclu, c'est obligatoire par définition : cet axiome T-E est derrière tous les théorèmes de LC concernant non P.
- En LI, idem : avant la définition explicite de non P, non P ne veut rien dire, voire pire : rien ne garantit la validité de nos raisonnements avec non P. En posant (non P)$_{LI}$ := (P => $\bot$), on voit qu'elle vérifie les axiomes de la LI. D'où la validité cette fois réelle (sans "étiquette vide" non P) du théorème :
(non P)$_{LI}$ <=> (P => tout)
Ainsi dans nos raisonnements sur l'irrationalité de $\sqrt2$ ("non P"), crois-tu que les termes (non-rationnel, etc.) ne sont pas définis ou utilise-t-on des "étiquettes vides" ? Puisqu'ils sont bien définis, tu comprendras alors que le tiers-exclu est partout (explicitement ou non) dans les théorèmes LC. C'est précisément ce que j'expliquais - sous tes pitreries dans la semoule.
Pour l'éviter, il faut changer de définition (et de logique) et passer en intuitionniste : désormais, ("$\sqrt2$ est irrationnelle")$_{LI}$ s'entend (et il faut le préciser) comme "la rationalité de $\sqrt2$ mène à une contradiction".
Bonne nuit.
[small](*) Tu as encore balancé ton ineptie sur l'AO. Exemple : "si x est ceci et x est cela, alors x existe". Pourquoi diable voudrais-tu changer cette phrase en "si x est ceci et y est cela, alors z existe, pour x=y=z" ?? Tu ne comprends toujours pas que c'est la règle contraire à la tienne qui s'impose en logique, mathématique, linguistique, etc. : deux mêmes mots ont le même sens sauf indication contraire. Sinon tu fais de la poésie. Ton entêtement est incroyable (pour paraphraser le lexique religieux). J'ai encore de quoi alimenter ton fil de l'arroseur arrosé ;-)[/small]
Je pense que tu espères "progresser en polemiquant". Ce n'est pas totalement idiot comme démarche si ça correspond un trait profond de caractère en toi, mais tu gaspilles une telle énergie autour que ça reste du gâchis de temps et de neurones. De mon téléphone.
Contrairement à ce que tu crois ce que tu racontes est très simple et "habituel" dans les parcours beotiens d'initiation. Mais cette posture "je suis le meilleur je sais tout" ne te sert pas dans la motivation des autres à t'informer. De mon téléphone
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Ltav ayant abandonné le discours mathématique pour un discours creux qui tourne sur lui-même et n'a plus aucun sens, je m'abstiendrai de perdre mon temps à lui répondre. Juste poser de temps en temps des avertissements de temps en temps.
O.k. je vais faire le novice. Supposons que je vous dise : super j'ai démontré que
(Bidule chouette rose violet) <=> 1+2=3
Ma démonstration est-elle correcte ou non ? Non, bien sûr vous me direz qu'elle est mal définie, tant que "Bidule chouette rose violet" n'est pas défini.
Hé bien, vos démontrations de non P <=> (P => tout) sont mal définies Gbzm et Cc puisque vous reconnaissez que non P n'est pas défini. Et qu'il est certain que dans les démonstrations courantes sur l'irrationalité de la racine de 2, les termes ont été définis auparavant. C'est de la sorcellerie ça ?
Mon objection est parfaitement mathématique : vos démontrations sont mal définies donc ne sont pas plus des démonstrations que celle sur bidule chouette rose violet. Tout le monde peut le vérifier immédiatement. Je vous mets au défi de montrer le contraire.
Bon, et bien en fait je ne crois pas Ltav. Je crois suis certain qu'ils sont lassés.
D'ailleurs, parfois je les lasse aussi car je repose les mêmes questions.
Toi, Ltav, tu demandes à ces messieurs "Que prenez-vous alors pour définition-départ de $non(.)$, si ce n'est pas $P\Rightarrow Tout$ ?". Moi j'avais compris qu'on prenait cela comme définition.
Et je pense même pouvoir retrouver un message où c'est ce que l'on choisit.
N'est-ce pas cela ta question ?
Une réponse très très récente de Christophe a été : c'est une notion primitive.
Et ensuite, j'ai compris qu'on voulait juste que cette notion primitive vérifient quelques axiomes.
Dom, si je te disais que bidule chouette rose violet vérifie juste certains axiomes, ma démonstration n'en serait pas moins mal définie.
En fait, je ne posais pas vraiment de question dans mon post, je maintenais que leurs démonstrations n'en étaient pas au sens où l'on démontre que la racine de 2 est irrationnelle.
Non, enfin disons plutôt qu’elle n’est pas irrationnelle.
Et dire que « ne pas être irrationnelle » entraîne « être rationnelle », c’est appliquer le RPA en LC.
@Dom : j'ai l'impression que tu te laisses encore enfumer.
Reprends la preuve classique : supposons qu'il existe un rationnel x tel que $x^{2}=2$.
Alors blablabla, et on arrive à antitruc.
Moralité, on a prouvé que (racine de 2 rationnel) implique antitruc, ce qui est exactement la définition de non(racine de 2 est rationnel).
Il n'y a pas de RPA là-dedans.
J'ai l'impression que ce qui te pose problème c'est de déduire "x est irrationnel" de "non(x est rationnel)". Là encore c'est une définition. C'est comme si la police démontre qu'à l'instant du meurtre le tueur ne pouvait pas être à l'intérieur de la maison de la victime. C'est donc qu'il était à l'extérieur, défini comme tout ce qui n'est pas à l'intérieur.
Si ça peut t'aider remets-toi dans le contexte de Pythagore, qui ne connaissait que les nombres rationnels, qu'il appelait d'ailleurs "nombres", pensant que c'étaient les seuls existants. Un jour il démontre qu'il n'existe pas de nombre $x$ dont le carré soit égal à 2. Et puis une semaine plus tard, en dessinant un triangle rectangle isocèle de côté 1 il s'aperçoit (grâce à un précédent théorème) que le carré de l'hypoténuse est égal à 2. Cela lui pose problème, car cette hypoténuse est une grandeur palpable, que l'on peut par exemple reporter avec un compas. Il en déduit qu'il existe des grandeurs qui ne sont pas des nombres, d'où le nom de grandeurs irrationnelles. Toujours pas de RPA là-dedans.
Je crois que pour ta santé mentale tu devrais faire comme GBZM : ne plus répondre aux messages de Ltav, voire même ne plus les lire, sinon tu vas devenir ouf.
Martial, donc tu définis selon tes propres mots "racine de 2 irrationnelle" par "racine de 2 implique tout" ? Mais c'est précisément le raisonnement intuitionniste. Il permet d'éviter le tiers-exclu mais comme je l'expliquais au prix de redéfinir l'irrationalité de racine de 2.
Ce que tu viens de démontrer est selon cette définition : "racine de 2 est irrationnelle" implique "racine de 2 est irrationnelle".
Ha zut, tu t'es fait avoir Martial.
J'ai bien compris : $(r \in \mathbb Q \Rightarrow Tout) \Rightarrow r \notin \mathbb Q$ sans RPA.
J'avais rédigé un raisonnement qui utilise tout de même le RPA.
C'est tarabiscoté, c'est inutile, c'est pompeux, mais c'est juste de qualifier le raisonnement suivant de raisonnement par l'absurde.
Mon cher Martial, tu vas voir... tu me diras si ça te convient.
Je parle aussi sous le contrôle de tous les intervenants, bien sûr.
Début de la preuve de : $(r^2=2$ et $r>0) \Rightarrow r \notin \mathbb Q$
On va démontrer cela par l'absurde.
On suppose : $non($ $(r^2=2$ et $r>0) \Rightarrow r \notin \mathbb Q))$ (***)
C'est-à-dire : $(r^2=2$ et $r>0) \ et \ non(r \notin \mathbb Q)$.
C'est-à-dire : $(r^2=2$ et $r>0) \ et \ \color{red}{non(non(r \in \mathbb Q))}$.
$\color{red}{}$
J'applique l'axiome RPA à la partie rouge, j'en déduis :
$(r^2=2$ et $r>0) \ et \ \color{red}{r \in \mathbb Q))}$.
J'obtiens avec les calculs classiques vus partout un antitruc.
C'est-à-dire : (***) => $Tout$
Je viens de démontrer :
$non(non($ $(r^2=2$ et $r>0) \Rightarrow r \notin \mathbb Q)))$
J'applique l'axiome RPA, j'en déduis :
$(r^2=2$ et $r>0) \Rightarrow r \notin \mathbb Q)$
Fin de la preuve de : $(r^2=2$ et $r>0) \Rightarrow r \notin \mathbb Q$
Qui démonte cette preuve ?
Le seul truc que je n'ai pas bien travaillé, c'est la négation du "ou" qui devient un "et" des négations (De Morgan, en gros). Je veux dire : je ne sais pas d'où on part pour démontrer les lois de De Morgan.
Rappel : quand tu dis que $(r \in \mathbb Q \Rightarrow Tout) \Rightarrow r \notin \mathbb Q$ est démontrable sans RPA, c'est vrai mais seulement en logique intuitionniste, au prix d'une redéfinition de ta négation : $r \notin \mathbb Q$ := ($r \in \mathbb Q$ => $ \bot$). C'est grâce à cette définition que $(r \in \mathbb Q \Rightarrow Tout) \Rightarrow r \notin \mathbb Q$ est correctement démontrable sans RPA - les "démonstrations" de Gbzm et Cc sur bidule chouette rose étant mal définies car portant sur un fantôme peut-être inexistant.
Dès que tu définis non P en logique classique, alors tu utilises forcément le tiers-exclu et le RPA (par définition de la LC).
@Dom : Pour une fois Ltav a PRESQUE raison :
des 4 lois de de Morgan (obtenues en ne prenant que les implications des 2 équivalences), la seule qui est fausse en LI est
non(P et Q) IMPLIQUE (nonP ou nonQ).
Donc ton raisonnement tient la route.
Mais tu le reconnaîtras aisément, c'est dégainer une Kalashnikov pour enc… une mouche.
C'est comme les mecs qui démontrent Tychonoff, AC à l'appui, pour en déduire qu'un produit de 2 compacts est compact !!!
Et c'est comme les mecs qui trouvent le moyen d'utiliser AC pour démontrer Cantor-Bernstein (là, MDR).
"Pour une fois Ltav a PRESQUE raison " : quand je disais ça je parlais de son avant-dernier message.
Pas du dernier, qui s'est croisé avec le mien, et auquel je n'ai rien compris.
Martial : pourquoi presque raison...? Ce que j'ai dit sur De Morgan est entièrement correct. Et j'ai raison sur toute la ligne dans ce débat. Mais si tu arrêtais de faire avec moi la politique de l'autruche à enfoncement de tête variable, peut-être verrais-tu mieux la lumière...
Ce que je raconte est très simple. Pour commencer, ça ne te gêne pas toi que nos deux amis Cc (:-D) et Gbzm (:-X) prétendent démontrer un pseudo-théorème T sur bidule chouette rose violet alias "non P" ?
Bidule chouette rose violet <=> (P => tout)
Or le théorème complet est :
Pour tout bidule chouette rose violet vérifiant certains axiomes alors :
Bidule chouette rose violet <=> (P => tout)
Donc si l'ensemble des propositions vérifiant ces axiomes est vide, alors T n'est plus garanti. Leur démonstration est donc fausse. Pour la rendre valide, on donne justement une définition explicite d'un bidule chouette rose violet vérifiant vraiment ces axiomes (suivant les cas : (non P)$_{LC}$ ou (non P)$_{LI}$).
C'est si dur à comprendre ? Tout théorème de maths sérieux portant sur un nouvel objet commence par démontrer que l'ensemble de ces objets n'est pas vide.
C'est si dur à comprendre ? Tout théorème de maths sérieux portant sur un nouvel objet commence par démontrer que l'ensemble de ces objets n'est pas vide.
Pour info, pour les lecteurs,des que Ltav dit quelque chose autre que de la langue de bois ca ne rate quasiment jamais c'est une connerie assez spectaculaire. C'est assez génial de l'avoir sur ce forum. Il offre un anti modèle de bluffage en science que personne n'espererait même décrire à ce point exhaustivement. Je ne sais pas s'il en est conscient (c'est toujours dur de se voir soi même avec des yeux extérieurs) je ne pense pas mais ça peut expliquer aussi qu'il s'enferme de plus en plus dans la LDB.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Mais arrête de croire qu'on ne te comprend pas. Ton cirque bien qu'un peu longuet est assez clair. On t'a compris. Mais tu crois abuser qui en rebondissant dur des virgules pendant 300 posts? Je pense que ce n'est pas toi même (ie tu sais ce que tu fais et es conscient de tes ruses) mais la quedtion EST QUI? On voit que tu galères c'est tout on pourrait même jouer à écrire ton post suivant en se trompant peu.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
1)
Enfin, je veux dire que pour moi, depuis le début de mon investissement (très léger) dans ce domaine, j’accepte la définition du $non(P)$ par $P=>Tout$.
Je ne sais toujours pas ce qu’est le $non$ sans ça.
Et je n’aime pas l’approche « table de vérité ».
Bref.
2)
« Dès que tu définis non P en logique classique, alors tu utilises forcément le tiers-exclu et le RPA (par définition de la LC). »
C’est effrayant mais j’ai l’impression que ça c’est faux.
Une impression, car très peu aguerri.
Ltav, dans ton discours qui va devenir un monologue un jour tu parles tout le temps de Tiers Exclu.
Dans les discours de Christophe et GaBuZoMeu, ils n’en parlent jamais.
L’approche n’est vraiment pas la même.
Ha ? Une question de Christophe.
La réponse m’intéresse !!!
T'inquiète avec ta phrase que j'ai cité tu vas avoir plein de matheux du quotidien qui vont te charrier à coups d'exemples variés , avec cette connerie merci tu auras offert un chti jeu mathématique à plein de lecteurs du forum qui grignotaient des cacahuètes en te lisant et qui maintenant se sont redressés dur leur chaise pour t'endevelir sous des contre exemples. Je n'ai rien d'autre à faire que d'attendre et deviner ce que tu vas leur répondre :-D
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
@dom : Ltav fume le seul élément de S_2 autre que l'identité depuis 50 posts et il a attaqué le filtre il y a 48 posté. C'edt juste ça qu'il veut dire (et comme je ne veux pas être cruel je n'evoqjerai pas l'éventualité qu'il pense peut être que tout anneau de Boole a un cardinal égal à 2. Il risque de l'affirmer puis de dire qu'il ne voulait pas dire ça ensuite pendant 205 posts
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
1)
Enfin, je veux dire que pour moi, depuis le début de mon investissement (très léger) dans ce domaine, j’accepte la définition du non(P) par P=>Tout.
Je ne sais toujours pas ce qu’est le non sans ça.
Et je n’aime pas l’approche « table de vérité ».
Bref.
Si tu n'aimes pas hélas, c'est que quelque chose cloche encore un peu dans ta compréhension. Pourquoi changer les définitions "officielles" de la LC avant d'avoir parfaitement compris ses raisons ? C'est grâce au tiers-exclu et à ses tables de vérité sous-jacentes que l'on définit explicitement non P, qu'on lui donne une existence si tu veux. Avant l'introduction des tables de vérité, ce non P ne veut rien dire, son existence est "implicite", hypothétique, ce que j'appelais un "fantôme", on lui impose de voir vérifier certaines propriétés mais peut-être n'existe t-il pas. Après les tables, non P devient explicite, réel, existant.
A fortiori, c'est avec ce non P bien défini - notons-le (non P)$_{LC}$ - que l'on démontre correctement que : non P <=> (P => tout). Les "démonstrations" de Gbzm et Cc, elles, s'appliquaient sur un fantôme, en pariant sur son existence. Si celui-ci n'existe pas, leur raisonnement prouvera tout et n'importe quoi.
2)
« Dès que tu définis non P en logique classique, alors tu utilises forcément le tiers-exclu et le RPA (par définition de la LC). »
C’est effrayant mais j’ai l’impression que ça c’est faux.
Une impression, car très peu aguerri.
Oui, ohlala, je crois que j'ai compris ce qui n'allait pas et je m'excuse de t'avoir brusqué en expliquant comme ça. Tu vas voir que c'est parfaitement limpide à comprendre : ferme d'abord les yeux, respire un instant...écoute ça quelques secondes :
Puis ouvre les yeux, doucement...Éteins la musique.
Bien, tu y es ?
Je reprends. Quand je dis que tu définis explicitement non P en LC, ça veut dire lui donner une expression explicite, une existence. Cette proposition non P doit vérifier tous les axiomes la concernant de la LC, dont le tiers-exclu, parce que les axiomes lui imposent cela. Point barre. Oui ou non ? Donc, toute définition explicite que tu vas proposer devra vérifier ces axiomes. Or, la définition par les tables de vérité est une telle définition explicite car elle vérifie (au moins) l'axiome du tiers-exclu : P ou non P, ou son équivalent RPA : non(non P) <=> P. Oui ou non ?
C'est en ce sens que je disais que toute définition explicite de non P utilise forcément le tiers-exclu et le RPA.
Ltav, dans ton discours qui va devenir un monologue un jour tu parles tout le temps de Tiers Exclu.
Dans les discours de Christophe et GaBuZoMeu, ils n’en parlent jamais.
L’approche n’est vraiment pas la même.
C'est parce que, comme je l'ai un peu expliqué, ils sont aveuglés par les axiomes de la LC ou la LI qui introduisent une entité indéfinie et implicite, "non P", un mot de quelques lettres, une simple étiquette, et raisonnent entièrement sur ce "fantôme" à l'existence hypothétique. Tandis que moi, je raisonne sur un non P explicite, en "chair et en os", si je puis dire, bien défini, existant, logiquement consistant : tables de vérité en LC, non P := (P => tout) en LI. Je raisonne sur les "vraies" démonstrations et les vrais concepts et négation utilisés en maths comme l'irrationalité de $\sqrt2$.
Il ne s'agit pas de deux visions différentes, à mon avis. Mais d'une approche inconsistante versus une approche correcte. Quand Cc dit par exemple qu'on définit non P par (P => tout) en LI parce qu'on sait démontrer que non P <=> (P => tout), [large]alors que non P n'est même pas encore défini[/large], c'est totalement faux, ce n'est même plus une vision personnelle mais une erreur logique de toute gravité (il n'en est pas à sa première, certes...). La réalité est complètement différente : on définit explicitement non P par (P => tout) parce que d'abord (P => tout) vérifie tous les axiomes que doit vérifier non P, et [large]c'est donc, à l'inverse, la bonne définition de non P par (P => tout) qui donne un sens à et valide la démonstration de non P <=> (P => tout).[/large]
Bon, ça c'est d'un autre degré de difficulté, tu pourras méditer ce paragraphe plus tard. Ne te laisse pas "impressionner" par la longueur de mes textes, ici je ne fais que répéter de différentes manières, avec des images, la même chose pour que tu comprennes. Il y a peu d'équations mathématiques dans ce débat, juste une nouvelle vision subtile à atteindre. Relis tranquillement...
[small]N.b. Quoi ? Tu n'avais pas éteint la musique ?[/small]
Méfie-toi, "ferme d'abord les yeux, respire un instant" était-il obligatoire ?
Tu peux te passer de ces conneries avec moi.
Tu n'as pas répondu à Christophe, est-ce volontaire ?
Je te cite : "on définit explicitement non P par (P => tout) parce que d'abord (P => tout) vérifie tous les axiomes que doit vérifier non P."
Lesquels ?
"et c'est donc, à l'inverse, la bonne définition de non P par (P => tout) qui donne un sens à et valide la démonstration de non P <=> (P => tout)".
Là c'est le pompon. Tu dis que définir A par B [...] valide la démonstration de A <=> B.
Ouf...
Méfie-toi, "ferme d'abord les yeux, respire un instant" était-il obligatoire ?
Tu peux te passer de ces conneries avec moi.
Tu n'as pas répondu à Christophe, est-ce volontaire ?
Qu'est-ce que tu racontes ?! Je voulais être sympa avec toi et j'étais sérieux en te demandant de te "vider l'esprit" (en gardant ton cerveau bien sûr) après tous ces échanges dans tous les sens de ce débat, pour mieux te concentrer sur ma réponse. Tu veux aussi devenir cynique plutôt que réfléchir ? De quelle question parles-tu ? J'espère que tu ne vas pas me soumettre à ton tour aux questions débiles paranoïaques à la Cc sans autre argument que ses ricaneries jaunes (mais lui c'est devenu pathologique, et Gbzm prend le même chemin), c'est de ça :
Mais tu crois abuser qui en rebondissant dur des virgules pendant 300 posts? Je pense que ce n'est pas toi même (ie tu sais ce que tu fais et es conscient de tes ruses) mais la quedtion EST QUI?
que tu parles et je vais perdre mon temps à y répondre...? Tu te moques de moi ?
Bien, reprenons calmement, mais je vais sûrement changer d'interlocuteur, je préfère les bonnes volontés - pas des gens qui veulent bien se faire voir par des "pense-petit" et des cinglés.
Je te cite : "on définit explicitement non P par (P => tout) parce que d'abord (P => tout) vérifie tous les axiomes que doit vérifier non P."
Lesquels ?
J'avais raison de te donner des conseils de re-concentration, tu as carrément oublié que j'avais déjà donné précisément ces axiomes quelques posts plus haut :
La condition ($P$ ou $\neg P$) fait obligatoirement partie de la démonstration de (non P <=> (P => tout)) si (non P) est bien définie. C'est aussi simple à prouver que ça.
J'espère que tu vois que ce que je raconte n'a strictement rien à voir avec cette bouillie que tu crois lire :
Réponses
Ici il m'a semblé qu'on parlait de choses sans savoir quelles étaient les définitions données.
Par exemple pour "parallélogramme", on peut donner plusieurs définitions puisqu'on a des caractérisations.
Bon, enfin, bref...
J'espère que Ltav aura vu mon message où je trouve une contradiction de ses propos.
Non P est une notion première. Comme on PEUT PROUVER même avec que de l'intuitionisme qu'elle équivaut à P=>tout , bien des gens présentent ensuite ça comme une abréviation.
J’ai l’impression que les échanges avec Ltav cachent de temps en temps ce genre de quiproquo. Chacun part de sa propre construction de la LC et du coup ça s’étend en échanges interminables alors que les présupposés ne sont peut-être pas les mêmes.
Bien étendu, ce ne doit pas être que ça. L’enfumage dénoncé par GaBuZoMeu relève d’autre chose.
C’est dramatique, mais c’est moi qui vais demander que chacun expose sa façon de définir la LC et la LI.
On pourrait alors travailler sur les équivalences entre les partis pris (RPA, TE, etc.).
Ça va faire répéter chacun une 48274722738e fois quelque chose, j’en conviens.
@Dom : il n'y a aucune contradiction et la réponse de Martial répond parfaitement à ton questionnement. Aucun ensorcellement non plus (ce genre de propos devient lassant). A partir du moment où tu démontres qu'une proposition est équivalente à une autre, tu peux la prendre sans problème comme définition. Encore faut-il que l'autre soit bien définie. Tout le problème est là.
Je vais répondre précisément et aussi brièvement que possible aux autres "arguments" de nos amis.
J'avais relevé : (j'ai remanié les dialogues dans la manières que je les ai comprises, ainsi les propos ne sont pas exactement les mêmes). Au lieu de dire "on définit", j'utilise le symbole :=.
---début du dialogue
Moi, en gros : En L.I. et en L.C., pour tout P, non(P):=(P=>Tout).
Ltav, en gros : Non,
En LC, non(P) := la proposition qui a une table de vérité opposée à celle de P.
On en déduit alors que non P <=> (P => tout).
En LI, non(P) := (P => tout).
Moi :
Ainsi tu nies qu’on a : non(P) := (P=>Tout) en LC ?
Sans s’occuper des tables de vérité ?
Ltav :
En LC, il est tout à fait possible de prendre cette définition.
---fin du dialogue---
Bon, ok, je comprends donc que quand tu parlais de table de vérité, ce n'était pas obligatoire pour définir ce "non".
On obtient toutefois un truc équivalent.
Je rebondis sur le propos de Christophe : "non" est une notion première.
Bon, c'est quoi alors ?
Oui, je ne comprends rien. J'ai l'impression que tantôt c'est ceci qu'on choisit (j'ai lu ça dans un message), tantôt c'est autre chose. D'où mes tergiversations.
En fait ton dernier post montre que tu as tout compris.
C'est juste qu'il faut que tu prennes une bonne douche pour te désenfumer, lol.
Je ne donnerai pas ma définition de la LI, car je ne suis pas suffisamment expert dans ce domaine, et je n'ai pas envie de raconter des conneries, on en a suffisamment lu comme ça.
D'autres le feront mieux que moi, j'en suis sûr.
Dans la logique classique ou intuitionniste, je l'ai déjà précisé, non P n'est pas définie explicitement mais doit obéir à certains axiomes bien précis. Il y a donc quelque part la définition des propriétés que doit vérifier une éventuelle non P : en LC ou LI, non P c'est toute proposition d'un ensemble S vérifiant ces axiomes. A partir de là, on peut démontrer, comme l'ont fait Cc et Gbzm que non P <=> (P => tout). Autrement dit, si non P appartient à S, alors ces démonstrations sont correctes. Oui ou non ?
Mais existe t-il une seule proposition réalisant ces propriétés ? Que se passerait-il si S était l'ensemble vide ? S'il était vide (en ce cas, aucune non P ne peut appartenir à S : ma condition soulignée n'est plus vérifiée) alors leurs "démonstrations" prouveraient tout et son contraire, plus rien ne garantirait leur validité.
Bien, à ce problème grave et très précis de logique, voici le genre de réponse à la Cc/Gbzm qui se dégage en substance : "il n'y a pas besoin de définir non P, c'est une notion première, nos démonstrations sur non P sont correctes sans avoir besoin de définir non P, etc.". Eh bien, dois-je le répéter : c'est totalement faux et je viens de le prouver.
Heureusement les logiciens de la LC et de la LI ont très bien compris ce problème et défini des propositions consistantes vérifiant les axiomes de non P. Ils ont "rempli" de matière logique ce qui n'était peut-être qu'un pur symbole vide (je sais, je poétise là). En LC, cette définition de non P (tables de vérité opposée à P) se base obligatoirement sur le tiers-exclu puisque par définition non P doit le vérifier en LC. En LI, non P ne vérifie plus le tiers-exclu, il fallait donc trouver autre chose : on a alors proposé non P := (P => tout), pas pour faire joli ou aller vite mais parce que cette définition réussissait à vérifier les axiomes liés à "non P" en LI (LC moins tiers-exclu), sans avoir besoin du tiers-exclu.
J'ai encore été trop long...! Pour résumer grossièrement, en LC et LI, on ne démontre pas tout seul :
non P <=> (P => tout)
Mais avec au moins une condition devant (j'ai défini S plus haut) :
(non P $\in $ S) => (non P <=> (P => tout))
Sans définition de non P par une proposition consistante, rien ne garantit que S ne soit pas vide, et la condition n'est plus vérifiée. Bien sûr ça ne va pas gêner certains logiciens vides. Mais des mathématiciens, si. Il ne suffit plus d'utiliser des symboles "étiquettes" quand on veut appliquer une axiomatique à nos raisonnements de tous les jours (comme avec "$\sqrt2$ irrationnelle, etc.), on ne veut pas parler dans le vide. Il faut des propositions réelles vérifiant ces axiomes.
Le tiers-exclu est inévitable en LC dès le moment où l'on veut légitimement définir un non P vérifiant les axiomes de LC dont le tiers-exclu. C'est une évidence. Et il est a fortiori inévitable dans la démonstration de non P <=> (P => tout) avec un non P bien défini, "non vide". En LI, on ne doit plus utiliser le tiers-exclu : il est donc inévitable de devoir changer la définition classique de non P.
Cc et Gbzm n'ont simplement jamais réfléchi à ces considérations.
N.b. ah, Cc : restons sur notre sujet et évitons de discuter AO ici. Nos derniers débats, où j'avais démontré que tu avais attaqué à tort la validité logique de l'AO (et où tu changeais poétiquement à ta guise le sens d'un même mot), ont été assez éloquents. Les lecteurs intéressés pourront juger par eux-mêmes.
Bonne soirée.
Difficilement de mon téléphone.
Bigre, ce fil me plaît : pas trop de bazar, quelques chagrinades dues aux écrits et donc aux quiproquos.
Allez ! On se concentre, moi le premier.
Édit : je n’avais pas ton dernier message, Ltav.
Édit : Dis-moi Martial, as-tu un document référence ?
Un site, un pdf, un bouquin ?
Je suis très très novice d’une part et en ce moment, c’est davantage pour ma culture générale et du loisir.
J’entends un document qui définit proprement le début du début en LC et/ou en LI.
Là, c’est difficile de retracer les liens adjacents. Je suis certain qu’en recoupant tout on aurait un truc extra mais c’est fastidieux.
Je me demande même si je ne vais pas (quand ?) taper un truc quitte à le modifier pour que ce soit propre, succinct et exhaustif. Tout ça grâce aux échanges.
1/ Soit blabla une structure (un quadruplet $(a,b,c,d)$ ) vérifiant blabla
2/ Théorème: dans ces conditions $a=c$
3/ Dorénavant, on donnera ce nom à $(a,b,c)$ et, au besoin, on se réfèrera à l'ancienne définition en parlant de $(a,b,a,c)$
? :-D
Par exemple:
1/ On appelle bidule un triplet $(E,\leq, non)$ où
1.1/ $\leq$ est un ordre sur $E$ tel que toute partie a une borne sup (donc un plus grand élément $1$ et un plus petit éléments $0$.
1.2/ Pour tout $a,b$ la borne supérieure de $A:=\{x\in E \mid inf(a,x) \leq b\}$ est un élément de $A$, noté $(a\to b)$
1.3/ non est une application décroissante de $E$ dans $E$ vérifiant: blabla.
2/ Théorème: pour tout $x\in E: (non(x) = (x\to 0))$
Dorénavant, on appellera "algèbre de Heyting complète" un couple $(E,\leq)$ tel que $(E,\leq , [x\mapsto (x\mapsto 0)])$ est un bidule.
La logique intuitionniste est le produit de toutes les algèbres de Heyting, ou, si tu préfères l'ensemble des expressions dont toute interprétation dans toute algèbre de Heyting vaut $1$.
Ensuite tu as le théorème suivant:
Soit $(E,\leq)$ une algèbre de Heyting. Alors elle est une algèbre de Boole si et seulement si $non$ est injective. Ce qui a entre pour conséquence que $\forall x\in E: [x = (non(non(x)))]$
Je pense que tu avais très bien compris en fait, mais bon...
En fait, je comprends des choses mais je ne « fixe » pas, faute de les récrire, de les travailler, de me les approprier.
Ça en devient pénible pour mes interlocuteurs (ça ne t’épargne pas ;-)).
Mea Culpa chers intervenants, merci de votre gratitude et patience.
C'est moi qui ai mis en rouge les passages.
Peut-être peux-tu voir plus facilement les choses en termes de définitions premières et secondaires (à distinguer des notions premières de Cc qu'il semble voir comme non définissables).
la logique intuitionniste est juste l'ensemble des propositions obtenues comme suit:
1/ j'abrège la phrase $Q:=A_1\to (A_2\to (\dot (A_n\to x) )\dots )$ par $A_1;A_2;\dots \vdash x$. Les $A_i$ sont appelées hypothèses de la phrase $Q$.
2/ Les axiomes sont les phrases où la conclusion $x$ figure parmi les hypothèses.
3/ partant d'une phrase déjà prouvée, tu peux:
3.1/ permuter ses hypothèses
3.2/ Contracter quand répétition. Autrement dit considérer comme théorème $..;A;..\vdash x$ quand $..;A;A;..\vdash x$ en est un.
3.3/ virer une hypothèse si par ailleurs tu sais que c'est un théorème que tu as déjà prouvé.
3.4/ Remplacer $A_1;A_2;\dots ; ..;U;V;..\vdash x$ par $A_1;A_2;\dots ; ..;(U\wedge V);.. \vdash x$ et réciproquement)
3.5/ Considérer $L+M\vdash (A\wedge
4/ Je te laisse ajouter des règles pour "ou" et "non".
Mais le plus important, ne cherche pas à retenir par coeur. Tout passage au "cas particulier" génère un théorème intuitionniste et réciproquement à ceci près que :
4.1/ le "A =>(A et A)" va générer des choses non triviales (mais qui le deviennent si tu gardes "A et A" à la place de A
4.2/ Tu t'autorises à considérer que A=>B est un cas particulier de B (ou si tu préfères que A et un cas particulier de A et
5/ En fait à (4.1) près la logique intuitionniste dit qu'un énoncé est un théorème ssi il est pseudo-trivial.
6/ "P est pseudo-trivialé veut dire il existe une application $f$ et une trivialité pure $Q$ tel que $P$ s'obtient en remplaçant chaque lettre $x$ (variable) dans $Q$ par $f(x)$.
7/ Je pense que tu vois bien que le raisonnement par l'absurde "ajoute quelque chose", non? Tu vois bien qu'il n'y a aucun moyen de l'obtenir comme ça?
Je te donne une autre description si tu veux :
On part des évidences pures (phrase où la conclusion figure parmi ses hypothèses) et on les conjoncte au sens large:
1/ On peut s'autoriser une conjonction des $(A_i\to B_i)$ comme suit: $(\bigwedge_i A_i)\to (\bigwedge_i B_i)$
2/ Et on considère $(A\to (B\to C)=((A\wedge
3/ On considère que $A=(A\wedge A)$
ET RIEN DE PLUS
Autre remarque: tu sera peut-être frustré que je ne parle pas de "ou" (ni avec bcp d'estime de $\wedge$ (et)). Cela provient de la polarité logique:
1/ pour savoir si $R(a\vee b)$ est un théorème et que l’occurrence de $(a\vee b)$ est positive, il suffit de se demander si
$[(a\to x) \wedge (b\to x)]\to R(x)$ en est un (avec $x$ fresh variable of course)
2/ pour savoir si $R(a\vee b)$ est un théorème et que l’occurrence de $(a\vee b)$ est négative, il suffit de se demander si $R(a)$ ainsi que $R(b)$ en sont, etc
Tout ceci, tu peux le faire tout seul. En gros, la seule chose qui manque à la logique intuitionniste pour être classique, c'est juste l'injectivité de la fonction qui à $X$ associe $X\to tout$.
Et il semble trop difficile de t'expliquer comment les parcours de débutants sont toujours un peu les mêmes, avec les mêmes pièges, les mêmes "inspirations" et les mêmes bisounourseries. Tu es attendrissant en apprenant (très doucement***), te plantant sans arrêt, rebifurquant sans cesse pour cacher ces plantes, etc
*** Le problème étant que PERSONNE, je dis bien PERSONNE ne comprend pourquoi, vu que tu es anonyme, tu n'avoue tout simplement pas que tu es béotien et que tu aimerais progresser. Du coup, tu passes 90% de tes posts à patauger pour planquer (sans aucun succès) que tu n'y connais rien, mais en plus que tu comprends très mal (et il n'y a pas de honte) et 10% à "améliorer" ta connaissance de telle ou telle petite information sans trop savoir si elle est importante. C'est vraiment du gâchis.
Cc, tu démontres une fois de plus ton incapacité à comprendre les phrases d'autrui (de là à interpréter leurs pensées)...
Je réécris mes phrases pour toi :
Et il (le tiers-exclu) est a fortiori inévitable dans la démonstration de (non P)$_{LC}$ <=> (P => tout) avec un non P bien défini [comme le veulent les axiomes LC], "non vide".
En LI, on ne doit plus utiliser le tiers-exclu [dans (non P)$_{LI}$ <=> (P => tout)]
Toute ta carrière de logicien t'a mené à ne plus comprendre des subtilités aussi basiques et à voir des contradictions imaginaires. C'est encore plus dommage.
** Étant sur mon téléphone
@Dom : merci, je dois avouer aussi que nous sommes contents de t'avoir comme fidèle compagnon à tous ces débats, dans ce rôle difficile - et ingrat - d'observateur, voire d'arbitre, scientifique, mais qui te plaît et que tu réussis malgré tout avec un certain talent.
@Cc (*) : tu sors "l'artillerie lourde" (si lourde qu'elle s'enraye...) pour expliquer comment tu définis la négation d'une proposition...? Tu as parlé de travailler avec des "notions premières", peux-tu préciser ce que tu entends personnellement par là ? A partir de quel moment as-tu besoin de les définir ? Est-il possible qu'elles ne correspondent à rien d'existant mathématiquement et invalident tes démonstrations en LC ou LI ?
http://www.les-mathematiques.net/phorum/read.php?16,1880930,1894780#msg-1894780
J'espère que tu as compris que tout mon discours se plaçait en aval de l'acte de définition explicite de non P en LC. L'amont ne m'intéresse pas mais doit surtout être évité par les mathématiciens, puisque non P n'y est qu'une étiquette vide pouvant cacher un concept contradictoire invalidant tous les raisonnements. Cette définition explicite doit par principe vérifier le tiers-exclu.
- Une fois (non P)$_{LI}$ définie en LC, on a bien grâce au T-E (je te précise l'indice pour éviter tes risques de confusion) le théorème qui avait été "démontré en sursis" avec l'étiquette vide non P (en attendant de lui donner une "âme" consistante) :
(non P)$_{LC}$ <=> (P => tout)
Dès qu'il y a définition de non P, il y a tiers-exclu, c'est obligatoire par définition : cet axiome T-E est derrière tous les théorèmes de LC concernant non P.
- En LI, idem : avant la définition explicite de non P, non P ne veut rien dire, voire pire : rien ne garantit la validité de nos raisonnements avec non P. En posant (non P)$_{LI}$ := (P => $\bot$), on voit qu'elle vérifie les axiomes de la LI. D'où la validité cette fois réelle (sans "étiquette vide" non P) du théorème :
(non P)$_{LI}$ <=> (P => tout)
Ainsi dans nos raisonnements sur l'irrationalité de $\sqrt2$ ("non P"), crois-tu que les termes (non-rationnel, etc.) ne sont pas définis ou utilise-t-on des "étiquettes vides" ? Puisqu'ils sont bien définis, tu comprendras alors que le tiers-exclu est partout (explicitement ou non) dans les théorèmes LC. C'est précisément ce que j'expliquais - sous tes pitreries dans la semoule.
Pour l'éviter, il faut changer de définition (et de logique) et passer en intuitionniste : désormais, ("$\sqrt2$ est irrationnelle")$_{LI}$ s'entend (et il faut le préciser) comme "la rationalité de $\sqrt2$ mène à une contradiction".
Bonne nuit.
[small](*) Tu as encore balancé ton ineptie sur l'AO. Exemple : "si x est ceci et x est cela, alors x existe". Pourquoi diable voudrais-tu changer cette phrase en "si x est ceci et y est cela, alors z existe, pour x=y=z" ?? Tu ne comprends toujours pas que c'est la règle contraire à la tienne qui s'impose en logique, mathématique, linguistique, etc. : deux mêmes mots ont le même sens sauf indication contraire. Sinon tu fais de la poésie. Ton entêtement est incroyable (pour paraphraser le lexique religieux). J'ai encore de quoi alimenter ton fil de l'arroseur arrosé ;-)[/small]
Contrairement à ce que tu crois ce que tu racontes est très simple et "habituel" dans les parcours beotiens d'initiation. Mais cette posture "je suis le meilleur je sais tout" ne te sert pas dans la motivation des autres à t'informer. De mon téléphone
O.k. je vais faire le novice. Supposons que je vous dise : super j'ai démontré que
(Bidule chouette rose violet) <=> 1+2=3
Ma démonstration est-elle correcte ou non ? Non, bien sûr vous me direz qu'elle est mal définie, tant que "Bidule chouette rose violet" n'est pas défini.
Hé bien, vos démontrations de non P <=> (P => tout) sont mal définies Gbzm et Cc puisque vous reconnaissez que non P n'est pas défini. Et qu'il est certain que dans les démonstrations courantes sur l'irrationalité de la racine de 2, les termes ont été définis auparavant. C'est de la sorcellerie ça ?
Mon objection est parfaitement mathématique : vos démontrations sont mal définies donc ne sont pas plus des démonstrations que celle sur bidule chouette rose violet. Tout le monde peut le vérifier immédiatement. Je vous mets au défi de montrer le contraire.
D'ailleurs, parfois je les lasse aussi car je repose les mêmes questions.
Toi, Ltav, tu demandes à ces messieurs "Que prenez-vous alors pour définition-départ de $non(.)$, si ce n'est pas $P\Rightarrow Tout$ ?". Moi j'avais compris qu'on prenait cela comme définition.
Et je pense même pouvoir retrouver un message où c'est ce que l'on choisit.
N'est-ce pas cela ta question ?
Une réponse très très récente de Christophe a été : c'est une notion primitive.
Et ensuite, j'ai compris qu'on voulait juste que cette notion primitive vérifient quelques axiomes.
Ltav, demandes-tu quels sont ces axiomes ?
En fait, je ne posais pas vraiment de question dans mon post, je maintenais que leurs démonstrations n'en étaient pas au sens où l'on démontre que la racine de 2 est irrationnelle.
Et dire que « ne pas être irrationnelle » entraîne « être rationnelle », c’est appliquer le RPA en LC.
Reprends la preuve classique : supposons qu'il existe un rationnel x tel que $x^{2}=2$.
Alors blablabla, et on arrive à antitruc.
Moralité, on a prouvé que (racine de 2 rationnel) implique antitruc, ce qui est exactement la définition de non(racine de 2 est rationnel).
Il n'y a pas de RPA là-dedans.
J'ai l'impression que ce qui te pose problème c'est de déduire "x est irrationnel" de "non(x est rationnel)". Là encore c'est une définition. C'est comme si la police démontre qu'à l'instant du meurtre le tueur ne pouvait pas être à l'intérieur de la maison de la victime. C'est donc qu'il était à l'extérieur, défini comme tout ce qui n'est pas à l'intérieur.
Si ça peut t'aider remets-toi dans le contexte de Pythagore, qui ne connaissait que les nombres rationnels, qu'il appelait d'ailleurs "nombres", pensant que c'étaient les seuls existants. Un jour il démontre qu'il n'existe pas de nombre $x$ dont le carré soit égal à 2. Et puis une semaine plus tard, en dessinant un triangle rectangle isocèle de côté 1 il s'aperçoit (grâce à un précédent théorème) que le carré de l'hypoténuse est égal à 2. Cela lui pose problème, car cette hypoténuse est une grandeur palpable, que l'on peut par exemple reporter avec un compas. Il en déduit qu'il existe des grandeurs qui ne sont pas des nombres, d'où le nom de grandeurs irrationnelles. Toujours pas de RPA là-dedans.
Je crois que pour ta santé mentale tu devrais faire comme GBZM : ne plus répondre aux messages de Ltav, voire même ne plus les lire, sinon tu vas devenir ouf.
Ce que tu viens de démontrer est selon cette définition : "racine de 2 est irrationnelle" implique "racine de 2 est irrationnelle".
Ha zut, tu t'es fait avoir Martial.
J'ai bien compris : $(r \in \mathbb Q \Rightarrow Tout) \Rightarrow r \notin \mathbb Q$ sans RPA.
J'avais rédigé un raisonnement qui utilise tout de même le RPA.
C'est tarabiscoté, c'est inutile, c'est pompeux, mais c'est juste de qualifier le raisonnement suivant de raisonnement par l'absurde.
Mon cher Martial, tu vas voir... tu me diras si ça te convient.
Je parle aussi sous le contrôle de tous les intervenants, bien sûr.
Début de la preuve de : $(r^2=2$ et $r>0) \Rightarrow r \notin \mathbb Q$
On va démontrer cela par l'absurde.
On suppose : $non($ $(r^2=2$ et $r>0) \Rightarrow r \notin \mathbb Q))$ (***)
C'est-à-dire : $(r^2=2$ et $r>0) \ et \ non(r \notin \mathbb Q)$.
C'est-à-dire : $(r^2=2$ et $r>0) \ et \ \color{red}{non(non(r \in \mathbb Q))}$.
$\color{red}{}$
J'applique l'axiome RPA à la partie rouge, j'en déduis :
$(r^2=2$ et $r>0) \ et \ \color{red}{r \in \mathbb Q))}$.
J'obtiens avec les calculs classiques vus partout un antitruc.
C'est-à-dire : (***) => $Tout$
Je viens de démontrer :
$non(non($ $(r^2=2$ et $r>0) \Rightarrow r \notin \mathbb Q)))$
J'applique l'axiome RPA, j'en déduis :
$(r^2=2$ et $r>0) \Rightarrow r \notin \mathbb Q)$
Fin de la preuve de : $(r^2=2$ et $r>0) \Rightarrow r \notin \mathbb Q$
Qui démonte cette preuve ?
Le seul truc que je n'ai pas bien travaillé, c'est la négation du "ou" qui devient un "et" des négations (De Morgan, en gros). Je veux dire : je ne sais pas d'où on part pour démontrer les lois de De Morgan.
Cordialement
Dom
non(P ou Q) <=> (non P et non Q),
est démontrable même en logique intuitionniste. L'autre loi de De Morgan ne l'est qu'en classique :
non(P et Q) <=> (non P ou non Q).
(*) du fait que A => B est équivalente à (B ou non A).
Dès que tu définis non P en logique classique, alors tu utilises forcément le tiers-exclu et le RPA (par définition de la LC).
des 4 lois de de Morgan (obtenues en ne prenant que les implications des 2 équivalences), la seule qui est fausse en LI est
non(P et Q) IMPLIQUE (nonP ou nonQ).
Donc ton raisonnement tient la route.
Mais tu le reconnaîtras aisément, c'est dégainer une Kalashnikov pour enc… une mouche.
C'est comme les mecs qui démontrent Tychonoff, AC à l'appui, pour en déduire qu'un produit de 2 compacts est compact !!!
Et c'est comme les mecs qui trouvent le moyen d'utiliser AC pour démontrer Cantor-Bernstein (là, MDR).
Pas du dernier, qui s'est croisé avec le mien, et auquel je n'ai rien compris.
En effet je ne sais pas à qui s’adresse le « quand TU dis ».
Ce que je raconte est très simple. Pour commencer, ça ne te gêne pas toi que nos deux amis Cc (:-D) et Gbzm (:-X) prétendent démontrer un pseudo-théorème T sur bidule chouette rose violet alias "non P" ?
Bidule chouette rose violet <=> (P => tout)
Or le théorème complet est :
Pour tout bidule chouette rose violet vérifiant certains axiomes alors :
Bidule chouette rose violet <=> (P => tout)
Donc si l'ensemble des propositions vérifiant ces axiomes est vide, alors T n'est plus garanti. Leur démonstration est donc fausse. Pour la rendre valide, on donne justement une définition explicite d'un bidule chouette rose violet vérifiant vraiment ces axiomes (suivant les cas : (non P)$_{LC}$ ou (non P)$_{LI}$).
C'est si dur à comprendre ? Tout théorème de maths sérieux portant sur un nouvel objet commence par démontrer que l'ensemble de ces objets n'est pas vide.
Pour info, pour les lecteurs,des que Ltav dit quelque chose autre que de la langue de bois ca ne rate quasiment jamais c'est une connerie assez spectaculaire. C'est assez génial de l'avoir sur ce forum. Il offre un anti modèle de bluffage en science que personne n'espererait même décrire à ce point exhaustivement. Je ne sais pas s'il en est conscient (c'est toujours dur de se voir soi même avec des yeux extérieurs) je ne pense pas mais ça peut expliquer aussi qu'il s'enferme de plus en plus dans la LDB.
1)
Enfin, je veux dire que pour moi, depuis le début de mon investissement (très léger) dans ce domaine, j’accepte la définition du $non(P)$ par $P=>Tout$.
Je ne sais toujours pas ce qu’est le $non$ sans ça.
Et je n’aime pas l’approche « table de vérité ».
Bref.
2)
« Dès que tu définis non P en logique classique, alors tu utilises forcément le tiers-exclu et le RPA (par définition de la LC). »
C’est effrayant mais j’ai l’impression que ça c’est faux.
Une impression, car très peu aguerri.
Ltav, dans ton discours qui va devenir un monologue un jour tu parles tout le temps de Tiers Exclu.
Dans les discours de Christophe et GaBuZoMeu, ils n’en parlent jamais.
L’approche n’est vraiment pas la même.
Ha ? Une question de Christophe.
La réponse m’intéresse !!!
Si tu n'aimes pas hélas, c'est que quelque chose cloche encore un peu dans ta compréhension. Pourquoi changer les définitions "officielles" de la LC avant d'avoir parfaitement compris ses raisons ? C'est grâce au tiers-exclu et à ses tables de vérité sous-jacentes que l'on définit explicitement non P, qu'on lui donne une existence si tu veux. Avant l'introduction des tables de vérité, ce non P ne veut rien dire, son existence est "implicite", hypothétique, ce que j'appelais un "fantôme", on lui impose de voir vérifier certaines propriétés mais peut-être n'existe t-il pas. Après les tables, non P devient explicite, réel, existant.
A fortiori, c'est avec ce non P bien défini - notons-le (non P)$_{LC}$ - que l'on démontre correctement que : non P <=> (P => tout). Les "démonstrations" de Gbzm et Cc, elles, s'appliquaient sur un fantôme, en pariant sur son existence. Si celui-ci n'existe pas, leur raisonnement prouvera tout et n'importe quoi.
Oui, ohlala, je crois que j'ai compris ce qui n'allait pas et je m'excuse de t'avoir brusqué en expliquant comme ça. Tu vas voir que c'est parfaitement limpide à comprendre : ferme d'abord les yeux, respire un instant...écoute ça quelques secondes :
Puis ouvre les yeux, doucement...Éteins la musique.
Bien, tu y es ?
Je reprends. Quand je dis que tu définis explicitement non P en LC, ça veut dire lui donner une expression explicite, une existence. Cette proposition non P doit vérifier tous les axiomes la concernant de la LC, dont le tiers-exclu, parce que les axiomes lui imposent cela. Point barre. Oui ou non ? Donc, toute définition explicite que tu vas proposer devra vérifier ces axiomes. Or, la définition par les tables de vérité est une telle définition explicite car elle vérifie (au moins) l'axiome du tiers-exclu : P ou non P, ou son équivalent RPA : non(non P) <=> P. Oui ou non ?
C'est en ce sens que je disais que toute définition explicite de non P utilise forcément le tiers-exclu et le RPA.
C'est parce que, comme je l'ai un peu expliqué, ils sont aveuglés par les axiomes de la LC ou la LI qui introduisent une entité indéfinie et implicite, "non P", un mot de quelques lettres, une simple étiquette, et raisonnent entièrement sur ce "fantôme" à l'existence hypothétique. Tandis que moi, je raisonne sur un non P explicite, en "chair et en os", si je puis dire, bien défini, existant, logiquement consistant : tables de vérité en LC, non P := (P => tout) en LI. Je raisonne sur les "vraies" démonstrations et les vrais concepts et négation utilisés en maths comme l'irrationalité de $\sqrt2$.
Il ne s'agit pas de deux visions différentes, à mon avis. Mais d'une approche inconsistante versus une approche correcte. Quand Cc dit par exemple qu'on définit non P par (P => tout) en LI parce qu'on sait démontrer que non P <=> (P => tout), [large]alors que non P n'est même pas encore défini[/large], c'est totalement faux, ce n'est même plus une vision personnelle mais une erreur logique de toute gravité (il n'en est pas à sa première, certes...). La réalité est complètement différente : on définit explicitement non P par (P => tout) parce que d'abord (P => tout) vérifie tous les axiomes que doit vérifier non P, et [large]c'est donc, à l'inverse, la bonne définition de non P par (P => tout) qui donne un sens à et valide la démonstration de non P <=> (P => tout).[/large]
Bon, ça c'est d'un autre degré de difficulté, tu pourras méditer ce paragraphe plus tard. Ne te laisse pas "impressionner" par la longueur de mes textes, ici je ne fais que répéter de différentes manières, avec des images, la même chose pour que tu comprennes. Il y a peu d'équations mathématiques dans ce débat, juste une nouvelle vision subtile à atteindre. Relis tranquillement...
[small]N.b. Quoi ? Tu n'avais pas éteint la musique ?[/small]
Tu peux te passer de ces conneries avec moi.
Tu n'as pas répondu à Christophe, est-ce volontaire ?
Je te cite : "on définit explicitement non P par (P => tout) parce que d'abord (P => tout) vérifie tous les axiomes que doit vérifier non P."
Lesquels ?
"et c'est donc, à l'inverse, la bonne définition de non P par (P => tout) qui donne un sens à et valide la démonstration de non P <=> (P => tout)".
Là c'est le pompon. Tu dis que définir A par B [...] valide la démonstration de A <=> B.
Ouf...
Quelle perte de temps...
Qu'est-ce que tu racontes ?! Je voulais être sympa avec toi et j'étais sérieux en te demandant de te "vider l'esprit" (en gardant ton cerveau bien sûr) après tous ces échanges dans tous les sens de ce débat, pour mieux te concentrer sur ma réponse. Tu veux aussi devenir cynique plutôt que réfléchir ? De quelle question parles-tu ? J'espère que tu ne vas pas me soumettre à ton tour aux questions débiles paranoïaques à la Cc sans autre argument que ses ricaneries jaunes (mais lui c'est devenu pathologique, et Gbzm prend le même chemin), c'est de ça :
que tu parles et je vais perdre mon temps à y répondre...? Tu te moques de moi ?
Bien, reprenons calmement, mais je vais sûrement changer d'interlocuteur, je préfère les bonnes volontés - pas des gens qui veulent bien se faire voir par des "pense-petit" et des cinglés.
J'avais raison de te donner des conseils de re-concentration, tu as carrément oublié que j'avais déjà donné précisément ces axiomes quelques posts plus haut :
http://www.les-mathematiques.net/phorum/read.php?16,1880930,1894432#msg-1894432
Toute proposition non P bien définie devant vérifier le tiers-exclu, on a bien obligatoirement par définition de non P :
($P$ ou $\neg P$) => (non P <=> (P => tout))
Je préfère l'écrire comme ça pour bien voir que non P a été bien définie explicitement :
($P$ ou $\neg P$) => ((non P)$_{LC}$ <=> (P => tout))
La condition ($P$ ou $\neg P$) fait obligatoirement partie de la démonstration de (non P <=> (P => tout)) si (non P) est bien définie. C'est aussi simple à prouver que ça.
J'espère que tu vois que ce que je raconte n'a strictement rien à voir avec cette bouillie que tu crois lire :
Oui quelle perte de temps...mais tu ne sais pas pour qui.
Bonne journée.