Formal proof of one of De Morgan's laws

Question

How to give a formal proof of $\vdash \neg (p\land q)\to\neg p\lor \neg q$ in the natural deduction proof system? Here is what I have:

0.                         (no premises)
   1.not(p and q)          (assumption)
      2.p                  (assumption) 
        .
        .
        .
      95.p and q       
      96.F                 (from 1,95)
   97.not(p)               (from 2-96)
   98.not(p) or not(q)     (from 97)
99.not(p and q) → not(p) or not(q)

But I don't know how to obtain $F$ from $p$... I tried to use the law of excluded middle but it didn't help.

Answer 1

Your proof strategy is never going to work, because $\neg p$ is not a logical consequence of $\neg (p \land q)$. So, you can't get to line 97 from line 1. Likewise, $p \land q$ is not a logical consequence of $\neg (p \land q)$ and $p$ ... so you can't get to line 95 from lines 2 and 3.

Instead, try to use a proof by contradiction: assume $\neg (\neg p \lor \neg q)$, and show that that leads to a contradiction:

$1. \neg(p \land q)$

$2. \quad \neg (\neg p \lor \neg q) $

...

$95. \quad p \land q$

$96. \quad \bot$

$97. \neg \neg (\neg p \lor \neg q)$

$98. \neg p \lor \neg q$

And how does that work? Well, try and get $p$ and $q$ individually within the subproof:

$1. \neg(p \land q)$

$2. \quad \neg (\neg p \lor \neg q) $

...

$50 \quad p$

...

$94. \quad q$

$95. \quad p \land q$

$96. \quad \bot$

$97. \neg \neg (\neg p \lor \neg q)$

$98. \neg p \lor \neg q$

OK, but how do you do that? Again, proof by contradiction!

$1. \neg(p \land q)$

$2. \quad \neg (\neg p \lor \neg q) $

$3. \quad \quad \neg p$

$4. \quad \quad \neg p \lor \neg q $

$5. \quad \quad \bot$

$6. \quad \neg \neg p$

$50 (=7) \quad p$

... (same for $q$)

$94. \quad q$

$95. \quad p \land q$

$96. \quad \bot$

$97. \neg \neg (\neg p \lor \neg q)$

$98. \neg p \lor \neg q$

Answer 2

not (p) is not absolute so don't try to prove it.

Do this instead:

0.                         (no premises)
  1.not(p and q)          (assumption)
    2.p                  (assumption) 
    .
    .
    .
    95.not(q)       
  96.p  → not(q)             (from 2-95)
    97.not(p)     (assumption)
  98. not (p) or not(q) (95 and 97)
99.not(p and q) → not(p) or not(q) (from 1 - 98)

Maybe a little clearer:

0.
   1. not (p and q) (assumption)
   2. p or not(p)   (excluded middle)
         3. not (p)    (assumption)
   4. (no statement)
         5. p (assumption)
            6. q (assumption)
            7. p and q (5 and 6)
            8. F  (1 and 7 contradiction)
          9. not q (6 -8)
   5. not (p) or not (q) (3 and 9)
6 not(p and q) → not(p) or not(q) (1-5)   

Answer 3

This proof is similar to what fleablood provided except it uses a proof checker.

It also uses the Law of the Excluded Middle (LEM) by first considering $P$ and then considering $¬P$ to arrive at the desired conclusion.