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

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.

The two proofs differ in whether existential elimination is outside or inside negation introduction. For the first proof, choose fresh $a$, derive the negation inside the witness subproof, and then discharge the witness:The conclusion at line 6 contains no free $a$. For the second proof, open the universal assumption first, eliminate the existential to derive falsity, and then discharge the universal assumption:At line 6 of the second proof, neither the exported conclusion $\perp$ nor the other open assumptions contains $a$ free, satisfying the eigenvariable condition. Neither proof needs RAA or double-negation elimination.

The displayed proof is invalid: its existential-elimination step exports $Q(x_0)$ while $x_0$ is still free in that conclusion. This is witness escape. Existential introduction afterwards cannot repair the invalid intermediate step.

Instead introduce the existential while the witness assumption is still open:The existential quantifier introduction rule at line 6 removes the free witness from the exported statement, so the final existential elimination satisfies its eigenvariable condition.

Write $H=\exists y\forall xR(x,y)$. For the first proof, eliminate the common witness before introducing the universal quantifier. Choose fresh $b$ and a further fresh arbitrary $a$:At line 5, $a$ occurs free in neither $H$ nor the witness assumption, so universal introduction is valid. At line 6, $b$ is absent from the conclusion and other open assumptions.

For the second proof, reserve arbitrary $a$, eliminate the common witness only as far as the particular existential, close that subproof, and then generalize:At line 5 the exported formula contains no free $b$; at line 6 the only open assumption $H$ contains no free $a$. These different orders of assumption discharge both respect the eigenvariable condition.

The converse is not valid. On the domain $\{0,1\}$, interpret $R(x,y)$ as $x=y$. Each $x$ has a witness $y=x$, so $\forall x\exists yR(x,y)$ holds, but no single $y$ equals both elements. Thus $\exists y\forall xR(x,y)$ is false. This is precisely the distinction in quantifier order and uniform witness.