= Quantifier order and uniform witness
{title2=$\exists y\,\forall x\,R(x,y)\ \Longrightarrow\ \forall x\,\exists y\,R(x,y)$}
A single witness working for every object supplies a witness for each object individually. Eliminate the outer existential with a fresh witness, instantiate the universal at an arbitrary object, and introduce the required existential. Generalization can occur either before or after closing the witness scope, provided the <eigenvariable condition> holds in the corresponding contexts. The converse fails on a two-element domain with $R(x,y)$ interpreted as equality: each object has itself as a witness, but no object works for both.
Back to article page
