Restons intuitionniste

Xavier Var

Bonjour.

J'ai beaucoup appris du RPA.
L'utilisation de l'axiome non(non(P)) implique P pour toute assertion P est responsable de ce raisonnement.
Je sais également que montrer non(P) en partant de P afin d'aboutir à une contradiction n'utilise pas le RPA et reste intuitionniste.
Néanmoins, j'aimerai éclaircir un petit point.
J'aimerais comprendre en quoi la démonstration dite par contraposition utilise le RPA ? Reste-t-on intuitionniste si à partir de P => Q, on affirme alors que non(Q) => non(P) ?

Médiat_Suprème

Juste une remarque : "Intuitionniste" désigne (peut désigner) un zélateur de l'intuitionnisme, du coup je pense qu'il aurait mieux valu écrire : "Reste-t-on dans le cadre de la logique intuitionniste si à partir de P => Q, on affirme alors que non(Q) => non(P) ?", la réponse est oui, dans l'autre sens, non

Xavier Var

D'accord merci, donc ce n'est pas équivalent.
Et concernant le première question. En quoi la démonstration dite par contraposition utilise le RPA dans ce cas  ?

Médiat_Suprème

En fait $(\neg Q \Rightarrow \neg P) \Rightarrow (P \Rightarrow \neg \neg Q)$ mais l'élimination de $\neg\neg$ est impossible dans le cadre intuitionniste

Dom

Il faut peut-être essayer de le démontrer ?

Xavier Var

Ah, oui bien vu ! Du coup Dom Médiat vient de le faire 

Dom

Ha oui, je n’avais pas vu le message. 

Foys

En logique intuitionniste on peut considérer que "$\neg A$" abrège $A\to \perp$ et du coup $(A \to B ) \to (\neg B \to \neg A)$ est un cas particulier du syllogisme $(A\to B )\to ((B \to C) \to (A \to C))$ avec $C:= \perp$.

Xavier Var

Merci de cette précision Foys !