Solution

ID: past-exam-of-the-logic-and-set-theory-course-of-the-university-of-oxford/2007/a/2/iv/solution

For this calculus the deduction theorem for propositional logic is
For the reverse logical implication, retain the logical derivation from , add the assumption , and use modus ponens rule.
For the forward logical implication, induct on a logical derivation from . For each line we construct a logical derivation of from . If , use (ii). If is an axiom instance or belongs to , it is already derivable from ; L1 gives , and modus ponens rule finishes that case.
If comes from and by modus ponens rule, the induction hypothesis supplies
Part (iii) supplies .
If comes by the elimination rule E from and , the induction hypothesis supplies
The L2 instance with combines these by two applications of modus ponens rule. Thus the rule E also survives the discharge construction. These are all possible lines, proving the theorem for the final line .

New to topics? Read the docs here!