Raisonnement par l'absurde (RPA)
Réponses
-
Bonjour,
http://www.les-mathematiques.net/phorum/read.php?16,1880930,1887800#msg-1887800
Ne remplace pas s'il te plaît mon argument par un autre complétement faux en général - c'est ce qu'on appelle faire un homme de paille avant de le brûler...
Je répète.
Prends Q = tout. La question c'est pourquoi pour démontrer non P, tu supposes systématiquement P au lieu de l'une parmi une infinité de propositions $Q_i$ entrant dans l'une parmi une infinité d'implications valides $q_i$ (voir définition dans mes posts ci-dessus) pour démontrer non P. La LC le justifie clairement par l'axiome du tiers-exclu et l'injectivité de la fonction non, alors que la LI se contente de matraquer : "parce que je l'ai décidé ainsi, en posant la définition non P := P => tout". -
1)
J’en suis là :
En logique classique on montre facilement : P => non(non(P))
On dispose d’un axiome appelé RPA qui dit : non(non(P)) => P.
On a donc l’équivalence : P <=> non(non(P)).
Ma question : existe-t-il une logique où l’on déclare le non involutif ?
Mon préambule prouve que la logique classique le fait.
Mais alors pourquoi je pose la question ?
Quand les gens déclarent « pour moi, non(non(P)) <=> P », ils ne parlent jamais du RPA.
Ils parlent, en les torturant un peu, du Tiers Exclu.
J’ai compris qu’il s’agissait d’une logique équivalente à la logique classique.
Est-ce la « logique naïve » ?
C’est exactement le thème du début du message de Christophe : http://www.les-mathematiques.net/phorum/read.php?16,1880930,1880930#msg-1880930
Il parle de « niveau grossier », de « faute ».
2)
Est-ce que tout le monde définit « non » par « implique TOUT » ?
Est-ce un choix de chaque auteur ?
Est-ce d’habitude plutôt fait en LI ? -
@Martial : je ne cherche pas à t'embrouiller mais au contraire à te suggérer une nouvelle clarté de raisonnement. Tu craignais d'avoir fait de lourdes erreurs dans tes livres à ce sujet mais ce n'est pas le cas à partir du moment où tu poses explicitement que tu raisonnes par l'absurde, ce qui implique automatiquement l'usage du tiers-exclu. Il n'y a rien d'une "terrible machine à gaz" à justifier ton raisonnement par l'absurde par le tiers-exclu, au contraire : tu lui apportes une véritable justification mathématique.
Dire que la proposition "racine(2) est irrationnelle" est vraie n'est pas plus lourd que dire que "racine (2) est rationnelle" est fausse... -
Tu dis que je déforme ton argument, puis tu répètes exactement le même. (:D
Pourquoi supposer $P$ pour démontrer $\bot$ et ainsi avoir une démonstration de $\neg P$ ?
Parce que la règle d'introduction du $\neg$ à droite est
$$\begin{array}{rcl} \Gamma, P&\vdash&\bot\\
\hline
\Gamma &\vdash&\neg P\end{array}$$
Ceci aussi bien en logique classique qu'en logique intuitionniste.
De même, pourquoi supposer $P$ pour démontrer $Q$ et ainsi avoir une démonstration de $P \Rightarrow Q$ ? Parce que que la règle d'introduction du $\Rightarrow$ à droite est
$$\begin{array}{rcl} \Gamma, P&\vdash&Q\\
\hline
\Gamma &\vdash& P\Rightarrow Q\end{array}$$
Même si on de définit pas $\neg P$ comme $P\Rightarrow \bot$, l'équivalence logique des deux se démontre aussi bien en logique intuitionniste qu'en logique classique.
Démontrer $\neg P$ en supposant $P$ pour en déduire l'absurde, c'est ce que tout le monde fait et c'est ce que formalisent les règles des systèmes de déduction conernant le $\neg$, qu'elles soient classiques ou intuitionnistes.
Ton baratin tourne complètement à vide, Ltav. -
Parlons sémantique, Ltav, puisque tu veux aller de ce côté. Quelle différence fais-tu entre "$P$ est fausse" et "$\neg P$ est vraie" ?? Du point de vue classique ? Du point de vue intuitionniste ?
-
@Dom :
Pour le point 1), il y a beaucoup de questions.
Du point de vue strictement syntaxique, $non$ n'est jamais involutif. Par contre, dans toute démonstration, tu as le droit de supposer tout ce que tu veux, tu peux même utiliser $0 = 1$ (et dans ce cas, on ne devra pas objecter que ta démonstration est fausse, mais qu'on est platement d'accord avec toi : en supposant $0 = 1$, on peut démontrer n'importe quoi). Il y a donc des démonstrations qui supposent $non(non(P)) \Leftrightarrow P$, d'autres non.
Si une des hypothèses d'une démonstration est $non(non(P)) \Rightarrow P$, on dit qu'elle "utilise l'axiome $RPA$". Si une des hypothèses est $P \ ou \ non(P)$, on dit qu'elle "utilise le tiers-exclu". Tiers-exclu et $RPA$, c'est "plus ou moins la même chose", dans le sens où si on admet d'autres axiomes logiques moins "polémiques", on peut facilement démontrer qu'on démontre les mêmes choses avec l'un ou avec l'autre.
Bref, si quelqu'un te dit "je travaille en logique classique", il n'aura pas le droit de te faire des objections sur $non(non(P)) \Rightarrow P$ si tu l'utilises dans une démonstration. Si quelqu'un te dit "je travaille en logique intuitionniste", si tu lui montres une démonstration où tu utilises $non(non(P)) \Rightarrow P$, il te dira "ha ben oui, mais bon moi je refuse ça, a priori".
Pour le point 2), de deux choses l'une :
- soit on décide d'utiliser l'abréviation $non(P) := P \Rightarrow \bot$ ;
- soit on décide que pour toute suite de caractères $P$ que l'on considère comme un énoncé, alors $non(P)$ doit aussi être considéré comme un énoncé ; et dans ce cas, si on choisit d'admettre une série d'énoncés pas très polémiques qui disent de $non$ ce qu'on voudrait qu'il soit, alors on peut démontrer que, pour tout $P$, $non(P) \Leftrightarrow (P\Rightarrow \bot)$.
Exemple : acceptons que les choses suivantes sont des démonstrations acceptables :
- on a $P$ et on a $non(P)$, et donc $\bot$ ;
- sous l'ensemble d'hypothèses $\Gamma$, supposons de plus $B$, blablablabla et donc $C$ ; et donc, sous l'ensemble d'hypothèses $\Gamma$, on a démontré $B \Rightarrow C$.
Alors $non(P) \Rightarrow (P \Rightarrow \bot)$ !
De plus, si on accepte que la chose suivante est une démonstration acceptable :
- sous l'ensemble d'hypothèses $\Gamma$, et l'hypothèse additionnelle $P$, on a conclu précédemment que $\bot$ ; et donc, sous l'ensemble d'hypothèses $\Gamma$, nous pouvons conclure que $non(P)$.
Alors $(P\rightarrow \bot) \Rightarrow non(P)$.
EDIT : J'ai oublié de conclure ! Bref, il ne faut pas trop s'inquiéter de savoir si $non(P)$ est défini comme $P\Rightarrow \bot$ ou non, quitte à ajouter des axiomes pour dire comment on voudrait que $non$ se comporte.
Et, remarque : quand je dis "polémique", ça dépend de la polémique :-D Ici, ça doit s'entendre comme "polémique au sens intuitionniste vs classique". -
Merci bien Georges.
Je crois que je viens de passer mon premier flocon sur ce thème.
;-) -
@Gbzm : http://www.les-mathematiques.net/phorum/read.php?16,1880930,1888046#msg-1888046
Je ne peux pas m'absenter quelques heures sans te retrouver étaler ton incompréhension totale (à supposer qu'elle soit de bonne foi) de mon argument. Tu l'as bel et bien changé mais tu le réaliserais mieux si tu arrêtais de prendre tes contradicteurs pour des baratineurs ou pire des...(désolé de parler ainsi).
A nouveau, il ne s'agit pas de remettre en cause que pour démontrer $(P => Q)$, je doive par définition supposer P pour en déduire Q. C'est absolument clair et évident et tu fais bien du radotage mais purement hors-sujet. Ma question est pourquoi, pour démontrer R, dois-je utiliser systématiquement $(P => Q) => R$ (supposée vraie), au lieu de l'une des relations $(Q_i => Q) => R$, vraie également pour tout $i \in \mathbb{N}$, avec des propositions $Q_i$ toutes différentes de P ? Eh bien, soit on impose ce choix par convention, en posant par exemple $R := (P => Q)$ comme en logique intuitionniste, soit on le démontre, comme en logique classique lorsque l'on déduit puissamment du tiers-exclu que : pour tout entier $i$, $Q_i = P$, ce qui justifie parfaitement en LC pourquoi on suppose P plutôt que l'une des innombrables $Q_i$. Est-ce plus clair pour toi ? -
Et que l'on puisse démontrer $(P => \perp) => non P$ aussi bien en LC qu'en LI ne change rien à ce raisonnement. Comme déjà dit, il existe une infinité de relations de ce genre toutes aussi démontrables en LI et pourtant celle-ci ne choisit que $(P => \perp) => non P$.
-
Ltav, toujours aussi creux.
Et tu ne réponds pas à ma question, que je répète.Quelle différence fais-tu entre "$P$ est fausse" et "$\neg P$ est vraie" ?? Du point de vue classique ? Du point de vue intuitionniste ? -
Ltav, tu écris:il ne s'agit pas de remettre en cause que pour démontrer $P\to Q$, je doive par définition supposer $P$ pour en déduire $Q$. C'est absolument clair et évident et tu fais bien du radotage mais purement hors-sujet
GBZM ne peut évidemment pas avoir dit une énorme connerie de ce genre. Tu insistes bien en disant que "c'est clair et évident" alors que c'est faux. Et tu ajoutes même l'adverbe "absolument".
Ce n'est qu'un exemple, je te connais, il n'y a pas d'hostilité de ma part, j'ai peu de dispo, je sais que tu n'y connais rien, et chaque passage que je me donne la peine de lire ou presque est grotesquement faux, même quand un débutant qui n'y connait rien pourrait voir lui-même que tu refuses d'être élémentairement logique.
Ca m'apparait être un choix de ta part, quelque chose de l'ordre de l'intime, peut-être une posture dissidente, je ne sais pas, mais c'est comme si tu essayais de battre des records de faussetés dans je ne sais quel but.
Mais en tout cas, je te rappelle une énième fois que le pseudo "L T A V" est un sigle qui ne donne aucune idée de ton identité (enfin pour moi), et que donc les aspects "fiers" de ta posture sont inutiles et ne facilitent pas la compréhension du message que tu veux envoyer. La longueur de tes posts non plus.
Si tu pouvais poster de petits posts (poste en PLUSIEURS SI TU VEUX). En dehors de GBZM, il est quasi-sûr que personne ne te lit plus, tu es ou bien trop faux ou trop vague dans tes déclarations. Tu as de la chance que GBZM t'accorde une (inexpliquable) attention aussi détaillée. Ne la gâche pas. Il finira lui aussi par ne plus te répondre sinon.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Tu écris aussi:Ltav a écrit:Ma question est pourquoi, pour démontrer R, [large]dois-je[/large] utiliser systématiquement $(P => Q) => R$ (supposée vraie), au lieu de l'une des relations $(Q_i => Q) => R$, vraie également pour tout $i \in \mathbb{N}$, avec des propositions $Q_i$ toutes différentes de P ?
Dans ce passage, tu affirmes un truc faux ET délirant (avec évocation de $\mathbb{N}$ qui pensait passer des vacances tranquilles :-D ) , mais en plus c'est une question :-D
Mais comment veux-tu que qui que ce soit réponde à ça. Ca n'a pas de sens autre que l'affirmation, fausse, présente dedans.
Ce sont tes mots et tes écrits, LTAV, pas ceux d'une autre personne!Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
De mon téléphone à dom
non est involutif en logique linéaire et affine. MAIS il porte un autre nom. Ces logiques sont strictement plus faible que la LI.
Ce n'est antinomique car le implique de la LI n'edt pas le même.
X implique intuitionnistement Y est une abréviation de "Avec X à volonté je peux obtenir UN exemplaire de Y"
Il suit que le X implique intuitionnistement Tout de la logique intuitionniste n'edt pas le vrai non X originel. Ce qui l'empêche d'être involutif. Car empêche d'être injectif.
Mais comme tout se joue sur le non clonage c'est transparent pour les gens qui discutent de ressources photocopiables. Dès lors les débats sont disjoints.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
La non injectivité est évidente quand tu remarques que nonLI (X+X) et nonLI( X) sont plus égaux que X+X et X ne le sont.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
-
Je suis dubitatif en raison de tes vulgarisations.
Mis je ne critique rien.
Ton « X+X » à la fin, est-ce un « X et X » ?
Je suis déjà ravi d’avoir ingurgité cette histoire de RPA.
Le cerveau est bizarre (le mien, au moins) : il a tout sous les yeux depuis quatre ans mais n’interprète les choses que depuis quatre jours.
Y a un temps pour tout comme dit....
[T’as vu AD ;-) ?]
[(tu) B-) AD] -
Oui X + X est un renomage de X et X pour insister sur la sensibilité au clonage.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
-
Dom sais tu programmer? Si oui je te donnerai les correspondances.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
-
Gbzm a écrit:Ltav, toujours aussi creux.
Voilà enfin un contrargument "plein"...Puisque tu n'as rien d'autre à rétorquer, ce débat est donc clos entre nous deux.
Pour ta question, ces propositions sont bien sûr sémantiquement équivalentes. Leurs démonstrations toutefois impliquent des techniques différentes dont j'ai maintes fois parlé (*). Je te renvoie à mes posts précédents.
[small](*) Pour démontrer Q vraie, où Q = non P, je suppose non Q, i.e. P par tiers-exclu, je montre l'absurde, donc P est faux, i.e. Q est vraie : c'est le raisonnement par l'absurde, valable en LC. Il explique pourquoi je suppose P et aucune autre proposition. Pour démontrer P fausse, je suppose P, j'arrive à l'absurde, donc P fausse : c'est la réduction à l'absurde, valable aussi en LI.[/small] -
Oui, dirais-je, car tu demanderas certainement des rudiments de programmation.
XCas à portée de main. Mais j’imagine que tout fait l’affaire. -
@Ltav
Ton astérisque contient des fautes évidentes attestant que tu ne te prends même pas toi-même au sérieux. C'est très difficile de capter tes intentions. À ce stade tu pourrais relire et corriger au moins les coquilles. Ou les laisses-tu exprès ?Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Je répondais à Ltav.
Dom : je demande juste que tu saches gérer en théorie pointeurs fonctions procédures. C'est bon ?Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Hum... « pointeur » est un vague mot... ça remonte (pour situer, DEUG MIAS, 1998, Turbo Pascal ou C++).
Mais vas-y, poste quand tu pourras, on sait être autodidacte de nos jours. On essaiera du moins.
Ça m’intrigue par contre, qu’est-ce que tu vas bien pouvoir me faire faire sur ce sujet ? -
Oui d'un PC je te ferai un topo. Essaie de te remettre au Pascal juste pour la différence entre
Procédure toto(s:intéger);
Et
Procédure toto(Var s: intéger);
C'est encore mieux que le C.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
@dom; plan de travail.
1/ Rouvre ton étude rapide du pascal.
2/ La logique intuitionniste c'est "que des fonctions et pas de var". Par exemple:
function carre (x:real): real; begin result:=x fois x end;
function prodac (a,b: real): real; begin result := a+b + ab end;
3/ La logique classique c'est des procédures et tu as droit au var.
Bien entendu, tu peux simuler la fonction précédente par exemple:
procedure prodac2 (a,b: real; var c:real); begin c:=a+b+ab end;
MAIS à la différence des fonctions, tu peux avoir plusieurs résultats comme dans:
procédure plusprod (a,b: real ; var s,p: real ) ; begin s:=a+b; p:=ab end;
Bien entendu, dans certains cas, tu peux simuler "totalement" avec des fonctions, des procédures contenant des var, mais d'autres fois non.
Soit X un type.
la procedure toto(a:Y; var b: X); begin blabla end
prend comme arguments l'objet $a$ de type $Y$, MAIS SURTOUT AUSSI l'objet $b$ de type $non(X)$
Dans un langage comme le C, une déclaration comme "var a:X" est remplacée par un pointeur. On écrira "a:@X", signifiant $a$ est de type "pointeur vers X".
Comme tu peux le noter, "pointeur vers X" a la même nature que "non(X)", c'est une des grandes et subtiles découvertes de la CCH récente. "On désire ce qu'on n'a pas"
Je te le dis autrement, mais vite: écrire dans a, c'est pareil que lire @a (autrement dit, écrire dans a, c'est lire non a). Il suit que si tu imposes une assymétrie PLUSSSS un droit de clonage, tu tombes sur une logique bancale, qui est précisément la logique intuitionniste, qui lit autant de fois qu'elle veut une ressource, mais doit payer un prix non nul ses droits en écriture.
La logique classique est équilibrée (symétrique) elle lit autant qu'elle veut ses ressources et écrit autant qu'elle veut dans ses ressources. Mais elle correspond à un traitement seulement réduit aux ressources clonables.
Les logiques linéaires et affines n'ont pas ces pouvoirs, mais analysent toutes les natures de ressources (logiques plus faibles s'appliquant donc à plus de mondes).
Le RPA correspond à prétendre qu'il y a une canonique permettant de manière universelle de lire dans a de type X à partir de b de type @(@X). C'est la découverte de Timothy Grffin (ou Griffith, je n'arrive jamais à me rappeler).
En bref, (hors informatique): le "vrai non" est involutif (il permute Lea et Bob dans un jeu où ils s'affrontent, l'appliquer 2 fois ramène à la situation de départ).
La fonction $x\mapsto $ (à volonté $x) \to Tout$ que je note nonLI, n'a strictement aucune raison d'être involutive (écris tout, tu verras)
Lorsqu'on ignore ça, (ie qu'on collapse $x$ avec $(x$ et $x)$) on voit émerger les deux logiques historiques "vieilles" que sont LI et LC.
Et au cas où ça te déstabiliserait, le fait que $(non(x)) = (x\to FAUX)$ se prouve exactement de la même manière dans toutes les logiques, mais, espièglement a des significations différentes, puisque concernent un "non" différent entre les 2 faibles (linéaires et affines) et les 2 fortes (LC et LI).
Seule la linéaire (parmi les 4) échappe à $FAUX = Tout$.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Ok, Christophe. Cela va certainement me prendre du temps pour embrayer sur "tout ça".
Je ne promets rien dans l'immédiat. Je te remercie tout de même. Coupe ton portable dans ton lit ! :-P
Digression :
Je suis une bille en théorie des ensembles.
Mais il me semble que l'on n'a "que" les symboles $\in$ et $\notin$ (je me comprends quand je dis "on n'a que").
Elle dit : si on $x \in \mathbb Q$ et $ x\notin \mathbb Q$, alors $x \in \emptyset$.
1) Quand on dit $non(\sqrt{2}$ est irrationnel$)$, qu'est-ce qu'on va chercher d'autre que : $\in \mathbb Q$ ou $\notin \mathbb Q$ ?
Je veux dire :
1a) est-ce la théorie des ensembles qui "ne pense pas à tout" ? qui est "incomplète" (mot naïf et non professionnel).
1b) est-ce la logique qui crée une autre "instance" que $\in \mathbb Q$ ou$_{exclusif}$ $\notin \mathbb Q$ ?
Dit-elle "on ne sait pas lequel est le bon" ou "il peut y avoir autre chose" ou "on peut avoir les deux" ou "on peut avoir ni l'un ni l'autre" ?
Je me restreins à ce cas trivial d'être ou non rationnel.
2) question déjà mal posée de ma part : quand on nie une proposition en changeant les $\forall$ en $\exists$ (et vice-versa, etc.), on fait de la logique classique et pas de la logique intuitionniste ?
Ou bien ça n'a rien à voir ? -
@Dom : Je ne suis pas sûr de ce que je vais dire, mais Christophe corrigera au besoin. Quand je disais, tout à l'heure, qu'il y avait différentes polémiques, c'est que le débat : "Est-ce que le RPA est un axiome qu'on veut dans nos maths ou non ?" a été fructueux car a suscité l'étude de la logique intuitionniste ; mais de nos jours, il y a d'autres débats, comme par exemple "Est-ce que si on suppose une hypothèse, cela va de soi que l'on peut l'utiliser plusieurs fois ?". Par exemple, pour citer Girard, si j'ai un euro, je peux acheter un café (à un euro) et je peux acheter un déca (à un euro), mais je ne peux pas acheter un café et un déca (puisque je n'ai qu'un euro). Ça donne lieu à d'autres logiques, etc. Et je crois que Christophe veut "te faire sentir" ce genre de problèmes.
-
@Dom
1) Veux-tu que je te fasse un tour de passe-passe toposique où l'on voit que la réunion des valeurs de vérité de "toto rationnel" et "toto irrationnel" n'est pas tout ?
Pas ce soir
2) Entre $\neg \exists x\ P$ et $\forall x\ \neg P$, y en a-t-il un qui entraîne l'autre intuitionnistement ? Si oui, lequel ? Je pense qu'intuitivement (à défaut d'intuitionnistement), tu peux le sentir. -
@Cc : http://www.les-mathematiques.net/phorum/read.php?16,1880930,1888206#msg-1888206
Au lieu de juste ricaner et partir dans tous les sens, pourrais-tu s'il te plaît préciser ce que tu contestes et pourquoi tu le contestes (entre "délire", "faux", "$\mathbb{N}$ qui voulait passer des vacances tranquilles", etc. on ne s'y retrouve plus).
Nota bene: Depuis pas mal de temps, sauf exception, tu n'oses plus rentrer dans le détail des arguments et préfères te cacher derrière des pitreries "quasi-désespérées" du même genre. Il est vrai que quand tu acceptes (toi ou d'autres du même comportement) de jouer le jeu de l'échange scientifique rigoureux, ça donne presque toujours des choses comme
http://www.les-mathematiques.net/phorum/read.php?16,1886712,1888360#msg-1888360
J'attends le détail de tes objections. Merci.
Bonne nuit à tous. -
OK Georges.
GaBuZoMeu :
Hum.
1) Je ne sais pas si je vais pouvoir suivre... mais je veux bien. On verra.
2) Je vais réfléchir à ça... -
@dom il me semble probable que GBZM avait L'INTENTION de te confronter à:
Non forall P
vs
Exists non P
Et qu'il a inversé par inadvertance.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Non Christophe. J'avais bien l'intention d'écrire ce que j'ai écrit. Ça te pose un problème ? Par ailleurs il est aussi intéressant de se poser la question que tu poses.
-
C'est quoi le problème, GA ?
-
Ah merci (pour moi et pour dom si je l'ai induit en erreur).
Les flèches ne sont pas des implications et le $+$ est le et tensoriel linéaire ("adjoint" du implique):
@dom: ne lis pas.
$$(R(a))\to (\exists xR(x))\to Tout$$
établit que $(non(\exists xR(x)))\to (\forall x: (non(R(x))))$
La réciproque vient du fait que $\exists x : (R(x))$ est la borne supérieure des $R(a)$ qui, pour chaque $a$, implique $(\forall x(non(R(x))))\to Tout$, dont il suit que:
$$(\exists x: R(x)) \to [(\forall x:nonR(x)) \to Tout ] $$
qui peut se réécrire:
$$[(\exists x: R(x)) + (\forall x:nonR(x))] \to Tout $$
et aussi
$$[ (\forall x:nonR(x))+(\exists x: R(x)) ] \to Tout $$
et aussi
$$ (\forall x:nonR(x))\to [(\exists x: R(x)) \to Tout ] $$
ce qui m'amenait à ne pas comprendre pourquoi tu demandais à dom "LAQUELLE".
Mais suis pressé et ai peut-être raté un épisode de vos échanges.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Haha !
Je ne tricherai pas !
La question de Christophe « n’as-tu pas plutôt voulu dire ça ? » m’a encouragé à revoir mon jugement sur « qu’est-ce qui intuitivement (sens courant) entraîne l’autre ? ». Mais je n’avais pas vraiment poussé la réflexion. J’entends par là fournir un argumentaire, du langage courant, qui pourrait inciter à convaincre.
Je vais réfléchir encore (il me faut du temps et du calme).
Aussi : je pense à des choses très concrètes comme.
Dans le plan, on sait définir « droite sécantes ».
Et on définit « droites parallèles » par « non(droites sécantes) ».
Dans l’espace, le même « droites sécantes » marche encore mais pas « non(droites sécantes) » car on n’obtient pas ce que l’on veut.
Mais j’imagine que le noyau du problème se situe à un autre niveau que ces rudiments de géométrie du secondaire.
Cela dit ça m’amuse* tout de même (sans prendre cela à la rigolade, hein, sans mépriser le thème des questions).
C’est ludique je trouve. -
Tu as raison Christophe, à la relecture j'ai sans doute mal formulé ma question. Il vaudrait mieux formuler comme ça, de façon plus neutre :
Dans le formalisme intuitionniste, quel rapport logique
- entre $\neg\exists x\ P$ et $\forall x\ \neg P$,
- entre $\neg\forall x\ P$ et $\exists x\ \neg P$ ? -
Ok.
Si une idée me vient, j’écris... -
En attendant, le tour de passe-passe toposique promis :
On se place dans le topos des faisceaux sur un espace topologique $X$. Dedans on a :
- un objet des nombres rationnels $\mathbb Q_X$, qui est le faiceau constant $\mathbb Q$. Ça veut dire que les sections de ce faiceau sur un ouvert $U$ de $X$ sont les fonctions localement constantes de $U$ dans $\mathbb Q$.
- un objet des nombres réels (de Dedekind) $\mathbb R_X$, qui est le faisceau des fonctions continues à valeurs réelles. Ça veut dire que les sections de ce faisceau sur un ouvert $U$ de $X$ sont les fonctions continues de $X$ dans $\mathbb R$.
Pas de panique donc, on travaille avec des objets bien rassurants : les fonctions localement constantes à valeur rationnelles, et les fonctions continues à valeurs réelles. On s'intéressera essentiellement aux sections globales (définies sur $X$), qu'on appellera "éléments" (bien que ce soit une très mauvaise idée de faire ça). Les "éléments" de $\mathbb R_X$ sont les fonctions continues $X\to \mathbb R$, et parmi elles les "éléments" de $\mathbb Q_X$ sont les fonctions localement constantes $X\to \mathbb Q$.
Prenons maintenant pour $X$ un espace bien sympathique : $X=\mathbb N\cup \{\infty\}$ le compactifié d'Alexandrov de $\mathbb N$ avec la topologie discrète. Rappelons que les voisinages de $\infty$ sont les complémentaires de parties finies de $\mathbb N$. Les "éléments" de $\mathbb R_X$ sont les couples $(u,\ell)$ où $u:\mathbb N\to \mathbb R$ est une suite réelle qui converge vers le réel $\ell$ ; parmi eux, les "éléments" de $\mathbb Q_X$ sont les $(u,\ell)$ où $u$ est une suite de nombres rationnels qui stationne à partir d'un certain rang, et $\ell$ la valeur rationnelle où $u$ stationne.
Si $(u,\ell)$ est un élément de $\mathbb R_X$, quelle est la valeur de vérité de la phrase "$(u,\ell)$ est rationnel". Une valeur de vérité, c'est un ouvert de $X$. L'intersection de la valeur de vérité de "$(u,\ell)$ est rationnel" avec $\mathbb N$ est l'ensemble des entiers naturels $n$ tels que $u(n)\in \mathbb Q$. Et $\infty$ appartient à cette valeur de vérité si et seulement si la suite $u$ stationne sur une valeur rationnelle à partir d'un certain rang.
Quelle est la valeur de vérité de "$(u,\ell)$ n'est pas rationnel" (ou "$(u,\ell)$ est irrationnel") ? La restriction de $(u,\ell)$ à tout ouvert contenu dans cette valeur de vérité n'a pas le droit d'être rationnelle ; la valeur de vérité de "$(u,\ell)$ est irrationnel" est l'intérieur du complémentaire de la valeur de vérité de "$(u,\ell)$ est rationnel". L'intersection de la valeur de vérité de "$(u,\ell)$ est irrationnel" avec $\mathbb N$ est l'ensemble des entiers naturels $n$ tels que $u(n)\not\in \mathbb Q$. Et $\infty$ appartient à cette valeur de vérité si et seulement si tous les $u(n)$ sont irrationnels à partir d'un certain rang.
Considérons l'élément de $\mathbb R_X$ donné par le développement décimal de $\sqrt2$ : $u=(1,1.4,1.41,1.414,\ldots)$ et $\ell=\sqrt 2$. Ce n'est pas un "élément" de $\mathbb Q_X$ : la valeur de vérité de "$(u,\ell)$ est rationnel" est $\mathbb N$, $\infty$ n'y appartient pas. Par contre, la valeur de vérité de "$(u,\ell)$ est irrationnel" est vide. Et par conséquent, la valeur de vérité de "$(u,\ell)$ n'est pas irrationnel" est tout $X$. Ceci montre que $\mathbb Q_X$ n'est pas non-non clos dans $\mathbb R_X$, contrairement à ce que j'aurais parié.
La raison de mon pari loupé : et si on était parti avec un espace $X$ localement connexe, au lieu de notre compactifié d'Alexandrov de $\mathbb N$ qui ne l'est pas ? -
@GaBuZoMeu : Pardon, c'est que je t'ai imaginé direGaBuZoMeu a écrit:Ça te pose un problème ?
-
Je suis trop loin.
J’ai vu pour la dernière fois les catégories en 2002.
J’ai eu un module de maîtrise en « topologie algébrique » mais honnêtement je dois bien reconnaître que j’étais une bille, même en algèbre linéaire toute bête.
Je ne sais pas ce qu’est un topos (j’en ai lu un topo (:P)).
Les faisceaux, ça m’interpelle au niveau du vécu...
Bon, merci bien entendu, qui sait, j’arriverais peut-être à récoler les morceaux.
Je vais quand même aller voir ces objets...ça prendra du temps. -
Dom : tu me feras un résumé, merci !
-
Haha.
Si j’en suis capable.
Mais la description de m’sieur GaBuZoMeu nous prend par la main...
À plus tard.
PS : faut rajouter un jour de WE en pleine semaine pour moi, mais je ne sais pas si c’est dans les tuyaux... -
Dom, il n'y a en fait pratiquement pas de catégorie dans mon message. Ça parle juste de topologie, de fonctions réelles continues et de fonctions localement constantes à valeurs rationnelles. Si tu surmontes ton sentiment a priori que tu n'y comprendras rien, je pense que tu peux parfaitement comprendre ce qui se passe.
-
Oui, oui, ton descriptif (est-ce le bon mot ?) des objets est clair pour que je parvienne à m'investir :-).
-
La description est formelle, mais je pense (je parle de l'image toposique de GBZM) que la difficulté est de se convaincre (et ça c'est la spécialité "topos") qu'on récupère bien toute la puissance, par exemple ici, des raisonnements intuitionnistes faisables "directement".
En tout cas, merci à toi, GBZM pour cet exemple. Je n'ai aucun dispo hélas et toujours pas taffé la partie "topos de faisceaux", mais je peux apporter un témoignage de ressenti immédiat à toute fin utile:
1/ Quand on est une structure, on peut s'amuser à travailler avec les structures "produits de copies de ladite" (ou même produit de diverses ayant même signature). Par exemple, si on a $M$ un modèle de ZF, et $J$ un ensemble quelconque, on peut prendre $M^J$ et tout répercuter.
Les vrai/faux deviennent des éléments de $\{vrai; faux\}^J$
si $f,g$ sont dans $M^J$, la valeur de $[f\in g]$ est $i\in J\mapsto [f(i)\in g(i)]$
2.1/ Ce que semble proposer le toposisme c'est un peu pareil, mais où au lieu de $M^J$, on ne prend que les éléments de $M^J$ qui sont continues de $J$ dans $M$. Mézalor, $J$, comme $M$ doivent êter doté d'une topologie. Alors pour $J$ elle est bêtement donnée, mais pour $M$, mystère, mystère... Et je pense que c'est là qu'on paie le ticket d'entrée de la spécialité, à savoir qu'on "sait depuis Grothendieck doter $M$ d'une topologie en fonction de celle de $J$ j'imagine"
2.2/ et derrière, la valeur d'un $f\in g$ n'est plus comme avant $\{i\in J \mid f(i)\in g(i)\}$, mais son intérieur.
Voilà, je délire peut-être totalement, c'était mon ressenti, provenant ce que je connais de domaines parents (ultrapuissances, forcgin).Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
A moins qu'on ne se prenne pas le chou et qu'on ne dote pas $M$ d'une topo, mais juste qu'on décide brutalement que $[f\in g]:= interieurDe(\{i\in J\mid f(i)\in g(i)\})$?Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
-
Il n'y a pourtant rien de mystérieux.
On a une fonction continue $f$ de $X$ dans $\mathbb R$, c.-à-d. un "élément" de $\mathbb R_X$. La valeur de vérité de "$f$ est rationnel" est le plus grand ouvert sur lequel $f$ est localement constante à valeurs rationnelles.
De manière générale on a un faisceau $F$ et un sous-faisceau $G$. Si $f$ est un "élément" de $F$, la valeur de vérité de $f\in G$ est le plus grand ouvert sur lequel $f$ est une section de $G$.
J'ai décrit quelles étaient les sections de $\mathbb R_X$ et $\mathbb Q_X$ sur un ouvert $U$ de $X$ : les fonctions réelles continues d'un côté, les fonctions rationnelles localement constantes de l'autre. -
Oui je comprends parfaitement ton post si j'admets ce que tu n'as pas justifié. Mais (mais attention tion je n'ai pas "encore travaillé" j'en suis resté au fait que la def de Max du mot faisceau avait un sens, pas obligé de me répondre donc) comme tu as l'air d'avoir des raccourcis personnels qui te permettent de voir vite que le IR de ce modèle est bien ce que tu dis (idem pour le IQ) , je me demaais s'ils étaient t exprimables. Tu m'as donc bien fourni l'info generale via le faisceau, mais il me manque: "sous faisceau" et une éventuelle "justification raccourcie de ta def "être un "élément"" faisant clin d'oeil aux topos.
Éventuellement comme je sais théoriquement ce qu'est un faisceau (comme prefaisceau cohérent au sens où max l'avait énoncé) si ça te prend 3 mn peux tu me donner la définition DU FAISCEAU merci ici que tu utilises? Merci. Et pas d'obligation, vu que tu as déjà donne un poly que je n'ai pas encore travaillé assez.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
J'utilise la même définition de faisceau que Maxtimax, il n'y en a pas 36 (juste 2, si on compte le point de vue "espace étalé" que je n'utilise pas ici).
Les classes de fonctions définies par une propriété de nature locale (continue, localement constante, $C^k$ ...) donnent naturellement des faisceaux. -
Merci je me mets le lien pour l'avoir sous la main.
Ce post de Max m'avait permis de vérifier qu'un faisceau est bien un prefaisceau particulier donc que j'étais sur le bon autoroute. Mais je ne me suis toujours pas familiarisé avec le "vocabulaire rapide" associé: section, sous faisceau, fibre etc.
Il va me falloir de la disponibilité.
http://www.les-mathematiques.net/phorum/read.php?16,1870394,1872212#msg-1872212Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.
Bonjour!
Catégories
- 164.6K Toutes les catégories
- 44 Collège/Lycée
- 22.1K Algèbre
- 37.4K Analyse
- 6.3K Arithmétique
- 57 Catégories et structures
- 1.1K Combinatoire et Graphes
- 13 Sciences des données
- 5.1K Concours et Examens
- 18 CultureMath
- 50 Enseignement à distance
- 2.9K Fondements et Logique
- 10.6K Géométrie
- 80 Géométrie différentielle
- 1.1K Histoire des Mathématiques
- 74 Informatique théorique
- 3.9K LaTeX
- 39K Les-mathématiques
- 3.5K Livres, articles, revues, (...)
- 2.7K Logiciels pour les mathématiques
- 24 Mathématiques et finance
- 332 Mathématiques et Physique
- 4.9K Mathématiques et Société
- 3.3K Pédagogie, enseignement, orientation
- 10.1K Probabilités, théorie de la mesure
- 789 Shtam
- 4.2K Statistiques
- 3.8K Topologie
- 1.4K Vie du Forum et de ses membres