# 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)$.
{"ft_lang_label":"__label__en","ft_lang_prob":0.8752723,"math_prob":0.99875194,"size":1066,"snap":"2020-45-2020-50","text_gpt3_token_len":276,"char_repetition_ratio":0.14500941,"word_repetition_ratio":0.015625,"special_character_ratio":0.27110693,"punctuation_ratio":0.10714286,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.99986386,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-10-28T23:00:06Z\",\"WARC-Record-ID\":\"<urn:uuid:6a36a911-5743-4189-aac3-ecc08a5e3b60>\",\"Content-Length\":\"153309\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:c8221a5f-071d-49a2-aa3e-8d80ef7401ef>\",\"WARC-Concurrent-To\":\"<urn:uuid:88d97145-bbf6-42d5-8795-b515fac83421>\",\"WARC-IP-Address\":\"151.101.65.69\",\"WARC-Target-URI\":\"https://math.stackexchange.com/questions/1158365/natural-deduction-distribute-neg-without-distribution\",\"WARC-Payload-Digest\":\"sha1:L26FYQ6RYIIUUC6XU6CV6AQAMOQFD56H\",\"WARC-Block-Digest\":\"sha1:MSSRPBIYIYNDVJGQJWEDWBIKW5S72MRT\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-45/CC-MAIN-2020-45_segments_1603107902038.86_warc_CC-MAIN-20201028221148-20201029011148-00557.warc.gz\"}"}