Raisonnement par l'absurde (RPA)
Je refais une 023784643648 ième fois un fil sur ce thème.
Plusieurs niveaux. Un niveau grossier (et fautif), un niveau correct, mais découvert au 20ième siècle.
1.1/ Au niveau grossier, parfois utilisé "fautivement" dans le secondaire, on a une égalité en amont bien au dessus de tout le reste qui est l'élimination de non non (en français ne pas ne pas être venu = être venu). C'est légalité "en dur" qui que soit $x$:
$$ non(non(x)) = x$$
1.2/ A ce niveau (je le répète non pertinent), le RPA n'est pas utile, puisque tout ce qu'on peut prouver avec peut l'être sans. Et "à ce niveau" toujours, la FORME de raisonnement appelée RPA est proche de "si je peux déduire une contradiction de P alors j'ai non P", ce qui vue l'égalité supposée "en dur" s'écrit aussi "si je peux déduire une contradiction de nonP, alors j'ai P"
Il n'y a rien de plus à dire sur ce niveau puisqu'il est de toute façon scientifiquement fautif. Enfin "fautiof" dans le sens où il présenterait le RPA comme nécessaire et non comme un simple raccourci.
2/ Le niveau correct: il est lié à deux découvertes majeures.
2.1/ D'une part on peut prouver que $non(x)=(x\to Tout)$ avec des axiomes très faibles, ce qui oblige à s'apercevoir qu'affirmer $non(non(x)) = x$ c'est affirmer $((x\to Tout) \to Tout) =x $. Tout de suite, vu comme ça, ça sent l'audace mystérieuse. De plus, si on n'admet plus que $((x\to Tout) \to Tout) =x $, on s'aperçoit vite qu'on ne parvient pas à le prouver avec "le reste des axiomes".
2.2/ Mais que veut dire "le reste"? Et bé, en fait, il a été découvert que ces notions sont robustes, qu'il n'y a pas 1000 manières de les présenter (enfin précisément que quelle que soit la façon dont on les présente, on retombe toujours à peu près sur les mêmes phénomènes) et du coup "le reste" s'est mis à porter un nom: logique intuitionniste
2.3/ En conséquence de quoi, l'axiome qui dit que $[((x\to Tout) \to Tout) ]\to x $ lui s'est mis aussi à porter un nom, et s'appelle l'axiome du raisonnement par l'absurde.
Voili, voilou, pour le premier volet. Ca permet aussi de rappeler que les gens qui croient faire un RPA en prouvant que $x\to Tout$ de la manière suivante: "je suppose $x$ et j'en déduis $Tout$" se trompent.
Exercice: prouver qu'en fait il suffit d'imposer l'injectivité de $non$ pour avoir le RPA, ie que le SEUL AJOUT DE $\forall x,y: $ si $non(x)=non(y)$ alors $x=y$ SUFFIT à récupérer le RPA.
3/ Bon, mais l'histoire ne s'arrête pas là. Il apparait en effet complètement gratuit de refuser le statut involutif à non. C'est même ... complètement ridicule. En effet, à ce jeu, on pourrait tout aussi bien enlever 3 axiomes au hasard aux systèmes et les étudier. On n'aurait pas fini. Pourquoi privilégier celui-ci? La suite des 3.i répond:
3.1/ La science n'est ni la religion ni la philosophie. Le sens n'y a strictement aucune place acceptable (le sens est là pour guider les humains à faire de la science, mais il ne fait pas partie du contenu qu'elle garantit à coups de preuves)
3.2/ Quand le jeu est équilibré, ie quand personne n'est handicapé dans un match entre 2 scientifiques pas d'accord sur un énoncé, ie quand on n'a pas décidé de dire que c'est Bil qui a la charge de la preuve et Tom qui peut se vautrer dans son hamac et répondre systématiquement "prouve-le" à chaque pas de Tom, le statut de "non" est parfaitement clair et IL EST BIEN INVOLUTIF. On a la situation suivante:
3.3/ Autrement dit, non(non(A))= A pour la simple raison que
et que $(x$\mapsto $ Tom défend $x)$ est injective
3.4/ Il suit une situation scientifique étrange.
"Bon, alors, me..e on l'adopte ou pas ce non non = id et par pitié ne me parlez pas d'intuitionnisme, je veux du sincère et technique, pas d ela philo"
3.5/ Pour résoudre cet apparent problème, il faut aller voir de plus près ce qu'est une garantie scientifique. Elle est photocopiable (une photocopie de la preuve $p$ a la même efficacité que l’originale).
3.6/ Alors pourquoi nous ne savons pas répondre par exemple à la question:
"Bil a acheté 3 pommes et Bil a acheté 3 pommes. Combien dépense-t-il sachant que la pomme coute 7 euros? "
Alors que nous savons répondre à la question
"Bil a acheté 3 pommes et Bil a acheté 3 poires. Combien dépense-t-il sachant que la pomme (ainsi que la poire) coute 7 euros? "
3.7/ Et bé tout simplement parce que nous préjugeons que les maths sont immuables. Très bien, vous me direz, "bin, voui, mais on a raison, elles le sont". Certes, mais il n'existe pas de preuve qu'elles le sont.
3.8/ La Nature ne peut donc pas avoir rendu prouvable des choses qui en s'identifiant feraient exister une telle preuve. Et ce n'est pas un petit truc subtil, nous cotoyons chaque jour des structures (par exemple $(\R, +)$ ) où $a\to b$ s'y rencontre très bien (sans que nous en ayons conscience), mais porte le nom $b-a$, etc. Bref, ce n'est pas le non non = id le problème, mais le $a = (a+a)$ généralement présenté sous la forme $a= (a\ et\ a)$ qui n'est pas rien car il dit, "toute garantie de $a$ est duplicable". S'il y a bien un truc qui est profondément faux (et les 14000 SDF logés sous la défense en savent quelque chose) c'est ça. Avec 5euros, vous n'avez pas 10euros.
3.9/ Comme à l'exception de celui-ci, TOUS LES AUTRES axiomes logiques marcheraient aussi très bien en mettant "garantie" à la place de "preuve", on voit bien que la duplication est un (et même LE) éément très fort de traduction de l'immuabilité des maths dans les axiomes.
3.10/ Bref, en conclusion, on a bien "non non = id". Le problème "n'était pas non plus là". L'obsession intuitionniste, et son étude pour elle-même est une très belle aventure de l'humanité, qui est tombée dans le ravin et au lieu de pleurer, a visité une forêt inattendue, mais elle coinçait en ce qu'elle n'assumait pas que n'importe qui adopte AVANT toute autre chose que non non ) id.
3.11/ In fine, on a étudié tout ça, fait des conférences, des programmes, embauché des gens, et tout est devenu clair (et il n'est pas devenu interdit d'étudier pour autant la logique intuitionniste).
3.12/ Les conclusions sont:
3.12.1/ On a bien "non(non(A)) = A" (même si on le dit autrement pour ne pas froisser le souvenir de gens (parfois morts et ne pouvant se défendre))
3.12.2/ On n'a pas A => (A et A). (Ce qui n'interdit pas de le supposer, mais alors faut l'assumer, et ça touche la reproductibilité scientifique qui par ailleurs est mise face au défi majeur de la quantique qui n'autorise pas la clonage)
3.12.3/ On obtient la logique intuitionniste en DEFINISSANT (elle devient émergente):
(A=>B) := (Avec autant de fois la garantie de A que je veux, je peux garantir
3.12.4/ On obtient la logique classique en DEFINISSANT (elle devient émergente elle aussi):
(A=>B) := (En clonant tout ce que je veux, quand je veux, où je veux, etc, je peux garantir B from A)
3.12.5/ Dans ce contexte le "ridicule" de vouloir prouver le raisonnement par l'absurde intuitionnistement se voit bien, puisqu'il demande de garantir A à partir d'une garantie qui, moyennant que vous lui apportiez tous les clones qu'elle demande de garanties de A, vous envoie au paradis.
3.12.6/ Ca se voit aussi très bien dans les jeux. Il est plus facile de "battre Kasparov ou Karpov" que de battre Kasparov (on admet que comme vous êtes un illustre inconnu, vous avez le droit de choisir la couleur). Il est ULTRAFACILE d'en battre au moins un des deux. Mais vous avez DEUX COPIES d'épreuves et vous n'épatez que les spectateurs locaux d'une des 2, et vous ne pouvez même pas prévoir à l'avance qui.
4/ Le "vrai" RPA:
Tout ce qui précède devrait vous convaincre que:
4.1/ Même quand vous prouvez A en concluant "donc A" après avoir prouvé ((A=>Tout)=>Tout) (ce qui est présenté, comme "le vrai" RPA, et bien ce n'en est pas tout à fait un vrai si vous n'avez utilisé QU UNE SEULE FOIS L HYPOTHESE A=>Tout (RPA light) dans votre preuve de ((A=>Tout)=>Tout)
4.2/ Bon, mais c'est un peu subtil pour les gens de compter combien de fois ils utilisent une hypothèse. C'est un hobby possible pour un matheux non expert de ça.
4.3/ En effet, tout ce que vous pourrez prouver via le RPA light sera prouvable sans AUCUN RPA (sauf à tricher vocabulairement.
4.4/ Le vrai de vrai de chez vrai RPA, c'est donc quand vous utilisez explictement l'axiome suivant (et je termine là, mal à la main):
$$ ((A\to Tout ) \to ((A\to Tout)\to Tout)) \to A $$
4.5/ En général on "le sent passer dans ses veines". La duplication d'une hypothèse, ça se ressent tactilement quand on fait des maths. Don't worry. Il y en a même que ça traumatise comme le montre l'argument qui suit:
4.6/ [small]With $e := \{x\mid (x\in 1x)\to (3=7)\}$, have:
$(e\in e) \to ((e\in e) \to (3=7))$ donc
$(e\in e) \to (3=7)$ donc
$e\in e$ (1)
On vient de prouver $e\in e$
$(e\in e) \to ((e\in e) \to (3=7))$ donc
$(e\in e) \to (3=7)$ donc
on vient de prouver $(e\in e) \to (3=7)$ (2)
par (1,2), donc $3=7$.[/small]
Plusieurs niveaux. Un niveau grossier (et fautif), un niveau correct, mais découvert au 20ième siècle.
1.1/ Au niveau grossier, parfois utilisé "fautivement" dans le secondaire, on a une égalité en amont bien au dessus de tout le reste qui est l'élimination de non non (en français ne pas ne pas être venu = être venu). C'est légalité "en dur" qui que soit $x$:
$$ non(non(x)) = x$$
1.2/ A ce niveau (je le répète non pertinent), le RPA n'est pas utile, puisque tout ce qu'on peut prouver avec peut l'être sans. Et "à ce niveau" toujours, la FORME de raisonnement appelée RPA est proche de "si je peux déduire une contradiction de P alors j'ai non P", ce qui vue l'égalité supposée "en dur" s'écrit aussi "si je peux déduire une contradiction de nonP, alors j'ai P"
Il n'y a rien de plus à dire sur ce niveau puisqu'il est de toute façon scientifiquement fautif. Enfin "fautiof" dans le sens où il présenterait le RPA comme nécessaire et non comme un simple raccourci.
2/ Le niveau correct: il est lié à deux découvertes majeures.
2.1/ D'une part on peut prouver que $non(x)=(x\to Tout)$ avec des axiomes très faibles, ce qui oblige à s'apercevoir qu'affirmer $non(non(x)) = x$ c'est affirmer $((x\to Tout) \to Tout) =x $. Tout de suite, vu comme ça, ça sent l'audace mystérieuse. De plus, si on n'admet plus que $((x\to Tout) \to Tout) =x $, on s'aperçoit vite qu'on ne parvient pas à le prouver avec "le reste des axiomes".
2.2/ Mais que veut dire "le reste"? Et bé, en fait, il a été découvert que ces notions sont robustes, qu'il n'y a pas 1000 manières de les présenter (enfin précisément que quelle que soit la façon dont on les présente, on retombe toujours à peu près sur les mêmes phénomènes) et du coup "le reste" s'est mis à porter un nom: logique intuitionniste
2.3/ En conséquence de quoi, l'axiome qui dit que $[((x\to Tout) \to Tout) ]\to x $ lui s'est mis aussi à porter un nom, et s'appelle l'axiome du raisonnement par l'absurde.
Voili, voilou, pour le premier volet. Ca permet aussi de rappeler que les gens qui croient faire un RPA en prouvant que $x\to Tout$ de la manière suivante: "je suppose $x$ et j'en déduis $Tout$" se trompent.
Exercice: prouver qu'en fait il suffit d'imposer l'injectivité de $non$ pour avoir le RPA, ie que le SEUL AJOUT DE $\forall x,y: $ si $non(x)=non(y)$ alors $x=y$ SUFFIT à récupérer le RPA.
3/ Bon, mais l'histoire ne s'arrête pas là. Il apparait en effet complètement gratuit de refuser le statut involutif à non. C'est même ... complètement ridicule. En effet, à ce jeu, on pourrait tout aussi bien enlever 3 axiomes au hasard aux systèmes et les étudier. On n'aurait pas fini. Pourquoi privilégier celui-ci? La suite des 3.i répond:
3.1/ La science n'est ni la religion ni la philosophie. Le sens n'y a strictement aucune place acceptable (le sens est là pour guider les humains à faire de la science, mais il ne fait pas partie du contenu qu'elle garantit à coups de preuves)
3.2/ Quand le jeu est équilibré, ie quand personne n'est handicapé dans un match entre 2 scientifiques pas d'accord sur un énoncé, ie quand on n'a pas décidé de dire que c'est Bil qui a la charge de la preuve et Tom qui peut se vautrer dans son hamac et répondre systématiquement "prouve-le" à chaque pas de Tom, le statut de "non" est parfaitement clair et IL EST BIEN INVOLUTIF. On a la situation suivante:
(Tom défend A) = (Tom attaque (non A) ) = (Bil défend non(A)) = (Bil attaque A) = ...
3.3/ Autrement dit, non(non(A))= A pour la simple raison que
Tom défend A = Tom attaque nonA = Tom défend non non A
et que $(x$\mapsto $ Tom défend $x)$ est injective
3.4/ Il suit une situation scientifique étrange.
"Bon, alors, me..e on l'adopte ou pas ce non non = id et par pitié ne me parlez pas d'intuitionnisme, je veux du sincère et technique, pas d ela philo"
3.5/ Pour résoudre cet apparent problème, il faut aller voir de plus près ce qu'est une garantie scientifique. Elle est photocopiable (une photocopie de la preuve $p$ a la même efficacité que l’originale).
3.6/ Alors pourquoi nous ne savons pas répondre par exemple à la question:
"Bil a acheté 3 pommes et Bil a acheté 3 pommes. Combien dépense-t-il sachant que la pomme coute 7 euros? "
Alors que nous savons répondre à la question
"Bil a acheté 3 pommes et Bil a acheté 3 poires. Combien dépense-t-il sachant que la pomme (ainsi que la poire) coute 7 euros? "
3.7/ Et bé tout simplement parce que nous préjugeons que les maths sont immuables. Très bien, vous me direz, "bin, voui, mais on a raison, elles le sont". Certes, mais il n'existe pas de preuve qu'elles le sont.
3.8/ La Nature ne peut donc pas avoir rendu prouvable des choses qui en s'identifiant feraient exister une telle preuve. Et ce n'est pas un petit truc subtil, nous cotoyons chaque jour des structures (par exemple $(\R, +)$ ) où $a\to b$ s'y rencontre très bien (sans que nous en ayons conscience), mais porte le nom $b-a$, etc. Bref, ce n'est pas le non non = id le problème, mais le $a = (a+a)$ généralement présenté sous la forme $a= (a\ et\ a)$ qui n'est pas rien car il dit, "toute garantie de $a$ est duplicable". S'il y a bien un truc qui est profondément faux (et les 14000 SDF logés sous la défense en savent quelque chose) c'est ça. Avec 5euros, vous n'avez pas 10euros.
3.9/ Comme à l'exception de celui-ci, TOUS LES AUTRES axiomes logiques marcheraient aussi très bien en mettant "garantie" à la place de "preuve", on voit bien que la duplication est un (et même LE) éément très fort de traduction de l'immuabilité des maths dans les axiomes.
3.10/ Bref, en conclusion, on a bien "non non = id". Le problème "n'était pas non plus là". L'obsession intuitionniste, et son étude pour elle-même est une très belle aventure de l'humanité, qui est tombée dans le ravin et au lieu de pleurer, a visité une forêt inattendue, mais elle coinçait en ce qu'elle n'assumait pas que n'importe qui adopte AVANT toute autre chose que non non ) id.
3.11/ In fine, on a étudié tout ça, fait des conférences, des programmes, embauché des gens, et tout est devenu clair (et il n'est pas devenu interdit d'étudier pour autant la logique intuitionniste).
3.12/ Les conclusions sont:
3.12.1/ On a bien "non(non(A)) = A" (même si on le dit autrement pour ne pas froisser le souvenir de gens (parfois morts et ne pouvant se défendre))
3.12.2/ On n'a pas A => (A et A). (Ce qui n'interdit pas de le supposer, mais alors faut l'assumer, et ça touche la reproductibilité scientifique qui par ailleurs est mise face au défi majeur de la quantique qui n'autorise pas la clonage)
3.12.3/ On obtient la logique intuitionniste en DEFINISSANT (elle devient émergente):
(A=>B) := (Avec autant de fois la garantie de A que je veux, je peux garantir
3.12.4/ On obtient la logique classique en DEFINISSANT (elle devient émergente elle aussi):
(A=>B) := (En clonant tout ce que je veux, quand je veux, où je veux, etc, je peux garantir B from A)
3.12.5/ Dans ce contexte le "ridicule" de vouloir prouver le raisonnement par l'absurde intuitionnistement se voit bien, puisqu'il demande de garantir A à partir d'une garantie qui, moyennant que vous lui apportiez tous les clones qu'elle demande de garanties de A, vous envoie au paradis.
3.12.6/ Ca se voit aussi très bien dans les jeux. Il est plus facile de "battre Kasparov ou Karpov" que de battre Kasparov (on admet que comme vous êtes un illustre inconnu, vous avez le droit de choisir la couleur). Il est ULTRAFACILE d'en battre au moins un des deux. Mais vous avez DEUX COPIES d'épreuves et vous n'épatez que les spectateurs locaux d'une des 2, et vous ne pouvez même pas prévoir à l'avance qui.
4/ Le "vrai" RPA:
Tout ce qui précède devrait vous convaincre que:
4.1/ Même quand vous prouvez A en concluant "donc A" après avoir prouvé ((A=>Tout)=>Tout) (ce qui est présenté, comme "le vrai" RPA, et bien ce n'en est pas tout à fait un vrai si vous n'avez utilisé QU UNE SEULE FOIS L HYPOTHESE A=>Tout (RPA light) dans votre preuve de ((A=>Tout)=>Tout)
4.2/ Bon, mais c'est un peu subtil pour les gens de compter combien de fois ils utilisent une hypothèse. C'est un hobby possible pour un matheux non expert de ça.
4.3/ En effet, tout ce que vous pourrez prouver via le RPA light sera prouvable sans AUCUN RPA (sauf à tricher vocabulairement.
4.4/ Le vrai de vrai de chez vrai RPA, c'est donc quand vous utilisez explictement l'axiome suivant (et je termine là, mal à la main):
$$ ((A\to Tout ) \to ((A\to Tout)\to Tout)) \to A $$
4.5/ En général on "le sent passer dans ses veines". La duplication d'une hypothèse, ça se ressent tactilement quand on fait des maths. Don't worry. Il y en a même que ça traumatise comme le montre l'argument qui suit:
4.6/ [small]With $e := \{x\mid (x\in 1x)\to (3=7)\}$, have:
$(e\in e) \to ((e\in e) \to (3=7))$ donc
$(e\in e) \to (3=7)$ donc
$e\in e$ (1)
On vient de prouver $e\in e$
$(e\in e) \to ((e\in e) \to (3=7))$ donc
$(e\in e) \to (3=7)$ donc
on vient de prouver $(e\in e) \to (3=7)$ (2)
par (1,2), donc $3=7$.[/small]
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
$A\to (A+A)$ est connu sous la forme $A\multimap (A\otimes A)$ (et comme n'étant pas un théorème)
(A implique intuitionnistement
Tout est plus souvent noté $\perp$ et défini par $\forall X: X$. A l'école, il est appelé "le faux".
Le "non" respectueux des anciens a été renommé comme suit $(x\mapsto x^\perp ):=(x\mapsto non(x))$
Le "non" intuitionniste n'existe pas (c'est juste $non(a):=[(!a)\multimap \perp ]$, mais en général qand les gens font de l'intuitionnisme, ils "ignorent" le niveau en amont, ils "se donnent" la logique intuitionniste, ils ne la font pas émerger)
L'annelé fait collapser intuitionnisme et classique (ie dès que vous avez $\forall x: x^2=x$, vous avez la logique classique (c'est d'ailleurs connu scolairement).
Le "non non A = A" se récrit donc (sobrement et réservé aux gentils et polis) $(A^\perp)^\perp = A$
L'axiome du RPA est donc (et audacieusement) : $(!((!A) \multimap \perp)) \multimap A$, et bien évidemment jamais usité dit comme ça. Mais cette forme permet de voir que ce n'est pas du tout "une évidence".
L'axiome d'extensionalité provoque $A=(!A)$, et force donc toute théorie des ensembles à être classique (je rappelle que les topos NE SONT PAS des modèles de ZF intuitionniste, il n'y a pas de modèle de ZF intuitionniste, en dehors de constructions "non arguésiennes" (métaphore géo) artificielles)
$!A$ est une abréviation de "j'ai autant de copies (y compris 0) de $A$ que je veux".
Le faux, c'est pas plutôt $"0"$ que $\perp$ ? (car on a alors $\Gamma, 0 \vdash \Delta$ pour tous séquents linéaires).
Aussi, sans bousiller le fil, « premier ordre » et « second ordre » c’est hors sujet ou bien ?
Par ailleurs, quels sont les axiomes très faibles qui permettent de prouver que $non(x)=(x\to Tout)$? Pourquoi sont-ils qualifiés de faibles ?
Indication: non(x) = non(non(non(x))) (à prouver)
Pour ton autre question:
En abrégeant par $x\leq y$ le fait que $y$ soit un cas particulier de $x$.
Dans l'autre sens
$$(a\to Tout) \leq [(non(Tout)) \to (non(a))]$$
Pour dire les choses proprement:
Etage1/ pure grammaire, appelée aussi logique linéaire, affirmant une "égalité en dur" entre les préphrases. Disons que c'est un niveau TRES LEGEREMENT quotienté par rapport à considérer les phrases (pas leur valeur) comme des suites de signes:
1.1/ (si A alors si B alors C) = si (A et
1.2/ et est associatif et commutatif
1.3/ $x\mapsto $ si $x$ alors $y$ est décroissante (pour la relation "est un cas particulier de")
1.4/ $x\mapsto $ si $y$ alors $x$ est croissante (pour la relation "est un cas particulier de")
1.5/ $1$ est neutre: $($si 1 alors $x) = x$
1.6/ non est une involution décroissante
1.7/ Il y a un plus grand élément (disons $T$) et un plus petit élément (disons $\perp$). On peut aussi noter par $0:=(non(1))$
1.8/ On déduit de otut ça aisément que $(non(x))=(x\to 0)$ (j'ai abrégé si a alors b par $a\to b$)
1.9/ La gratuité des poubelles s'exprime à travers le théorème suivant:
$$(\forall x,y: [x\leq (y\to x)])\iff (1=T)$$
1.10/ J'ai posté initialement en considérant que la gratuité des poubelles est acceptée, autrement dit, j'ai considéré pour le but à atteindre que $1=T$ et $0=\perp$. Ca a engendré la remarque de foys.
1.11/ Admettre la gratuité des poubelles est se placer en logique affine (hélas, maltraitée par la recherche)
Etage3: il n'y a pas d'étage2, car traité de 1. L'étage2 est juste admettre $1=T$ (ou équivalemment $0=\perp$)
3.1/ C'est la duplication: on peut l'ajouter "brutalement" en prétendant que $\forall x: (x\ et\ x)=x$. Hélas faire ça plonge directement tout le monde dans une algèbre de Boole et "fait sauter" la logique intuitionniste.
3.2/ Il est mieux de rester dans le contexte initial mais de dire "j'ai décidé de m'intéresser aux $x$ qui sont $\geq$ à la borne inférieure $W$ des $(y\to (y\ et\ y))$"
3.3/ Mais là encore c'est relativement peu édifiant et maladroit. Dans la plupart des structures concrètes "prises au hasard", on risque d'avoir $W=\perp$. En outre, ça consiste à faire la même erreur que calculer dans des plans non arguésiens.
3.4/ Le mieux (recherche récente) est plutôt de considérer $\Rightarrow$ tel que $\forall x,y: $
$$ (x\Rightarrow y ) = ((!x)\to y) $$
où $(!x)$ est la borne inférieure du plus petit ensemble contenant $1;x$ et stable par "et". (On peut l'appeler "j'ai $a$ à volonté"). L'usage est aussi de renommer $\to$ en $\multimap$.
3.5/ On comprend alors mieux l'exoticité du RPA. On voit d'ailleurs tout de suite son rôle dans les maths: le retour en arrière platonicien: "tu viens de me donner $x$ dans les hypothèses de notre partie au prouveur sceptique, j'ai donc gagner car il y a 38 coups, c'est $x$ que je devais prouver, et en me le donnant, tu avoues, vieux frère, que $x$ est vrai et donc, par retour dans le passé me déclare victorieux il y a 38 coups"
L'autorisation de dire ça est très exactement ce qui différencie l'intuitionnisme du classique (pouvoir décharger les conclusions et pas seulement les hypothèses).
1/ Tout d'abord on parle de formes et non de fond.
2/ Un RPA est la forme suivante et aucune autre:
2.1/ je suppose A => B
2.2/ je raisonne, raisonne
2.3/ j'arrive à la conclusion A.
2.4/ je prétends alors avoir prouve A par l'absurde.
2.5/ Et si on me signale que j'ai juste prouvé
(A=>B)=>A, je réplique, oui et j'utilise "l'axiome du raisonnement par l'absurde" qui dit
((A=>B)=>A)=>A
pour dire "donc A"
Ha non, je ne "comprends rien" finalement.
Edit : on se fiche de B ou bien ?
Ce doit être fait exprès que tu n'en parles pas...
Tu n'as pas quantifié, grand gredin !
Je n'y connais rien en intuitionnisme mais je sais que si tu rajoutes la loi de Pierce à la logique intuitionniste tu récupères la logique classique :
https://fr.wikipedia.org/wiki/Loi_de_Peirce
Si $A,B,C$ sont des énoncés, $\left [\left ([C \to (A \to
Ce qui entraîne la disjonction de cas classique (mais intuitionnistiquement fausse): si $\Gamma, A \vdash C$ et $\Gamma, A\to B \vdash C$ alors $\Gamma \vdash C$.
Par contre je ne comprends rien à ta démo en 3 lignes, c'est te dire mon niveau en intuitionnisme !
$$ A\to B\to C = A\to (B\to C)$$
Rappel: $(non(non(A))): = ((A\to Tout) \to Tout)$
$$((A\to Tout) \to Tout)\to A$$
est un cas particulier de
$$((A\to Tout) \to A)\to A$$
Pour ma part, je vais réécrire de manière exhaustive les FAITS DE VOCABULAIRE PURS ET DURS et ne nécessitant absolument pas débat, puisque ce sont des noms donnés à des formes et rien de plus.
1/ Un raisonnement est une forme. Comme tout théorème a plusieurs preuves, c'est idiot de parler de "théorème prouvé par l'absurde", puisqu'il faut préciser quelle preuve est qualifiée.
2/ Le RPA est LA FORME suivante de raisonnement:
Je prouve d'abord que $non(A) \to FAUX$ et j’enchaîne sans transition par "donc $A$"
3/ Pour plus de précision, $FAUX$ est une abréviation de $Tout$ qui lui-même est une abréviation de la phrase $\forall X: X$ qui en français dit "tout est vrai".
4/ A strictement parler il n'y a donc pas de raisonnements très identifiables dans les textes avachis de maths, un peu trop informels, puisque les propositions qui y apparaissent ont souvent des négations notées autrement, comme par exemple $non(3=4)$ qui est plus souvent écrit $3\neq 4$.
5/ Pour signaler le cas très précis de l'irrationalité de $\sqrt{2}$, et dès lors qu'on admet que la variable propositionnelle est $\sqrt{2}\in \mathbb{Q}$ (je la note A)et que sa négation non(A) est l'énoncé $\sqrt{2}\notin \mathbb{Q}$, on a un raisonnement habituelle et académique qui a la forme suivante:
je prouve $A\to FAUX$ et j'écris sans transition autre "donc non(A)".
Il n'y a aucun débat et les enseignants, livres et autres qui prétendent que c'en est un commettent une faute de vocabulaire logique, point à la ligne.
6/ Après, attention: même si c'est exotique, il existe bien des raisons (en recherche approfondie) de considérer que la proposition primitive est $\sqrt{2}\notin \mathbb{Q}$ et que sa négation $\sqrt{2}\in \mathbb{Q}$, serait en fait réellement une abréviation de $non(\sqrt{2}\notin \mathbb{Q})$. MAIS C'EST UNE TOUT AUTRE AFFAIRE, rare, spécialisée, et aucun chercheur non logicien, aucun enseignant lambda ne me fera avaler qu'il a SINCEREMENT ET DE LUI MEME fait ce choix.
7/ Maintenant, c'est très simple, pour qui contesterait:
7.1/ Je donne 1000 euros à la première personne capable de déduire $A$ de $non(A) \to Faux$ (sans l'admettre ou admettre des axiomes proches (en termes savant sans sortir de l'intuitionnisme))
7.2/ Je vends 5euros chaque mail que j'enverrai à chaque demandeur/euse où je prouve de manière triviale et intuitionnistiquement que si $A\to FAUX$ alors $non(A)$.
Si (7.2) était un RPA, je ne pourrais pas le faire.
Si (7.1) n'en était pas un, je risquerais gros financièrement.
8/ Merci à dom ou autre de mettre un lien du fil homonyme en péda vers le présent fil.
Une légère question :
N'est-ce pas plutôt $A := \sqrt{2} \notin \mathbb Q$ ?
En gros "$A$" est le truc que l'on veut démontrer dans cette histoire.
Alors on suppose : $non(A) := non(\sqrt{2} \notin \mathbb Q)$.
Et on souhaite démontrer que ça implique $Tout$ (ou $Faux$ qui est un synonyme si j'ai bien compris Edit : la réponse est dans ton "3.").
Autre digression parallèle :
2a)
Au lieu d'écrire $ \sqrt{2} \notin \mathbb Q$, serait-ce plus malin*, coquin*, diabolique* d'écrire $ \sqrt{2} \in \mathbb R\setminus\mathbb Q$ (je ne sais plus comment on fait le slash pour dire "$\mathbb R$ privé de $\mathbb Q$" [\setminus. AD].
2b)
Ou alors au lieu d'écrire $ \sqrt{2} \notin \mathbb Q$, proposer $ \sqrt{2} \in \mathbb Q^c$ (le complémentaire de $\mathbb Q$ dans $\mathbb R$).
*je dis "coquin, malin, diabolique" car ça cache (supprime ?) la négation du "appartient".
[merci pour la correction AD]
[À ton service. :-) AD]
> 1) Une légère question : N'est-ce pas plutôt $A := \sqrt{2} \notin \mathbb Q$ ?
> En gros "$A$" est le truc que l'on veut démontrer dans cette histoire.
Oui, c'est ce qu'on veut démontrer, et on sait bien que pour démontrer $B\Rightarrow C$, on suppose $B$ et on cherche à en déduire $C$ (ça a dû déjà être répété mille fois, non ?).
Si tu prends A= "racine de 2 n'appartient pas à $\Q$"***, et si tu supposes non(A), tu ne pourras rien en déduire du tout en intuitionnisme, parce que l'axiome (non non P implique P) ne fait pas partie de la logique intuitionniste. (Pour être plus précis, "non non P implique P" est équivalent au RPA, c'est l'une des formes du tiers exclu, l'autre étant "P ou non P"). En particulier tu ne pourras pas en déduire "racine de 2 appartient à $\Q$", et tu seras coincé dans ton raisonnement.
En revanche si tu raisonnes en logique classique tu pourras utiliser non non P implique P, tu en déduiras que racine de 2 appartient à $\Q$, et le raisonnement habituel te permettra d'en déduire Tout (ou le faux).
Moralité : non(A) implique Tout, donc non(nonA), donc A puisqu'on est en logique classique.
Et là tu pourras clamer haut et fort : "Voyez les gars les filles, il a bien fallu que j'utilise le RPA pour démontrer A".
Mais, il faut bien le reconnaître, il faut avoir l'esprit sacrément tordu pour raisonner de cette façon.
@Christophe : n'hésite pas à m'incendier si j'ai raconté des conneries ci-dessus, ça voudra dire que je suis peut-être un bon prof mais en tous cas un très mauvais élève, lol.
***Sorry pour ma nullité en LaTeX.
Je lisais le texte de Christophe où l'on trouve :
5/ Pour signaler le cas très précis de l'irrationalité de $\sqrt{2}$, et dès lors qu'on admet que la variable propositionnelle est $\sqrt{2} \in \mathbb Q$ (je la note A) et que sa négation $non(A)$ est l'énoncé $\sqrt{2} \notin \mathbb Q$, on a un raisonnement habituelle et académique qui a la forme suivante:
[small]NB : C'est moi qui éclaire en rouge et qui souligne.[/small]
J'admets ne pas comprendre "dès lors que l'on admet que la variable propositionnelle est".
Mais il m'avait semblé que quand il dit "le cas très précis de l'irrationalité de $\sqrt{2}$" est justement que l'on veut démontrer $\sqrt{2} \notin \mathbb Q$ et donc que c'est cela que l'on note $A$.
Ainsi, $non(A)$ est $non(\sqrt{2} \notin \mathbb Q)$ et c'est là que le $non(non(.)$, quand on est intuitionniste, ne permet pas d'avancer, alors que quand on est classisiste on admet que $non(non(A))$ est équivalent à $A$.
Et il me semble que le message de Martial (salut ;-)) répond davantage à mes/ces tracasseries.
C'est là qu'est ton erreur. Ce préjugé t'a bloqué dans la lecture de mon post. Relis-le sans préjuger ça et tu verras que tout te sera clair et précis.
"Relis mon poste" est une phrase que j'utilise aussi, mais là, imagine que je te dise "bah relis ce que j'ai écrit"... on n'avancera pas et la discussion va tourner autour du pot Shtamesque ou de la polémique qui aura l'air puérile.
Bon, comme je vous fais confiance (vous ne jouez pas, vous bossez pour que je comprenne), je récris un truc. Non pas pour avoir raison, mais pour comprendre ce truc et tourner une grande page, voire, changer de tome de ma vie de logicien en herbe. J'entends ce que tu dis, Christophe, quand tu parles de mon aveuglement et je pense que c'est une des raisons principales de mes tracas.
L'exercice classique : (où on se prend, en majorité, les pieds dans le tapis de la sémantique RPA)
Démontrer que $\sqrt{2}$ n'est pas rationnel.
Correction de Dom :
Je définis $A_d$ par ce que l'on veut démontrer.
Dans ce cas $A_d := \sqrt{2}$ n'est pas rationnel.
Ou encore : $A_d := \sqrt{2} \notin \mathbb Q$.
Dom raconte alors cette histoire :
0d) J'ai voulu démontrer $A_d$.
1d) J'ai supposé $non(A_d)$.
2d) J'ai démontré $Tout$.
3d) J'ai donc démontré $non(A_d) \Rightarrow Tout$.
4d) J'ai donc démontré $non(non(A_d))$ par définition de $non(.)$.
5d) J'en déduis $A_d$.
Correction de Chistophe :
Je définis $A_c:= \sqrt{2} \in \mathbb Q$.
Dans ce cas $non(A_c):= non(\sqrt{2} \in \mathbb Q)$.
Je veux démontrer $non(A_c)$. Remarque : Ici, le $non(A_c)$ c'est exactement le $A_d$ de Dom.
Édit : sauf à considérer la remarque 6) du message de Christophe.
Christophe raconte cette histoire :
0c) J'ai voulu démontrer $non(A_c)$
1c) J'ai supposé $A_c$.
2c) J'ai démontré $Tout$.
3c) J'ai donc démontré $A_c \Rightarrow Tout$.
4c) J'ai donc démontré $non(A_c)$ par définition de $non(.)$.
Retour au discours :
Je vois bien que c'est sacrément plus compliqué, ce que Dom fait.
Il cache d'ailleurs des détails dans sa preuve (un $non(non(.))$ notamment qu'il ne mentionne pas...).
Par contre ce qu'il dit est-il correct si on le croit sur parole ?
Et comment peut-il justifier son passage de 4d) à 5d) ?
Pardon si je demande des réponses qui ont été dites des milliers de fois.
Et merci, bien entendu.
Dom
PS : là je n'ai pas parlé de Tiers Exclu (TE), de Logique Intuitionniste (LI), de Logique Classique (LC).
Mais j'ai dû cacher les trucs sous le tapis, j'en suis conscient.
Evidemment, en LC tu peux.
Et il y a pire, c'est qu'en LI tu ne peux même pas passer de 1d) à 2d)… parce que non(racine de 2 n'appartient pas à $\Q$ ne te permet pas d'affirmer que racine de 2 appartient à Q donc tu ne peux même pas faire le raisonnement habituel pour démontrer Tout.
Sur LE FOND EXTÉRIEUR tu nous décris hélas des exemples où D'AUTRES PREUVES intuitionnistes marchent.
En effet, le théorème suivant est intuitionniste:
(non non non A ) => (non A)
Tu as même l'équivalence suivante.
On peut prouver (non non X ) implique X si et seulement si il existe Y tel qu'on peut prouver l'équivalence entre X et non Y
où utilise ici prouver pour "prouver sans RPA"
1) Supposons TE vrai.
Pour démontrer RPA, on fait l'hypothèse que non non P est vraie.
D'après TE, on a soit P soit non P.
Si P est vrai, tant mieux.
Sinon, non P est vrai, et dans ce cas on a à la fois non P et non non P, ce qui est une contradiction.
2) Supposons RPA vrai.
La proposition non (P ou non P) entraîne qu'on a à la fois non P et non non P, donc elle est contradictoire.
On a donc non non (P ou non P), ce qui entraîne P ou non P d'après le TE.
Extrait du livre de Pierre Ageron : "Logique, ensembles, catégories", Page 4
Ce n’est pas faute d’avoir tout sous les yeux depuis au moins quatre ans !
Pour chacun de nous, il y a un temps pour tout.
Je retourne à l’apéro...
J'ai moi-même du mal avec ces trucs, et je suis obligé à chaque fois de réfléchir intensément pour savoir si j'utilise ou non RPA. Ce fil m'a entre autres permis de découvrir que j'avais écrit des énormités dans le Chap.0 de mon "futur" livre ***. Il va falloir que je remette de l'ordre là-dedans, et ce n'était pas prévu au programme.
Un autre truc qui peut aider à comprendre est une remarque dans l'un des précédents posts de Christophe, à savoir que non non non Q implique non Q est un théorème en LI.
En d'autres termes, si ta proposition P peut se mettre sous la forme non Q, tu n'as pas besoin de RPA pour prouver que non non P implique P.
Et c'est ça qui fait toute la différence entre "racine de 2 est irrationnel", qui est visiblement la négation de quelque chose, et "$\C$ est algébriquement clos". En effet, la proposition "Tout polynôme non constant admet une racine" ne peut pas se mettre sous la forme d'une négation (sauf évidemment en supposant RPA), et donc, là, quelle que soit la preuve de d'Alembert-Gauss que tu souhaites rédiger, tu es obligé d'utiliser RPA.
Par ailleurs, l'apéro me paraît une excellente idée.
*** en admettant que Dieu (s'il existe) me prête vie suffisamment longtemps, comme on dit puis dans les chaumières.
@Dom, tu n'as pas précisé ce que tu avais compris ou pas.
Je crois comprendre, à confirmer, des interventions de nos amis qu'ils reconnaissent (...même si de manière très contorsionnée) l'existence et la validité d'une vraie démonstration par l'absurde (RPA) d'une proposition non P telle que l'irrationalité de $\sqrt{2}$. Qu'il existe ou non une version intuitionniste de ce raisonnement, sur quoi ils semblent lourdement insister, n'a qu'une importance parfaitement secondaire par rapport au véritable historique du débat : à savoir qu'un premier camp avait affirmé haut et fort depuis des années que les démonstrations classiques (LC) par l'absurde de propositions non P ("Je veux démontrer non P, je suppose P, j'arrive à l'absurde, etc. donc non P") n'étaient pas de vrais RPA, que ce soit en logique classique ou intuitionniste, car n'utilisant pas l'axiome du tiers-exclu.
Des centaines (ou milliers) de posts témoignent de cette position, face à laquelle a émergé un second camp qui a insisté pour démontrer au contraire que oui, on pouvait démontrer non P (tout comme P) par de vrais RPA (avec tiers-exclu), très simples et très naturels, un peu comme tu l'as fait avec ton raisonnement valide 0-5d).
Merci de bien vouloir clarifier tes pensées (*).
Bonne nuit.
[small](*) D'autres lecteurs ont soif de vraies certitudes à ce sujet et ne veulent plus - tout comme toi - se contenter d'écrans de fumée permanents pour cacher la vérité, ou pires de manœuvres "diplomatiques" exagérées pour faire passer la thèse "gagnante" dans le camp "perdant".[/small]
1) En calcul des séquents intuitionniste LJ, la règle d'introduction du "non" à droite est :
$$\begin{array}{rcl}
\Gamma, A&\vdash&\bot\\
\hline
\Gamma &\vdash&\neg A
\end{array}$$
qui se lit : une démonstration de l'absurde sous les hypothèses $\Gamma$ et l'hypothèse $A$ donne une démonstration de $\neg A$ sous les hypothèses $\Gamma$.
2) En déduction naturelle intuitionniste, la règle d'introduction du "non" est
$$ \begin{array}{c} [A]\\ \vdots \\ \bot\\\hline \neg A \end{array}$$
qui se lit : une démonstration de l'absurde dans laquelle on décharge l'hypothèse $A$ donne une démonstration de $\neg A$.
3) Pour la sémantique topologique du calcul propositionnel intuitionniste : si l'intersection de l'ouvert $U$ (valeur de vérité de $A$) et de l'ouvert $V$ est vide, alors $V$ est contenu dans l'intérieur du complémentaire de $U$ (valeur de vérité de $\neg A$).
Par contre, le fait que l'intersection de l'intérieur du complémentaire de $U$ avec $V$ soit vide n'entraîne pas que $V$ soit contenu dans $U$, bien sûr.
L'axiome du RPA dit que non(non(X)) implique X
Par contre X implique non(non(X)) est un théorème intuitionniste.
@Ltav: peut être pourrais tu séparer les différents thèmes que tu veux aborder. La tu postes souvent des longs pavés multithematiques sans contexte de sorte qu'on ne lit pas ou à tout le moins on est obligé de répondre à des extraits.
Mais dans son post il prétend à un moment légitimer son discours par "l'histoire humaine imparfaite". De sorte qu'on ne sait même pas s'il a changé de matière ou non.
Je l'invite à faire plusieurs petits posts à la place de longs.
Je lis depuis quelques mois (peut-être parce que je me penche sur la question) que certains de ceux qui annonçaient faire un RPA pour notre fameux $\sqrt{2}$ ne savaient pas qu’ils n’en faisaient pas un, voire que d’autres étaient de mauvaise foi quand ils disaient qu’ils avaient supposé « $\sqrt{2}$ non irrationnel ».
C’est assez prétentieux de dire « t’avais pas ça en tête ».
C’est possible bien entendu.
Cependant je me souviens très bien dans des cours amphi/TD de plusieurs profs dire à haute voix « supposons que ce ne soit pas le cas ».
Là j’espère que l’on accorderait au moins à ces gens là le bénéfice du doute, non ?
« Soit à montrer $P\Rightarrow Q$
Supposons que ce ne soit pas le cas.
Je suppose alors $P$ et $non(Q)$. »
Là ça démarre bien comme un RPA si j’ai bien compris.
Reprenons :
Avec $P= (x^2=2, x>0)$ et $Q=(x$ est irrationnel $)$.
« Soit à montrer $P\Rightarrow Q$
Supposons que ce ne soit pas le cas.
Je suppose alors $P$ et $non(Q)$
C’est à dire P et $x$ est rationnel. »
Bénéfice du doute ou incompétence et confusion ?
Là encore, si j’ai bien compris, on attend que l’auteur écrive : « j’utilise le fait que $x$ n’est pas irrationnel entraîne que $x$ est rationnel ».
Christophe : est-ce cela « la première cartouche du RPA » dont tu parles ?
C’est à dire le premier « non(non(truc)) entraîne (truc) ».
C’est à dire le premier « (non(truc) => tout) entraîne (truc) ».
Édit : j’ai rayé et modifié mais finalement j’ai encore un doute...la définition du « non » me perturbe encore un peu certainement.
Jusqu'à présent on n'a rien démontré. À partir de ces hypothèses on démontre l'absurde de la façon habituelle, et ça nous fait une démonstration parfaitement intuitionniste (techniquement sans RPA) que sous l'hypothèse $x^2=2$, $x>0$, on a non($x$ rationnel).
J'ai l'impression de radoter.
Je connais ta patience. Et celle du Christophe qui annonce souvent avoir dit les choses « 178364728273 fois ».
Et je sais que ces choses ont déjà été dites ici et là.
Je creuse encore pour lever MES tracas. Et si ça peut servir à d’autres, tant mieux.
Ce que je veux savoir :
J’ai bien compris que l’on peut s’en passer grandement.
Si on rédige tout ce préambule (comme tu le dis) est-ce tout de même un vrai RPA ?
Même s’il est « très artificiel ».
Édit : mon problème vient de ce qui suit, je pense
Quel que soit $A$ :
1) La définition de $non(.)$ :
$non(A):=(A\Rightarrow tout)$ (j’essaye de me l’approprier)
2) Le fait que je lise qu’en logique classique :
$non(non(A))$ est équivalent à $A$.
3) Le fait qu’en logique classique :
l’axiome RPA c’est $(non(A)\Rightarrow Tout) \Rightarrow A$
C’est à dire que l’axiome RPA est $non(non(A)) \Rightarrow A$.
Je vois une incohérence entre 2) et 3).
Quoique ... je me demande, dans un topos, est-ce que le sous-objet des rationnels dans l'objet des réels est complémenté ? (:P)
PS. Non pas complémenté c'est sûr, mais je parie sur non-non clos.
Ça veut dire qu'on n'a pas "tout nombre réel est rationnel ou irrationnel", mais qu'on aurait " tout nombre réel qui n'est pas irrationnel est rationnel", ce qui est beaucoup plus faible (un ouvert peut être égal à l'intérieur de son adhérence sans être fermé).
« Piètre consolation » me diras-tu ;-)
Plaisanterie mise à part : vraiment merci !
Remarque 1 : J’avais ajouté un « édit » pour scier l’ultime branche du quiproquos qui m’envahit.
Le 2) et 3) bizarres...
[small]Remarque 2 : J’attends que Christophe confirme que dans ce cas c’est « le premier coup ». C’est très accessoire en ce qui me concerne.
Il avait parlé jadis « d’utiliser au moins deux fois... ».[/small]
Évidemment je suis incapable, par méconnaissance, de comprendre ta dernière phrase.
À plus tard.
Voilà un bon dénouement. J'espère Dom que tu es rassurée : le raisonnement par l'absurde pour démontrer l'irrationalité de $\sqrt2$ ("non P") qu'utilise la grande majorité des profs, des livres, des étudiants, etc. est un vrai raisonnement par l'absurde. Il leur suffit justement d'annoncer : "démontrons-le par l'absurde, je suppose le contraire de ce que je veux démontrer [non(non P)] à savoir $\sqrt2$ rationnelle [P], etc.', pour en faire un vrai RPA utilisant le tiers-exclu. C'est de la logique classique.
On peut aussi utiliser formellement la logique intuitionniste - sans tiers-exclu - pour le faire mais alors...se pose un problème grave. Qu'est-ce qui justifie en LI le recours à l'hypothèse P pour démontrer non P ?
En LC, on sait grâce au TE que P est simplement la négation de non P, car non(non P) <=> P. Or, il n'y a absolument aucun moyen en LI de remonter sémantiquement (en analysant la vérité des propositions) de non P à P, de même qu'il existe une infinité de propositions $(Q_i)_i$ en LI vérifiant pour tout entier $i$ :
($Q_i$ => $\perp$) => $non P$ $\quad \quad$ ($q_i$)
comme par exemple : $Q_1= P$, $Q_2= non(non P)$, $Q_3 = non(non(non(non P)))$, etc. etc., une infinité...Alors :
1) pourquoi choisir formellement P plutôt qu'une autre ?
2) pourquoi choisir [(P => $\perp$) => $non P$] pour démontrer non P, plutôt que l'un des théorèmes ($q_i$) ?
En termes probabilistes, en LI il y a une probabilité nulle de tomber au hasard sur P plutôt qu'une autre. Seule la logique classique permet de justifier ce choix du professeur qui lève les yeux au ciel ou du livre qui commence sa démonstration en disant : "Je veux démontrer non P. Je suppose P...", même sans parler clairement de "contraire", "absurde", ou autre. Il ne dit pas qu'il va supposer non(non P), ou non(non(non(non P))), ou non(non(non(non(non(non P))))), etc. toutes possibilités distinctes et équiprobables en LI, mais bien qu'il va supposer [large]P[/large]...En LC, toutes ces propositions $Q_i$ sont "égales" à $P$ : il y a donc une probabilité de 1 de tomber sur P.
De même que l'on va utiliser explicitement : [(P => $\perp$) => non P] plutôt que l'une des relations (valides dans les deux logiques) :
- (non(non P) => $\perp$) => non P,
- (non(non(non(non P))) => $\perp$) => non P,
- (non(non(non(non(non(non P))))) => $\perp$) => non P,
- etc.
Pourquoi ?
La LI ne permet pas d'expliquer ce choix de l'esprit. La LC le peut : toutes les propositions non(non P), non(non(non(non P))), non(non(non(non(non(non P))))), etc. se réduisent à P en logique classique grâce au TE, mais pas en intuitionniste. D'où l'avantage à la fois syntaxique (formel) et sémantique (signification) de la LC, alors que la LI n'apporte aucune justification sur le choix de P parmi une infinité d'autres propositions $(Q_i)_i$ fonctions de non P...
@Gbzm : en effet, tu t'es trop fatigué à répéter quelque chose qui n'était pas le cœur du débat. Bien sûr que l'on peut réécrire la démonstration de non P de façon purement syntaxique sans tiers-exclu (intuitionniste), mais on peut aussi la réécrire de façon purement classique avec tiers-exclu. Point barre. Affirmer le contraire est totalement faux (tiens encore un tiers-exclu) et tu l'admets raisonnement (on met de côté l'ego hein...). Mais par contre, seule la logique classique peut expliquer sémantiquement et syntaxiquement ce choix de P dans le raisonnement par l'absurde. Tu as déjà acquiescé à cela lorsque l'on discutait sur le fil de Flora de fonctions surjectives, données de deux réels $x,y$, etc. Je ne reviens pas là-dessus, sauf si Dom ou d'autres intervenants veulent des précisions.
En LC : le RPA c’est quel que soit $P$, $non(non(P)) \Rightarrow P$.
Tu dis plus loin :
En LC : quel que soit $P$, $non(non(P)) \Leftrightarrow P$.
Sans mentionner le RPA.
Quid ?
Remarque :
C’est un problème que j’ai soulevé plus haut dans une remarque « incohérence entre 2) et 3) ».
Remarque 2 :
Les critiques quant à la démo courante de l’irrationnalité de $\sqrt{2}$ sont très fondées (depuis que je commence à comprendre).
Je comprends la chose comme ça :
A quelques exceptions près, beaucoup n’avaient pas conscience qu’ils appliquaient $non(x$ est irrationnel $)$ donc $x$ est rationnel d’après le RPA. Personne d’ailleurs ne mentionne d’avoir appliqué À CET ENDROIT le RPA.
C’est toujours à la fin que les démos concluent par « j’obtiens un truc absurde (tout) » donc d’après RPA, ce nombre est rationnel.
J'y avais déjà répondu.
[small](*) En LC, c'est clair grâce au TE. En LI, on a défini non P := (P => $\perp$), d'où non(non P) = [(P => $\perp$) => $\perp$]. Ainsi, en supposant P vraie, on a bien : [(P => $\perp$) => $\perp$] vraie, car $\perp$ => $\perp$ (tautologie).[/small]
Ta réflexion est intéressante psychologiquement...Il est possible - et je le crois aussi - que beaucoup de monde ne prenait pas ou plus conscience de l'existence du RPA (précisément du TE) à cet endroit du début, à commencer par...les critiques eux-mêmes : en effet, au lieu de critiquer cet "aveuglement" des amateurs du RPA quant à l'emplacement du TE dans leur raisonnement, ils semblent bien plutôt en avoir été "victimes" en niant l'existence même de ce RPA. Alors que pour les partisans du caractère RPA des démonstrations style $\sqrt2 \notin \mathbb Q$, il est relativement facile d'admettre l'existence du TE en début (puisqu'ils acceptent l'idée de chercher à démontrer le contraire de n'importe quelle proposition, P ou non P, qui leur "résiste de face"), les critiques du caractère RPA de $\sqrt2 \notin \mathbb Q$ ont rejeté jusqu'à présent la moindre possibilité d'envisager sa démonstration autrement que sous l'angle de la logique intuitionniste...
Si tu as - à la suite du camp L - tant et tant et tant et tant et tant...et tant insisté (et bravo pour ta patience) pour obtenir les "aveux" de nos amis du camp C que les "raisonnements par l'absurde" que tu avais écrits (avec TE) pour l'irrationalité de $\sqrt2$ étaient de vrais RPA, et pas seulement formalisables en logique intuitionniste, c'est bien qu'ils avaient farouchement nié ce fait très clair mais certes assez subtil. Il est possible qu'ils ne l'aient pas ou plus vu à force de raisonner en LI. Sinon, il aurait été beaucoup plus simple et rapide pour eux de dire : "Oui c'est formalisable rigoureusement en LI, mais aussi en LC avec le tiers-exclu, même si c'est plus long, (ou que sais-je)".
Ainsi, au lieu de critiquer ceux qui ne voyaient plus l'axiome RPA au début du raisonnement, nos critiques du camp C ont fini par...critiquer ceux qui le voyaient encore (notamment le camp L), en maintenant que ces pauvres gens rêvaient, affabulaient ou autre joyeusetés. Tu comprendras donc que selon moi des critiques sont loin d'être "très fondées" lorsqu'elles deviennent elles-mêmes la cause de ce qu'elles critiquent.
En résumé, je te rejoindrais sur le fait qu'il faut - et il suffit - d'être un tant soit peu vigilant avec nos raisonnements par l'absurde afin de bien localiser les différentes étapes, surtout lorsqu'on a affaire à des étudiants. Bien leur expliquer les différentes variantes de raisonnement possible, avant d'en privilégier une pour telle ou telle raison.
Relis également si tu veux bien ce post (j'y ai apporté quelques améliorations) où je réexplique pourquoi à mon sens il est beaucoup plus naturel et justifié de formaliser nos raisonnements en LC au lieu de LI pour démontrer des propositions non P, style $\sqrt2 \notin \mathbb Q$.
N.B. @Gbzm : je t'avais très bien répondu ici.
Allez, bonne nuit.
il n'y a absolument aucun moyen en LI [et en LC non plus, d'ailleurs] de remonter sémantiquement (en analysant la vérité des propositions) de P =>Q à P. Pourquoi choisir de supposer P et en déduire Q pour démontrer P => Q ?
Ce trop-plein rhétorique associé à un tel vide scientifique dans les interventions de Ltav, c'est vraiment du grand art !
Ce qui me trouble c'est quand il dit : on veut démontrer que racine de 2 est irrationnel, on suppose le contraire, soit non (non (racine de 2 est rationnel)), et là on est obligé d'utiliser TE pour affirmer que racine de 2 est rationnel et dérouler le processus usuel.
Mais qu'est-ce qu'il prend comme définition d'un nombre irrationnel ? Selon moi, x est irrationnel est un raccourci dans la langue courante pour dire non (x est rationnel).
Alors je sais bien que, en l'absence de TE, on ne peut pas affirmer que, x étant un réel, on a forcément "x est rationnel" ou " x est irrationnel". Mais pour moi on s'en tape : notons P la proposition "racine de 2 est rationnel".
Tu veux montrer que P est fausse, c'est-à-dire que non(P).
Tu supposes P, tu en déduis antitruc par la méthode standard.
Tu as démontré que P implique antitruc, donc tu as démontré non(P).
Et, par définition de l'irrationalité, tu as bien démontré que racine de 2 est irrationnel.
Ai-je raison ?
Merci de me rassurer, et sorry pour mon absence de LaTeX.
Cordialement
Martial
Mais pour moi ça revient à armer une Kalashnikov pour dégommer une mouche.
C'est comme dans un fil précédent où on utilisait un raisonnement par récurrence pour démontrer que 0=0.
C'est aussi comme les gens qui utilisent l'axiome de l'ultrafiltre (ou même AC) pour démontrer Tychonoff, et qui ensuite ne s'en servent que dans le cas d'un produit fini de compacts.