Prouvez les lois de DeMorgan

21

L'utilisation des dix inférences du système de déduction naturelle prouve les lois de DeMorgan .

Les règles de déduction naturelle

  • Introduction à la négation: {(P → Q), (P → ¬Q)} ⊢ ¬P

  • Élimination de la négation: {(¬P → Q), (¬P → ¬Q)} ⊢ P

  • Et introduction: {P, Q} ⊢ P ʌ Q

  • Et élimination: P ʌ Q ⊢ {P, Q}

  • Ou introduction: P ⊢ {(P ∨ Q),(Q ∨ P)}

  • Ou élimination: {(P ∨ Q), (P → R), (Q → R)} ⊢ R

  • Introduction à l'IFF: {(P → Q), (Q → P)} ⊢ (P ≡ Q)

  • Élimination Iff: (P ≡ Q) ⊢ {(P → Q), (Q → P)}

  • Si introduction: (P ⊢ Q) ⊢ (P → Q)

  • Si élimination: {(P → Q), P} ⊢ Q

Structure de preuve

Chaque énoncé de votre preuve doit être le résultat d'une des dix règles appliquées à certaines propositions précédemment dérivées (pas de logique circulaire) ou une hypothèse (décrite ci-dessous). Chaque règle opère à travers certaines propositions du côté gauche de (opérateur de conséquence logique) et crée un nombre quelconque de propositions du côté droit. L'introduction If fonctionne légèrement différemment des autres opérateurs (décrits en détail ci-dessous). Il fonctionne à travers une déclaration qui est la conséquence logique d'une autre.

Exemple 1

Vous avez les déclarations suivantes:

{(P → R), Q}

Vous pouvez utiliser Et Introduction pour faire:

(P → R) ʌ Q

Exemple 2

Vous avez les déclarations suivantes:

{(P → R), P}

Vous pouvez utiliser If Elimination pour faire:

R

Exemple 3

Vous avez les déclarations suivantes:

(P ʌ Q)

Vous pouvez utiliser And Elimination pour faire:

P

ou pour faire:

Q

Propagation des hypothèses

Vous pouvez à tout moment assumer toute déclaration que vous souhaitez. Toute déclaration dérivée de ces hypothèses sera "dépendante" d'eux. Les déclarations dépendront également des hypothèses sur lesquelles s'appuient leurs déclarations mères. La seule façon d'éliminer les suppositions est d'utiliser If Introduction. Pour l'introduction Si vous commencez par une déclaration Qqui dépend d'une déclaration Pet finissez par (P → Q). La nouvelle déclaration est tributaire de chaque hypothèse Qsur laquelle repose, à l' exception de l'hypothèse P. Votre déclaration finale ne doit reposer sur aucune hypothèse.

Spécificités et notation

Vous construirez une preuve pour chacune des deux lois de DeMorgan en utilisant seulement les 10 inférences du calcul de déduction naturelle.

Les deux règles sont:

¬(P ∨ Q) ≡ ¬P ʌ ¬Q

¬(P ʌ Q) ≡ ¬P ∨ ¬Q

Votre score est le nombre d'inférences utilisées plus le nombre d'hypothèses faites. Votre déclaration finale ne doit pas reposer sur des hypothèses (c'est-à-dire doit être un théorème).

Vous êtes libre de formater votre épreuve comme bon vous semble.

Vous pouvez reporter n'importe quel lemme d'une épreuve à l'autre sans frais.

Exemple de preuve

Je vais prouver que (P and not(P)) implies Q

(Chaque puce correspond à +1 point)

  • Présumer not (Q)

  • Présumer (P and not(P))

  • Utiliser And Elim sur (P and not(P))dériver{P, not(P)}

  • Utilisation et introduction sur Pet not(Q)pour dériver(P and not(Q))

  • Utilisez And Elim sur la déclaration qui vient d'être dérivée pour faire P

La nouvelle Pproposition est différente de l'autre que nous dérivons plus tôt. À savoir, il dépend des hypothèses not(Q)et (P and not(P)). Alors que la déclaration d'origine ne reposait que sur (P and not(P)). Cela nous permet de faire:

  • Si Introduction à l' Pintroduction not(Q) implies P(toujours tributaire de l' (P and not(P))hypothèse)

  • Utilisez Et Introduction sur not(P)et not(Q)(à partir de l'étape 3) pour dériver(not(P) and not(Q))

  • Utilisez And Elim sur la déclaration que vous venez de dériver not(P) (maintenant dépendante not(Q))

  • Si Introduction sur la nouvelle not(P)introductionnot(Q) implies not(P)

  • Nous allons maintenant utiliser l'élimination de la négation sur not(Q) implies not(P)et not(Q) implies Ppour dériverQ

Cela Qne dépend que de l'hypothèse (P and not(P))afin que nous puissions terminer la preuve avec

  • Si Introduction Qà dériver(P and not(P)) implies Q

Cette preuve obtient un total de 11.

Assistant de blé
la source
7
Bien que le consensus sur la méta soit clair, tout le monde ne l'aura pas encore vu, c'est juste pour souligner que le golf de preuve est sur le sujet .
trichoplax
2
Je pense que vous devriez expliquer la structure des preuves et (le symbole ne s'affiche pas non plus sur mobile).
xnor
3
Je pense que les explications aident certainement. Ce que je trouverais le plus utile serait un exemple travaillé et noté d'une preuve simple qui comprend If-Introduction et des hypothèses, de préférence imbriquées. Peut-être de contrapositif?
xnor
1
Dans votre exemple, je pense que les deux premières hypothèses devraient être inversées; nulle part il n'est indiqué que (P ⊢ (Q ⊢ R)) ⊢ (Q ⊢ (P ⊢ R))(dans ce cas, ¬Q ⊢ ((P ʌ ¬P) ⊢ P)to a (P ʌ ¬P) ⊢ (¬Q ⊢ P)été utilisé).
LegionMammal978
1
Êtes-vous autorisé à prouver plusieurs choses dans un seul "contexte d'hypothèse", puis à extraire plusieurs déclarations d'implication, pour économiser sur le nombre de "lignes d'hypothèse" nécessaires? par exemple (assume (P/\~P); P,~P by and-elim; (assume ~Q; P by assumption; ~P by assumption); ~Q->P by impl-intro; ~Q->~P by impl-intro; Q by neg-elim); P/\~P->Q by impl-intropour obtenir un score de 9?
Daniel Schepler

Réponses:

6

Résultat: 81

Chaque ligne devrait valoir 1 point. Les lois de De Morgan se trouvent aux déclarations (3) et (6). Les étiquettes entre parenthèses indiquent les instructions précédentes dont dépend une ligne si elles ne sont pas immédiatement précédentes.

(a) assume P {
    (aa) P ^ P
    (ab) P
    (ac) P v Q
} (a1) P -> P
  (a2) P -> P v Q
(1) assume ~P ^ ~Q {
    (1a) assume P v Q {
        (1aa) assume Q {
            (1aaa) assume ~P {
                (1aaaa) Q ^ Q [1aa]
                (1aaab) Q
                (1aaac) ~Q [1]
            } (1aaa1) ~P -> Q
              (1aaa2) ~P -> ~Q
            (1aab) P
        } (1aa1) Q -> P
        P [1a, a1, 1aa1]
        ~P [1]
    } (1a1) P v Q -> P
      (1a2) P v Q -> ~P
    (1b) ~(P v Q)
} (11) ~P ^ ~Q -> ~(P v Q)
(2) assume ~(P v Q) {
    (2a) ~(P v Q) ^ ~(P v Q)
    (2b) assume P {
        (2aa) ~(P v Q) [2a]
    } (2b1) P -> ~(P v Q)
    (2c) ~P [a2, 2b1]
    (2d) assume Q {
        (2da) ~(P v Q) [2a]
        (2db) P v Q
    } (2d1) Q -> ~(P v Q)
      (2d2) Q -> P v Q
    (2e) ~Q
    (2f) ~P ^ ~Q
} (21) ~(P v Q) -> ~P ^ ~Q
(3) ~(P v Q) == ~P ^ ~Q [11, 21]
(4) assume ~P v ~Q {
    (4a) assume ~P {
        (4aa) assume P ^ Q {
            (4aaa) P
            (4aab) ~P ^ ~P [4a]
            (4aac) ~P
        } (4aa1) P ^ Q -> P
          (4aa2) P ^ Q -> ~P
        (4ab) ~(P ^ Q)
    } (4a1) ~P -> ~(P ^ Q)
    (4b) assume ~Q {
        (4ba) assume P ^ Q {
            (4baa) Q
            (4bab) ~Q ^ ~Q [4b]
            (4bac) ~Q
        } (4ba1) P ^ Q -> Q
          (4ba2) P ^ Q -> ~Q
        (4bb) ~(P ^ Q)
    } (4b1) ~P -> ~(P ^ Q)
    (4c) ~(P ^ Q) [4, 4a1, 4b1]
} (41) ~P v ~Q -> ~(P ^ Q) 
(5) assume ~(P ^ Q) {
    (5a) assume ~(~P v ~Q) {
        (5aa) ~(~P v ~Q) ^ ~(P ^ Q) [5, 5a]
        (5ab) assume ~P {
            (5aba) ~P v ~Q
            (5abb) ~(~P v ~Q) [5aa]
        } (5ab1) ~P -> ~P v ~Q
          (5ab2) ~P -> ~(~P v ~Q)
        (5ac) P
        (5ad) assume ~Q {
            (5ada) ~P v ~Q
            (5adb) ~(~P v ~Q) [5aa]
        } (5ad1) ~Q -> ~P v ~Q
          (5ad2) ~Q -> ~(~P v ~Q)
        (5ae) Q
        (5af) P ^ Q [5ac, 5ae]
        (5ag) ~(P ^ Q) [5aa]
    } (5a1) ~(~P v ~Q) -> P ^ Q
      (5a2) ~(~P v ~Q) -> ~(P ^ Q)
    (5b) ~P v ~Q
} (51) ~(P ^ Q) -> ~P v ~Q
(6) ~(P ^ Q) == ~P v ~Q [41, 51]
feersum
la source
4

Résultat: 59

Explication

Je vais utiliser une structure arborescente pour la preuve car je trouve ce style assez lisible. Chaque ligne est annotée par le nombre de règles utilisées, par exemple "l'exemple 1" dans le défi serait représenté comme cet arbre (croissant de bas en haut):

AIntro

Notez les nombres inconnus A, B et aussi l'hypothèse Γ - ce n'est donc pas un théorème. Pour démontrer comment prouver un théorème, supposons A et utilisons une introduction Or comme suit:

OIntro

Maintenant, cela dépend toujours de l'hypothèse A mais nous pouvons dériver un théorème en appliquant une If-introduction:

IIntro

Nous avons donc pu dériver le théorème ⊢ A → ( AB ) en 3 étapes au total (1 hypothèse & 2 règles appliquées).

Avec cela, nous pouvons continuer à prouver quelques nouvelles règles qui nous aident à prouver les lois de DeMorgan.

Règles supplémentaires

Dérivons d'abord le principe d'explosion et notons-le avec PE dans d'autres preuves:

PE

Nous en déduisons une autre forme: A ⊢ ¬ AX - nous l'appellerons CPE :

PE

Nous en aurons besoin d'un autre où le terme nié (¬) est une hypothèse et nous l' appellerons CPE - :

NCPE

Des deux règles que nous venons de dériver ( CPE et CPE - ), nous pouvons dériver une règle importante Double Négation :

DN

La prochaine chose à faire est de prouver quelque chose comme Modus Tollens - d'où MT :

MT

Lemmas

Lemme A

Lemme A1

Nous aurons besoin de la règle suivante deux fois:

LA1

Lemme A

En instanciant deux fois le lemme qui vient d'être démontré, nous pouvons montrer une direction d'équivalence, nous en aurons besoin dans la preuve finale:

LA

Lemme B

Afin de montrer une autre direction, nous devons faire deux fois certains trucs assez répétitif (pour les deux arguments A et B dans ( AB )) - ce qui signifie ici que je pourrais peut - être la preuve de golf plus ..

Lemme B1 '

LB1_

Lemme B1

LB1

Lemme B2 '

LB2_

Lemme B2

LB2

Lemme B

Enfin la conclusion de B1 et B2 :

KG

Preuve réelle

Une fois que nous avons prouvé ces deux déclarations:

  • Lemme A : ⊢ ( AB ) → ¬ (¬ A ʌ ¬ B )
  • Lemme B : ⊢ ¬ ( AB ) → (¬ A ʌ ¬ B )

On peut prouver la première équivalence (¬ ( AB ) ≡ ¬ A ʌ ¬ B )) comme suit:

P1

Et avec la règle qui vient d'être prouvée avec Iff-Elimination, nous pouvons également prouver la deuxième équivalence:

P2

Je ne suis pas sûr du score - si je l'ai bien fait, faites-moi savoir s'il y a quelque chose qui ne va pas.

Explication

La source

Si quelqu'un veut la source tex (a besoin de mathpartir ):

In the following a rule \textbf{XYZ'} will denote the rule XYZ's second last
step, for example \textbf{PE'} will be $ A \land \lnot A \vdash X $.

\section*{Principle of Explosion [PE]}

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=10]
    {\inferrule*[Left=$\lnot$-Elim,Right=9]
      {\inferrule*[Left=$\to$-Intro,Right=4]
        {\inferrule*[Left=$\land$-Elim,Right=3]
          {\inferrule*[Left=Axiom,Right=2]
            { }
            { A \land \lnot A, \lnot X \vdash A \land \lnot A }
          }
          { A \land \lnot A, \lnot X \vdash A }
        }
        { A \land \lnot A \vdash \lnot X \to A } \\
       \inferrule*[Right=$\to$-Intro,Left=4]
          {\inferrule*[Right=$\land$-Elim,Left=3]
            {\inferrule*[Right=Axiom,Left=2]
              { }
              { A \land \lnot A, \lnot X \vdash A \land \lnot A }
            }
            { A \land \lnot A, \lnot X \vdash \lnot A }
          }
        { A \land \lnot A \vdash \lnot X \to \lnot A }
      }
      { A \land \lnot A \vdash X }
    }
    { \vdash (A \land \lnot A) \to X }
\end{mathpar}

\section*{Conditioned PE [CPE]}

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=5]
  {\inferrule*[Left=$\to$-Elim,Right=4]
    {\inferrule*[Left=$\land$-Intro,Right=3]
      {\inferrule*[Left=Axiom,Right=1]
        { } { A \vdash A } \\
       \inferrule*[Right=Axiom,Left=1]
        { } { \lnot A \vdash \lnot A }
      }
      { A, \lnot A \vdash A \land \lnot A } \\
     \inferrule*[Right=PE,Left=0]
      { } { \vdash (A \land \lnot A) \to X }
    }
    { A, \lnot A \vdash X }
  }
  { A \vdash \lnot A \to X }
\end{mathpar}

to get \textbf{CPE$^-$}:

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=1]
    {\inferrule*[Left=CPE',Right=0]
      { }
      { A, \lnot A \vdash X }
    }
    { \lnot A \vdash A \to X }
\end{mathpar}

\section*{Double Negation [DN]}

\begin{mathpar}
  \inferrule*[Left=$\equiv$-Intro,Right=5]
    {\inferrule*[Left=$\to$-Intro,Right=2]
      {\inferrule*[Left=$\lnot$-Elim,Right=1]
        {\inferrule*[Left=CPE$^-$,Right=0]
          { }
          { \lnot\lnot A \vdash \lnot A \to X } \\
          \inferrule*[Right=CPE$^-$,Left=0]
          { }
          { \lnot\lnot A \vdash \lnot A \to \lnot X }
        }
        { \lnot\lnot A \vdash A }
      }
      { \vdash \lnot\lnot A \to A } \\ \\ \\
      \inferrule*[Left=$\to$-Intro,Right=2]
        {\inferrule*[Left=$\lnot$-Intro,Right=1]
          {\inferrule*[Left=CPE,Right=0]
            { }
            {  A \vdash \lnot A \to X } \\
            \inferrule*[Right=CPE,Left=0]
            { }
            { A \vdash \lnot A \to \lnot X }
          }
          { A \vdash \lnot\lnot A }
        }
        { \vdash A \to \lnot\lnot A }
    }
    { \vdash \lnot\lnot A \equiv A  }
\end{mathpar}

\section*{Modus Tollens [MT]}

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=6]
    {\inferrule*[Left=$\lnot$-Intro,Right=5]
      {\inferrule*[Left=Axiom,Right=1]
       { }
       { A \to \lnot B \vdash A \to \lnot B } \\
       \inferrule*[Right=$\to$-Intro,Left=3]
         {\inferrule*[Right=Axiom,Left=2]
           { }
           { A, B \vdash B }
         }
         { B \vdash A \to B }
       }
      { A \to \lnot B, B \vdash \lnot A }
    }
    { A \to \lnot B \vdash B \to \lnot A }
\end{mathpar}

\section*{Lemma A}

\textbf{Lemma A1}:

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=9]
    {\inferrule*[Left=$\lor$-Elim,Right=8]
       { \inferrule*[Left=CPE,Right=3]
          {\inferrule*[Left=$\land$-Elim,Right=2]
            {\inferrule*[Left=Axiom,Right=1]
              { }
              { A \land B \vdash A \land B }
            }
            { A \land B \vdash B}
          }
          { A \land B \vdash \lnot B \to X } \\
         \inferrule*[Right=CPE,Left=3]
          {\inferrule*[Right=$\land$-Elim,Left=2]
            {\inferrule*[Right=Axiom,Left=1]
              { }
              { A \land B \vdash A \land B }
            }
            { A \land B \vdash A }
          }
          { A \land B \vdash \lnot A \to X } \\ \\ \\
         \inferrule*[Right=Axiom,Left=1]
          { }
          { \lnot A \lor \lnot B \vdash \lnot A \lor \lnot B }
       }
       { A \land B, \lnot A \lor \lnot B \vdash X }
    }
    { \lnot A \lor \lnot B \vdash (A \land B) \to X }
\end{mathpar}

\textbf{Lemma A}:
ბიმო
la source
1
Pour autant que je sache, le système de preuve de déduction naturelle ici ne permet pas de prouver une déclaration une fois avec des variables de proposition génériques, puis de l'instancier. Donc, chaque fois que vous avez une instanciation différente de l'un de vos lemmes en termes de variables Pet Q, vous devez compter ses pas séparément dans le total final. (En d'autres termes, le système de preuve ne permet pas directement de prouver des lemmes de "second ordre" comme "pour toutes les propositions A et B A/\B -> B/\A", puis de l'utiliser pour prouver les deux P/\(Q/\R) -> (Q/\R)/\Pet (P/\Q)/\R -> R/\(P/\Q).)
Daniel Schepler
@DanielSchepler: Oui, mais il n'y a pas de dépendances circulaires et dans la règle, il est stipulé que vous pouvez reporter n'importe quel lemme d'une épreuve à l'autre sans frais pour marquer. , donc ça ira. Edit : En fait, si cela n'était pas autorisé, je suis certain que cette question n'aurait qu'une seule réponse éligible.
ბიმო
J'interprétais cela comme signifiant simplement que vous pourriez avoir des preuves communes d'un ensemble de formules concrètes partagées entre les preuves des deux déclarations finales.
Daniel Schepler
1

Résultat: 65

Les lois de Morgan sont les lignes 30 et 65.

(Je n'ai pas fait d'effort particulier pour jouer au golf, par exemple pour voir s'il y a des preuves répétées qui pourraient être résumées au début.)

 1. assume ~(P\/Q)
 2.   assume P
 3.     P\/Q  by or-introl, 2
 4.   P -> P\/Q  by impl-intro, 2, 3
 5.   P -> ~(P\/Q)  by impl-intro, 2, 1
 6.   ~P  by neg-intro, 4, 5
 7.   assume Q
 8.     P\/Q  by or-intror, 7
 9.   Q -> P\/Q  by impl-intro, 7, 8
10.   Q -> ~(P\/Q) by impl-intro, 7, 1
11.   ~Q  by neg-intro, 9, 10
12.   ~P /\ ~Q  by and-intro, 6, 11
13. ~(P\/Q) -> ~P/\~Q  by impl-intro, 1, 12
14. assume ~P /\ ~Q
15.   ~P, ~Q  by and-elim, 14
16.   assume P \/ Q
17.     assume P
18.     P -> P  by impl-intro, 17, 17
19.     assume Q
20.       assume ~P
21.       ~P -> Q  by impl-intro, 20, 19
22.       ~P -> ~Q  by impl-intro, 20, 15
23.       P  by neg-elim, 21, 22
24.     Q -> P  by impl-intro, 19, 23
25.     P  by or-elim, 16, 18, 24
26.   P\/Q -> P  by impl-elim, 16, 25
27.   P\/Q -> ~P  by impl-elim, 16, 15
28.   ~(P\/Q)  by neg-intro, 26, 27
29. ~P/\~Q -> ~(P\/Q)  by impl-intro, 14, 28
30. ~(P\/Q) <-> ~P/\~Q  by iff-intro, 13, 29
31. assume ~(P/\Q)
32.   assume ~(~P\/~Q)
33.     assume ~P
34.       ~P\/~Q  by or-introl, 33
35.     ~P -> ~P\/~Q  by impl-intro, 33, 34
36.     ~P -> ~(~P\/~Q)  by impl-intro, 33, 32
37.     P  by neg-elim, 35, 36
38.     assume ~Q
39.       ~P\/~Q  by or-intror, 38
40.     ~Q -> ~P\/~Q  by impl-intro, 38, 39
41.     ~Q -> ~(~P\/~Q)  by impl-intro, 38, 32
42.     Q  by neg-elim, 40, 41
43.     P /\ Q  by and-intro, 37, 42
44.   ~(~P\/~Q) -> P /\ Q  by impl-intro, 32, 43
45.   ~(~P\/~Q) -> ~(P /\ Q)  by impl-intro, 32, 31
46.   ~P \/ ~Q  by neg-elim, 44, 45
47. ~(P/\Q) -> ~P\/~Q  by impl-intro, 31, 46
48. assume ~P\/~Q
49.   assume ~P
50.     assume P/\Q
51.       P, Q  by and-elim, 50
52.     P/\Q -> P  by impl-intro, 50, 51
53.     P/\Q -> ~P  by impl-intro, 50, 49
54.     ~(P/\Q)  by neg-intro, 52, 53
55.   ~P -> ~(P/\Q)  by impl-intro, 49, 54
56.   assume ~Q
57.     assume P/\Q
58.       P, Q  by and-elim, 57
59.     P/\Q -> Q  by impl-intro, 57, 58
60.     P/\Q -> ~Q  by impl-intro, 57, 56
61.     ~(P/\Q)  by neg-intro, 59, 60
62.   ~Q -> ~(P/\Q)  by impl-intro, 56, 61
63.   ~(P/\Q)  by or-elim, 48, 55, 62
64. ~P\/~Q -> ~(P/\Q)  by impl-intro, 48, 63
65. ~(P/\Q) <-> ~P\/~Q  by iff-intro, 47, 64
Daniel Schepler
la source