= Solution
\b[The displayed derivation is invalid, although its final conjecture is valid.] Its existential-elimination step exports $T(x_0)$ with the local witness name still free, violating the <eigenvariable condition>. Introducing an existential quantifier afterwards does not repair that earlier invalid rule application.
Move the <existential quantifier introduction rule> inside the witness scope:
|| Line
|| Formula
|| Justification
| 1
| $\forall x\,(S(x)\to T(x))$
| Premise
| 2
| $\exists x\,S(x)$
| Premise
| 3
| $S(u)$
| Assume with fresh $u$
| 4
| $S(u)\to T(u)$
| <Universal quantifier elimination rule>, 1
| 5
| $T(u)$
| <Implication elimination rule>, 3 and 4
| 6
| $\exists x\,T(x)$
| <Existential quantifier introduction rule>, 5
| 7
| $\exists x\,T(x)$
| <Existential quantifier elimination rule>, 2 and 3–6
The exported formula contains no free $u$, and neither original premise contains that name. The witness assumption is now discharged legally.
Back to article page
