Propositional Calculus Proofs (13)

Th52.) ⊢ [H ⇒ (K ∧ L)] ⇒ [(H ⇒ L) ∧ (H ⇒ K)]
1.) ⊢ {[H ⇒ (K ∧ L)] ⇒ (H ⇒ L)} ⇒ {([H ⇒ (K ∧ L)] ⇒ (H ⇒ K)) ⇒ [[H ⇒ (K ∧ L)] ⇒ ((H ⇒ L) ∧ (H ⇒ K))]}                                                                                                               Th37

2.) ⊢ [H ⇒ (K ∧ L)] ⇒ (H ⇒ L)                                                                                      Th38

3.) ⊢ [H ⇒ (K ∧ L)] ⇒ (H ⇒ K)                                                                                      Th39

4.) ⊢ {([H ⇒ (K ∧ L)] ⇒ (H ⇒ K)) ⇒ [[H ⇒ (K ∧ L)] ⇒ ((H ⇒ L) ∧ (H ⇒ K))]}       MP 1,2

5.) ⊢ [H ⇒ (K ∧ L)] ⇒ [(H ⇒ L) ∧ (H ⇒ K)]                                                                 MP 3,4

Th53.) (A ⇔ B) ⊢ (¬A ⇔ ¬B)
1.) ⊢ A ⇔ B                                                                                                Hyp
2.) ⊢ (A ⇒ B) ∧ (B ⇒ A)                                                                            Definition of ⇔
3.) ⊢ [(A ⇒ B) ∧ (B ⇒ A)] ⇒ (A ⇒ B)                                                       Th35
4.) ⊢ [(A ⇒ B) ∧ (B ⇒ A)] ⇒ (B ⇒ A)                                                       Th34
5.) ⊢ (A ⇒ B)                                                                                              MP 2,3
6.) ⊢ (B ⇒ A)                                                                                              MP 2,4
7.) ⊢ (A ⇒ B) ⇒ (¬B ⇒ ¬A)                                                                       Th29
8.) ⊢ (B ⇒ A) ⇒ (¬A ⇒ ¬B)                                                                       Th29
9.) ⊢ ¬B ⇒ ¬A                                                                                            MP 5,7
10.) ⊢ ¬A ⇒ ¬B                                                                                           MP 6,8
11.) ⊢ (¬B ⇒ ¬A) ⇒ [(¬A ⇒ ¬B) ⇒ ((¬B ⇒ ¬A) ∧ (¬A ⇒ ¬B))]             Th36
12.) ⊢ (¬A ⇒ ¬B) ⇒ ((¬B ⇒ ¬A) ∧ (¬A ⇒ ¬B))                                       MP 9,11
13.) ⊢ [(¬B ⇒ ¬A) ∧ (¬A ⇒ ¬B)]                                                              MP 10,12
14.) ⊢ ¬B ⇔ ¬A                                                                                          Definition of ⇔
15.) ⊢ ¬A ⇔ ¬B                                                                                          Th41 

Th54.) ⊢ P ⇔ P
1.) ⊢ P ⇒ P                                Th3
2.) ⊢ P ⇒ P                               Th3
3.) ⊢ P ⇔ P                               Th40

Propositional Calculus Proofs (12)

Th49.) ⊢ ¬(¬P) ⇔ P
1.) ⊢ ¬¬P ⇒ P                         Th24

2.) ⊢ P ⇒ ¬¬P                         Th25

3.) ⊢ ¬(¬P) ⇔ P                     Th40

Th50.) ⊢ ¬(A ∧ B) ⇔ (¬A ∨ ¬B)  De Morgan's First Law
1.) ⊢ ¬(A ∧ B) ⇔ ¬{¬[A ⇒ (¬B)]}                Definition of ∧
2.) ⊢ ¬{¬[A ⇒ (¬B)]} ⇔ [A ⇒ (¬B)]            Th49
3.) ⊢ ¬(A ∧ B) ⇔ [A ⇒ (¬B)]                         Th42
4.) ⊢ ¬(A ∧ B) ⇔ [¬(¬A) ⇒ (¬B)]                 Th49
5.) ⊢ ¬(A ∧ B) ⇔ (¬A ∨ ¬B)                           Definition of ∨

Th51.) ⊢ ¬(A ∨ B) ⇔ (¬A ∧ ¬B)  De Morgan's Second Law
1.) ⊢ ¬(A ∨ B) ⇔ ¬(¬A ⇒ B)                          Definition of ∨
2.) ⊢ ¬(A ∨ B) ⇔ ¬[¬A ⇒ ¬(¬B)]                 Th49
3.) ⊢ ¬(A ∨ B) ⇔ (¬A ∧ ¬B)                           Definition of ∧

Propositional Calculus Proofs (11)

Th38.)

Th39.) ⊢ [P ∧ (Q ∧ R)] ⇒ [(P ∧ Q) ∧ R]  Associativity of ∧
1.) ⊢ [R ⇒ (P ⇒ ¬Q)] ⇒ [P ⇒ (R ⇒ ¬Q)]                           Th15
2.) ⊢ ¬[P ⇒ (R ⇒ ¬Q)] ⇒ ¬[R ⇒ (P ⇒ ¬Q)]                      Th24
3.) ⊢ ¬[P ⇒ ¬(R ∧ Q)] ⇒ ¬[R ⇒ ¬(P ∧ Q)]                        Definition of ∧
4.) ⊢ [P ∧ (R ∧ Q)] ⇒ [R ∧ (P ∧ Q)]                                    Definition of ∧
5.) ⊢ [P ∧ (Q ∧ R)] ⇒ [(P ∧ Q) ∧ R]                                    Th32 Twice

Th40.) ⊢ A ∨ ¬A  Law of Excluded Middle
1.) ⊢ ¬A ⇒ ¬A                      Th3
2.) ⊢ A ∨ ¬A                         Definition of ∨

Th41.) ⊢ (A ∨ B) ⇒ (B ∨ A) Commutativity of ∨
1.) ⊢ [(¬A) ⇒ B] ⇒ [(¬B) ⇒ ¬(¬A)]                              Th24
2.) ⊢ ¬(¬A) ⇒ A                                                              Th19
3.) ⊢ [(¬A) ⇒ B] ⇒ [(¬B) ⇒ A]                                      Th14
4.) ⊢ (A ∨ B) ⇒ (B ∨ A)                                                   Definition of ∨

Th42.) ⊢ P ⇒ (P ∨ Q)
1.) ⊢ P ⇒ (¬P ⇒ Q)                                                         Th18
2.) ⊢ P ⇒ (P ∨ Q)                                                            Definition of ∨

Th43.) ⊢ Q ⇒ (P ∨ Q)
1.) ⊢ Q ⇒ (¬Q ⇒ P)                                                         Th18
2.) ⊢ Q ⇒ (Q ∨ P)                                                            Definition of ∨
3.) ⊢ (Q ∨ P) ⇒ (P ∨ Q)                                                   Th41
4.) ⊢ Q ⇒ (P ∨ Q)                                                            Th5

Th44.) ⊢ [P ∨ (Q ∨ R)] ⇒ [(P ∨ Q) ∨ R]  Associativity of ∨
1.) ⊢ [¬P ⇒ (¬R ⇒ Q)] ⇒ [¬R ⇒ (¬P ⇒ Q)]                           Th15
2.) ⊢ [¬P ⇒ (R ∨ Q)] ⇒ [¬R ⇒ (P ∨ Q)]                                  Definition of ∧
4.) ⊢ [P ∨ (R ∨ Q)] ⇒ [R ∨ (P ∨ Q)]                                         Definition of ∧
5.) ⊢ [P ∨ (Q ∨ R)] ⇒ [(P ∨ Q) ∨ R]                                         Th45 Twice