Propositional Calculus Proofs (8)

Th27) ⊢ (P ∧ Q) ⇒ (Q ∧ P)   Commutativity of ∧
1.) ⊢ (Q ⇒ ¬P) ⇒ [¬(¬P) ⇒ ¬Q]                                                    Th24
2.) ⊢ P ⇒ ¬(¬P)                                                                               Th20
3.) ⊢ (Q ⇒ ¬P) ⇒ (P ⇒ ¬Q)                                                            Th13
4.) ⊢ [(Q ⇒ ¬P) ⇒ (P ⇒ ¬Q)] ⇒ [¬(P ⇒ ¬Q) ⇒ ¬(Q ⇒ ¬P)]      Th24
5.) ⊢ ¬(P ⇒ ¬Q) ⇒ ¬(Q ⇒ ¬P)                                                       MP 3,4
6.) ⊢ (P ∧ Q) ⇒ (Q ∧ P)                                                                   Definition of ∧

Th28) ⊢ (P ∧ Q) ⇒ Q

1.) ⊢ ¬Q ⇒ (P ⇒ ¬Q)                                                    Lk1

2.) ⊢ [¬Q ⇒ (P ⇒ ¬Q)] ⇒ [¬(P ⇒ ¬Q) ⇒ ¬(¬Q)]      Th24

3.) ⊢ ¬(P ⇒ ¬Q) ⇒ ¬(¬Q)                                            MP1,2

4.) ⊢ ¬(¬Q) ⇒ Q                                                           Th19

5.) ⊢ ¬(P ⇒ ¬Q) ⇒ Q                                                    Th5

6.) ⊢ (P ∧ Q) ⇒ Q                                                          Definition of ∧

Th29) ⊢ (P ∧ Q) ⇒ P

1.) ⊢ ¬P ⇒ (Q ⇒ ¬P)                                                      Lk1

2.) ⊢ [¬P ⇒ (Q ⇒ ¬P)] ⇒ [¬(Q ⇒ ¬P) ⇒ ¬(¬P)]       Th24
3.) ⊢ ¬(Q ⇒ ¬P) ⇒ ¬(¬P)                                            MP1,2
4.) ⊢ ¬(¬P) ⇒ P                                                            Th19
5.) ⊢ ¬(Q ⇒ ¬P) ⇒ P                                                    Th5
6.) ⊢ (Q ∧ P) ⇒ P                                                          Definition of ∧
7.) ⊢ (P ∧ Q) ⇒ (Q ∧ P)                                                Th27
8.) ⊢ (P ∧ Q) ⇒ P                                                          Th5

Th30) ⊢ P ⇒ [Q ⇒ (P ∧ Q)]
1.) ⊢ P ⇒ [(P ⇒ ¬Q) ⇒ ¬Q]                                              Th16
2.) ⊢ [(P ⇒ ¬Q) ⇒ ¬Q] ⇒ [¬(¬Q) ⇒ ¬(P ⇒ ¬Q)]           Th24
3.) ⊢  P ⇒ [¬(¬Q) ⇒ ¬(P ⇒ ¬Q)]                                     Th5
4.) ⊢ Q ⇒ ¬(¬Q)                                                                Th20
5.) ⊢  P ⇒ [Q ⇒ ¬(P ⇒ ¬Q)]                                             Th13
6.) ⊢  P ⇒ [Q ⇒ (P ∧ Q)]                                                   Definition of ∧

Propositional Calculus (1)

Definition: 

A ∧ B stands for ¬[A ⇒ (¬B)]

A ∨ B stands for (¬A) ⇒ B

A ⇔ B stands for ¬[(A ⇒ B) ⇒ ¬(B ⇒ A)] which is equivalent to (A ⇒ B) ∧ (B ⇒ A).

Propositional Calculus Proofs (7)

Th25) ⊢ (B ⇒ ¬B) ⇒ ¬B
1.) ⊢ (B ⇒ ¬B) ⇒ [¬(¬B) ⇒ ¬B]                            Th24
2.) ⊢ ¬(¬B) ⇒ [¬B ⇒ ¬(B ⇒ B)]                            Th17
3.) ⊢ [¬(¬B) ⇒ ¬B] ⇒ [¬(¬B) ⇒ ¬(B ⇒ B)]         Th2
4.)  [¬(¬B) ⇒ ¬(B ⇒ B)] ⇒ [(B ⇒ B) ⇒ (¬B)]   Lk3
5.) ⊢ (B ⇒ ¬B) ⇒ [(B ⇒ B) ⇒ (¬B)]                      Th8
6.) ⊢ B ⇒ B                                                              Th3
7.) ⊢ (B ⇒ ¬B) ⇒ ¬B                                               Th6

Th26) ⊢ (P ⇒ Q) ⇒ [(P ⇒ ¬Q) ⇒ ¬P]
1.) ⊢ (P ⇒ Q) ⇒ (¬Q ⇒ ¬P)                                                                         Th24
2.) ⊢ P ⇒ [(P ⇒ Q) ⇒ (¬Q ⇒ ¬P)]                                                              Th1
3.) ⊢ {P ⇒ [(P ⇒ Q) ⇒ (¬Q ⇒ ¬P)]} ⇒ {(P ⇒ Q) ⇒ [P ⇒ (¬Q ⇒ ¬P)]}   Th15
4.) ⊢ (P ⇒ Q) ⇒ [P ⇒ (¬Q ⇒ ¬P)]                                                              MP 2,3
5.)  [P ⇒ (¬Q ⇒ ¬P)] ⇒ [(P ⇒ ¬Q) ⇒ (P ⇒ ¬P)]                                    Lk2
6.) ⊢ (P ⇒ Q) ⇒ [(P ⇒ ¬Q) ⇒ (P ⇒ ¬P)]                                                   Th5
7.) ⊢ (P ⇒ ¬P) ⇒ ¬P                                                                                    Th25
8.) ⊢ (P ⇒ Q) ⇒ [(P ⇒ ¬Q) ⇒ ¬P]                                                              Th14

Propositional Calculus Proofs (6)

Th21) U ⇒ I ⊢ (O ⇒ U) ⇒ (O ⇒ I)
1.) ⊢ (U ⇒ I) ⇒ [(O ⇒ U) ⇒ (O ⇒ I)]             Th11 
2.) ⊢ U ⇒ I                                                        Hyp
3.) ⊢ (O ⇒ U) ⇒ (O ⇒ I)                                  MP 1,2

Th22) E ⇒ F ⊢ (F ⇒ G) ⇒ (E ⇒ G)

1.) ⊢ (E ⇒ F) ⇒ [(F ⇒ G) ⇒ (E ⇒ G)]             Th12

2.) ⊢ E ⇒ F                                                        Hyp

3.) ⊢ (F ⇒ G) ⇒ (E ⇒ G)                                  MP 1,2

Th23) P ⇒ Q , R ⇒ S ⊢ (Q ⇒ R) ⇒ (P ⇒ S)

1.) ⊢ P ⇒ Q                                                         Hyp

2.) ⊢ (Q ⇒ R) ⇒ (P ⇒ R)                                   Th22

3.) ⊢ R ⇒ S                                                         Hyp

4.) ⊢ (P ⇒ R) ⇒ (P ⇒ S)                                    Th21

5.) ⊢ (Q ⇒ R) ⇒ (P ⇒ S)                                   Th5

Th24) ⊢ (P ⇒ Q) ⇒ (¬Q ⇒ ¬P)  

1.) ⊢ ¬(¬P) ⇒ P                                                    Th19

2.) ⊢ Q ⇒ ¬(¬Q)                                                  Th20

3.) ⊢ (P ⇒  Q) ⇒ [¬(¬P) ⇒ ¬(¬Q)]                    Th23

4.) ⊢ (¬¬P ⇒ ¬¬Q) ⇒ (¬Q ⇒ ¬P)                      Lk3

5.)  ⊢ (P ⇒ Q) ⇒ (¬Q ⇒ ¬P)                                Th5