Does contraction of quantifiers require axiom of empty set?

80 Views Asked by At

We can contract multiple unbounded quantifiers to one unbounded quantifier via the notion of ordered pair(or sequence). I am reading Devlin's book Constructibility, and he claims that a theory $T$ of the language of set theory which includes axiom of empty set and axiom of pairing can contract the quantifiers. Do we really need axiom of empty set here? Let's consider the case where we want to contract the unbounded existential quantifiers of $\Sigma_1$ formula to a single unbounded existential quantifier followed by a $\Sigma_0$ formula. For example we want to contract $\exists x \exists y \phi(x, y)$ where $\phi(x, y)$ is $\Sigma_0$. Then let's consider this formula $(\exists z)[z \text{ is an ordered pair} \land \phi((z)_1, (z)_2)]$. This is a $\Sigma_1$ formula and I think just axiom of pairing suffices to get $$T \vdash \exists x \exists y \phi(x, y) \leftrightarrow (\exists z)[z \text{ is an ordered pair} \land \phi((z)_1, (z)_2)]$$ Where could be axiom of empty set used?