= Solution
In a finite domain $\{d_1,\ldots,d_n\}$, a true existential premise says that at least one $d_j$ satisfies $\phi$. The <subproof> treats its witness as an unknown object named $v$, derives $\kappa$ without relying on which object was chosen, and can therefore be applied to the actual witness. Thus $\kappa$ follows whenever the existential premise is true. This argument does not require knowing the domain's size or selecting a particular named element in advance.
The <existential quantifier elimination rule> in sequent form records the same <assumption discharge>: a derivation of $\Gamma,\phi(v)\vdash\kappa$ yields $\Gamma,\exists x\,\phi(x)\vdash\kappa$. The natural-deduction box represents the temporary witness assumption that the sequent rule replaces by the existential premise.
The <eigenvariable condition> requires that $v$ have no free occurrence in the other undischarged assumptions, the existential premise or the exported conclusion $\kappa$. Bound occurrences can be renamed harmlessly. This freshness condition keeps $v$ from denoting a previously special object and prevents <witness escape>. Without it, one could export $S(v)$ from $\exists x\,S(x)$, falsely asserting that an arbitrarily named object has the witness property. A two-element domain with only one element satisfying $S$ supplies an immediate counterexample.
Back to article page
