Propositional Calculus Proofs (3)

Derived Rule
Th1) T ⊢ Q ⇒ T (Using Johnstone's Axioms)
1.) ⊢ T                                        Hypothesis
2.) ⊢ T ⇒ [Q ⇒ T]                   Sub (P, T) J1
3.) ⊢ Q ⇒ T                              MP 1,2
∴ T ⊢ Q ⇒ T

Th3) ⊢P ⇒ P (Using Johnstone's Axioms)
1.) ⊢ P ⇒ [(P ⇒ P) ⇒ P]                                                                     Sub ((P ⇒ P), Q) J1
2.) ⊢ {P ⇒ [(P ⇒ P) ⇒ P]} ⇒ {[P ⇒ (P ⇒ P)] ⇒ [P ⇒ P]}          Sub ((P ⇒ P), Q) (P, R) J2
3.) ⊢ [P ⇒ (P ⇒ P)] ⇒ [P ⇒ P]                                                         MP 1,2
4.) ⊢ P ⇒ [P ⇒ P]                                                                                Sub (P, Q) J1
∴ ⊢P ⇒ P                                                                                              MP 3,4


Th3) ⊢P ⇒ P (Using Lukawitz Alternative Axioms)
1.)⊢[P ⇒ (¬P ⇒ Q)] ⇒ {[(¬P ⇒Q) ⇒P] ⇒ (P ⇒P)}
        Sub (P,A) ((¬P ⇒ Q), B) (P, C) Lka1
2.) P ⇒ (¬P ⇒ Q)                                                                  Ax Lka3
3.) ⊢ [(¬P ⇒ Q) ⇒ P] ⇒ (P ⇒ P)                                       MP 1,2
4.) ⊢ [(¬P ⇒ P) ⇒ P] ⇒ (P ⇒ P)                                        Sub (P, Q) Line 3
5.) (¬P ⇒ P) ⇒ P                                                                   Ax Lka2
∴ ⊢P ⇒ P                                                                                MP 4,5

Derived Rule (Using Lukawitz Alternative Axioms)
T ⊢ ¬T ⇒ Q 
1.) ⊢ T                                Hypothesis
2.) ⊢ T ⇒ (¬T ⇒ Q)        Sub (T, P) Lka3
3.) ⊢ ¬T ⇒ Q                   MP 1,2
∴ T ⊢ ¬T ⇒ Q

Th3) ⊢P ⇒ P (Using Tarski's Axioms)
1.) ⊢ P ⇒ (P ⇒ P)                             Sub (P, Q) T1
2.) ⊢ [P ⇒ (P ⇒ P)] ⇒ (P ⇒ P)      Sub (P, Q) T2
∴ ⊢ P ⇒ P                                           MP 1,2

Derived Rule
T, (¬R ⇒ ¬T) ⊢ R (Using Tarski's Axioms)
1.) ⊢ T                                                                             Hypothesis1
2.) ⊢ (¬R ⇒ ¬T)                                                           Hypothesis2
3.) ⊢ (¬R ⇒ ¬T) ⇒ [(¬T ⇒ ¬R) ⇒ (¬R ⇒ ¬R)]    Sub (¬R, P) (¬R, R) (¬T, Q) T3
4.) ⊢ (¬T ⇒ ¬R) ⇒ (¬R ⇒ ¬R)                                 MP 2,3
5.) ⊢ (¬R ⇒ ¬T) ⇒ (T ⇒ R)                                       Sub (R, Q) (P, T) T7
6.) ⊢ T ⇒ R                                                                   MP 2,5
7.) ⊢ R                                                                            MP 1,6
∴ ⊢ R