Un peu de logique

Merci pour ta vigilance.
Tu as raison, en effet.

Si ((non(non A)) <=> A) est une proposition vraie, la démonstration est valide.
Sinon, j'avoue que je ne trouve pas de solution ce soir. Je vais continuer à chercher...

PS : une solution de facilité ne serait-elle pas de démontrer, par table logique, que cette proposition est de fait vraie ?

(Merci encore)

Je m’étais fait la même réflexion en lisant ce matin, en fait l’implication A => non(non A) est toujours vraie (mais il faut la prouver), et l’implication non(non A) => A est équivalente au tiers-exclu.
Pour démontrer rigoureusement ce genre de choses je pense qu’il vaut mieux utiliser des arbres de preuve plutôt que garder les notations usuelles en maths, mais c’est beaucoup plus long à expliquer… J’ai trouvé ce cours de L1 d’info de l'université Joseph Fourier de Grenoble qui contient les trois arbres de preuves qui nous intéressent aux pages 108 et 109, mais pour comprendre les notations il faut lire au moins en partie ce qu’il y a avant; ce n’est pas si long que ça car ce sont des transparents.
À la page 106 de ce document on dit que non(non A) => A est nécessaire pour démontrer l'implication non(A et B) => (non A) ou (non B), donc on ne peut pas démontrer A => non(non A) en écrivant que c’est équivalent à (non A) ou (non (non A)), puis à non(A et (non A)) (arnaque 1), puis à non(faux), puis à vrai (arnaque 2); je ne vois pas comment faire sans arbre de preuve sans introduire d’arnaque involontairement.

En effet.
Je n'ai pas trouvé non plus d'autre méthode.

J'ai l'impression qu'on peut démontrer que (non(non(non A))) <=> (non A) est toujours vraie, sans que (non(non A)) <=> A ne le soit nécessairement, mais j'ai le sentiment que cela ne doit pas être très simple. (En plus, cela ne suffirait pas...)

Feuille de brouillon :
Je remarque d'après la définition de la négation :

A	non A	non non A
V	F	V
F	V	F

Mais clairement, ce n'est pas une démonstration.

En fait, on peut définir une formule comme « vraie » de plusieurs façons :
-- formule prouvable à partir de quelques axiomes et règles de déduction; quand on écrit un arbre de preuve on montre qu'une formule est prouvable;
-- formule valide, c'est-à-dire que si on évalue la formule pour n'importe quelles valeurs des variables, on arrive à vrai; quand on utilise des tables de vérité on montre que la formule est valide (dans la logique booléenne au moins).
Si les formules prouvables sont valides on dit que le système logique est cohérent; si les formules valides sont prouvables il est complet.
Le (premier) théorème de complétude de Gödel dit que la logique booléenne est complète, donc si on montre qu'une formule est valide avec des tables de vérité, elle est prouvable dans la logique booléenne, et la preuve de la logique booléenne est aussi valable comme preuve dans la logique du premier ordre, donc la formule est prouvable (et valide) dans la logique du premier ordre.
J’ai triché en allant voir les notes du cours de logique et théorie des ensembles là (chapitre 6 sur la logique booléenne, 7 pour le premier ordre).

Oui, et ici elles sont valides, mais je ne suis pas sûr qu'elles soient prouvables.
Pourquoi valides ? parce que :
(non(non A)<=>A) est toujours vraie (cf ci-dessus).
et (non A ou A) <=> (A => A) est toujours vraie.

Donc ce sont deux tautologies en logique classique, elles sont donc équivalentes.

JPhMM a écrit:Oui, et ici elles sont valides, mais je ne suis pas sûr qu'elles soient prouvables.
Pourquoi valides ? parce que :
(non(non A)<=>A) est toujours vraie (cf ci-dessus).
et (non A ou A) <=> (A => A) est toujours vraie.

C'est A => non (non A) seulement qui est toujours vraie, et dans la deuxième équivalence on a seulement l'autre implication: (non A ou A) <=> (non (non A) => A).
Comme elles sont valides elles sont prouvables par le théorème de complétude de Gödel (voir mon message précédent), mais c’est un peu prendre un marteau pour écraser une mouche que d’utiliser cet argument alors qu’on peut écrire les arbres de preuve.

FD a écrit:

JPhMM a écrit:Oui, et ici elles sont valides, mais je ne suis pas sûr qu'elles soient prouvables.
Pourquoi valides ? parce que :
(non(non A)<=>A) est toujours vraie (cf ci-dessus).
et (non A ou A) <=> (A => A) est toujours vraie.

C'est A => non (non A) seulement qui est toujours vraie, et dans la deuxième équivalence on a seulement l'autre implication: (non A ou A) <=> (non (non A) => A).
Comme elles sont valides elles sont prouvables par le théorème de complétude de Gödel (voir mon message précédent), mais c’est un peu prendre un marteau pour écraser une mouche que d’utiliser cet argument alors qu’on peut écrire les arbres de preuve.

Merci pour cette précision.
Et oui, en effet.

Bonsoir,
je fais un peu la mouche du coche, mais il me semble qu'il serait préférable d'exhiber une preuve, au lieux de dire : "il y en a une en vertu d'un théorème de Gödel".

Par ailleurs le mélange entre logique booléenne et logique formelle en général ne me semble pas du meilleur gout.
La logique booléenne est une logique du tiers exclu, le démontrer dans ce cadre ne présente donc aucun intérêt : si on suppose (axiome) A démontrer A relève du vide.

En fait j'aimerais voir une démonstration formelle de (A ou non(A))<=>(A<=>non(non(A))

-- formule prouvable à partir de quelques axiomes et règles de déduction; quand on écrit un arbre de preuve on montre qu'une formule est prouvable;

Je ne suis pas d'accord quand on écrit une preuve, on prouve. Certes cela montre que l'affirmation est prouvable,mais c'est un peu plus.

verdurin a écrit:En fait j'aimerais voir une démonstration formelle de (A ou non(A))<=>(A<=>non(non(A))

Moi aussi.
J'essaie et je dois avouer que pour l'instant elle me résiste. Mais je ne désespère pas.

Je ne pense pas qu'il soit possible de faire une preuve convaincante de cette équivalence sans s'extraire de la logique classique, parce que dans cette logique (qui est une formalisation de la logique des mathématiques usuelles), les deux membres de l'équivalence sont toujours vrais : on montre donc « vrai ⇔ vrai ».

On distingue usuellement 3 grands systèmes logiques : la logique classique, la logique intuitionniste et la logique minimale (ou implicative). Ces 3 logiques diffèrent essentiellement par leur traitement de la négation (¬).

La logique minimale (NM) ne lui donne pas de traitement spécifique. On peut tout au plus y voir la négation comme un cas particulier d'implication. En effet, en logique, il est usuel d'introduire un symbole spécial pour le « faux » : ⊥. Alors, la négation « ¬q » se voit comme « q ⇒ ⊥ ».

La logique intuitionniste (NJ) ajoute la règle ex falso sequitur quod libet (EFSQL) : si on a une preuve, en utilisant un ensemble d'hypothèses E, du faux ⊥, alors on peut en déduire une preuve de n'importe quelle formule q. Formellement, la relation « permet de prouver » s'écrit « ⊢ », si bien que la règle EFSQL dit que si E ⊢ ⊥, alors E ⊢ q (pour q quelconque).

La logique classique (NK), la nôtre, peut s'obtenir en ajoutant aux règles de la logique intuitionniste le tiers exclu (TE) : quelle que soit la formule q, on a toujours q ou ¬q, et ce sans aucune hypothèse. La règle dit donc ∅ ⊢ (q ∨ ¬q).

Mais au lieu du tiers exclu, on peut choisir de rajouter l'élimination de la double négation (Élim¬¬) : si E ⊢ ¬¬q, alors E ⊢ q. On peut montrer que la logique ainsi obtenue est la même que la logique classique : c'est en ce sens là que le (TE) et (Élim¬¬) sont équivalents.

Concrètement, on prend la logique intuitionniste (NJ), on lui rajoute la règle (Élim¬¬) et on prouve dans ce système la règle (TE) ; puis on prend le système (NJ)+(TE) et on y montre (Élim¬¬). Notez que (TE) et (Élim¬¬) sont aussi équivalents au raisonnement par l'absurde (RA), qui dit que si l'on a montré le faux ⊥ à partir de l'ensemble d'hypothèses E augmenté de la formule ¬q, alors on a montré q à partir de E : si E, ¬q ⊢ ⊥, alors E ⊢ q.

Merci pour ces éclaircissements.