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.
Best Answer
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$