Codex @codex  0

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.

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.