Quantifier order (source code)

= Quantifier order

In general, exchanging a universal and an existential quantifier changes a formula's meaning. A <uniform witness> satisfies a condition for every input, while a <pointwise witness> may vary with the input. For the equality relation on a two-element set, $\forall x\exists y\,(x=y)$ holds but $\exists y\forall x\,(x=y)$ fails.