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 isFor the reverse logical implication, retain the logical derivation from $\Gamma$, add the assumption $\alpha$, and use modus ponens rule.

For the forward logical implication, induct on a logical derivation from $\Gamma \cup \{\alpha \}$. For each line $\delta$ we construct a logical derivation of $\alpha \to \delta$ from $\Gamma$. If $\delta =\alpha$, use (ii). If $\delta$ is an axiom instance or belongs to $\Gamma$, it is already derivable from $\Gamma$; L1 gives $\delta \to (\alpha \to \delta )$, and modus ponens rule finishes that case.

If $\delta$ comes from $\eta$ and $\eta \to \delta$ by modus ponens rule, the induction hypothesis suppliesPart (iii) supplies $\Gamma ⊢\alpha \to \delta$.

If $\delta$ comes by the elimination rule E from $\eta \to \delta$ and $\neg \eta \to \delta$, the induction hypothesis suppliesThe L2 instance with $(\alpha ,\beta ,\gamma )=(\alpha ,\eta ,\delta )$ 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 $\beta$.