Le raisonnement par l'absurde, le vrai !

Si on peine à se retrouver dans le roman de Christphe :

On veut montrer $P\Rightarrow Q$

On fait l'hypothèse $P \text{ et } \neg Q$ , on en déduit l'absurde. On a donc montré $P\Rightarrow ( \neg Q \Rightarrow\bot)$, c.-à-d. $P\Rightarrow \neg \neg Q $. On utilise l'axiome RPA $\neg\neg Q\Rightarrow Q$ et on arrive bien à $P\Rightarrow Q$. C'est un vrai RPA.

En écho à ce que tu dis GBMZ, j'ajoute une nuance (qui effectivement intéressera peu les matheux quotidiens).

C'est un vrai RPA

On a effectivement utilisé non(non(Q)) implique Q pour passer de P=>non(non(Q)) à P=>Q à la fin d'une preuve (***) qui aboutit à tout en supposant P et non(Q).

Mais sur la "substantifique moelle de chez moelle" :-D du fond, tout dépend pour savoir, si on a tiré un vrai coup de kalach, de combien de fois on a utilisé l'hypothèse non(Q) dans le raisonnement (***). J'ai coutume de dire que si ce n'est pas au moins deux fois, ça devrait porter un autre nom que RPA :-D

L'axiome $[(A\to tout) \to tout] \to A$ est inoffensif pris tout seul. Celui qui est violentissime, c'est:
$$[(A\to tout) \to ((A\to tout) \to tout)] \to A$$

En effet, prenons un gardien de l'Olympe qui nous offre une garantie d'aller au paradis à la condition qu'on donne une clé qui ouvre la porte séparant $A$ du paradis, ie la porte $A\to tout$ (les portes sont à sens unique). On pourra aller dans $A$ sans problème. On lui donne une fausse clé (indiscernable de la vraie) et il démarre. Il ne s'apercevra qu'on l'a trahi qu'en mettant la clé dans la serrure de la porte $A\to tout$. Or on sera content, on sera arrivé dans $A$ (on avai tmenti, on voulait juste aller dans A pas au paradis). Il suit qu'une seule utilisation de $A\to tout$ pour prouver tout permet scientifiquement de reconstruire un trajet vers $A$ sans problème. Il en va tout autrement si on utilise plusieurs fois $A\to tout$. La fausse clé subit alors toute une aventure inextricable. Elle est en particulier dupliquée, donnée à des sous-gardiens qui la prennent, etc. Bref. Elle peut être donnée à une procédure qui elle-même attend une clé qui, pire que ça, elle peut être donnée à ... une hypothèse courante antérieure! etc.

Exemple: faisons les hypothèses que $A\to Z$ et que $(A\to \to Z$. Un RPA nous donne qu'on devrait avoir $Z$. Faisons le RPA:

je suppose $Z\to tout$.
Il suit $A\to tout$
donc $A\to B$
donc $Z$. Mais à ce moment-là, j'ai besoin à nouveau de $Z\to tout$, pour aller dans $tout$. Or je l'ai consommé en l'échangeant contre $A\to tout$ (combiné à $A\to Z$)
Je le réutilise, et j'obtiens tout


Voyons ce que ça donne en termes de gardien de l'Olympe. Son circuit est le suivant: on lui propose deux clés, deux fausses clés qui prétendent mener de $Z$ à tout (elles sont factices). Il échange sa première clé avec la fée qui branche $A\to Z$ et $Z\to tout$ bout à bout. Cela donne un circuit qui mène (qui prétend mener) de $A$ à $tout$. Les portes du paradis sont ainsi faites que n'importe quel habitant du paradis peut rejoindre la zone qu'il veut (toutes les portes sont ouvertes). En particulier, le fait de pouvoir aller de $A$ à tout fait qu'on peut aller de $A$ à $B$. On fournit donc à l'hypothèse $(A\to \to Z$ ce billet aller simple qui va de $A$ à $B$ en contrepartie de quoi, elle nous offre un accès à $Z$. Mais le billet en question est un chèque sans provision, une promesse. On n'est donc plus du tout sûr de pouvoir aller dans $Z$ (c'est sous réserve d'encaissement du chèque par la fée). Or non content d'aller dans $Z$, on voudrait bien aller dans $tout$. Etc, etc. Il faut bien comprendre que le chèque factice d'une des deux clé a été donné à une hypothèse sur laquelle on n'a plus droit d'accès, c'est une boite noire.
Alors me direz-vous, ce RPA ne serait-il pas finalement faux? ou en tout cas abusif? La réponse est non. Car ceci n'est qu'un extrait d'un grand balet censé nous mener au paradis. L'hypothèse qu'on a fait est en réalité provisoire et elle sera un jour utilisée comme un théorème. A ce moment, son exécuteur encaissera le chèque, donc mettra la clé dans la serrure qui sépare $Z$ de $tout$ dans un contexte tel qu'on sera entrain, comme dans mission impossible, de l'espionner et donc de repérer où se trouve $Z$ ce qui nous permettra d'y aller. On a donc gagné un transfert à défaut d'un accès au paradis.

@samok, j'ai mieux pour illustrer la coexistence peu pacifique des deux "et" logiques. Je le répète (je l'ai déjà signalé dans un autre fil).


Les pommes coutent 2 euros et les poires coutent 3 euros.

Bil a acheté 5 pommes et Bil a acheté 3 poires donc il a payé 19 euros (1)

Bil a acheté 5 pommes et Bil a acheté 5 pommes donc il a payé 20 euros (2)

Bil a acheté 5 pommes et Bil a acheté 5 pommes donc il a payé 10 euros (3)

(3) est dû à l'équivalence entre [Bil a acheté 5 pommes et Bil a acheté 5 pommes] et [Bil a acheté 5 pommes]

(2) n'est que l'application de la même règle logique que celle utilisée en (1).

avant de faire un pet
fête la paix

un conseil en passant

S

$ \perp$ est une abréviation de "tout"

En général les matheux, en ce qui concerne les phrases, préfèrent ne supposer des égalités que très rarement (je veux dire, préfèrent placer "la théorie des phrases" dans un cadre quasiment syntaxique où $A\to B$ est le couple $(A,B)$ de sorte qu'on n'a égalité entre $A\to B$ et $C\to D$ uniquement si $A=C$ et $B=D$).

Cette démarche provient de l'envie d'analyser en détails toutes les règles de syntaxe (si on commence à quotienter la structure libre, c'est généralement peu usité).

Cela dit, personnellement, c'est ce que j'ai fait, je te mettrai un lien***. Je n'ai retenu que ce qui est "de chez sûr, de chez sûr considérable comme pouvant être égal". Et ce qui est rigolo, c'est qu'on peut malgré tout déduire tout le reste sans rajouter grand chose.

Par contre, $non(non(A)) \iff A$ est équivalent bien sûr au RPA. De mon point de vue, une des meilleures versions du RPA est l'énoncé qui affirme que $non$ est injectif, ie $(non(A)\iff non(B) )\to (A\iff $. C'est aussi équivalent au RPA, mais ça a le mérite de sembler affirmer peu de choses.

*** en attendant, comme ce n'est pas long, je te résume formellement les choses.

Soit $(E,\leq, \to, 1)$ un ensemble muni d'un ordre complet, d'une opération binaire $\to$ et d'un élément $1$, vérifiant les 4 choses suivantes:

1) $(1\to x)=x$
2) $[a\to (b\to c) ]= [b\to (a\to c)]$
3) $1\leq (x\to y)$ si et seulement si $x\leq y$
4) l'application $x\mapsto (a\to x)$ est croissante

Et ce pour toutes valeurs de $a,b,c,x$

Alors j'appelle $E$ un structure de phrases. Chaque propriété traduit une idée parfaitement sûre sur notre perception de ce que doit valoir une phrase scientifique.

Les théorèmes de la structure sont par définition les éléments $\geq 1$.
Les hypothèses jetables sont les éléments $\leq 1$. C'est marrant, tu es "prouvé" si tu es $\geq 1$ et pour tout $y: x\leq (y\to x)$ ssi $x\leq 1$.

On a alors le théorème suivant:

1) les théorèmes de la logique linéaire sont les expressions $\geq 1$ dans toute structure de phrases
2) les théorèmes de la logique affines sont les expressions $ = 1$ dans toute structure de phrase où $1$ est le maximum de $E$
3) les théorèmes de la logique intuitionnistes sont les expressions $=1$ dans toute structure de phrases où $1$ est maximum et $\forall a,b: (a\to (a\to b))\leq (a\to b)$
4) les théorèmes de la logique intuitionniste sont les expressions $=1$ dans toute structure de phrases vérifiant les propriété de (3), + telle que $non:=(x\mapsto 0)$ est injective ($0$ est le plus petit élément). Remarque: $non$ est alors involutive et la structure est forcément une algèbre de Boole complète.

L'avantage d'une structure de phrase c'est aussi (quand l'ordre est complet**, je l'ai rajouté, mais on peut considérer ça comme une option) qu'on dispose de tous les connecteurs avec leur définition naturelle et correcte:

** tout ensemble a une borne inf (donc aussi une borne sup)

J'abrège $inf_{i\in X} a_i$ par $\forall i\in X: a_i$. Alors

il y a deux "et",
le "et" numéro1 noté $\otimes$, qui commute avec $\to$, défini par $a\otimes b:=\forall x: ((a\to (b\to x))\to x)$. Il est l'unique opération telle que $\forall a,b,c: (a\otimes b)\to c=a\to (b\to c)$

le "et" numéro2 qui est tout bêtement la borne inf de deux éléments $a\wedge b:=inf(a,b)$

De la même manière, tu as plusieurs "ou" (en général moins usités), à part le "ou" qui est défini par $a\ ou\ b:=sup(\{a;b\})$

Le $\forall$, je viens de le définir. Le sup général, tu devines aisément que c'est $\exists$.

Si tu veux tout comprendre sans rien confondre, la logique intuitionniste se résume à exiger en plus de tout ça que $\otimes = \wedge$. C'est une des "erreurs" énorme qui a été faite de le comprendre trop tard, après que de nombreux travaux qui ne vont pas aboutir aient été lancés (le fait que $\otimes \neq \wedge$ est essentiel dans la compréhension de la science)

Il est aussi important de voir que cette notion permet de faire comprendre aux gens la différence profonde qu'il y a entre prouver un truc de la forme $\forall xA$ et prouver une conjonction. Fondamentalement, $\forall xA$ n'est rien d'autre qu'un objet unique qui peut prendre tous les aspects particuliers qu'ont les $A$ où on a remplacé $x$ par quelque chose. Alors que quand tu prouves $A\otimes B$, tu as une preuve de $A$ ainsi qu'une preuve de $B$ qui peuvent être foncièrement différentes. En gros, la différence est aussi énorme entre $\forall$ et le "et" habituel des matheux qu'entre une intersection et un produit cartésien. Quand les pédago racontent que $\forall xR(x)$ c'est $R(0)$ et $R(1)$ et etc, en mettant tout le monde, ils installent une très mauvaise perception du monde mathématique. C'est comme quelqu'un qui essaierait de confondre $A\times B$ et $A\cap B$.

Comme exemple simple de structure de phrases qui ne se comporte pas de façon logiquement habituelle, tu as $(\R, \leq_{usuel}, --,0)$ où $a--b:=b-a$. Les théorèmes de cette structure sont les nombres réels positifs.

Il y a d'autres structures intéressantes, mais bon, tu as compris je pense.

C'est bel et bien un raisonnement par l'absurde : $(P \text{ et }(\text{non } Q))\Rightarrow \text{ faux}$ est équivalent (du point de vue intuitionniste) à $P\Rightarrow (\text{non non } Q)$.
Il reste à "composer" avec l'axiome de raisonnement par l'absurde : $(\text{non non } Q) \Rightarrow Q$ pour obtenir $P\Rightarrow Q$.

dom a écrit:

C'est dans la sémantique de @christophe c qu'on trouve des nuances

Non, non, sur ces sujets-là, GBMZ et moi disons toujours strictement la même chose. Je suis pressé mais rappels rapides:

non A est une abréviation de A=> tout
Le RPA est l'utilisation de l'axiome (non(nonA)) =>A
L'énoncé A=>non(nonA) est un théorème intuitionniste (ce n'est qu'un cas particulier de A=>((A=>B)=>B), avec B:=tout

Dans le lien que tu mets, il n'y a aucun RPA, comme le signale gb. Il y a une preuve directe et intuitionniste de "rac 2 rationnel => tout"

Comme te le dit GBMZ dans ton raisonnement de ton avant dernier post, tu as besoin de non(nonQ) =>Q. Essaie de t'en passer, tu vas voir comme c'est difficile (c'est peut-être le mieux pour toi comme expérience à faire, d'essayer)