Une section du faisceau $F$ sur $U$, c'est simplement un élément de $F(U)$, un sous-faisceau d'un faisceau $F$ c'est un faisceau $G$ tel que $G(U)\subset F(U)$ pour tout ouvert $U$, la fibre du faisceau $F$ en $x$ est la limite inductive des $F(U)$ pour $U$ voisinage ouvert de $x$ : un élément de la fibre est représenté par une section $s\in F(U)$ où $U$ est un voisinage ouvert de $x$, et $t\in F(V)$ représente le même élément de la fibre si et seulement s'il existe un voisinage ouvert $W$ de $x$ tel que les restrictions de $s$ et $t$ à $W$ soient égales.
Si $F(U)$ est défini comme l'ensemble des fonctions $U\to \mathbb R$ possédant une certaine propriété de caractère local (être continue, être localement constante), il est évident d'après la définition rappelée par Maxtimax que $F$ est un faisceau.
Petit exercice pratique pour Christophe : au lieu de travailler comme précédemment avec le compactifié d'Alexandrov de $\mathbb N$, on va travailler avec son compactifié de Stone-Cech $\beta\mathbb N$ qui est l'ensemble des ultrafiltres de parties de $\mathbb N$, où un élément de $\mathbb N$ est identifié à l'ultrafiltre des parties qui le contiennent ; la topologie de ce compactifié a une base d'ouverts quasi compacts formée des $\widehat A=\{\mathcal U \in \beta\mathbb N\mid A \in \mathcal U\}$ pour $A$ partie de $\mathbb N$.
Pour se donner un faisceau sur $\beta\mathbb N$, il suffit de préciser ses sections sur le ouverts de base $\widehat A$.
Le faisceau de fonctions continues à valeurs réelles $\mathbb R_{\beta\mathbb N}$ a pour sections sur $\widehat A$ les suites bornées de nombres réels indexées par $A$ : vérifier qu'une telle suite se prolonge de manière unique en une fonction continue $\widehat A\to \mathbb R$.
C'est un sous-faisceau du faisceau dont les sections sur $\widehat A$ sont toutes les suites de nombres réels indexées par $A$. Exercice (facile) : montrer que la fibre de ce faisceau en un $\mathcal U\in \beta\mathbb N$ est l'ultrapuissance de $\mathbb R$ par rapport à $\mathcal U$. Un faisceau dont les fibres sont les ultrapuissances, voila qui devrait te faire plaisir, Christophe !
Merci oui j'ai le projet de le faire complètement cet exercice. Mais il me faut acquérir des mots (fibre, sous faisceau,..) et une vue de l'isomorphisme entre ton corpus et celui de Max. J'ai créé un fil "patient" pour cette acquisition.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Décidément ça me déprime : à chaque fois que je pense avoir enfin tout compris, je m'aperçois un peu plus tard qu'il me manque un maillon de la chaîne.
Je n'ai pas bien compris la preuve par Georges Abitbol (vers le haut de la page 2 de la discussion) du fait que (P implique antitruc) implique non P. (Dans l'autre sens ça va).
Je sais bien qu'on peut prendre ça comme définition du "non", mais quand même j'aimerais bien comprendre l'argument.
Si quelqu'un pouvait développer un peu…
Merci d'avance
GBZM, si je peux me permettre, il y aura toujours un malaise si tu t'y prends comme ça pour démontrer non P. On démontre quelque chose qu'on a défini d'abord. Comment définis-tu non P en logique intuitionniste ? Prends s'il te plaît un exemple très concret, comme non P := "la racine de 2 n'est pas rationnelle". Que devient, en bon français, cette proposition en logique intuitionniste ? Par exemple, je dirais en prenant la définition intuitionniste non P := (P => tout), que la proposition "La racine de 2 n'est pas rationnelle" n'est qu'une abréviation en LI de : "Supposer la rationalité de la racine de 2 mène à l'absurde". Or, c'est compliqué de le dire comme ça, il est évident que personne ne définit spontanément l'irrationalité de racine de 2 de cette manière.
En logique classique, la définition de non P est très simple, c'est le contraire (valeur de vérité opposée) de P. Connais-tu une définition aussi simple, traduisible en bon français, de non P en logique intuitionniste ?
(je me permets, même si je n’y connais rien)
Je ne vois pas le problème Ltav. Tu sembles poser une question mais tu y réponds apparemment.
Le « c’est compliqué de le dire comme ça » n’est que psychologique. Qu’est-ce qu’on se fout du caractère « compliqué » d’une proposition ?
Pourquoi les maths seraient simples dans les énoncés en français ?
Ou alors je n’ai pas compris ce que tu veux dire.
@Dom : La question : "quelle définition intuitionniste de non P utilises-tu avant de démontrer non P ?" a un intérêt parfaitement mathématique.
Ensuite, la question d'utiliser une définition la plus proche possible de celle qu'utilisent les gens qui démontrent l'irrationalité de la racine de 2 a également une importance sémantique et logique dans la traduction formelle de ce raisonnement.
Si on pense que les gens raisonnent en mode intuitionniste (sans tiers-exclu) pour démontrer non P, alors il faut justifier qu'ils utilisent également une définition intuitionniste de non P, qu'ils sont en "mode intuitionniste jusqu'au bout". Or je n'ai jamais vu personne poser la définition "racine de 2 irrationnelle" := ("racine de 2 rationnelle" => tout) avant de démontrer l'irrationalité de $\sqrt{2}$. Je demande donc, et la question est ouverte à tous, sans animosité quelconque, s'il existe une définition intuitionniste de non P qui puisse convaincre que nous raisonnons parfois en logique intuitionniste pour démontrer l'irrationalité de $\sqrt{2}$.
Je crois que c'est un aspect qui semblait aller de soi dans nos échanges mais qui n'a jamais été réellement justifié.
"Les gens pensent"
On n'a pas a interpréter ce que les gens pensent. Enfin, pas dans ce débat là je veux dire.
La personne qui effectue un raisonnement doit nous dire quel est son type de raisonnement.
Bien entendu, comme moi, je ne savais pas il y a quelques années, qu'il existait plusieurs logiques.
La définition du "non" :
Je suis d'accord avec toi pour "je n'ai jamais vu personne poser "racine de 2 irrationnelle" := ("racine de 2 rationnelle" => tout)"".
En fait j'ai toujours vu (sauf depuis...) "racine 2 irrationnelle" := "racine 2 n'est pas rationnel".
Je n'avais jamais vu jadis : "non(P) := P => tout".
Sur la définition du $non$ en L.I. ou en L.C. il m'a semblé que c'était la même justement :
Pour tout $P$, $non(P):=(P\Rightarrow Tout)$.
Ltav : même si tu persistes à embrouiller les choses, à peu près tout le monde démontre que $\sqrt 2$ est irrationnel (non A) en démontrant que si $\sqrt 2$ est rationnel (A), alors absurde, ce qui est une déduction classique tout à fait valide, et aussi une déduction intuitionniste tout à fait valide.
"Les gens pensent"
On n'a pas a interpréter ce que les gens pensent. Enfin, pas dans ce débat là je veux dire.
La personne qui effectue un raisonnement doit nous dire quel est son type de raisonnement.
Bien entendu, comme moi, je ne savais pas il y a quelques années, qu'il existait plusieurs logiques.
Si on pense que les gens raisonnent en mode intuitionniste (sans tiers-exclu) pour démontrer non P, alors il faut justifier qu'ils utilisent également une définition intuitionniste de non P, qu'ils sont en "mode intuitionniste jusqu'au bout".
Donc je suis d'accord avec toi qu'il ne suffit pas d'interpréter, il faut rechercher des signes formels visibles de leur pensée. Or, la logique intuitionniste est une logique très spéciale, fondamentalement différente de la logique classique, même si certains raisonnements se ressemblent, comme (P => tout) => non P (*). On ne peut pas prétendre raisonner "en intuitionniste" sans des indices forts que nous sommes vraiment en train de le faire : l'un d'eux est de poser une nouvelle définition, "LI-compatible", de la négation d'une proposition.
Ce n'est pas une mince affaire, les logiciens y ont beaucoup réfléchi : le plus simple a été de poser non P := (P => $\bot$). Autrement dit, non P est devenue une simple abréviation de la preuve (car en LI on veut que toute proposition démontrée ait une preuve constructible) que P implique $\bot$. Mais où voit-on (en dehors des ouvrages intuitionnistes) l'auteur d'une preuve de l’irrationalité de $\sqrt{2}$ avertir qu'il va utiliser cette définition spéciale :
La définition du "non" :
Je suis d'accord avec toi pour "je n'ai jamais vu personne poser "racine de 2 irrationnelle" := ("racine de 2 rationnelle" => tout)"".
En fait j'ai toujours vu (sauf depuis...) "racine 2 irrationnelle" := "racine 2 n'est pas rationnel".
Je n'avais jamais vu jadis : "non(P) := P => tout".
Dans la définition "racine 2 irrationnelle" := "racine 2 n'est pas rationnel", on voit bien l'utilisation grammaticale et sémantique tout à fait classique d'une négation de la proposition "racine 2 est rationnelle".
Le problème aussi est que les gens ne savent pas toujours ce qu'ils pensent, même en écrivant formellement leurs raisonnements. On l'a assez vu au cours de ces échanges.
Sur la définition du non en L.I. ou en L.C. il m'a semblé que c'était la même justement :
Pour tout $P$, $non(P):=(P\Rightarrow Tout)$.
Non, elles sont différentes, précisons-le : en LC, non P est par définition la proposition qui a une table de vérité exactement opposée à celle de P. On en déduit alors que non P <=> (P => tout) (mêmes tables de vérité à gauche et à droite de l'équivalence). Mais en LI (pour la définition la plus simple), on ne parle plus de tables de vérité (vrai/faux) : non P devient une pure abréviation de P => tout.
[small](*) Ce n'est une démonstration "sérieuse" (acceptable sur la copie d'un élève ou dans une revue mathématique) de non P qu'en LC. En LI, cette implication n'est autre que non P => non P.[/small]
à peu près tout le monde démontre que $\sqrt2$ est irrationnel (non A) en démontrant que si $\sqrt2$ est rationnel (A), alors absurde, ce qui est une déduction classique tout à fait valide, et aussi une déduction intuitionniste tout à fait valide.
Ton "embrouilleur" a justement beaucoup milité ici-même pour que ces deux types de raisonnements soient reconnus valides et acceptables (alors que je te rappelle que plusieurs intervenants dont toi ne semblaient voir et accepter que la "version intuitionniste").
Par contre, je rajoute que quasiment personne d'entre les prouveurs de l'irrationalité de $\sqrt2$ (dans les livres, etc.) ne fait réellement cette déduction intuitionniste valide, puisqu'elle demande de redéfinir explicitement la négation d'une proposition de façon intuitionniste - et a fortiori de raisonner d'une manière radicalement différente de la logique classique : ne plus parler de valeurs vrai/faux, mais de propositions soit démontrables, soit démontrant l'absurde, soit indémontrables, etc.
Dire, sans toutes ces précautions techniques, que l'on démontre de façon intuitionniste non P en prouvant (P => $\bot$), est une erreur monumentale.
Bonjour
Je ne sais pas faire une citation correctement.
Quelqu'un peut-il m'expliquer ? [Tu utilises le bouton "guillemet" en 16ème position sur la fenêtre d'édition. AD]
En attendant, je fais ça à l'ancienne.
Non, elles sont différentes, précisons-le : en LC, non P est par définition la proposition qui a une table de vérité exactement opposée à celle de P. On en déduit alors que non P <=> (P => tout) (mêmes tables de vérité à gauche et à droite de l'équivalence). Mais en LI (pour la définition la plus simple), on ne parle plus de tables de vérité (vrai/faux) : non P devient une pure abréviation de P => tout.
Là, tu confonds allègrement syntaxe et sémantique.
La définition que tu donnes de non P en LC est purement sémantique : non P est vraie ssi P est fausse, et réciproquement.
Le fait que non P est équivalent à (P implique tout) est alors un théorème trivial, il suffit effectivement d'examiner les deux cas possibles.
En LI tu as un langage composé des symboles antitruc, et, ou, implique, équivalent et ta syntaxe est censée obéir à certaines règles qui peuvent varier d'un système intuitionniste à l'autre. Et, pour des raisons de commodité d'écriture, tu utilises le symbole non P comme un raccourci pour (P implique antitruc).
En clair tu compares deux trucs qui ne sont pas comparables. C'est comme si tu nous demandais qu'est-ce qu'il y a de meilleur entre un Pommard 1848 et une Ferrari Testarosa (orthographe approximative, sans doute).
De mon téléphone @Ltav: LI inclus dans LC. Les raisonnements dits faits en LI sont TOUS sans exception valables en LC et de même pour les définitions.
Si tu as la chance que je prenne quelques secondes pour t'instruire avec ce présent post c'est parce ayant très peu de disponibilité il y a longtemps que je n'ai pas posté et suis détendu et ai oublié tes simulations rhétoriques.
GBZM n'a manifestement plus la passion.
Tout au long de tes interventions j'ai aussi remarqué que de tps à autre, malgré que tu n'y connaisses rien, tu captés un nouveau truc que tu présentes ensuite comme quelque chose que tu as toujours su.
En peu d'années sur le forum tu t'es déclaré pas moins que monsieur je sais tout en physique quantique +relativité + thermodynamique + logique mathématique. Et on attend la prochaine érudition avec une impatience insoutenable .
Tout ceci en plus de dégrader ton image de marque et amicalité forumique est un formidable gâchis. Si tu acceptais de te présenter novice (et manifestement littéraire cherchant à aborder la science pour la première fois avec tous les efforts sur soi que ça présente) tu multiplierais PAR DIX AU MOINS ta vitesse de progrès en infos captées et récupérées. J'ai CHOISI mon DIX en me voulant REALISTE!
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Bon c’est vrai que c’est pénible.
Ici, Ltav, tu fais de la prose de décor.
Dans d’autres discussions, ce n’est pas toi mais un autre intervenant qui fait des message à rallonge pour peu de contenu finalement.
C’est bizarre cette envie de raconter des trucs.
Balance des choses plus pures.
En LC la définition de $non(.)$ est :
En LI c’est ça :
Il faut aller droite à l’essentiel.
Sinon plus personne ne lit et ça fait aussi penser à du Stham ou du simple troll.
Les désaccords entre toi et d’autres ne durent plus bien longtemps.
Tu épuises et l’intervenant se casse, purement et simplement.
@Cc : qui a dit que la LI n'était pas incluse (*) dans la LC...? Relis bien mon message. Il n'y a qu'un axiome en plus (le TE) dans la LC, tout théorème de logique intuitionniste est valable syntaxiquement en logique classique. Sauf qu'il utilise une définition tout à fait distincte de la négation classique d'une proposition. On ne peut passer d'un théorème à l'autre qu'en précisant que l'on a changé de logique et de définition. Sinon, dire que l'on a démontré un théorème de façon intuitionniste et qu'il vaut aussi "tel quel" en logique classique est soit une grossière erreur, soit une pure arnaque sophistique du genre de celles qui prétendent dire la même chose que quelqu'un alors que l'on utilise ses mots avec des définitions différentes.
Il faudrait pour être précis utiliser la proposition non P avec un indice pour la LC et un pour la LI (par exemple $\neg P_{LC}$ et $\neg P_{LI}$) et réécrire les théorèmes. Dire qu'il n'y a pas de tiers-exclu dans (P => tout) => non P (i.e. que cette démonstration est intuitionniste) n'est correct que si l'on prend une définition intuitionniste de $\neg P$, autrement dit : (P => tout) => $\neg P_{LI}$. Or aucun d'entre vous n'avait précisé que dans sa bouche "racine de 2 irrationnelle" devenait l'abréviation de "si je suppose racine de 2 rationnelle alors j'en déduis l'absurde".
@Martial : ce que je viens d'écrire est valable pour toi aussi, j'abonde justement dans ton sens : on ne peut comparer que ce qu'il y a de comparable. L'identité de deux théorèmes en LC et LI est trompeuse, ils utilisent des définitions différentes. Et définir non P par (P => tout) n'est pas qu'un artifice pour aller vite. Les intuitionnistes ont eu très peu le choix s'ils voulaient éviter le tiers-exclu. Sans cette précaution, le tiers-exclu est inévitable.
[small](*) Au sens où l'ensemble de ses axiomes est un sous-ensemble de l'ensemble des axiomes de la LC. Il y a 2 axiomes en LI (resp. 3 en LC avec le tiers-exclu) précisant, sans la définir, les propriétés que devrait vérifier toute négation d'une proposition.[/small]
@Dom : chacune de mes phrases, voire de mes mots, a de l'importance pour différents niveaux de lecture. Je déroule une trame d'idées dans un ordre bien précis. Si tu as pu y prendre ce qui t'intéressait, eh bien ne refuse pas à d'autres de voir également du contenu dans le reste. Ai-je été concis là ? Ensuite tu donnes l'impression de confirmer d'autres interventions ("c'est vrai que c'est pénible...etc."), alors que rien ne te garantit que les intentions réelles de ces intervenants soient identiques aux tiennes (demande de clarté, concision, etc.).
Bravo l'Auguste, joli numéro ! Bon, il est un peu usé , ce numéro, et toujours aussi creux.
L'équivalence logique de $P\Rightarrow \bot$ et de $\neg P$ est tout aussi valable en logique classique qu'en logique intuitionniste, bien évidemment.
Bravo l'Auguste, joli numéro ! [...] L'équivalence logique de $P\Rightarrow \bot$ et de $\neg P$ est tout aussi valable en logique classique qu'en logique intuitionniste, bien évidemment.
Bon, puisque je dois donner la réplique au clown blanc (*)...la voici (même si je me répète, mais il a l'air amnésique) :
Cette équivalence n'est valable en logique intuitionniste que si l'on admet une nouvelle définition intuitionniste de $\neg P$, dont la plus simple est : $\neg P := (P \Rightarrow \bot)$. Si tu n'es pas d'accord, apporte donc une preuve de cette équivalence en LIsans changer la définition classique de $\neg P$. Précise bien dans tous les cas la définition de $\neg P$ que tu utilises. J'attends (**).
[small](*) Définition de l'Auguste :
Clown portant un costume déformé, des souliers en bateau et une chevelure hirsute, qui donne souvent la réplique au clown blanc
J'aurais peut-être aussi pu te répondre : "merci, on m'appelle Octave", en regard de l'autre définition d'auguste ;-)
(**) Tous tes essais passés utilisent une définition intuitionniste. Ici je te demande en d'autres termes de démontrer l'équivalence $\neg P \Leftrightarrow (P \Rightarrow \bot)$ en logique classique, mais sans utiliser le tiers-exclu.
[/small]
De mon téléphone pour les novices, abrégeant par T l'affirmation que toutes les phrases sont vraies. Je redonne pour la 475636 ième fois la preuve de équivalence valable dans TOUTES LES LOGIQUES sauf la linéaire (donc pas juste LC et LI)
DE A=>T on déduit non T => non A puis non A.
De non A on déduit non T => non A puis non non A = non non T puis A=> T du fait que A=> non non A et que non non T => T.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Merci à vous deux. Nous y (re)voilà. Vous avez encore répété l'erreur que je qualifiais de "monumentale". Il manque quelque chose de fondamental à vos démonstrations intuitionnistes, et ce n'est pas faute de vous l'avoir demandé et d'avoir bien insisté plusieurs fois :
Si tu n'es pas d'accord, apporte donc une preuve de cette équivalence en LI sans changer la définition classique de $\neg P$. Précise bien dans tous les cas la définition de $\neg P$ que tu utilises.
Quelle définition avez-vous utilisée pour $\neg P$ ?
Répondez brièvement s'il vous plaît. Tout le monde peut voir que vous n'en parlez absolument pas dans ces démonstrations. Il ne suffit pas de démontrer, encore faut-il savoir ce que "veut dire" ce que l'on démontre. Et c'est à votre réponse que l'on reconfirmera une fois de plus qu'il est impossible de garder la même définition de $\neg P$ en LC et en LI. J'ai déjà répondu à cette question mais j'attends que vous le disiez vous-mêmes pour faire cesser vos "cachotteries".
[small]Pour ceux qui ont déjà compris et pour ne pas alourdir le texte : voilà, il ne suffit pas d'appliquer les 3 axiomes logiques sur $\neg P$ de la logique classique ou les 2 de la logique intuitionniste (*) ou autre, pour dire que l'on a démontré quelque chose sur $\neg P$ : ces axiomes ne définissent pas $\neg P$, ils précisent les propriétés que $\neg P$ doit vérifier, c'est complètement différent. La LC va alors vérifier ces propriétés en définissant $\neg P$ comme la proposition de valeur de vérité opposée à $P$, tandis que la LI va le faire en posant $\neg P$ comme la preuve que $P$ implique une contradiction (la LI ne raisonne qu'en preuves construites, elles n’utilise plus les valeurs de vérité vrai/faux comme la LC). Il existe aussi la logique naturelle avec la théorie de la démonstration de Gentzen. Là on définit de façon "axiomatique" $\neg P$ par une règle déductive dite règle d'introduction du $\neg$ :
P $\vdash \bot$
________
$\vdash \neg$ P
Autrement dit, "$\neg P$ est la proposition que l'on déduit automatiquement de la déduction $P \vdash \bot$". Remplacer $\neg P$ par "$\sqrt2$ non rationnelle" pour voir ce que ça donne et si vous définissez souvent l'irrationalité de $\sqrt2$ comme cela.
(*) Voici ces axiomes valables à la fois en LC et LI, pour toutes propositions $A, B$ :
Tu as de la chance que je te réponde car les copies collés de mon téléphone c'est pénible.
l ne suffit pas de démontrer, encore faut-il savoir ce que "veut dire" ce que l'on démontre.
Comme à tout le moins on peut croire que tu as une bonne mémoire le fait de faire exprès comme ça d'affirmer la plus grosse énormité qui t'est reproché depuis que tu viens sur le forum comme si de rien n'était et que tu ne t'étais pas aperçu que tu avais reçu 1000 fois la réponse (que si si démontrer" suffit" et que toute le corpus des définitions est de toute façon circulzire) s'apparente à de la PARFAITE MAUVAISE FOI. Tu cherches juste à nous le faire répéter. Pour jouer à Je ne sais jeu.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
@Cc : je ne joue à aucun jeu idiot de répétitions ou autre. Ma question est simple. Quelle est ta définition de non P dans ta démonstration intuitionniste ? J'ai l'impression que tu veuilles dire qu'une définition est inutile. Vais-je t'apprendre qu'une définition garantit aussi une existence ? Savoir que non P doive vérifier certains axiomes ne sert strictement à rien s'il n'existe aucune proposition non P qui vérifie bien ces axiomes. Les logiciens ont donc défini non P par une proposition existante précise, aussi bien en LC qu'en LI.
@Dom : merci de ta question (tu voulais dire pour définir non P en LC ?). Pour définir non P en LC, la réponse est parfaitement claire : OUI, on utilise fondamentalement des tables de vérité vrai/faux pour définir non P en LC. Et que pour définir ces tables de vérité en LC, nous avons fondamentalement besoin de l'axiome du tiers-exclu.
Donc que toute démonstration de non P à partir de (P => tout) soit utilise le tiers-exclu (LC), soit n'utilise pas le tiers-exclu (LI) mais une définition radicalement différente de non P. Et dans ce dernier cas, il faut absolument le préciser pour que la démonstration fonctionne.
Et que dans ce dernier cas, les mots veulent dire tout autre chose : "racine de 2 irrationnelle" devient une abréviation de "je déduis l'absurde de racine de 2 rationnelle". Dire que l'on démontre sans tiers-exclu par P => tout que la racine de 2 est irrationnelle sans préciser ce changement de définition fondamental est donc une erreur logique monumentale (et une arnaque absolue si c'est intentionnel).
Bon, cc : penses-tu donc vraiment qu'une définition ne sert à rien (même pas à garantir l'existence de ce qui est décrit) pour appliquer un système axiomatique ?
penses-tu donc vraiment qu'une définition ne sert à rien (même pas à garantir l'existence de ce qui est décrit) pour appliquer un système axiomatique
Tu connais la réponse, puisqu'elle t'a déjà été faite. Il n'y a pas de définition en maths. Ce sont des abréviations pour écrire moins long. Le fait que tu fasses semblant (ou plus gravement que tu ne comprennes pas) de ne pas le comprendre, voire même de ne pas te souvenir qu'on te l'a déjà dit, montre, à mon sens que tu as envie de relancer une discussion sur ce sujet.
Le problème est que tu ne le dis pas franchement. Et vu que je ne suis quasiment pas dispo...
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Maintiens-tu cette erreur logique énorme de croire qu'une définition ne sert à rien dans la validation d'une démonstration ? Nierais-tu que celle-ci peut être fausse ou invalide si elle utilise une proposition mal définie, e.g. référant à un objet de l'ensemble vide ?
Un exemple que tu connais (*) : "Soit un ensemble $E$ tel que pour tout $x\in E$, $x \notin \emptyset$, alors $E \neq \emptyset$".
Raisonnement faux si E est mal défini au sens où déjà égal à l'ensemble vide. Mais vrai sinon. De même pour une démonstration de non P avec un non P contradictoire (non P => $\bot$), sans objet : elle serait fausse. Quelle est ta définition de non P à toi ? Est-elle consistante ?
[small](*) C'était ta traduction fausse de l'AO si tu te souviens.[/small]
Ltav ne voit pas d'erreur (donc ne comprend pas que les gens d'accord avec 1 et 2 peuvent pourtant ne pas du tout adhérer à 3 même s'ils lisent l'argument 4 qui suit):
1/ Dieu n'a pas de défaut
2/ ne pas exister est un défaut
3/ Dieu existe
4/ si 1 et 2 alors 3. Sinon Dieu aurait le défaut de ne pas exister.
Je crois même qu'il s'est inscrit pour ça. Je n'aurai pas la cruauté de mettre un lien vers ses tous premiers posts concernant ça :-D
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Cc, au contraire, ce sujet m'honore : l'un des titres était je crois "Retour vers l'AO", aux éventuels intéressés. J'avais obtenu la proposition logique exacte et valide correspondant à l'AO. Mais restons sur notre sujet s'il te plaît.
@Christophe : si 3) est faux, 1) est faux, donc 1) et 2) est faux, donc 1) et 2) implique 3) est vrai, comme dit 4).
Je ne vois pas où il pourrait y avoir un problème.
Si Ltav s'est inscrit pour cela, son inscription est nulle et non avenue.
CQFD.
Ltav :
Ainsi tu nies qu’on puisse définir $non(P)$ par $P \Rightarrow Tout$ en LC ?
Sans s’occuper des tables de vérité ?
On n’obtiendrait pas quelque chose d’équivalent ?
Christophe :
Là tu abuses. Une définition existe en maths justement pour abréger.
Et dans ce débat ça sert pour savoir de quoi on parle quand on dit ce qu’est le « $non$ » par exemple.
Ne prends pas le même angle que Ltav.
@Dom, pourquoi nierais-je cela ? En LC, il est tout à fait possible de prendre cette définition, oui puisque non P et (P => tout) sont parfaitement équivalentes mais elles le sont grâce au tiers-exclu (tu peux oublier un instant les tables de vérité binaire, qui ne sont qu'une conséquence du tiers-exclu). Ça ne changera rien aux théorèmes classiques. Par contre si tu veux te passer entièrement du tiers-exclu en LC, pour te métamorphoser en majestueuse LI, il faudra les "forcer" à être équivalentes, grâce à une redéfinition adéquate de non P, dont la plus simple est comme déjà dit : non P := (P => tout).
Comprends que la LC étant plus puissante que la LI, elle a plus le choix de ses définitions. En LC, pas besoin de forcer pour avoir très naturellement une vraie démonstration de non P (prouvable grâce au tiers-exclu donc vrai RPA) : (P => tout) => non P. En LI, dénaturer et affaiblir ce raisonnement est le prix à payer pour éviter le tiers-exclu, il devient : non P => non P - ce qui l'on en conviendra est une démonstration "ridicule" de non P (on démontre CQFD par CQFD). La LI va réellement prouver "son" non P en démontrant par définition l'absurde à partir de P.
non P et (P => tout) sont parfaitement équivalentes mais elles le sont grâce au tiers-exclu
C'est factuellement faux.
Les élucubrations de Ltav, c'est genre "Dire que l'on a démontré un théorème pour la loi de composition interne d'un groupe et qu'il vaut aussi "tel quel" pour une groupe abélien est soit une grossière erreur, soit une pure arnaque sophistique du genre de celles qui prétendent dire la même chose que quelqu'un alors que l'on utilise ses mots avec des définitions différentes." L'argument pour les groupes tiendrait d'ailleurs plus debout puisqu'on a l'habitude d'appeler et de noter la l.c.i. d'un groupe abélien différemment de la l.c.i. d'un groupe général.
Ltav s'est trompé de forum. Il a d'indéniables talents de charlatanisme, mais c'est peu apprécié sur un forum de mathématiques.
Je voulais écrire "même style" et cela a été corrigé en "même angle" je pense. Mea Culpa.
Je cite des passages intrigants : Moi : Sur la définition du non en L.I. ou en L.C. il m'a semblé que c'était la même justement :
Pour tout P, non(P):=(P=>Tout).
Ltav :Non [small]c'est moi qui mets en gras[/small], elles sont différentes, précisons-le : en LC, non P est par définition la proposition qui a une table de vérité exactement opposée à celle de P. On en déduit alors que non P <=> (P => tout) (mêmes tables de vérité à gauche et à droite de l'équivalence). Mais en LI (pour la définition la plus simple), on ne parle plus de tables de vérité (vrai/faux) : non P devient une pure abréviation de P => tout.
Moi :
Ainsi tu nies qu’on puisse définir non(P) par P=>Tout en LC ?
Sans s’occuper des tables de vérité ?
On n’obtiendrait pas quelque chose d’équivalent ?
Ltav :
En LC, il est tout à fait possible de prendre cette définition, oui puisque non P et (P => tout) sont parfaitement équivalentes
Je précise que je suis novice sur ce sujet.
Je vois une contradiction de tes propos Ltav.
Même en piochant dans tes propos, bien entendu, ils sont tronqués, j'ai gardé la prose pénible (à mon goût, c'est personnel, bien sûr).
@Martial: si le Dieu de " Dieu n'a pas de défaut " est le même que le Dieu de "Dieu existe" un logiciel de reconnaissance de preuves formelles validera.
Mais ce que Ltav voulait c'était que les gens acceptant 1 et 2 dans la vraie vie acceptent 3. Il ne voulait évidemment pas juste faire remarquer la forme. Il a même tenté d'écrire plein de choses en .. TDE .. (c'est courageux car tu aurais vu les fautes ça faisait peur pour lui) pour essayer de prouver que les deux occurrences du mot Dieu désignent le même Dieu.
Un peu comme un élève de 5ie qui n'est demordrait pas qu'une solution à l'équation [ X= 3 et 3X=700; inconnue X ] existe car sinon elle ne pourrait pas être égale à 3.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
@dom: tu confonds maths et matheux. Oui EN PRATIQUE il est commode d'abréger. Le "en pratique" ne fait pas partie des maths mais ne concerne que la sociologie et les limites matérielles humaines pour faire tenir dans une page ou un fichier des informations qui non abrégées seraient trop longues. En ce qui concerne les définitions circulaires, elles sont mal nommées puisqu'elles s'insèrent à titre d'axiomes.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
M’enfin !
Si je dis que « $non(P)$ » est équivalent à « Q », faut-il encore savoir ce que moi j’appelle $non(P)$ ?
C’est un matheux qui pose une question de math.
Ne te laisse pas ensorceler par Ltav qui souhaite parler bien plus que d’écrire des maths.
On se demande qui joue finalement.
Ou alors je n’ai rien compris, après tout, ça me convient très bien.
@Dom : il n'y a pas d'ensorcellement là-dedans.
Quand tu énonces le théorème : "Pour tout espace métrique (E,d), on a l'équivalence entre (E,d) est compact et toute suite à valeurs dans E admet une valeur d'adhérence", tu pourrais en théorie tout écrire dans le langage de ZF en remplaçant espace métrique par une phrase qui rappelle la définition, et idem pour compact, suite, suite extraite et valeur d'adhérence…
Même s'il n'y a peut-être pas suffisamment d'atomes dans l'univers pour écrire un tel énoncé… et je ne parle même pas de la démonstration.
Réponses
Si $F(U)$ est défini comme l'ensemble des fonctions $U\to \mathbb R$ possédant une certaine propriété de caractère local (être continue, être localement constante), il est évident d'après la définition rappelée par Maxtimax que $F$ est un faisceau.
Pour se donner un faisceau sur $\beta\mathbb N$, il suffit de préciser ses sections sur le ouverts de base $\widehat A$.
Le faisceau de fonctions continues à valeurs réelles $\mathbb R_{\beta\mathbb N}$ a pour sections sur $\widehat A$ les suites bornées de nombres réels indexées par $A$ : vérifier qu'une telle suite se prolonge de manière unique en une fonction continue $\widehat A\to \mathbb R$.
C'est un sous-faisceau du faisceau dont les sections sur $\widehat A$ sont toutes les suites de nombres réels indexées par $A$. Exercice (facile) : montrer que la fibre de ce faisceau en un $\mathcal U\in \beta\mathbb N$ est l'ultrapuissance de $\mathbb R$ par rapport à $\mathcal U$. Un faisceau dont les fibres sont les ultrapuissances, voila qui devrait te faire plaisir, Christophe !
Je n'ai pas bien compris la preuve par Georges Abitbol (vers le haut de la page 2 de la discussion) du fait que (P implique antitruc) implique non P. (Dans l'autre sens ça va).
Je sais bien qu'on peut prendre ça comme définition du "non", mais quand même j'aimerais bien comprendre l'argument.
Si quelqu'un pouvait développer un peu…
Merci d'avance
$$\frac{P\ \vdash\ P\qquad \bot\ \vdash\ \bot}{\dfrac{P,\ P\Rightarrow \bot\ \vdash\ \bot}{P\Rightarrow \bot\ \vdash\ \neg P}}$$
$\Rightarrow$ gauche, $\neg$ droit.
Aurais-je plutôt contracté ?
Voir un mode d'emploi du calcul des séquents.
http://www.les-mathematiques.net/phorum/read.php?16,1889932,1889932#msg-1889932
C'est du lourd, mais j'essaierai de bosser ça quand j'aurai un peu de disponibilité
http://www.les-mathematiques.net/phorum/read.php?16,1880930,1890218#msg-1890218
GBZM, si je peux me permettre, il y aura toujours un malaise si tu t'y prends comme ça pour démontrer non P. On démontre quelque chose qu'on a défini d'abord. Comment définis-tu non P en logique intuitionniste ? Prends s'il te plaît un exemple très concret, comme non P := "la racine de 2 n'est pas rationnelle". Que devient, en bon français, cette proposition en logique intuitionniste ? Par exemple, je dirais en prenant la définition intuitionniste non P := (P => tout), que la proposition "La racine de 2 n'est pas rationnelle" n'est qu'une abréviation en LI de : "Supposer la rationalité de la racine de 2 mène à l'absurde". Or, c'est compliqué de le dire comme ça, il est évident que personne ne définit spontanément l'irrationalité de racine de 2 de cette manière.
En logique classique, la définition de non P est très simple, c'est le contraire (valeur de vérité opposée) de P. Connais-tu une définition aussi simple, traduisible en bon français, de non P en logique intuitionniste ?
Merci d'avance.
Je ne vois pas le problème Ltav. Tu sembles poser une question mais tu y réponds apparemment.
Le « c’est compliqué de le dire comme ça » n’est que psychologique. Qu’est-ce qu’on se fout du caractère « compliqué » d’une proposition ?
Pourquoi les maths seraient simples dans les énoncés en français ?
Ou alors je n’ai pas compris ce que tu veux dire.
Ensuite, la question d'utiliser une définition la plus proche possible de celle qu'utilisent les gens qui démontrent l'irrationalité de la racine de 2 a également une importance sémantique et logique dans la traduction formelle de ce raisonnement.
Si on pense que les gens raisonnent en mode intuitionniste (sans tiers-exclu) pour démontrer non P, alors il faut justifier qu'ils utilisent également une définition intuitionniste de non P, qu'ils sont en "mode intuitionniste jusqu'au bout". Or je n'ai jamais vu personne poser la définition "racine de 2 irrationnelle" := ("racine de 2 rationnelle" => tout) avant de démontrer l'irrationalité de $\sqrt{2}$. Je demande donc, et la question est ouverte à tous, sans animosité quelconque, s'il existe une définition intuitionniste de non P qui puisse convaincre que nous raisonnons parfois en logique intuitionniste pour démontrer l'irrationalité de $\sqrt{2}$.
Je crois que c'est un aspect qui semblait aller de soi dans nos échanges mais qui n'a jamais été réellement justifié.
On n'a pas a interpréter ce que les gens pensent. Enfin, pas dans ce débat là je veux dire.
La personne qui effectue un raisonnement doit nous dire quel est son type de raisonnement.
Bien entendu, comme moi, je ne savais pas il y a quelques années, qu'il existait plusieurs logiques.
La définition du "non" :
Je suis d'accord avec toi pour "je n'ai jamais vu personne poser "racine de 2 irrationnelle" := ("racine de 2 rationnelle" => tout)"".
En fait j'ai toujours vu (sauf depuis...) "racine 2 irrationnelle" := "racine 2 n'est pas rationnel".
Je n'avais jamais vu jadis : "non(P) := P => tout".
Sur la définition du $non$ en L.I. ou en L.C. il m'a semblé que c'était la même justement :
Pour tout $P$, $non(P):=(P\Rightarrow Tout)$.
On me corrigera à loisir.
Voilà ce que j'ai dit plus exactement :
Donc je suis d'accord avec toi qu'il ne suffit pas d'interpréter, il faut rechercher des signes formels visibles de leur pensée. Or, la logique intuitionniste est une logique très spéciale, fondamentalement différente de la logique classique, même si certains raisonnements se ressemblent, comme (P => tout) => non P (*). On ne peut pas prétendre raisonner "en intuitionniste" sans des indices forts que nous sommes vraiment en train de le faire : l'un d'eux est de poser une nouvelle définition, "LI-compatible", de la négation d'une proposition.
Ce n'est pas une mince affaire, les logiciens y ont beaucoup réfléchi : le plus simple a été de poser non P := (P => $\bot$). Autrement dit, non P est devenue une simple abréviation de la preuve (car en LI on veut que toute proposition démontrée ait une preuve constructible) que P implique $\bot$. Mais où voit-on (en dehors des ouvrages intuitionnistes) l'auteur d'une preuve de l’irrationalité de $\sqrt{2}$ avertir qu'il va utiliser cette définition spéciale :
Alors qu'au contraire, comme tu l'as souligné :
Dans la définition "racine 2 irrationnelle" := "racine 2 n'est pas rationnel", on voit bien l'utilisation grammaticale et sémantique tout à fait classique d'une négation de la proposition "racine 2 est rationnelle".
Le problème aussi est que les gens ne savent pas toujours ce qu'ils pensent, même en écrivant formellement leurs raisonnements. On l'a assez vu au cours de ces échanges.
Non, elles sont différentes, précisons-le : en LC, non P est par définition la proposition qui a une table de vérité exactement opposée à celle de P. On en déduit alors que non P <=> (P => tout) (mêmes tables de vérité à gauche et à droite de l'équivalence). Mais en LI (pour la définition la plus simple), on ne parle plus de tables de vérité (vrai/faux) : non P devient une pure abréviation de P => tout.
[small](*) Ce n'est une démonstration "sérieuse" (acceptable sur la copie d'un élève ou dans une revue mathématique) de non P qu'en LC. En LI, cette implication n'est autre que non P => non P.[/small]
Ton "embrouilleur" a justement beaucoup milité ici-même pour que ces deux types de raisonnements soient reconnus valides et acceptables (alors que je te rappelle que plusieurs intervenants dont toi ne semblaient voir et accepter que la "version intuitionniste").
Par contre, je rajoute que quasiment personne d'entre les prouveurs de l'irrationalité de $\sqrt2$ (dans les livres, etc.) ne fait réellement cette déduction intuitionniste valide, puisqu'elle demande de redéfinir explicitement la négation d'une proposition de façon intuitionniste - et a fortiori de raisonner d'une manière radicalement différente de la logique classique : ne plus parler de valeurs vrai/faux, mais de propositions soit démontrables, soit démontrant l'absurde, soit indémontrables, etc.
Dire, sans toutes ces précautions techniques, que l'on démontre de façon intuitionniste non P en prouvant (P => $\bot$), est une erreur monumentale.
Je ne sais pas faire une citation correctement.
Quelqu'un peut-il m'expliquer ?
[Tu utilises le bouton "guillemet" en 16ème position sur la fenêtre d'édition. AD]
En attendant, je fais ça à l'ancienne.
Là, tu confonds allègrement syntaxe et sémantique.
La définition que tu donnes de non P en LC est purement sémantique : non P est vraie ssi P est fausse, et réciproquement.
Le fait que non P est équivalent à (P implique tout) est alors un théorème trivial, il suffit effectivement d'examiner les deux cas possibles.
En LI tu as un langage composé des symboles antitruc, et, ou, implique, équivalent et ta syntaxe est censée obéir à certaines règles qui peuvent varier d'un système intuitionniste à l'autre. Et, pour des raisons de commodité d'écriture, tu utilises le symbole non P comme un raccourci pour (P implique antitruc).
En clair tu compares deux trucs qui ne sont pas comparables. C'est comme si tu nous demandais qu'est-ce qu'il y a de meilleur entre un Pommard 1848 et une Ferrari Testarosa (orthographe approximative, sans doute).
Si tu as la chance que je prenne quelques secondes pour t'instruire avec ce présent post c'est parce ayant très peu de disponibilité il y a longtemps que je n'ai pas posté et suis détendu et ai oublié tes simulations rhétoriques.
GBZM n'a manifestement plus la passion.
Tout au long de tes interventions j'ai aussi remarqué que de tps à autre, malgré que tu n'y connaisses rien, tu captés un nouveau truc que tu présentes ensuite comme quelque chose que tu as toujours su.
En peu d'années sur le forum tu t'es déclaré pas moins que monsieur je sais tout en physique quantique +relativité + thermodynamique + logique mathématique. Et on attend la prochaine érudition avec une impatience insoutenable .
Tout ceci en plus de dégrader ton image de marque et amicalité forumique est un formidable gâchis. Si tu acceptais de te présenter novice (et manifestement littéraire cherchant à aborder la science pour la première fois avec tous les efforts sur soi que ça présente) tu multiplierais PAR DIX AU MOINS ta vitesse de progrès en infos captées et récupérées. J'ai CHOISI mon DIX en me voulant REALISTE!
Ici, Ltav, tu fais de la prose de décor.
Dans d’autres discussions, ce n’est pas toi mais un autre intervenant qui fait des message à rallonge pour peu de contenu finalement.
C’est bizarre cette envie de raconter des trucs.
Balance des choses plus pures.
En LC la définition de $non(.)$ est :
En LI c’est ça :
Il faut aller droite à l’essentiel.
Sinon plus personne ne lit et ça fait aussi penser à du Stham ou du simple troll.
Les désaccords entre toi et d’autres ne durent plus bien longtemps.
Tu épuises et l’intervenant se casse, purement et simplement.
Un peu d'ouverture d'esprit s'il vous plaît.
@Cc : qui a dit que la LI n'était pas incluse (*) dans la LC...? Relis bien mon message. Il n'y a qu'un axiome en plus (le TE) dans la LC, tout théorème de logique intuitionniste est valable syntaxiquement en logique classique. Sauf qu'il utilise une définition tout à fait distincte de la négation classique d'une proposition. On ne peut passer d'un théorème à l'autre qu'en précisant que l'on a changé de logique et de définition. Sinon, dire que l'on a démontré un théorème de façon intuitionniste et qu'il vaut aussi "tel quel" en logique classique est soit une grossière erreur, soit une pure arnaque sophistique du genre de celles qui prétendent dire la même chose que quelqu'un alors que l'on utilise ses mots avec des définitions différentes.
Il faudrait pour être précis utiliser la proposition non P avec un indice pour la LC et un pour la LI (par exemple $\neg P_{LC}$ et $\neg P_{LI}$) et réécrire les théorèmes. Dire qu'il n'y a pas de tiers-exclu dans (P => tout) => non P (i.e. que cette démonstration est intuitionniste) n'est correct que si l'on prend une définition intuitionniste de $\neg P$, autrement dit : (P => tout) => $\neg P_{LI}$. Or aucun d'entre vous n'avait précisé que dans sa bouche "racine de 2 irrationnelle" devenait l'abréviation de "si je suppose racine de 2 rationnelle alors j'en déduis l'absurde".
@Martial : ce que je viens d'écrire est valable pour toi aussi, j'abonde justement dans ton sens : on ne peut comparer que ce qu'il y a de comparable. L'identité de deux théorèmes en LC et LI est trompeuse, ils utilisent des définitions différentes. Et définir non P par (P => tout) n'est pas qu'un artifice pour aller vite. Les intuitionnistes ont eu très peu le choix s'ils voulaient éviter le tiers-exclu. Sans cette précaution, le tiers-exclu est inévitable.
[small](*) Au sens où l'ensemble de ses axiomes est un sous-ensemble de l'ensemble des axiomes de la LC. Il y a 2 axiomes en LI (resp. 3 en LC avec le tiers-exclu) précisant, sans la définir, les propriétés que devrait vérifier toute négation d'une proposition.[/small]
« Buvez les paroles, chacun en prendra des richesses. »
Ok...
J’ai du mal à m’enrichir, mais je ne demande rien, je te rassure.
L'équivalence logique de $P\Rightarrow \bot$ et de $\neg P$ est tout aussi valable en logique classique qu'en logique intuitionniste, bien évidemment.
http://www.les-mathematiques.net/phorum/read.php?16,1880930,1894240#msg-1894240
Bon, puisque je dois donner la réplique au clown blanc (*)...la voici (même si je me répète, mais il a l'air amnésique) :
Cette équivalence n'est valable en logique intuitionniste que si l'on admet une nouvelle définition intuitionniste de $\neg P$, dont la plus simple est : $\neg P := (P \Rightarrow \bot)$. Si tu n'es pas d'accord, apporte donc une preuve de cette équivalence en LI sans changer la définition classique de $\neg P$. Précise bien dans tous les cas la définition de $\neg P$ que tu utilises. J'attends (**).
[small](*) Définition de l'Auguste :
J'aurais peut-être aussi pu te répondre : "merci, on m'appelle Octave", en regard de l'autre définition d'auguste ;-)
(**) Tous tes essais passés utilisent une définition intuitionniste. Ici je te demande en d'autres termes de démontrer l'équivalence $\neg P \Leftrightarrow (P \Rightarrow \bot)$ en logique classique, mais sans utiliser le tiers-exclu.
[/small]
$$\begin{array}{rcl} P&\vdash&P\\ \hline P,\neg P&\vdash&\bot\\ \hline \neg P&\vdash &P\Rightarrow \bot\end{array}$$
Les deux déductions appartiennent au calcul des séquents classique LK et au calcul des séquents intuitionnistes LJ.
DE A=>T on déduit non T => non A puis non A.
De non A on déduit non T => non A puis non non A = non non T puis A=> T du fait que A=> non non A et que non non T => T.
Merci à vous deux. Nous y (re)voilà. Vous avez encore répété l'erreur que je qualifiais de "monumentale". Il manque quelque chose de fondamental à vos démonstrations intuitionnistes, et ce n'est pas faute de vous l'avoir demandé et d'avoir bien insisté plusieurs fois :
Quelle définition avez-vous utilisée pour $\neg P$ ?
Répondez brièvement s'il vous plaît. Tout le monde peut voir que vous n'en parlez absolument pas dans ces démonstrations. Il ne suffit pas de démontrer, encore faut-il savoir ce que "veut dire" ce que l'on démontre. Et c'est à votre réponse que l'on reconfirmera une fois de plus qu'il est impossible de garder la même définition de $\neg P$ en LC et en LI. J'ai déjà répondu à cette question mais j'attends que vous le disiez vous-mêmes pour faire cesser vos "cachotteries".
[small]Pour ceux qui ont déjà compris et pour ne pas alourdir le texte : voilà, il ne suffit pas d'appliquer les 3 axiomes logiques sur $\neg P$ de la logique classique ou les 2 de la logique intuitionniste (*) ou autre, pour dire que l'on a démontré quelque chose sur $\neg P$ : ces axiomes ne définissent pas $\neg P$, ils précisent les propriétés que $\neg P$ doit vérifier, c'est complètement différent. La LC va alors vérifier ces propriétés en définissant $\neg P$ comme la proposition de valeur de vérité opposée à $P$, tandis que la LI va le faire en posant $\neg P$ comme la preuve que $P$ implique une contradiction (la LI ne raisonne qu'en preuves construites, elles n’utilise plus les valeurs de vérité vrai/faux comme la LC). Il existe aussi la logique naturelle avec la théorie de la démonstration de Gentzen. Là on définit de façon "axiomatique" $\neg P$ par une règle déductive dite règle d'introduction du $\neg$ :
P $\vdash \bot$
________
$\vdash \neg$ P
Autrement dit, "$\neg P$ est la proposition que l'on déduit automatiquement de la déduction $P \vdash \bot$". Remplacer $\neg P$ par "$\sqrt2$ non rationnelle" pour voir ce que ça donne et si vous définissez souvent l'irrationalité de $\sqrt2$ comme cela.
(*) Voici ces axiomes valables à la fois en LC et LI, pour toutes propositions $A, B$ :
$(A \Rightarrow
$A \Rightarrow (\neg A \Rightarrow
La LC rajoute l'axiome du tiers-exclu : $A$ ou $\neg A$
[/small]
Comme à tout le moins on peut croire que tu as une bonne mémoire le fait de faire exprès comme ça d'affirmer la plus grosse énormité qui t'est reproché depuis que tu viens sur le forum comme si de rien n'était et que tu ne t'étais pas aperçu que tu avais reçu 1000 fois la réponse (que si si démontrer" suffit" et que toute le corpus des définitions est de toute façon circulzire) s'apparente à de la PARFAITE MAUVAISE FOI. Tu cherches juste à nous le faire répéter. Pour jouer à Je ne sais jeu.
Ltav, dis-tu plus haut que pour définir la LC on est obligé de parler de table de vérité ?
À la fin de ce message interminable : http://www.les-mathematiques.net/phorum/read.php?16,1880930,1893710#msg-1893710
Cordialement
@Dom : merci de ta question (tu voulais dire pour définir non P en LC ?). Pour définir non P en LC, la réponse est parfaitement claire : OUI, on utilise fondamentalement des tables de vérité vrai/faux pour définir non P en LC. Et que pour définir ces tables de vérité en LC, nous avons fondamentalement besoin de l'axiome du tiers-exclu.
Donc que toute démonstration de non P à partir de (P => tout) soit utilise le tiers-exclu (LC), soit n'utilise pas le tiers-exclu (LI) mais une définition radicalement différente de non P. Et dans ce dernier cas, il faut absolument le préciser pour que la démonstration fonctionne.
J'attends également la réponse de Gbzm.
Merci d'avance.
Tu connais la réponse, puisqu'elle t'a déjà été faite. Il n'y a pas de définition en maths. Ce sont des abréviations pour écrire moins long. Le fait que tu fasses semblant (ou plus gravement que tu ne comprennes pas) de ne pas le comprendre, voire même de ne pas te souvenir qu'on te l'a déjà dit, montre, à mon sens que tu as envie de relancer une discussion sur ce sujet.
Le problème est que tu ne le dis pas franchement. Et vu que je ne suis quasiment pas dispo...
Maintiens-tu cette erreur logique énorme de croire qu'une définition ne sert à rien dans la validation d'une démonstration ? Nierais-tu que celle-ci peut être fausse ou invalide si elle utilise une proposition mal définie, e.g. référant à un objet de l'ensemble vide ?
Un exemple que tu connais (*) : "Soit un ensemble $E$ tel que pour tout $x\in E$, $x \notin \emptyset$, alors $E \neq \emptyset$".
Raisonnement faux si E est mal défini au sens où déjà égal à l'ensemble vide. Mais vrai sinon. De même pour une démonstration de non P avec un non P contradictoire (non P => $\bot$), sans objet : elle serait fausse. Quelle est ta définition de non P à toi ? Est-elle consistante ?
[small](*) C'était ta traduction fausse de l'AO si tu te souviens.[/small]
Oui certes, une définition est une abréviation, mais une abréviation de quelque chose (idéalement consistant), non ?
Ltav ne voit pas d'erreur (donc ne comprend pas que les gens d'accord avec 1 et 2 peuvent pourtant ne pas du tout adhérer à 3 même s'ils lisent l'argument 4 qui suit):
1/ Dieu n'a pas de défaut
2/ ne pas exister est un défaut
3/ Dieu existe
4/ si 1 et 2 alors 3. Sinon Dieu aurait le défaut de ne pas exister.
Je crois même qu'il s'est inscrit pour ça. Je n'aurai pas la cruauté de mettre un lien vers ses tous premiers posts concernant ça :-D
Je ne vois pas où il pourrait y avoir un problème.
Si Ltav s'est inscrit pour cela, son inscription est nulle et non avenue.
CQFD.
Si j'en crois Ltav je suis à côté de la plaque.
Aux autres d'en juger.
LOL
P.S. Ton manque de cruauté t'honore grave
Ainsi tu nies qu’on puisse définir $non(P)$ par $P \Rightarrow Tout$ en LC ?
Sans s’occuper des tables de vérité ?
On n’obtiendrait pas quelque chose d’équivalent ?
Christophe :
Là tu abuses. Une définition existe en maths justement pour abréger.
Et dans ce débat ça sert pour savoir de quoi on parle quand on dit ce qu’est le « $non$ » par exemple.
Ne prends pas le même angle que Ltav.
Comprends que la LC étant plus puissante que la LI, elle a plus le choix de ses définitions. En LC, pas besoin de forcer pour avoir très naturellement une vraie démonstration de non P (prouvable grâce au tiers-exclu donc vrai RPA) : (P => tout) => non P. En LI, dénaturer et affaiblir ce raisonnement est le prix à payer pour éviter le tiers-exclu, il devient : non P => non P - ce qui l'on en conviendra est une démonstration "ridicule" de non P (on démontre CQFD par CQFD). La LI va réellement prouver "son" non P en démontrant par définition l'absurde à partir de P.
N.b. De quel angle à ne pas suivre parles-tu ?
Les élucubrations de Ltav, c'est genre "Dire que l'on a démontré un théorème pour la loi de composition interne d'un groupe et qu'il vaut aussi "tel quel" pour une groupe abélien est soit une grossière erreur, soit une pure arnaque sophistique du genre de celles qui prétendent dire la même chose que quelqu'un alors que l'on utilise ses mots avec des définitions différentes." L'argument pour les groupes tiendrait d'ailleurs plus debout puisqu'on a l'habitude d'appeler et de noter la l.c.i. d'un groupe abélien différemment de la l.c.i. d'un groupe général.
Ltav s'est trompé de forum. Il a d'indéniables talents de charlatanisme, mais c'est peu apprécié sur un forum de mathématiques.
Je cite des passages intrigants :
Moi : Sur la définition du non en L.I. ou en L.C. il m'a semblé que c'était la même justement :
Pour tout P, non(P):=(P=>Tout).
Ltav : Non [small]c'est moi qui mets en gras[/small], elles sont différentes, précisons-le : en LC, non P est par définition la proposition qui a une table de vérité exactement opposée à celle de P. On en déduit alors que non P <=> (P => tout) (mêmes tables de vérité à gauche et à droite de l'équivalence). Mais en LI (pour la définition la plus simple), on ne parle plus de tables de vérité (vrai/faux) : non P devient une pure abréviation de P => tout.
Moi :
Ainsi tu nies qu’on puisse définir non(P) par P=>Tout en LC ?
Sans s’occuper des tables de vérité ?
On n’obtiendrait pas quelque chose d’équivalent ?
Ltav :
En LC, il est tout à fait possible de prendre cette définition, oui puisque non P et (P => tout) sont parfaitement équivalentes
Je précise que je suis novice sur ce sujet.
Je vois une contradiction de tes propos Ltav.
Même en piochant dans tes propos, bien entendu, ils sont tronqués, j'ai gardé la prose pénible (à mon goût, c'est personnel, bien sûr).
Mais ce que Ltav voulait c'était que les gens acceptant 1 et 2 dans la vraie vie acceptent 3. Il ne voulait évidemment pas juste faire remarquer la forme. Il a même tenté d'écrire plein de choses en .. TDE .. (c'est courageux car tu aurais vu les fautes ça faisait peur pour lui) pour essayer de prouver que les deux occurrences du mot Dieu désignent le même Dieu.
Un peu comme un élève de 5ie qui n'est demordrait pas qu'une solution à l'équation [ X= 3 et 3X=700; inconnue X ] existe car sinon elle ne pourrait pas être égale à 3.
Si je dis que « $non(P)$ » est équivalent à « Q », faut-il encore savoir ce que moi j’appelle $non(P)$ ?
C’est un matheux qui pose une question de math.
Ne te laisse pas ensorceler par Ltav qui souhaite parler bien plus que d’écrire des maths.
On se demande qui joue finalement.
Ou alors je n’ai rien compris, après tout, ça me convient très bien.
Quand tu énonces le théorème : "Pour tout espace métrique (E,d), on a l'équivalence entre (E,d) est compact et toute suite à valeurs dans E admet une valeur d'adhérence", tu pourrais en théorie tout écrire dans le langage de ZF en remplaçant espace métrique par une phrase qui rappelle la définition, et idem pour compact, suite, suite extraite et valeur d'adhérence…
Même s'il n'y a peut-être pas suffisamment d'atomes dans l'univers pour écrire un tel énoncé… et je ne parle même pas de la démonstration.