Logique propositionelle démonstration selon Hilbert

Bonjour voici mon problème :

Démontrer par la méthode de Hilbert que (P->Q)->(¬P OU Q) est un théorème.
C'est sûrement basique mais je bloque depuis déjà un certains temps...

Merci de votre aide

Réponses

  • Pour moi, c’est la définition de l’implication.
    Sinon, essaie par un tableau.
    Algebraic symbols are used when you do not know what you are talking about.
            -- Schnoebelen, Philippe
  • nicolas.patrois Écrivait:
    > Pour moi, c’est la définition de l’implication.

    Oui c'est bien la dessus que je suis parti mais je sais pas, y a un truc qui dois m'echapper la.
  • Bonjour Dad,
    Comme le dit Nicolas Patrois, c'est par définition de l'implication. Sinon, souviens toi que pour établir que P implique (Q ou R), on suppose que P et (nonQ) est vrai et on établit R.
    Dans ton cas tu supposeras que tu as P implique Q et (non nonP). Conclusion Q est vrai d'après le modus tollens.
    Tu peux aussi supposer que tu as P implique Q et nonQ. Conclusion nonP est vrai d'après le modus ponens.
    Bonne journée.
  • il faudrait peut-être avant tout dire ce que tu entends par "méthode de Hilbert" ..
  • Chercherais-tu une preuve du genre suivant :

    \begin{tabular}{r|l|l|ll}
    1 & & \multicolumn{2}{|l}{$P \Rightarrow Q$} & hypothèse A \\
    2 & & \multicolumn{2}{|l}{$P \vee \neg P$} & tiers exclu (axiome) \\
    & & \multicolumn{3}{c}{~} \\
    3 & & & $P$ & hypothèse B \\
    4 & & & $P \Rightarrow Q$ & réitération de l'hypothèse A \\
    5 & & & $Q$ & modus ponens 3 ; 4 \\
    6 & & & $\neg P \vee Q$ & introduction de $\vee$ \\
    & & \multicolumn{3}{c}{~} \\
    7 & & & $\neg P$ & hypothèse C \\
    8 & & & $\neg P \vee Q$ & introduction de $\vee$ \\
    & & \multicolumn{3}{c}{~} \\
    9 & & \multicolumn{2}{|l}{$\neg P \vee Q$} & élimination de $\vee$ 2 ; 3\_6 ; 7\_8 \\
    & \multicolumn{4}{c}{~} \\
    10 & \multicolumn{3}{l}{$(P \Rightarrow Q) \Rightarrow (\neg P \vee Q)$} & introduction de $\Rightarrow$ 1 ; 9
    \end{tabular}

    rédigée éventuellement avec la méthode des séquents, ou en formalisme hilbertien strict.

    Il faudrait de toute façon préciser dans quelle logique tu te places (minimale, intuitionniste, classique), quel sont les axiomes et les règles que tu te donnes.
  • En premier lieu merci a tout le monde pour votre aide.

    GB : Effectivement je cherche une preuve comme tu la décrit dans ton post. Je me place dans le cas de la logique intuititioniste.

    Les différents axiomes que j'ai a ma disposition sont le suivant :

    P -> (Q-> P)
    (P-> (Q -> R)) -> ((P->Q) -> (P->R))

    P ^ Q -> P
    p -> (Q-> P ^ Q)

    p -> P OU Q
    (P -> R) -> ((Q -> R) -> ((P OU Q) -> R)

    ((P -> Q) ^ (P -> ¬Q)) -> ¬P
    ¬P -> (p -> Q)

    La règle dont je dispose est celle du modus ponens.
  • Dad,

    Il me semblait bien avoir compris le genre de problème auquel tu es confronté.
    Je réfléchis à une preuve de ton truc, mais pour l'instant, je ne vois pas comment me passer du tiers exclu...
  • Ouuups excuse moi j'ai oublié de mentionner le tiers exclu.

    Je pouvais également m'en servir :)

    Merci pour ton aide
  • Avec le tiers exclu dans les axiomes ce n'est plus vraiment intuitionniste...

    Voici une preuve de $(P \Rightarrow Q) \vdash (\neg P \vee Q)$

    1. $P \Rightarrow Q$ (hypothèse)
    2. $Q \Rightarrow (\neg P \vee Q)$ (axiome)
    3. $[Q \Rightarrow (\neg P \vee Q)] \Rightarrow [P \Rightarrow (Q \Rightarrow (\neg P \vee Q))]$ (axiome)
    4. $P \Rightarrow (Q \Rightarrow (\neg P \vee Q))$ (modus ponens 3-2)
    5. $[P \Rightarrow (Q \Rightarrow (\neg P \vee Q))] \Rightarrow [(P \Rightarrow Q) \Rightarrow (P \Rightarrow (\neg P \vee Q))]$ (axiome)
    6. $(P \Rightarrow Q) \Rightarrow (P \Rightarrow (\neg P \vee Q))$ (modus ponens 5-4)
    7. $P \Rightarrow (\neg P \vee Q)$ (modus ponens 6-1)
    8. $[P \Rightarrow (\neg P \vee Q)] \Rightarrow [(\neg P \Rightarrow (\neg P \vee Q)) \Rightarrow ((P \vee \neg P) \Rightarrow (\neg P \vee Q))]$ (axiome)
    9. $(\neg P \Rightarrow (\neg P \vee Q)) \Rightarrow ((P \vee \neg P) \Rightarrow (\neg P \vee Q))$ (modus ponens 8-7)
    10. $\neg P \Rightarrow (\neg P \vee Q)$ (axiome)
    11. $(P \vee \neg P) \Rightarrow (\neg P \vee Q)$ (modus ponens 9-10)
    12. $P \vee \neg P$ (tiers exclu)
    13. $\neg P \vee Q$ (modus ponens 11-12)

    Dès lors, le théorème de déduction permet d'affirme qu'il existe une preuve de $(P \Rightarrow Q) \Rightarrow (\neg P \vee Q)$, et qu'on peut l'écrire algorithmiquement...
  • Bonjour,

    Juste une petite remarque : il y a effectivement peu de chances de pouvoir faire une preuve intuitionniste, vu qu'elle fournirait (pour Q = P) une preuve intuitionniste du tiers exclus !

    Cordialement,

    MC
  • bonjour,
    j'y ai aussi pensé, mais avec les axiomes donnés par Dad, je n'ai pas réussi à démontrer d'abord que p => p est un théorème ! N'avais-je pas les yeux en face des trous ? :)
  • gb, je n'ai pas réussi non plus à démontrer le théorème de la déduction que tu utilises (il me manque toujours p=>p, même avec le tiers exclu).
  • La preuve de $P \Rightarrow P$ est :

    1. $((P \Rightarrow ((P \Rightarrow P) \Rightarrow P)) \Rightarrow ((P \Rightarrow (P \Rightarrow P)) \Rightarrow (P \Rightarrow P))$ (axiome)
    2. $P \Rightarrow ((P \Rightarrow P) \Rightarrow P)$ (axiome)
    3. $(P \Rightarrow (P \Rightarrow P)) \Rightarrow (P \Rightarrow P)$ (modus ponens 1-2)
    4.$P \Rightarrow (P \Rightarrow P)$ (axiome)
    5. $P \Rightarrow P$ (modus ponens 3-4)
  • Ah, oui, merci gb !
  • Pour raccourcir, $A$ désigne la proposition de la ligne numéro $i$ de mon message de 16:36:15, et $B$ désigne la proposition $P \Rightarrow Q$. Le début est inchangé (on supprime la première ligne, puisque l'on raisonne sans hypothèse).

    1. $A[2]$ (axiome)
    2. $A[3]$ (axiome)
    3. $A[4]$ (modus ponens 2-1)
    4. $A[5]$ (axiome)
    5. $A[6]$ (modus ponens 4-3)

    En fait, on a $A[6] \equiv (B \Rightarrow A[7])$, et on repart :
    5. $B \Rightarrow A[7]$
    6. $A[8] \Rightarrow (B \Rightarrow A[8])$ (axiome)
    7. $A[8]$ (axiome)
    8. $B \Rightarrow A[8] \equiv B \Rightarrow (A[7] \Rightarrow A[9]$ (modus ponens 6-7)
    9. $[B \Rightarrow (A[7] \Rightarrow A[9])] \Rightarrow [(B \Rightarrow A[7]) \Rightarrow (B \Rightarrow A[9])]$ (axiome)
    10. $(B \Rightarrow A[7]) \Rightarrow (B \Rightarrow A[9])$ (modus ponens 9-8)
    11. $B \Rightarrow A[9] \equiv B \Rightarrow (A[10] \Rightarrow A[11])$ (modus ponens 10-5)
    12. $A[10] \Rightarrow (B \Rightarrow A[10])$ (axiome)
    13. $A[10]$ (axiome)
    14. $B \Rightarrow A[10]$ (modus ponens 12-13)
    15. $[B \Rightarrow (A[10] \Rightarrow A[11])] \Rightarrow [(B \Rightarrow A[10]) \Rightarrow (B \Rightarrow A[11])]$ (axiome)
    16. $(B \Rightarrow A[10]) \Rightarrow (B \Rightarrow A[11])$ (modus ponens 15-11)
    17. $B \Rightarrow A[11] \equiv B \Rightarrow (A[12] \Rightarrow A[13])$ (modus ponens 16-14)
    18. $A[12] \Rightarrow (B \Rightarrow A[12])$ (axiome)
    19. $A[12]$ (axiome du tiers exclu)
    20. $B \Rightarrow A[12]$ (modus ponens 18-19)
    21. $[B \Rightarrow (A[12] \Rightarrow A[13])] \Rightarrow [(B \Rightarrow A[12]) \Rightarrow (B \Rightarrow A[13])]$ (axiome)
    22. $(B \Rightarrow A[12]) \Rightarrow (B \Rightarrow A[13])$ (modus ponens 21-17)
    23. $B \Rightarrow A[13]$ (modus ponens 22-20)

    Et c'est bien $(P \Rightarrow Q) \Rightarrow (\neg P \vee Q)$.

    Il y a certainement plus rapide, mais c'est le résultat brutal de l'algorithme du théorème de déduction.
  • Dad: si tu veux comprendre tout ça, sache qu'il existe une spécialité qui en donne une approche éclairée. Grace à elle, plus besoin d'être inspirée pour trouver les solutions proposées, par exemple, par gb (que je félicite au passage pour sa disponibilité et son inspiration s'il ne connait pas la correspondance ci-après)

    Cette spécialité s'occupe de la correspondance de Curry Howard, entre les preuves et les programmes (les actions algorythmiques disons).

    Et plus précisément, dans un système à la Hilbert (ou il n'y a pas de "séquents"), il s'agit de la correspondance entre la logique propositionnelle et les combinateurs.

    Une opération binaire est donnée une bonne fois pour toute, et un combinateur est un "objet" qui "fait quelquechose" d'abstrait.

    (priorité à gauche pour les parenthèses sous-entendues, dans la suite)

    Par exemple:

    K.x.y=x pour tout x,y

    S.x.y.z=(x.z).(y.z)

    Il s'avère que K et S permettent de "représenter" toutes les "manipulations" que pourrait réussir un "programme" quelconque.

    Je te le prouve "vite fait":

    Imaginons que tu aies une expression E avec des lettres et l'opération "."

    De plus dans E il y a une lettre "x" que tu voudrais bien considérer comme une variable. Tu veux fabriquer une AUTRE expression, disons, F telle que tu puisses prouver que F.x=E (ainsi, en quelque sorte, F est un "programme" qui, si on lui donne x, parvient à renvoyer E)

    Par récurrence, montrons que S et K suffisent: ton expression E est de la forme U.V

    Disons qu'on peut trouver une expression U' sans x, telle que U'.x=U est prouvable et idem avec V, ie V'.x=V est prouvable

    Alors (S.(U').(V')).x=(U'.x).(V'.x)=U.V=E ... cqfd

    Ah, mais il y a le problème que peut-être E ne contient pas x: dans ce cas, (K.(E)).x=E

    Il reste l'initialisation: si E est l'expression "x" comment faire?

    On voudrait I.x=x démontrable.

    Look: S.K.K.x=(K.x).(K.x)=x et c'est gagné

    Dans la correspondance (essaie de comprendre pourquoi) de Curry Howard,

    S correspond aux axiomes (1) (A->(B->C))->((A->B)->(A->C)). Faire correspondre une expression avec des S et des K à une preuve s'appelle "typer" l'expression (qu'on appelle "terme" soit dit en passant)

    K aux axiomes (2) A->(B->A)

    Et probablement que gb t'a donné une preuve (de P implique P) qui correspond à la construction S.K.K

    Remarque: une preuve en logique intuitionniste propositionnelle donne (telle quelle) une expression avec des S et des K. *

    L'axiome du tiers exclus a résisté longtemps à cette approche... Ca m'emmènerait trop loin de te raconter comment l'histoire s'est terminée...


    * Par exemple: disons que tu veux prouver dans Hilbert (3) (B->C)->((A->B)->(A->C))

    En regardant bien, tu vois que c'est la composition de fonction:

    tu veux construire un "programme" qui compose des "sous-programmes"

    ie tu veux un T qui fait ca (je n'écris plus le point , c'est lourd):

    Tabx=a(bx) pour tous a,b,x (il compose a, b)

    Voyons voir:

    Déjà, je vais fabriquer Tab: ca me donne S(Ka)b en effet:

    S(Ka)b=(Kax).(bx)=a(bx)

    Ta peut etre considéré comme S(Ka) manifestement

    Now fabriquons T:

    T:=S(KS)K semble marcher car Ta=(KSa)(Ka)=S(Ka)

    Et bien une preuve de (3) à partir de (1) et (2) t'est donnée telle quelle:

    Chaque "." (S.(K.S)).K correspond à un modus ponens dans la preuve. Chaque S est une utilisation de (1) et chaque K est une utilisation de (2)
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.