= Solution
In a finite domain, an <existential quantifier> says that at least one candidate satisfies $\phi$. Reason with a fresh name $v$ for such an unspecified witness. If the same conclusion $\kappa$ follows using only $\phi(v)$ and the original premises, without depending on which candidate $v$ names, then $\kappa$ follows from the existential premise itself.
This is exactly <existential elimination> in boxed form: the sequent $\Gamma,\phi(v)\vdash\kappa$ is the branch inside the box. The <eigenvariable> $v$ must not occur free in the original undischarged context or in the exported conclusion $\kappa$. Otherwise the proof could smuggle in information about a specially chosen individual or export a fact about a witness whose name has just left scope. Freshness does not mean that the domain contains an additional object; it means that its temporary name carries no other assumptions.
Back to article page
