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