= Solution
\b[The displayed proof is invalid:] its existential-elimination step exports $Q(x_0)$ while $x_0$ is still free in that conclusion. This is <witness escape>. Existential introduction afterwards cannot repair the invalid intermediate step.
Instead introduce the existential while the witness assumption is still open:
$$
\begin{array}{rll}
1&\forall x\,(P(x)\to Q(x))&\text{premise}\\
2&\exists x\,P(x)&\text{premise}\\
3&\quad P(a)&\text{fresh witness assumption}\\
4&\quad P(a)\to Q(a)&\forall E\ 1\\
5&\quad Q(a)&\to E\ 4,3\\
6&\quad\exists x\,Q(x)&\exists I\ 5\\
7&\exists x\,Q(x)&\exists E\ 2,3\text{--}6
\end{array}
$$
The <existential quantifier introduction rule> at line 6 removes the free witness from the exported statement, so the final <existential elimination> satisfies its <eigenvariable condition>.
Back to article page
