Bonjour,
je suis en train d'essayer de comprendre quelque chose à la théorie des modèles, et à la la logique en général. Mais c'est pas facile...
Par exemple, je viens de lire qu'en logique intuitionniste:
¬A <=> ¬¬¬A est vrai.
Mais: A <=>¬¬A n'est pas vrai.
Là j'avoue que ça me dépasse... Vous pourriez m'expliquer?
Ha et, pour savoir si je suis sur la bonne voie:
A <=>¬¬A est vrai en logique classique non?
OuiA <=>¬¬A est vrai en logique classique non?
Oui.en logique intuitionniste:¬A <=> ¬¬¬A est vrai. Mais: A <=>¬¬A n'est pas vrai.
Je peux ajouter qu'en logique intuitionniste A => ¬¬A.
Une approche intuitive de l'intuitionnisme consiste à remplacer (dans sa tête) "A est vrai", par "j'ai une démonstration de A". Sous cette forme, on comprend bien que si j'ai une démonstration de A alors je n'ai pas de démonstration que je n'ai pas de démontration de A (je viens de traduire A => ¬¬A).
Par contre "Ne pas avoir de démonstration que je n'ai pas de démonstration de A", n'est pas une démonstration de A (je viens d'illustrer que ¬¬A => A est faux)
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Un truc qui m'aide bien à y voir plus clair avec la logique intuitionniste, c'est de faire comme s'il y avait une troisième valeur de vérité possible pour une proposition, genre "vrai", "faux" et "?". Je ne sais pas dans quelle mesure ce "truc" est sérieux, mais pour ma part j'ai plus de facilité à sortir du contexte classique, et il me semble que ça marche bien quand on le teste sur les implications, en tout cas pour comprendre que P n'est pas pareil que non non(P), et on retrouve bien non(P) équivalent à non non non(P).
Je m'étais intéressé à une façon de faire à une époque :
On définit :
A => B comme "de A je déduis B"
-A (non A) comme " pour tout B, A implique B"
A et B comme "A et B"
A ou B comme "pour tout C, (A =>C et B=>C)=>C"
A <=> B comme ((A=>B) et (B=>A))
Montrons que A => non non A:
Supposons A
_Prenons un B
__Supposons -A (=pour tout C, A => C)
___Appliquons cela à B
___Donc A => B
___Or A
___Donc B
__Donc -A =>B
_Donc pour tout B -A =>B
_Donc --A
Donc A => --A
Montrons que ---A => -A :
Supposons ---A
_Prenons un B
__Supposons A
___Donc --A (voir démo plus haut)
___Or --A=>B d'après ---A
___Donc B
__Donc A=>B
_Donc pour tout B, A =>B
_Donc -A
Donc ---A => -A
Il me semble que j'avais aussi démontré ainsi (A ou -A)<=>(--A=>A)
