CIC Proofs (4)

Th11) ⊢ (Q ⇒ R) ⇒ [(P ⇒ Q) ⇒ (P ⇒ R)]
2.) ⊢ (Q ⇒ R) ⇒ {[P ⇒ (Q ⇒ R)] ⇒ [(P ⇒ Q) ⇒ (P ⇒ R)]}                           Th1
3.) ⊢ {(Q ⇒ R) ⇒ [P ⇒ (Q ⇒ R)]} ⇒ {(Q ⇒ R) ⇒ [(P ⇒ Q) ⇒ (P ⇒ R)]}     Th2
4.) ⊢ (Q ⇒ R) ⇒ ( P ⇒ (Q ⇒ R))                                                                        Lk1
5.) ⊢ (Q ⇒ R) ⇒ [( P ⇒ Q ) ⇒ ( P ⇒ R )]                                                         MP 3,4

CIC Proofs (3)

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

1.) ⊢ P ⇒ Q                        Hyp

2.) ⊢ Q ⇒ R                       Hyp

3.) ⊢ P ⇒ R                       Th5

4.) ⊢ R ⇒ S                        Hyp

5.) ⊢ P ⇒ S                         Th5 

Th9) H ⇒ (K ⇒ L), H ⇒ [K ⇒ (L ⇒ M)] ⊢ H ⇒ (K ⇒ M)

1.) ⊢ H ⇒ [K ⇒ (L ⇒ M)]                                                   Hyp

2.) ⊢ [K ⇒ ( L ⇒ M )] ⇒ [( K ⇒ L ) ⇒ ( K ⇒ M )]           Lk2

3.) ⊢ H ⇒ [( K ⇒ L ) ⇒ ( K ⇒ M )]                                   Th5

4.) ⊢ [H ⇒ ( K ⇒ L )] ⇒ [H ⇒ ( K ⇒ M )]                       Th2

5.) ⊢ H ⇒ (K ⇒ L)                                                               Hyp

6.) ⊢ H ⇒ ( K ⇒ M )                                                          MP 4,5

Th10) ⊢ [P ⇒ (P ⇒ Q)] ⇒ (P ⇒ Q)
1.) ⊢ P ⇒ P                                                               Th3
2.) ⊢ [P ⇒ (P ⇒ Q)] ⇒ P ⇒ P                                Th1
3.) ⊢ [P ⇒ (P ⇒ Q)] ⇒ [(P ⇒ P) ⇒ (P ⇒ Q)]       Lk2
4.) ⊢ [P ⇒ (P ⇒ Q)] ⇒ (P ⇒ Q)                            Th4

CIC Proofs (2)

Th6) K, H ⇒ ( K ⇒ L ) ⊢ H ⇒ L
1.) ⊢ [H ⇒ ( K ⇒ L )] ⇒ [( H ⇒ K ) ⇒ ( H ⇒ L )]      Lk2
2.) ⊢ H ⇒ ( K ⇒ L )                                                        Hyp
3.) ⊢ ( H ⇒ K ) ⇒ ( H ⇒ L )                                          MP 1,2
4.) ⊢ K                                                                              Hyp
5.) ⊢ H ⇒ K                                                                     Th1
6.) ⊢ H ⇒ L                                                                     MP 3,5

Th7) P ⇒ Q, P ⇒ ( Q ⇒ R ), P ⇒ ( R ⇒ S ) ⊢ P ⇒ S
1.) ⊢ P ⇒ Q                                         Hyp
2.) ⊢ P ⇒ ( Q ⇒ R )                           Hyp
3.) ⊢ P ⇒ R                                         Th4
4.) ⊢ P ⇒ ( R ⇒ S )                            Hyp
5.) ⊢ P ⇒ S                                          Th4

CIC Proofs (1)

Th4) H ⇒ K , H ⇒ (K ⇒ L) ⊢ H ⇒ L.
1.) ⊢ H ⇒ K                                                                       Hyp
2.) ⊢ H ⇒ (K ⇒ L)                                                           Hyp
3.) ⊢ [H ⇒ ( K ⇒ L )] ⇒ [( H ⇒ K ) ⇒ ( H ⇒ L )]      Lk2
4.) ⊢ ( H ⇒ K ) ⇒ ( H ⇒ L )                                           MP 2,3
5.) ⊢ H ⇒ L                                                                       MP 1,4

Th5) H ⇒ K, K ⇒ L ⊢ H ⇒ L

1.) ⊢ H ⇒ K                                       Hyp

2.) ⊢ K ⇒ L                                       Hyp

3.) ⊢ H ⇒ (K ⇒ L)                                Th1

4.) ⊢ (H ⇒ K) ⇒ (H ⇒ L)               Th2

5.) ⊢ H ⇒ L                                      MP 1,4

Thought Mechanics (4)

formuture - a thought that redistributes a future from it's original trajectory.

I derived this term from the words 'future' and 'form'. This term can be used as a verb. 

Time To Think

Classical Implicational Calculus (CIC)

Lk1, Lk2, Sub, and MP form the basis for CIC. Notice Lk3 uses ¬ but Lk1 and Lk2 do not use ¬. Since, CIC does not use Lk3, its theorems are variations on the transitivity of ⇒. 

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