Formal proof of one of De Morgan's laws 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.
 A: 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$
A: 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)   

A: 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.

