= Solution
\b[The proposed proof is invalid:] its existential-elimination step exports $Q(x_0)$ while the witness name $x_0$ still occurs free in that conclusion. Introducing an existential quantifier later does not retrospectively repair that scope error.
Introduce the existential quantifier before discharging the witness box:
``
1 ∀x (P(x) → Q(x)) premise
2 ∃x P(x) premise
3 | P(a) assumption, a fresh
4 | P(a) → Q(a) ∀-elim 1
5 | Q(a) →-elim 4,3
6 | ∃x Q(x) ∃-intro 5
7 ∃x Q(x) ∃-elim 2,3–6
``
The conclusion of <existential elimination> now has no free occurrence of $a$, and the name occurs in neither original premise, satisfying the <eigenvariable> condition.
Back to article page
