Démonstration formelle en logique
Je dispose des axiomes (Axx) et théorèmes (Thxx) suivants :
A1 P1 => (P2 => P1)
A2 (P1 => (P2 => P3)) => ((P1 => P2) => (P1 => P3))
A3 P1 => ¬¬P1
A4 ¬¬P1 => P1
A5 (P1 => P2) => (¬P2 => ¬P1)
A6 P1 => (P2 => (P1 /\ P2))
A7 (P1 /\ P2) => P1
A8 (P1 /\ P2) => P2
A9 P1 => (P1 \/ P2)
A10 P2 => (P1 \/ P2)
A11 ¬P1 => ((P1 \/ P2) => P2)
Th1 (P1 \/ P1) => P1
Th2 (P1 => P2) => ((P2 => P3) => (P1 => P3))
J'aimerai en déduire les théorèmes suivants :
P1 \/ ¬P1
(P1 \/ P2)=> ((P1 => P3) => ((P2 => P3) => P3))
J'ajoute que toute la puissance du "Ou" est incluse dans l'axiome A11.
Pour info les axiomes sont ceux que Patrick Dehornoy mentionne dans son cours de logique.
Le contexte est un vérifieur informatique de démonstration de logique.
Toute aide est la bienvenue.
A1 P1 => (P2 => P1)
A2 (P1 => (P2 => P3)) => ((P1 => P2) => (P1 => P3))
A3 P1 => ¬¬P1
A4 ¬¬P1 => P1
A5 (P1 => P2) => (¬P2 => ¬P1)
A6 P1 => (P2 => (P1 /\ P2))
A7 (P1 /\ P2) => P1
A8 (P1 /\ P2) => P2
A9 P1 => (P1 \/ P2)
A10 P2 => (P1 \/ P2)
A11 ¬P1 => ((P1 \/ P2) => P2)
Th1 (P1 \/ P1) => P1
Th2 (P1 => P2) => ((P2 => P3) => (P1 => P3))
J'aimerai en déduire les théorèmes suivants :
P1 \/ ¬P1
(P1 \/ P2)=> ((P1 => P3) => ((P2 => P3) => P3))
J'ajoute que toute la puissance du "Ou" est incluse dans l'axiome A11.
Pour info les axiomes sont ceux que Patrick Dehornoy mentionne dans son cours de logique.
Le contexte est un vérifieur informatique de démonstration de logique.
Toute aide est la bienvenue.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Attention, il y a une erreur de saisie au niveau de l'axiome A10.
Pour l'aide attendue, je t'avoue que je veux bien te mettre un des mes 13646 prouveurs-caml compulsifs automatiques en ligne (je crois que j'en ai deja is plusieurs) , mais j'ai un peu la flemme de me taper toutes les transformations de déductions naturelles en Hilbert-modus-ponens-seul-raisonnements
Bon, je vais regarder ça...
C'est largement suffisant, tu ajoutes tout ce que tu veux en "l'admettant" au sens "CuHO", ie comme des "instructions magiques"
Bon, non, mais je vais regarder ça, t'inquiète...
amicalement,
e.v.
Q:=P ou nonP.
Si nonQ alors en particulier nonP et donc Q, donc tu as bien que (nonQ)=>Q dans ton système (tu hilbertises tout àa avec A1,A2).
Ensuite avec le "tout" préfabriqué de ci-dessus (c'est pas très joli):
(Q=>tout)=>Q donc (Q=>tout)=>(Q et (Q=>tout)) donc (Q=>tout) =>tout donc non(nonQ) donc Q.
Je te prouve l'équivalence entre non Q et (Q=>tout):
si non Q alors (non(tout))=>(nonQ) donc non(nonQ)=>non(non(tout)) donc Q=>tout
réciproquement: si Q=>tout alors non(tout)=>nonQ et donc non(non(X=>X))=>nonQ et donc nonQ
Tu n'as plus qu'à mettre les étapes faciles et à hilbertiser
Si tu ne sais pas hilbertiser je te dirai comment faire.
A chaque fois que tu dis "supposons A...donc B", tu remplaces le dernier modus ponens [X=>B; X ]---> B par A=>(X=>B) ; A=>X et tu utilises (A2) pour arriver à A=>B.
Tu remontes ainsi dans l'arbre jusqu'à éliminer toutes les suppositions provisoires. Il se peut que certains B ne soient pas dû au A que tu as supposé, et là tu utilises (A1) pour pouvoir obtenir A=>B quand-même.
Du coup, quel genre de solutions rédigées formellement souhaites-tu à ta demande? Bon après, il y a les concours d'esthétiques, trouver la preuve la plus courte possible avec juste le modus ponens, mais la plupart même des plus courtes preuves sont longues.
Sinon, à mon post précédant la blague des 200 lignes, je t'ai donné essentiellement la solution.
Je pourrai admettre ces résultats bien connus de logique propositionnelle, mais j'aimerai rester le plus rigoureux (et formel) possible.
il suffit de prouver non(non c) et par ce qui précède (non c)=>c
donc tu supposes non c: et tu veux prouver c.
de non c tu peux déduire non a (car tu as a=>c) donc b donc c
(Je ne reposte pas le hilbertisé de ce raisonnement, AD ne serait pas content )
En posant z:= "a ou non a"
[size=x-small]non tout
(non z)=>(non z)
(non z)=>((a)=>(z))
(non z)=>(((a)=>(z))=>((non z)=>(non a)))
(non z)=>((non z)=>(non a))
(non z)=>(non a)
(non z)=>((non a)=>(z))
(non z)=>(z)
(non z)=>((non tout)=>(non z))
(non z)=>(((non tout)=>(non z))=>((z)=>(tout)))
(non z)=>((z)=>(tout))
(non z)=>(tout)
((non z)=>(tout))=>((non tout)=>(non(non z)))
(non tout)=>(non(non z))
(non(non z))=>(z)
non(non z)
z
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>(non tout)))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(a ou b))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(non c))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((a)=>(c)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(((a)=>(c))=>((non c)=>(non a))))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((non c)=>(non a)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(non a))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((non a)=>((a ou b)=>(b))))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((a ou b)=>(b)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(b))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((b)=>(c)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(c))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((non tout)=>(non c)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(((non tout)=>(non c))=>((c)=>(tout))))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>((c)=>(tout)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non c)=>(tout))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>(((non c)=>(tout))=>((non tout)=>(non(non c))))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non tout)=>(non(non c)))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>(non(non c))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>((non(non c))=>(c))))
(a ou b)=>(((a)=>(c))=>(((b)=>(c))=>(c)))[/size]
démontre le théorème (5.2) que j'y affirme (tu as now tout le matos caml pour le fair en deux coups de cuillere)
A ou non A
(A ou => (A =>C) => (B =>C) =>C