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

A variable $v$ is fresh for the relevant context when it occurs free in none of its undischarged assumptions. For the existential quantifier elimination rule, it must also not occur free in the final conclusion $\kappa$ or the existential premise: it is a new eigenvariable, allowed in the temporary witness assumption $\varphi (v)$ and formulas inside that witness subproof. Bound variable names can always be renamed to avoid collisions.

The premise $\exists x\varphi (x)$ guarantees some witness, without saying which object it is. Temporarily call one such witness $v$ and assume $\varphi (v)$. If the subproof yields $\kappa$ without depending on any special identity or extra property of $v$, its conclusion holds whichever witness exists. The existential quantifier elimination rule therefore discharges $\varphi (v)$ and retains only the original existential premise and other open assumptions.This eigenvariable condition prevents inferring $\varphi (v)$ for a previously chosen object merely from existence. In particular, $\exists xQ(x)$ does not license $Q(v)$ outside the discharged witness subproof.