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 / d

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.