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

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 $\varphi (v)$ and formulas inside that witness subproof. Bound variable names can always be renamed to avoid collisions.

The premise $\exists x\varphi (x)$ guarantees some witness, without saying which object it is. Temporarily call one such witness $v$ and assume $\varphi (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 $\varphi (v)$ and retains only the original existential premise and other open assumptions.This eigenvariable condition prevents inferring $\varphi (v)$ for a previously chosen object merely from existence. In particular, $\exists xQ(x)$ does not license $Q(v)$ outside the discharged witness subproof.

The existential premise is $\exists x(Q(x)\to R(x))$, with the logical implication inside the existential quantifier. Eliminate it using a fresh witness $a$, specialize $\forall xQ(x)$ to that same witness, and introduce the required existential quantifier before closing the witness subproof:

The eigenvariable $a$ is absent from the premises and from $\exists xR(x)$. Consequently,

Extract the universally quantified logical implication and the existentially quantified logical conjunction from the premise. Use one fresh witness $a$ for both conjuncts of the latter, so that the resulting $R(a)$ and $\neg S(a)$ concern the same object:

The witness $a$ occurs in no undischarged premise or final conclusion. Therefore the existential quantifier elimination rule is valid and gives

Use the equality introduction rule to prove $t_1=t_1$. In the equality elimination rule, choose the first-order formula $\varphi (z)$ to be $z=t_1$. Substituting $t_2$ for $t_1$ in its first position proves symmetry:

Thus $\boxed{t_1=t_2⊢t_2=t_1}$. This uses only the two supplied equality rules; symmetry has not been assumed as an additional rule.

Eliminate the existential premise with fresh witness $a$. Its first conjunct gives $Q(a)$ and its second gives $\forall y(Q(y)\to y=a)$. For a fresh arbitrary $b$, one direction of the desired logical biconditional follows by universal elimination. For the other, $b=a$ must be reversed before transporting $Q(a)$ to $Q(b)$ using the supplied oriented equality elimination rule.

Here $b$ is absent from every open assumption when line 12 uses universal introduction. In line 13 the existential quantifier binds the witness position occupied by $a$; the conclusion then has no free $a$, allowing line 14 to close its witness subproof. HenceThe premise says an object satisfying $Q$ exists and every object satisfying $Q$ equals it. The logical biconditional adds the converse explicitly: every object equal to that witness also satisfies $Q$.