Natural Deduction Distribute Neg without Distribution? I have been given a list of statements which are provably equivalent, and it is my job to prove them. They are all quite similar in structure, but I'm having a difficult time proving even the first one, given the rules provided. I'm confident I can do the rest, if I can see the mechanics of the first in action.
The statement is:
$$
\neg (p \wedge q) \leftrightarrow \neg q \vee \neg p
$$
The only rules I have at my disposal are:
$$
\wedge (AND, \wedge i - introduction, \wedge e - elimination) 
$$
$$
\vee (OR, \vee i - introduction, \vee i - elimination) 
$$
$$
\rightarrow (implication, \rightarrow i - introduction, \rightarrow e - elimination)
$$
$$
\neg (negation, \neg i - introduction, \neg e - elimination)
$$
$$
\bot (contradiction)
$$
$$
\neg\neg (double negation)
$$
Now, I know from other logic courses and books that De Morgans laws state that the negation of a conjunction is the disjunction of the negations, but how to I prove this step by step in a proof given the rules above. I keep running into the need to have a rule that distributes negation.
 A: With Natural Deduction, we have to prove the bi-conditional in two steps.
The first one is :

$\vdash (¬q∨¬p) \to ¬(p∧q)$.

1) $(¬q∨¬p)$ --- assumed
2) $p \land q$ --- asumed [a]
3) $p$ --- from 2) by $\land$-elim
4) $q$ --- from 2) by $\land$-elim
5) $\lnot q$ --- assumed [b] from 1) for $\lor$-elim
6) $\bot$ --- contradiction from 4) and 5)
7) $\lnot p$ --- assumed [c] from 1) for $\lor$-elim
8) $\bot$ --- contradiction from 3) and 7)
9) $\bot$ --- from 5)-6) and 7)-8) and 1) by $\lor$-elim, discharging assumptions [b] and [c]

10) $\lnot (p \land q)$ --- from 2) and 9) by $\lnot$-introduction, discharging assumption [a].

Thus, form 1) and 10) we have :

$(¬q∨¬p) \vdash \lnot (p \land q)$

and we conclude by $\to$-introduction with :


11) $\vdash (¬q∨¬p) \to \lnot (p \land q)$.



In the same way we have to prove the other conditional :

$\vdash \lnot (p \land q) \to (¬q∨¬p)$.

In this case we need Double Negation :
1) $\lnot (p \land q)$ --- assumed
2) $\lnot (¬q∨¬p)$ --- assumed [a]
3) $\lnot p$ --- assumed [b]
4) $(¬q∨¬p)$ --- from 3) by $\lor$-introduction
5) $\bot$ --- from 2) and 4)
6) $p$ --- from 3) and 5) by Double Negation, discharging [b]
7) $q$ --- assumed [c]
8) $p \land q$ --- from 6) and 7) by $\land$-introduction
9) $\bot$ --- from 1) and 8)
10) $\lnot q$ --- from 7) and 9), discharging [c]
11) $(¬q∨¬p)$ --- from 10) by $\lor$-introduction
12) $\bot$ --- from 2) and 11)

13) $(¬q∨¬p)$ --- from 2) and 12) by Double Negation, discharging [a]

Thus, form 1) and 13) by $\to$-introduction we conclude with :


14) $\vdash \lnot (p \land q) \to (¬q∨¬p)$




Finally, having :

$(¬q∨¬p) \to ¬(p∧q)$

and :

$\lnot (p \land q) \to (¬q∨¬p)$

we conclude by $\leftrightarrow$-introduction with :


$\lnot (p \land q) \leftrightarrow (¬q∨¬p)$.


