What would be an example of a tautology in first-order logic involving a definite sequence of quantifiers?

Question

This question might be silly, but while teaching a tutorial as a TA, I suddenly had the need to bring up a tautological statement in first order logic that involved the quantifiers $\forall\exists\forall\exists$ in this order. That is, a tautology of the form $\forall x\exists y\forall z\exists w $ $\phi(x,y,z,w)$ for some first order formula $\phi$. This came up while I was trying to convey to the class the essence of skolemization in this case. However, for some reason, I just couldn't come up quickly with such an example. Any help is appreciated.

Answer 1

There's always $(y=x)\land (w=z)$ of course. But this has the disadvantage that $w$ doesn't need to depend on $x$, though. The best I can think of where this is not the case would be something like

$$(y\ne x \lor z=x) \land (z=x \to w=y) \land (z\ne x \to w=x)$$ In a structure with three elements, $w$ will have to depend on both $x$ and $z$.

Answer 2

Try a stronger version of the infinitude of primes!

Given any natural $m$, there is a least prime bigger than $m$.

Which can be stated over first-order arithmetic (with $+,\cdot,<,0,1$) as: $\def\imp{\rightarrow}$

$φ \overset{def}= \forall m\ \exists p\ ( p > m \land prime(p) \land \forall q\ ( q > m \land prime(p) \imp q \ge p ) )$.

where:

$prime(p) \overset{def}\equiv p > 1 \land \forall x,y\ ( x \cdot y = p \imp x = p \lor y = p )$.

It is a good exercise to put $φ$ into Skolem-normal form and then Skolemize it.