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.

• Those aren't rules, they are symbols. – James Feb 21 '15 at 2:26
• To explain James' comment: The rules of a natural deduction system are not standard and vary from author to author, so even if they have been labeled by such terse names as "$\land$" we don't know what rules those are. Can you locate your rules from the list on WP? If you use the names there we may be able to help you. – Mario Carneiro Feb 21 '15 at 4:25
• Also see commons.wikimedia.org/wiki/… – Mario Carneiro Feb 21 '15 at 4:30
• I have updated the rules – 333Mhz Feb 24 '15 at 9:32

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)$.