We will start with proofs of several standard results that we can re-use in the proofs below.
Distribution
1 (1) (p∧q)∨(p∧r) A
2 (2) p∧q A
2 (3) p 2 ∧E
2 (4) q 2 ∧E
2 (5) q∨r 4 ∨I
2 (6) p∧(q∨r) 3,5 ∧I
7 (7) p∧r A
7 (8) p 7 ∧E
7 (9) r 7 ∧E
7 (10) q∨r 9 ∨I
7 (11) p∧(q∨r) 8,10 ∧I
1 (12) p∧(q∨r) 1,2,6,7,11 ∨EDistribution
1 (1) (p∨q)∧(p∨r) A
1 (2) p∨q 1 ∧E
1 (3) p∨r 1 ∧E
4 (4) p A
4 (5) p∨(q∧r) 4 ∨I
6 (6) q A
7 (7) r A
6,7 (8) q∧r 6,7 ∧I
6,7 (9) p∨(q∧r) 8 ∨I
1,6 (10) p∨(q∧r) 3,4,4,7,9 ∨E
1 (11) p∨(q∧r) 2,4,4,6,10 ∨EMaterial conditional
1 (1) ¬p∨q A
2 (2) ¬p A
2 (3) p→q 2 neg.para
4 (4) q A
4 (5) p→q 4 pos.para
1 (6) p→q 1,2,3,4,5 ∨EMaterial conditional
1 (1) p→q A
2 (2) ¬(¬p∨q) A
3 (3) q A
3 (4) ¬p∨q 3 ∨I
2,3 (5) (¬p∨q)∧¬(¬p∨q) 4,2 ∧I
2 (6) ¬q 3,5 RA
1,2 (7) ¬p 1,6 MT
1,2 (8) ¬p∨q 7 ∨I
1,2 (9) (¬p∨q)∧¬(¬p∨q) 8,2 ∧I
1 (10) ¬¬(¬p∨q) 2,9 RA
1 (11) ¬p∨q 10 DNMaterial conditional
1 (1) p∧¬q A
2 (2) p→q A
1 (3) p 1 ∧E
1,2 (4) q 2,3 MP
1 (5) ¬q 1 ∧E
1,2 (6) q∧¬q 4,5 ∧I
1 (7) ¬(p→q) 2,6 RAMaterial conditional
1 (1) ¬(p→q) A
2 (2) ¬p A
2 (3) p→q 2 neg.para
1,2 (4) (p→q)∧¬(p→q) 3,1 ∧I
1 (5) ¬¬p 2,4 RA
1 (6) p 5 DN
7 (7) q A
7 (8) p→q 7 pos.para
1,7 (9) (p→q)∧¬(p→q) 8,1 ∧I
1 (10) ¬q 7,9 RA
1 (11) p∧¬q 6,10 ∧IDeMorgans: first proof
1 (1) ¬(p∧q) A
2 (2) ¬(¬p∨¬q) A
3 (3) ¬p A
3 (4) ¬p∨¬q 3 ∨I
2,3 (5) (¬p∨¬q)∧¬(¬p∨¬q) 4,2 ∧I
2 (6) ¬¬p 3,5 RA
2 (7) p 6 DN
8 (8) ¬q A
8 (9) ¬p∨¬q 8 ∨I
2,8 (10) (¬p∨¬q)∧¬(¬p∨¬q) 9,2 ∧I
2 (11) ¬¬q 8,10 RA
2 (12) q 11 DN
2 (13) p∧q 7,12 ∧I
1,2 (14) (p∧q)∧¬(p∧q) 13,1 ∧I
1 (15) ¬¬(¬p∨¬q) 2,14 RA
1 (16) ¬p∨¬q 15 DNDeMorgans: second proof
1 (1) ¬(p∧q) A
2 (2) p A
3 (3) q A
2,3 (4) p∧q 2,3 ∧I
1,2,3 (5) (p∧q)∧¬(p∧q) 4,1 ∧I
1,2 (6) ¬q 3,5 RA
1 (7) p→¬q 2,6 CP
1 (8) ¬p∨¬q 7 mat.conExcluded middle
1 (1) ¬(p∨¬p) A
2 (2) p A
2 (3) p∨¬p 2 ∨I
1,2 (4) (p∨¬p)∧¬(p∨¬p) 3,1 ∧I
1 (5) ¬p 2,4 RA
1 (6) p∨¬p 5 ∨I
1 (7) (p∨¬p)∧¬(p∨¬p) 6,1 ∧I
(8) ¬¬(p∨¬p) 1,7 RA
(9) p∨¬p 8 DNP → Q ⊢ ¬(P∧¬Q)
1 (1) p→q A
2 (2) p∧¬q A
2 (3) p 2 ∧E
1,2 (4) q 1,2 MP
2 (5) ¬q 2 ∧E
1,2 (6) q∧¬q 4,5 ∧I
1 (7) ¬(p∧¬q) 2,6 RA¬(P∧Q) ⊢ ¬P ∨ ¬Q
This is DeMorgans. It’s proved above.
¬(P→Q) ⊢ P ∧ ¬Q
1 (1) ¬(p→q) A
2 (2) ¬p A
3 (3) p A
4 (4) ¬q A
2,3 (5) p∧¬p 3,2 ∧I
2,3 (6) ¬¬q 4,5 RA
2,3 (7) q 6 DN
2 (8) p→q 3,7 CP
1,2 (9) (p→q)∧¬(p→q) 8,1 ∧I
1 (10) ¬¬p 2,9 RA
1 (11) p 10 DN
12 (12) q A
12 (13) p→q 3,12 CP
1,12 (14) (p→q)∧¬(p→q) 13,1 ∧I
1 (15) ¬q 12,14 RA
1 (16) p∧¬q 11,15 ∧I⊢ (P→Q) ∨ (Q→P)
There’s no short proof (in our system) of this result, but the reason why it holds is simple: either p is true or ¬p is true. If p is true, then q→p is true, and hence (q→p)∨(p→q). If ¬p is true, then p→q is true, and hence (q→p)∨(p→q).
1 (1) ¬(p∨¬p) A
2 (2) p A
2 (3) p∨¬p 2 ∨I
1,2 (4) (p∨¬p)∧¬(p∨¬p) 3,1 ∧I
1 (5) ¬p 2,4 RA
1 (6) p∨¬p 5 ∨I
1 (7) (p∨¬p)∧¬(p∨¬p) 6,1 ∧I
(8) ¬¬(p∨¬p) 1,7 RA
(9) p∨¬p 8 DN
10 (10) q A
2 (11) q→p 10,2 CP
12 (12) ¬p A
13 (13) ¬q A
2,12 (14) p∧¬p 2,12 ∧I
2,12 (15) ¬¬q 13,14 RA
2,12 (16) q 15 DN
12 (17) p→q 2,16 CP
2 (18) (p→q)∨(q→p) 11 ∨I
12 (19) (p→q)∨(q→p) 17 ∨I
(20) (p→q)∨(q→p) 9,2,18,12,19 ∨EP → (Q∨R) ⊢ (P→Q) ∨ (P→R)
(1) p∨¬p EM
2 (2) p→(q∨r) A
3 (3) p A
2,3 (4) q∨r 2,3 MP
5 (5) q A
5 (6) p→q 3,5 CP
5 (7) (p→q)∨(p→r) 6 ∨I
8 (8) r A
8 (9) p→r 3,8 CP
8 (10) (p→q)∨(p→r) 8 ∨I
2,3 (11) (p→q)∨(p→r) 4,5,7,8,11 ∨E
12 (12) ¬p A
13 (13) ¬q A
3,12 (14) p∧¬p 3,12 ∧I
3,12 (15) ¬¬q 13,14 RA
3,12 (16) q 14 DN
12 (17) p→q 3,16 CP
12 (18) (p→q)∨(p→r) 16 ∨I
2 (19) (p→q)∨(p→r) 1,3,11,12,18 ∨E(P∧Q) → ¬Q ⊢ P → ¬Q
1 (1) (p∧q)→¬q A
2 (2) p A
3 (3) q A
2,3 (4) p∧q 2,3 ∧I
1,2,3 (5) ¬q 1,4 MP
1,2,3 (6) q∧¬q 3,5 ∧I
1,2 (7) ¬q 3,6 RA
1 (8) p→¬q 2,7 CPP ∧ ¬Q ⊢ ¬(P→Q)
⊢ ((P→Q)→P) → P
One possibility is to first prove ⊢ P ∨ ¬P, and then argue by cases. The first case is easy if you remember positive paradox. For the second case, use negative paradox, i.e. that ¬p implies p→q.)
P → (Q∨R) ⊢ ¬R → (¬Q→¬P)
1 (1) p→(q∨r) A
2 (2) ¬r A
3 (3) ¬q A
4 (4) p A
1,4 (5) q∨r 1,4 MP
6 (6) q A
3,6 (7) q∧¬q 6,3 ∧I
3,6 (8) ¬¬r 2,7 RA
3,6 (9) r 8 DN
10 (10) r A
1,3,4 (11) r 5,6,9,10,10 ∨E
1,2,3,4 (12) r∧¬r 11,2 ∧I
1,2,3 (13) ¬p 4,12 RA
1,2 (14) ¬q→¬p 3,13 CP
1 (15) ¬r→(¬q→¬p) 2,14 CPP → ¬Q ⊢ (P∧Q) → R
P → ¬Q ⊢ P → (Q→R)
¬(P→Q) ⊢ P → ¬Q
P ⊣ ⊢ (P∧Q) ∨ (P∧¬Q)
P → (Q→R) ⊣ ⊢ (P→Q) → (P→R)
P → ¬P ⊣ ⊢ ¬P
P → (Q→¬Q) ⊣ ⊢ P → ¬Q
(P→Q) → (P→¬Q) ⊣ ⊢ P → ¬Q
P ⊣ ⊢ P ∧ (Q∨¬Q)
P ⊣ ⊢ P ∨ (Q∧¬Q)
(P→Q) → Q ⊢ (Q→P) → P
(P→Q) → R ⊢ (P→R) → R
1 (1) (p→q)→r A
2 (2) p→r A
3 (3) ¬r A
2,3 (4) ¬p 2,3 MT
5 (5) p A
6 (6) ¬q A
2,3,5 (7) p∧¬p 5,4 ∧I
2,3,5 (8) ¬¬q 6,7 RA
2,3,5 (9) q 8 DN
2,3 (10) p→q 5,9 CP
1,2,3 (11) r 1,10 MP
1,2,3 (12) r∧¬r 11,3 ∧I
1,2 (13) ¬¬r 3,12 RA
1,2 (14) r 13 DN
1 (15) (p→r)→r 2,14 CP(P→R) → R ⊣ ⊢ P ∨ R
1 (1) (p→r)→r A
2 (2) ¬(p∨r) A
3 (3) p A
3 (4) p∨r 3 ∨I
2,3 (5) (p∨r)∧¬(p∨r) 4,2 ∧I
6 (6) ¬r A
2,3 (7) ¬¬r 6,5 RA
2,3 (8) r 7 DN
2 (9) p→r 3,8 CP
1,2 (10) r 1,9 MP
1,2 (11) p∨r 10 ∨I
1,2 (12) (p∨r)∧¬(p∨r) 11,2 ∧I
1 (13) ¬¬(p∨r) 2,12 RA
1 (14) p∨r 13 DN1 (1) p∨r A
2 (2) p→r A
3 (3) p A
2,3 (4) r 2,3 MP
5 (5) r A
1,2 (6) r 1,3,4,5,5 ∨E
1 (7) (p→r)→r 2,6 CP(P→Q) → P ⊢ P
Exercise S1. Show that ¬¬¬p ⊢ ¬p in intuitionistic logic. i.e. don’t use DN elimination to prove it.
Exercise S2. Suppose that we add the rule ¬(p∧q) ⊢ ¬p∨¬q to intuitionistic logic. Show that we get full classical logic. That is, use this new rule to prove excluded middle, or equivalently, DN elimination.