Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 8 / a / Solution

In a finite domain, an existential quantifier says that at least one candidate satisfies $\varphi$. Reason with a fresh name $v$ for such an unspecified witness. If the same conclusion $\kappa$ follows using only $\varphi (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 ,\varphi (v)⊢\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.