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