Sequent Proofs for DeMorgan's Laws

Theodore Sider (2009) presents a sequent proof for a "DeMorgan" sequent as follows:

∼(P ∨ Q) ⇒ (∼P ∧ ∼Q):

1. ∼(P ∨ Q) ⇒ ∼(P ∨ Q)                            RA
2. P ⇒ P                                                  RA
3. P ⇒ P ∨ Q                                           2,∨I
4. ∼(P ∨ Q), P ⇒ (P ∨ Q) ∧ ∼(P ∨ Q)       1,3,∧I
5. ∼(P ∨ Q) ⇒ ∼P                                     4,RAA
6. Q ⇒ Q                                                  RA
7. Q ⇒ P ∨ Q                                           6,∨I
8. ∼(P ∨ Q), Q ⇒ (P ∨ Q) ∧ ∼(P ∨ Q)       1,7,∧I
9. ∼(P ∨ Q) ⇒ ∼Q                                     8,RAA
10. ∼(P ∨ Q) ⇒ ∼P ∧ ∼Q                          5,9,∧I 

(Each line is numbered, and to the right of each line is written the sequent line and the inference rule that justify it: ∨I stands for "v introduction," ∧I stands for "∧ introduction," DN stands for "double negation," RA stands for "rule of assumption," and RAA stands for "reductio ad absurdum.")¹

      DeMorgan's Laws are two rules of inference that define the relation between negation, disjunction, and conjunction. They are: ~(p v q) ↔ (~p ∧ ~q), which can be read as "the negation of the disjunction of two statements is logically equivalent to the conjunction of their negations," and ~(p ∧ q) ↔ (~p v ~q), which can be read as "the negation of the conjunction of two statements is logically equivalent to the disjunction of their negations."

      Below are sequent proofs for the other side of the first law and both sides of the second. These proofs are outlined by Fergus Duniho in his "Logic Lesson 15: Proving DeMorgan's Theorem with Indirect Proof."²

SHOW: (∼P ∧ ∼Q) ⇒ ∼(P v Q)

1. (∼P ∧ ∼Q) ⇒ (∼P ∧ ∼Q)                         RA
2. (P ∨ Q) ⇒ (P ∨ Q)                                 RA
3. (∼P ∧ ∼Q) ⇒ ∼P                                    1,∧E
4. (∼P ∧ ∼Q) ⇒ ∼Q                                    1,∧E
5. (P ∨ Q), ∼P ⇒ Q                                   3,vE

6. (P v Q), (∼P ∧ ∼Q) ⇒ Q ∧ ∼Q                4,5,∧I
7. (∼P ∧ ∼Q) ⇒ ∼(P v Q)                            RAA

SHOW: ∼(P ∧ Q) ⇒ (∼P ∨ ∼Q)

1. ∼(P ∧ Q) ⇒ ∼(P ∧ Q)                               RA
2. ∼(∼P v ∼Q) ⇒ ∼(∼P v ∼Q)                        RA
3. ∼P ⇒ ∼P                                                  RA
4. ∼P ⇒ ∼P v ∼Q                                         3,vI
5. ∼P, ∼(∼P v ∼Q) ⇒ (∼P v ∼Q) ∧ ∼(∼P v ∼Q)
                                                                   2,4,∧I
6. ∼(∼P v ∼Q) ⇒ P                                       RAA
7. ∼Q ⇒ ∼Q                                                 RA
8. ∼Q ⇒ ∼P v ∼Q                                         8,vI
9. ∼Q,∼(∼P v ∼Q) ⇒ (∼P v ∼Q) ∧ ∼(∼P v ∼Q)
                                                                   2,8,∧I
10. ∼(∼P v ∼Q) ⇒ Q                                    RAA
11. ∼(∼P v ∼Q) ⇒ P ∧ Q                              6,10,∧I
12. ∼(P ∧ Q), ∼(∼P v ∼Q) ⇒ (P ∧ Q) ∧ ∼(P ∧ Q)
                                                                   1,11,∧I
13. ∼(P ∧ Q) ⇒ (∼P v ∼Q)                            RAA

SHOW: (∼P ∨ ∼Q) ⇒ ∼(P ∧ Q)

1. (∼P ∨ ∼Q) ⇒ (∼P ∨ ∼Q)                           RA
2. P ⇒ P                                                     RA
3. (P ∧ Q) ⇒ (P ∧ Q)                                   RA
4. (P ∧ Q) ⇒ P                                             3,∧E
5. (P ∧ Q) ⇒ Q                                            3,∧E
6. P ⇒ ∼∼P                                                  DN
7. (∼P ∨ ∼Q), ∼∼P ⇒ ∼Q                              2,vE
8. (P ∧ Q), (∼P v ∼Q) ⇒ Q ∧ ∼Q                5,7,∧E
9. (∼P v ∼Q) ⇒ ∼(P ∧ Q)                              RAA


FOOTNOTES

¹Theodore Sider, Logic for Philosophy (Oxford: Oxford University Press, 2010), p. 55.

²Fergus Duniho, "Logic Lesson 15: Proving DeMorgan's Theorem with Indirect Proof" (2015), online on YouTube, https://www.youtube.com/watch?v=HqJIoz1lCXE