Équivalence tiers exclu et double négation
Bonjour :-)
En logique intuitionniste, le tiers exclu équivaut à l'élimination de la double négation.
Ci-dessous une preuve (les soulignés sont là pour la clarté des changements de contexte, par contre les barres verticales sont involontaires).
On se place en logique intuitionniste avec tiers exclu.
_On considère une proposition $A$ telle que $\neg \neg A$.
_Par le tiers exclu, $A \vee \neg A$.
__Si $A$, alors $A$.
__Si $\neg A$, alors $\neg A \wedge \neg \neg A$, donc $\bot$, puis $A$ par explosion.
_Par élimination de $\vee$, on a bien $A$.
On se place maintenant en logique intuitionniste avec élimination de la double négation.
_On considère une proposition $A$.
_Par élimination de la double négation, il nous suffit de prouver $\neg \neg (A \vee \neg A)$.
__Supposons $\neg (A \vee \neg A)$ et montrons $\bot$.
___Si $A$, alors $(A \vee \neg A)$, donc $\bot$.
__On a donc $\neg A$.
___Si $\neg A$, alors $(A \vee \neg A)$, donc $\bot$.
__On a donc $\neg \neg A$.
__Ainsi, $\neg A \wedge \neg \neg A$, d'où $\bot$.
Je me suis alors demandé si cette équivalence était toujours valable en logique minimale.
L'une des preuves est toujours valable, mais l'autre ne l'est plus (utilisant l'explosion).
L'élimination de la double négation serait-elle strictement plus forte que le tiers exclu en logique minimale ?
Merci d'avance :-D
En logique intuitionniste, le tiers exclu équivaut à l'élimination de la double négation.
Ci-dessous une preuve (les soulignés sont là pour la clarté des changements de contexte, par contre les barres verticales sont involontaires).
On se place en logique intuitionniste avec tiers exclu.
_On considère une proposition $A$ telle que $\neg \neg A$.
_Par le tiers exclu, $A \vee \neg A$.
__Si $A$, alors $A$.
__Si $\neg A$, alors $\neg A \wedge \neg \neg A$, donc $\bot$, puis $A$ par explosion.
_Par élimination de $\vee$, on a bien $A$.
On se place maintenant en logique intuitionniste avec élimination de la double négation.
_On considère une proposition $A$.
_Par élimination de la double négation, il nous suffit de prouver $\neg \neg (A \vee \neg A)$.
__Supposons $\neg (A \vee \neg A)$ et montrons $\bot$.
___Si $A$, alors $(A \vee \neg A)$, donc $\bot$.
__On a donc $\neg A$.
___Si $\neg A$, alors $(A \vee \neg A)$, donc $\bot$.
__On a donc $\neg \neg A$.
__Ainsi, $\neg A \wedge \neg \neg A$, d'où $\bot$.
Je me suis alors demandé si cette équivalence était toujours valable en logique minimale.
L'une des preuves est toujours valable, mais l'autre ne l'est plus (utilisant l'explosion).
L'élimination de la double négation serait-elle strictement plus forte que le tiers exclu en logique minimale ?
Merci d'avance :-D
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Si c'est le cas, ça reste vrai en partant d'une logique classique, c'est donc ce que je vais faire. Prenant alors $C= \top$, on obtient une logique qui satisfait le tiers exclu (car $A\to C$ est évidemment vérifiée donc $A\lor (A\to C)$, i.e. $A\lor \neg^C A$ aussi), mais pas le principe de double négation (car $\neg^C\neg^C A$ est valide, indépendamment de $A$).
Si mon premier paragraphe est faux, je n'ai aucune idée de comment te répondre :-D
EDIT : pour une justification de mon premier paragraphe, voir : https://fr.wikipedia.org/wiki/Logique_minimale - je n'étais pas sûr de me souvenir de toutes les règles de la logique minimale, d'où mon hésitation. Le fait que $\bot$ ne joue aucun rôle privilégié à part "je suis $\bot$" explique qu'on puisse y mettre un $C$ quelconque
Si j'ai bien compris, en prenant $C = \top$, si la logique obtenue est cohérente, alors on peut choisir une proposition $A$ indémontrable, qui vérifie le tiers exclu, mais pas l'élimination de la double négation.
L'élimination de la double négation est donc bien strictement plus forte que le tiers exclu (sous réserve de la cohérence de la théorie ci-dessus), c'est ça ?
Pas besoin de beaucoup de connaissances en théorie des modèles, l'argument n'utilise que des tables de vérité à la fin : tu montres (par récurrence sur la taille des preuves, le point qui fait que ça marche est lors de l'usage des règles de déduction ou des axiomes selon ton système de preuves préféré) que si $p$ est prouvable, alors $p^C$ l'est aussi où $p^C$ est la formule qu'on obtient en remplaçant dans $p$ toute occurrence de $\bot$ par $C$ ($C$ étant disons une variable - c'est défini comme d'habitude par récurrence sur la taille de la formule).
Donc si “tiers exclu implique double négation“ était prouvable, la preuve ne faisant appel qu'à un nombre fini d'utilisations du tiers exclu, tu pourrais prouver un truc de la forme “$p\to q$“ (que j'appelle $f$) où $p$ est une conjonction d'énoncés de la forme $b\lor \neg b$ et $q$ est $\neg\neg a \to a$.
Donc $f^C$ serait prouvable, or il n'est même pas prouvable classiquement (là on peut utiliser des tables de vérité, c'est à peine de la théorie des modèles :-D )
Mettre un "ou" en logique minimale me paraît assez sulfureux mais à la rigueur c'est pas grave.
Sans "ou" on peut simuler le "ou" mais ça sort du sujet.
Donc pour info l'équivalent des TE et non non = id exprimés en logique minimale son t, au choix:
((A=>B)=>A)=>A
(A=>C)=>(((A=>B)=>C)=>C)
celui ci te plaira "c'est" le TE
J'aime bien aussi
((A=>B)=>B)=>((B=>A)=>A)
qui sous l'air innocent d'affirmer commutativité de ou ajouté non chqlemment le TE.
C'est un truc encore plus minimaliste que la logique intuitionniste ?
Merci d'éclairer ma lanterne d'ignare notoire.
Maxtimax : Je ne suis pas sûr de savoir ce qui permet l'utilisation de raisonnement par récurrence/induction en logique. La logique est-elle ici perçue comme une branche des mathématiques (et possède donc une sous-logique implicite) ? Dans ce cas, les théorèmes prouvés ont-ils une valeur dans la logique implicite (celle qui permet d'exprimer des maths) ?
En tout cas, je n'avais jamais vu ce raisonnement, mais on dirait un argument diagonal
christophe c : C'est étrange, car ce que vous appelez "tout" n'est pourtant pas grand chose en logique minimale. Sinon, sans méchanceté, je doute que la 'loyauté' et 'dame nature' aient quelque chose à voir avec des démonstrations mathématiques.
Quoiqu'il en soit, je me demande quelle est la signification de ce que vous nommez 'TE'.
Foys : Cette fois, il est clair que l'on étudie la logique comme branche des mathématiques ! J'ai l'impression d'un peu mieux comprendre la théorie des modèles : est-ce (au moins en partie) l'étude des valeurs possibles de $F$ ?
Sinon, j'ai l'impression que votre formulation s'approche des systèmes à la Hilbert ; est-ce le cas ?
Ce qu'on prouve en logique mathématique a une valeur en logique "implicite" dans la mesure où la logique mathématique modélise la logique "implicite". Au delà de ça, on rentre dans de la philo, mais là tu ne pourras rien "prouver"
(A ou nonA)
ou bien encore
non non A implique A
Je l'avais vu mais d'ordinaire je préfète tes explications aux pages wiki
De toute façon (foys en a donné une réalisation avec les combinateurs K et S) , je répète qu'elle n'a rien de minimale à cause de S qui duplique un de ses entrées:
S est la fonction x-->[y-->[z--> (xz)(yz)]] et elle duplique z.
Or il a été découvert depuis 50ans que la puissance mathématique ne vient pas du raisonnement par l'absurde mais de la duplication.
Pour distinguer chaque ingrédient il vaut mieux changer la définition de foys en la définition EQUIVQLENTE DUIVANTE:
À=>(B=>À)
(À=>(À=>B))=>(À=>B)
(À=>B)=>((B=>C)=>(À=>C))
ignorer les accents imposés par mon téléphone
Où le CLONEUR (la formule du milieu) est bien visible. Ne rien changer de la définition de foys par ailleurs