Prove DeMorgan's laws

Question

Using the the ten inferences of the Natural Deduction System prove DeMorgan's laws.

The Rules of Natural Deduction

• Negation Introduction: {(P → Q), (P → ¬Q)} ⊢ ¬P

• Negation Elimination: {(¬P → Q), (¬P → ¬Q)} ⊢ P

• And Introduction: {P, Q} ⊢ P ʌ Q

• And Elimination: P ʌ Q ⊢ {P, Q}

• Or Introduction: P ⊢ {(P ∨ Q),(Q ∨ P)}

• Or Elimination: {(P ∨ Q), (P → R), (Q → R)} ⊢ R

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

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

• If Introduction: (P ⊢ Q) ⊢ (P → Q)

• If Elimination: {(P → Q), P} ⊢ Q

Proof structure

Each statement in your proof must be the result of one of the ten rules applied to some previously derived propositions (no circular logic) or an assumption (described below). Each rule operates across some propositions on the left hand side of the ⊢ (logical consequence operator) and creates any number of propositions from the right hand side. The If Introduction works slightly differently from the rest of the operators (described in detail below). It operates across one statement that is the logical consequent of another.

Example 1

You have the following statements:

{(P → R), Q}

You may use And Introduction to make:

(P → R) ʌ Q

Example 2

You have the following statements:

{(P → R), P}

You may use If Elimination to make:

R

Example 3

You have the following statements:

(P ʌ Q)

You may use And Elimination to make:

P

or to make:

Q

Assumption Propagation

You may at any point assume any statement you wish. Any statement derived from these assumptions will be "reliant" on them. Statements will also be reliant on the assumptions their parent statements rely on. The only way to eliminate assumptions is by If Introduction. For If introduction you start with a Statement Q that is reliant on a statement P and end with (P → Q). The new statement is reliant on every assumption Q relies on except for assumption P. Your final statement should rely on no assumptions.

Specifics and scoring

You will construct one proof for each of DeMorgan's two laws using only the 10 inferences of the Natural Deduction Calculus.

The two rules are:

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

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

Your score is the number of inferences used plus the number of assumptions made. Your final statement should not rely on any assumptions (i.e. should be a theorem).

You are free to format your proof as you see fit.

You may carry over any Lemmas from one proof to another at no cost to score.

Example Proof

I will prove that (P and not(P)) implies Q

(Each bullet point is +1 point)

• Assume not (Q)

• Assume (P and not(P))

• Using And Elim on (P and not(P)) derive {P, not(P)}

• Use And Introduction on P and not(Q) to derive (P and not(Q))

• Use And Elim on the statement just derived to make P

The new P proposition is different from the other one we derive earlier. Namely it is reliant on the assumptions not(Q) and (P and not(P)). Whereas the original statement was reliant only on (P and not(P)). This allows us to do:

• If Introduction on P introducing not(Q) implies P (still reliant on the (P and not(P)) assumption)

• Use And Introduction on not(P) and not(Q) (from step 3) to derive (not(P) and not(Q))

• Use And Elim on the statement just derived to make not(P) (now reliant on not(Q))

• If Introduction on the new not(P) introducing not(Q) implies not(P)

• We will now use negation elimination on not(Q) implies not(P) and not(Q) implies P to derive Q

This Q is reliant only on the assumption (P and not(P)) so we can finish the proof with

• If Introduction on Q to derive (P and not(P)) implies Q

This proof scores a total of 11.

Answer 1

Score: 81

Each line should be worth 1 point. The De Morgan's laws are found at statements (3) and (6). Labels in brackets denote the previous statement(s) a line depends on if they are not immediately preceding.

(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]

Answer 2

Score: 59

Explanation

I'll use a tree like structure for the proof as I find this style quite readable. Each line is annotated by the count of used rules, for example the "Example 1" in the challenge would be represented as this tree (growing bottom to top):

Note the unknown counts A,B and also the assumption Γ - so this is no theorem. To demonstrate how to prove a theorem, let us assume A and use an Or-introduction as follows:

Now this is still depending on the assumption A but we can derive a theorem by applying an If-introduction:

So we were able to derive the theorem ⊢ A → (A ∨ B) in a total of 3 steps (1 assumption & 2 applied rules).

With this we can go on to prove a few new rules that help us to prove DeMorgan's Laws.

Additional Rules

Let's first derive the Principle of Explosion and denote it with PE in further proofs:

From this we derive another form of it: A ⊢ ¬A → X - we'll call it CPE:

We'll need another one where the negated term (¬) is an assumption and refer to it as CPE^-:

From the two rules we just derived (CPE and CPE^-), we can derive an important rule Double Negation:

The next thing to do is to prove something like Modus Tollens - hence MT:

Lemmas

Lemma A

Lemma A1

We'll need the following rule two times:

Lemma A

By instantiating the just proved lemma twice we can show one direction of an equivalence, we will need it in the final proof:

Lemma B

In order to show another direction, we'll need to do two times some quite repetitive stuff (for both arguments A and B in (A ∨ B)) - this means here I could possibly golf the proof further..

Lemma B1'

Lemma B1

Lemma B2'

Lemma B2

Lemma B

Finally the conclusion of B1 and B2:

Actual proof

Once we proved these two statements:

• Lemma A: ⊢ (A ∨ B) → ¬(¬A ʌ ¬B)
• Lemma B: ⊢ ¬(A ∨ B) → (¬A ʌ ¬B)

We can prove the first equivalence (¬(A ∨ B) ≡ ¬A ʌ ¬B)) as follows:

And with the just proved rule together with Iff-Elimination we can prove the second equivalence too:

Not sure about the score - if I did it right, let me know if there's something wrong.

Explanation

Source

If somebody wants the tex source (needs 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}:

Answer 3

Score: 65

The de Morgan laws are line 30 and line 65.

(I haven't made any particular effort to golf this, for example to see if there are some repeated proofs that could be abstracted out at the beginning.)

 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