Ceci est en réponse à Mathador.
En bleu la logique classique, en rouge la logique intuitionniste :
- Avec
- "P(A)" qui signifie : "il est prouvé que A" ou plus simplement : "A est vraie" ou encore : "A : vraie".
- A et non A : des propositions quelconques pouvant chacune être vraie ou fausse, mais pas l'une et l'autre vraies ou fausses en même temps.
- (A et non A) : nécessairement faux __ Principe de non contradiction
- (A ou non A) : nécessairement vrai __ Principe du tiers exclu
- P(A) <=> A __________________________ => A : vraie
P(non A) <=> non A ___________________ => A : fausse
non P(A) <=> ? ______________________ => A : indéterminée 1
non P(non A) <=> non non A ____________ => A : indéterminée 2
- On note que :
- non P(A) <≠> non P(non A)
- Démonstration par l'absurde :
- A <=> P(A)
non A <=> P(non A)
non (non A) <=> P (non P (non A)) <=> non P(non A)
On retrouve bien les 2 théorèmes de base de la Li :
- non A <≠> non non A
- (étant donné que P(A) n'est pas davantage équivalent à non P(non A) qu'à non P(A).)
- et
- non A <=> non non non A
- Preuve :
- Preuve :
Remarque 1 :
- A <≠> non non A
- En revanche :
- A => non non A
- En revanche :
Remarque 2 :
- Le fait que A <≠> non non A, mais que non non non A <=> non A est tout à fait intéressant, car l'on peut en inférer ceci :
- A, non A et non non A
- Tels que :
- A <≠> non A <≠> non non A <≠> A
- Tels que :
- Et que mis à part ces trois cas l'on a toujours des configurations comme :
- non A <=> (non non) non A
non non A <=> (non non) non non A
(non non) non A <=> (non non) (non non) non A
Etc.
Ce qui revient à dire qu'en Li, on peut toujours supprimer un "non non" devant un non A. - non A <=> (non non) non A
- Et que mis à part ces trois cas l'on a toujours des configurations comme :
- A, non A et non non A
- Démonstration par l'absurde :
.