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
Friday, February 26, 2016
Wednesday, February 24, 2016
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.) ⊢ (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
Subscribe to:
Posts (Atom)