= 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 $\phi(v)$ and formulas inside that witness subproof. Bound variable names can always be renamed to avoid collisions.
The premise $\exists x\,\phi(x)$ guarantees some witness, without saying which object it is. Temporarily call one such witness $v$ and assume $\phi(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 $\phi(v)$ and retains only the original existential premise and other open assumptions.
$$
\boxed{\Gamma,\phi(v)\vdash\kappa\quad\Longrightarrow\quad\Gamma,\exists x\,\phi(x)\vdash\kappa,\qquad v\notin\operatorname{FV}(\Gamma,\kappa,\exists x\,\phi(x)).}
$$
This <eigenvariable condition> prevents inferring $\phi(v)$ for a previously chosen object merely from existence. In particular, $\exists x\,Q(x)$ does not license $Q(v)$ outside the discharged witness subproof.
Back to article page
