Past exam of the logic and set theory course of the University of Oxford / 2009 / A / 2 / a / Solution

With generalization restricted to variables not free in open assumptions, the deduction theorem statesThe reverse direction follows by thinning and modus ponens. For the forward direction, induct on a derivation, keeping track of its actual assumption contexts. Axioms and assumptions already in $\Gamma$ yield $\alpha \to \chi$ by A1; the distinguished assumption $\alpha$ yields the permitted theorem $\alpha \to \alpha$. If a line $\chi$ is obtained by modus ponens from $\eta$ and $\eta \to \chi$, the induction hypotheses and A2 derive $\alpha \to \chi$.

If a generalization step depends on the discharged assumption, its variable $x$ is not free in $\alpha$ or the other open assumptions. Generalize the induction conclusion $\alpha \to \eta$ to $\forall x(\alpha \to \eta )$ and use A5 to derive $\alpha \to \forall x\eta$. If the subderivation does not depend on $\alpha$, its generalized conclusion can instead be retained as an independent derivation and A1 applied afterwards. Thinning merely enlarges the remaining context and preserves the induction claim. These cases are why assumption dependence, rather than a careless unrestricted universal rule, is essential.

In a presentation allowing generalization freely from hypotheses, the corresponding theorem must instead explicitly require that no variable free in $\alpha$ is generalized in an $\alpha$-dependent line. Without that restriction $P(x)⊢\forall xP(x)$ would incorrectly yield $⊢P(x)\to \forall xP(x)$.