= Solution
For this calculus the <deduction theorem for propositional logic> is
$$
\boxed{\Gamma\cup\{\alpha\}\vdash\beta
\quad\Longleftrightarrow\quad\Gamma\vdash\alpha\to\beta.}
$$
For 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> supplies
$$
\Gamma\vdash\alpha\to\eta,\qquad
\Gamma\vdash\alpha\to(\eta\to\delta).
$$
Part (iii) supplies $\Gamma\vdash\alpha\to\delta$.
If $\delta$ comes by the elimination rule E from $\eta\to\delta$ and $\neg\eta\to\delta$, the <induction hypothesis> supplies
$$
\Gamma\vdash\alpha\to(\eta\to\delta),\qquad
\Gamma\vdash\alpha\to(\neg\eta\to\delta).
$$
The 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$.
Back to article page
