= Solution
On a finite domain $\{d_1,\ldots,d_m\}$, $\exists x\,\phi(x)$ says that at least one of $\phi(d_1),\ldots,\phi(d_m)$ holds. A derivation from a fresh generic witness shows how to obtain the same conclusion $\kappa$ whichever witness works, just as <disjunction elimination> handles all cases. If empty domains were allowed, the existential premise would be false there; ordinary first-order semantics normally assumes a nonempty domain.
Writing the other open assumptions as $\Gamma$, the <existential elimination> rule in sequent form is
$$
\frac{\Gamma,\phi(v)\vdash\kappa}{\Gamma,\exists x\,\phi(x)\vdash\kappa}.
$$
Combining this with a derivation of the existential premise gives the displayed natural-deduction version. The <eigenvariable condition> requires $v$ to occur free in neither $\Gamma$ nor $\kappa$, with capture-free substitution in $\phi(v)$. It is a temporary name for an unspecified witness, not information about a chosen object. Without freshness, the invalid inference $\exists x\,P(x)\vdash P(v)$ would identify an arbitrary named object with that witness. The <witness escape> restriction prevents this error.
Back to article page
