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

In a finite domain $\{d_1,\dots ,d_n\}$, a true existential premise says that at least one $d_j$ satisfies $\varphi$. The subproof treats its witness as an unknown object named $v$, derives $\kappa$ without relying on which object was chosen, and can therefore be applied to the actual witness. Thus $\kappa$ follows whenever the existential premise is true. This argument does not require knowing the domain's size or selecting a particular named element in advance.

The existential quantifier elimination rule in sequent form records the same assumption discharge: a derivation of $\Gamma ,\varphi (v)⊢\kappa$ yields $\Gamma ,\exists x\varphi (x)⊢\kappa$. The natural-deduction box represents the temporary witness assumption that the sequent rule replaces by the existential premise.

The eigenvariable condition requires that $v$ have no free occurrence in the other undischarged assumptions, the existential premise or the exported conclusion $\kappa$. Bound occurrences can be renamed harmlessly. This freshness condition keeps $v$ from denoting a previously special object and prevents witness escape. Without it, one could export $S(v)$ from $\exists xS(x)$, falsely asserting that an arbitrarily named object has the witness property. A two-element domain with only one element satisfying $S$ supplies an immediate counterexample.