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

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.

The displayed derivation is invalid, although its final conjecture is valid. Its existential-elimination step exports $T(x_0)$ with the local witness name still free, violating the eigenvariable condition. Introducing an existential quantifier afterwards does not repair that earlier invalid rule application.

Move the existential quantifier introduction rule inside the witness scope:

The exported formula contains no free $u$, and neither original premise contains that name. The witness assumption is now discharged legally.

For readability write $R(s,t)$ for the uninterpreted relation $s\ni t$. In the first proof, introduce the universal quantifier inside the existential witness scope:

In the second proof, first close the witness scope and then generalize the arbitrary object:

These are distinct proof trees: the final two rule applications are interchanged, and their freshness conditions have been checked in their respective contexts. They express the quantifier order and uniform witness principle: a single witness working for every object also supplies a witness for each object individually.

The converse is not valid. In a domain $\{0,1\}$ interpret $R(s,t)$ as equality of its arguments. Every object has a witness, namely itself, but no one object equals both 0 and 1. The premise of the converse is true and its conclusion false. The symbol $\ni$ is an arbitrary binary relation here; no set-membership axioms may be imposed on it without an additional premise.

Let $K$ abbreviate $Q(c_1)\vee Q(c_2)$, and group the three equality alternatives on the left. The proof uses the binary disjunction elimination rule twice, so no unproved three-way derived rule is needed.

The witness name is absent from $K$ and from every assumption remaining after line 19, so the existential elimination is legal. Each equality is used in the forward direction supplied by the printed equality rule. The three named constants need not denote distinct objects: the case proof requires only that they exhaust the domain. This is existential quantification over a finitely named domain followed by exclusion of the first case.