Démonstration formelle en logique

SylvainK
SylvainK
dans Fondements et 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.

Réponses

  • Martial
    Martial
    Bonjour, SylvainK
    Attention, il y a une erreur de saisie au niveau de l'axiome A10.
  • SylvainK
    SylvainK
    Merci c'est corrigé.
  • bisam
    bisam
    Je suis étonné que CC n'ait pas encore fondu sur ce fil...;)
  • remarque
    remarque
    Ah bah, il n'est pas obligé d'être connecté 24h/24 !
    21020
  • JLT
    JLT
    Son réveil a peut-être fondu.
    21022
  • SylvainK
    SylvainK
    Oui après avoir posté, j'ai vu un de ses posts sur la logique combinatoire, ceci dit je ne sais pas faire ça avec des "ou" et des "non", ma correspondance de Curry-Howard s'arrêtant à l'implication simple et le type fonction de base.
  • christophe c
    christophe c
    :)-D non j'étais parti déjeuner avec un grand mathématicien et j'ai fait un saut à la bibli pour emprunter un super livre de géométrie conseillé par Bruno...

    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 :D

    Bon, je vais regarder ça...
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    ceci dit je ne sais pas faire ça avec des "ou" et des "non", ma correspondance de Curry-Howard s'arrêtant à l'implication simple et le type fonction de base.

    C'est largement suffisant, tu ajoutes tout ce que tu veux en "l'admettant" au sens "CuHO", ie comme des "instructions magiques" :D

    Bon, non, mais je vais regarder ça, t'inquiète...
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • ev
    ev
    Comme dirait Cidrolin, il faut pas confondre Curry-Howard avec Hurry coward !

    amicalement,

    e.v.
    Personne n'a raison contre un enfant qui pleure.


  • christophe c
    christophe c
    En fait, j'ai l'impression que la seule chose qui manque à ton petit système est le "tout". Donc il faut le simuler. Par exemple, tu peux essayer tout:= non(X=>X) . Comme tu as Y=>(X=>X) tu as bien que [non(X=>X)]=>nonY (pour tous les Y que tu auras envie) et donc avec A4 tu peux remplacer Y par non Z. Tu disposes donc bien d'un "tout".

    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 :D

    Si tu ne sais pas hilbertiser je te dirai comment faire.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Et si "X=>X" te gêne (vu que c'est pas un axiome), tu peux prendre un axiome de ton systeme et le nier (par exemple non(A1)) en guise de "tout".
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Comme je vais me déco, je te dis comment "hilbertiser".

    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.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • SylvainK
    SylvainK
    X=>X ne me gêne pas je l'ai déja démontré (enfin Patrick Dehornoy l'a fait pour nous...)
  • christophe c
    christophe c
    ma solution te convient tu vois comment la construire ou tu veux plus de détails?
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Bon, évidemment, c'est optimisable :D mais c'est pour te donner un idée de pourquoi je te demandais "tu veux plus de détails" (en fait j'ai passer à peu près le raisonnement précédent à un hilbertiseur naturel sans optimiser (et encore j'ai retiré quelques redondances qui font que c'est raccourci)) :D
    [size=x-small]
(non(non(p ou nonp)))=>(p ou non p)
((non(p ou nonp))=>(non(a=>a)))=>(((a)=>(a))=>(non(non(p ou nonp))))
((non(p ou nonp))=>(((p)=>(non(a=>a)))=>(non(a=>a))))=>(((non(p ou nonp))=>((p)=>(non(a=>a))))=>((non(p ou nonp))=>(non(a=>a)))) 
[/size]
...
[200 à 300 lignes illisibles qui de toutes façons n'auraient été lues par personne. AD]
...
[size=x-small]
(non(p ou nonp))=>(((a)=>(a))=>((non(p ou nonp))=>(nonp)))
(non(p ou nonp))=>(((a)=>(a))=>(nonp))
(non(p ou nonp))=>((p)=>(non(a=>a)))
(non(p ou nonp))=>(non(a=>a))
((a)=>(a))=>(non(non(p ou nonp)))
(a)=>(a)
non(non(p ou nonp))
p ou non p
[/size]
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • SylvainK
    SylvainK
    Les 200 à 300 lignes me font un petit peu peur...
  • christophe c
    christophe c
    C'était juste pour te dire qu'il y a une façon automatique (quelques lignes de caml pour obtenir ça) de passer d'une preuve avec des "supposons A... donc B; donc au final, sans supposer A, on a prouvé A=>B" à une preuve n'utilisant que le modus ponens.

    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.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • SylvainK
    SylvainK
    Et bien il me faut juste de quoi donner à manger à mon vérifieur (écrit lui aussi en OCaml).
    Je pourrai admettre ces résultats bien connus de logique propositionnelle, mais j'aimerai rester le plus rigoureux (et formel) possible.
  • SylvainK
    SylvainK
    Pour "a ou non a" je vois l'idée oui, et pour (a oub) =>((a=>c) =>( (b=>c) =>c)) ?
  • christophe c
    christophe c
    bin tu supposes a ou b; puis a=>c ; puis b=>c et tu veux prouver c:

    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 :D )
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    En petits caractères, un peu nettoyé (pas beaucoup), ça devrait être acceptable pour une lecteure attentive par Sylvain:

    En posant z:= "a ou non a"
    [size=x-small]non tout
(non a)=>(z)
((non a)=>(z))=>((non z)=>(non(non a)))
((non z)=>((non a)=>(z)))=>((non z)=>((non z)=>(non(non a))))
(non z)=>((non z)=>(non(non a)))
((non z)=>(non z))=>((non z)=>(non(non a)))
(non z)=>(non(non a))
(non(non a))=>(a)
((non z)=>(non(non a)))=>((non z)=>(a))
(non z)=>(a)
(a)=>(z)
((a)=>(z))=>((non z)=>(non a))
((non z)=>((a)=>(z)))=>((non z)=>((non z)=>(non a)))
(non z)=>((non z)=>(non a))
((non z)=>(non z))=>((non z)=>(non a))
(non z)=>(non a)
((non a)=>(non a))=>((non z)=>((non a)=>(non a)))
(non z)=>((non a)=>(non a))
(non a)=>((non tout)=>(non a))
((non tout)=>(non a))=>((a)=>(tout))
(((non a)=>(((non tout)=>(non a))=>((a)=>(tout))))=>(((non a)=>((non tout)=>(non a)))=>((non a)=>((a)=>(tout)))))=>((non z)=>(((non a)=>(((non tout)=>(non a))=>((a)=>(tout))))=>(((non a)=>((non tout)=>(non a)))=>((non a)=>((a)=>(tout))))))
(non z)=>(((non a)=>(((non tout)=>(non a))=>((a)=>(tout))))=>(((non a)=>((non tout)=>(non a)))=>((non a)=>((a)=>(tout)))))
((non z)=>((non a)=>(((non tout)=>(non a))=>((a)=>(tout)))))=>((non z)=>(((non a)=>((non tout)=>(non a)))=>((non a)=>((a)=>(tout)))))
(non z)=>(((non a)=>((non tout)=>(non a)))=>((non a)=>((a)=>(tout))))
((non z)=>((non a)=>((non tout)=>(non a))))=>((non z)=>((non a)=>((a)=>(tout))))
(non z)=>((non a)=>((a)=>(tout)))
((non z)=>(non a))=>((non z)=>((a)=>(tout)))
(non z)=>((a)=>(tout))
((non z)=>(a))=>((non z)=>(tout))
(non z)=>(tout)
((non z)=>(tout))=>((non tout)=>(non(non z)))
(non tout)=>(non(non z))
non(non z)
(non(non z))=>(z)
z[/size]
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    L'autre exo explose littéralement :D désolé ...
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Tu as ausi une autre façon de "jouer" à ça: au lieu de "hilbertisier" à chaque fois que tu décharges une hypothèse d'un raisonnementnaturel, tu rajoutes "H=>blabla" à chaque ligne comprises entre sa supposition et son déchargement. C'est "moins savant", mais ça ne rajoute que des axiomes inoffensifs (faut une structure de preuve linéaires, des suites de phrases)
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Ce qui te donne:

    [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]
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • SylvainK
    SylvainK
    Merci beaucoup :)
  • christophe c
    christophe c
    Vus tes MP je pense que l'exercice suivant t'intéressera: http://www.les-mathematiques.net/phorum/read.php?3,700037,700176#msg-700176
    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)
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • SylvainK
    SylvainK
    Les solutions que j'ai trouvées, je ne sais même plus comment.
    A ou non A
    (A ou B) => (A =>C) => (B =>C) =>C
  • Poirot
    Poirot
    Et ça t'a pris 9 ans ? :-D
  • raoul.S
    raoul.S
    ::o
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 19

AmadouCyranoMatricule_63NicoLeProfRescassolalmbiguine_equationgai requin +11 Invités