= Solution
For readability write $R(s,t)$ for the uninterpreted relation $s\ni t$. In the first <proof>, introduce the universal quantifier \i[inside] the existential witness scope:
|| Line
|| Formula
|| Justification
| 1
| $\exists y\,\forall x\,R(x,y)$
| Premise
| 2
| $\forall x\,R(x,w)$
| Assume with fresh witness name $w$
| 3
| $R(u,w)$
| <Universal quantifier elimination rule>, 2; choose fresh arbitrary $u$
| 4
| $\exists y\,R(u,y)$
| <Existential quantifier introduction rule>, 3
| 5
| $\forall x\,\exists y\,R(x,y)$
| <Universal quantifier introduction rule>, 4; $u$ is absent from open assumptions
| 6
| $\forall x\,\exists y\,R(x,y)$
| <Existential quantifier elimination rule>, 1 and 2–5
In the second <proof>, first close the witness scope and \i[then] generalize the arbitrary object:
|| Line
|| Formula
|| Justification
| 1
| $\exists y\,\forall x\,R(x,y)$
| Premise; choose $u$ arbitrary and fresh for this premise
| 2
| $\forall x\,R(x,w)$
| Assume with fresh $w$, also different from $u$
| 3
| $R(u,w)$
| <Universal quantifier elimination rule>, 2
| 4
| $\exists y\,R(u,y)$
| <Existential quantifier introduction rule>, 3
| 5
| $\exists y\,R(u,y)$
| <Existential quantifier elimination rule>, 1 and 2–4
| 6
| $\forall x\,\exists y\,R(x,y)$
| <Universal quantifier introduction rule>, 5
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.
\b[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.
Back to article page
