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

Propositional Calculus Proofs (2)

Th3) ⊢ P ⇒ P

1.) ⊢ P ⇒ [ (P ⇒ P) ⇒ P ]                                                                        Lk1

2.) ⊢ [ P ⇒ (P ⇒ P) ] ⇒ (P ⇒ P)                                                             Th2
3.) ⊢  P ⇒ (P ⇒ P)                                                                                    Lk1
4.) ⊢ P ⇒ P                                                                                                MP 2,3

Propositional Calculus Proofs (1)

A proof of a theorem R is a finite sequence of logical formulae P, Q, ... , ∴R, in which each formula is either a substitution in an axiom or in a previously proven formula, or results from the rule MP.

For all logical formulae P, Q,... , R, the notation ⊢ R means that there exists a proof of R (in other words R is a theorem),  P ⊢ R means that with P added to the axioms there exists a proof of R, and P, Q.... ⊢ R or P1, P2, P3, P, Q.... ⊢ R means that with P, Q.... and the axioms, there exists a proof of R. The formula R is then derivable from P, Q,..., iff P, Q.... ⊢R.


Derived Rules (ie proof using a hypothesis)
Th1) T ⊢ ( S ⇒ T )
1.) ⊢ T                                Hyp
2.)  T ⇒ (S ⇒ T)               Lk1
3.) ⊢ S ⇒ T                       MP 1,2

Th2) [H ⇒ (K ⇒ L)] ⊢ [(H ⇒ K) ⇒ (H ⇒ L)]

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

2.)  [H ⇒ (K ⇒ L)] ⇒ [(H ⇒K) ⇒ (H ⇒ L)]                  Lk2

3.) ⊢ (H ⇒ K) ⇒ (H ⇒ L)                                                 MP 1,2