Raisonnement par l'absurde (repetita)

Thierry Poma

@Christophe :

nonA
1=>nonA
non(nonA)=>non1
A=>non1
A=>0

En ne considérant que ce qui est en rouge, quelles règles de la logique minimale utilises-tu pour passer de la première ligne à la seconde ?

gai requin

Je crois qu'on peut démontrer A=>non(nonA). J'essaie :
A
1=>A
non(A)=>non(1)
non(A)=>0
non(0)=>non(nonA)
1=>non(nonA)
non(nonA)

christophe c

Merci GR (pour 2 choses :m'avoir signalé la coquille du premier post et avoir répondu à titi). Je corrigerai la coquille d'un pc

Thierry Poma

J'avais oublié. En vertu de la règle d'introduction de la négation,\[\dfrac{\Gamma\cup\{A,\,\neg\,A\}\vdash\perp}{\Gamma\cup\{A\}\vdash{}\neg\neg\,A}\]alors qu'en vertu de la règle d'introduction de l'implication\[\dfrac{\Gamma\cup\{A\}\vdash{}\neg\neg\,A}{\Gamma\vdash{}A\rightarrow\neg\neg\,A}\]Partant, $\vdash_m\,A\rightarrow\neg\neg\,A$

Dom

À la ligne :
« non(A)=>0 » on a tout de suite « non(non(A)) ».

christophe c

Si on voulait être parfaitement honnête, vu qu'on évoquait ces récréations pour le fun de voir non comme une notion première, il faut noter qu'on a admis de façon cruciale et systématique que :

$$ \forall x,y: (x\to y) \to ([non(y)]\to [non(x)]) $$

et qu'on peut mettre à concours les différents arguments pour "justifier" cet axiome (j'ai quelques vieilles idées en réserve, mais je ne vois pas mon clavier car je n'ai pas allumé la lumière et la nuit est tombée, je renvoie à plus tard)

gai requin

On peut montrer que $\forall x,y: (x\to y) \to ([non(y)]\to [non(x)])$ si et seulement si $\forall x:non(x)\leftrightarrow (x\to 0)$.
Est-ce qu'on n'est pas en train de faire des raisonnements circulaires ?