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

On a finite domain $\{d_1,\dots ,d_m\}$, $\exists x\varphi (x)$ says that at least one of $\varphi (d_1),\dots ,\varphi (d_m)$ holds. A derivation from a fresh generic witness shows how to obtain the same conclusion $\kappa$ whichever witness works, just as disjunction elimination handles all cases. If empty domains were allowed, the existential premise would be false there; ordinary first-order semantics normally assumes a nonempty domain.

Writing the other open assumptions as $\Gamma$, the existential elimination rule in sequent form isCombining this with a derivation of the existential premise gives the displayed natural-deduction version. The eigenvariable condition requires $v$ to occur free in neither $\Gamma$ nor $\kappa$, with capture-free substitution in $\varphi (v)$. It is a temporary name for an unspecified witness, not information about a chosen object. Without freshness, the invalid inference $\exists xP(x)⊢P(v)$ would identify an arbitrary named object with that witness. The witness escape restriction prevents this error.