Is the Null Set Axiom necessary in ZF?

Question

Kind of a dumb question but, is the Null Set Axiom necessary in the ZF axiomatization of set theory?

As I understand it, the NSA states: $\exists x \ \forall y \ (y \notin x)$. But is the explicit stating of the existence of such a set truly necessary? Can one not derive its existence from the Axiom (Schema) of Separation and the fact that a model's universe cannot be empty?

Perhaps such a question is —in solely thinking of the ZF axiomatization as a set of sentences to be modelled by (possibly) a certain model— too constrained by the framework of logic and model theory, and the explicit stating of the existence of some set is indeed necessary outside such contexts; but I suppose I would be interested to know if, indeed, within FOL (at the very least), its inclusion is redundant.

That is, given that $\mathrm{Mod}(\lambda_1)$ is the (proper) class of all models (i.e., nonemptiness is a requirement for any model's universe), we can know that $\mathrm{ZF} \vdash \exists x \ (x = x)$ (this also by FOL's Completeness).

Hence, by the SAS ($\forall u_1 \dots u_k \ [\forall w \ \exists v \ \forall r \ (r \in v \leftrightarrow r \in w \land \psi(r, u_1, \dots, u_k))]$), we have, given $\psi \equiv x \neq x$, that $\forall x \ [\forall w \ \exists v \ \forall r \ (r \in v \leftrightarrow r \in w \land x \neq x)] \vdash \exists v \ \forall r \ (r \notin v)$ (this a simple exercise in NK), and thus $\mathrm{ZF} \vdash \exists x \ \forall y \ (y \notin x)$.

I do not know if such a derivation could be carried in a different manner (perhaps via the existence stated in the Axiom of Infinity? Although such seems dependant on a previous characterization of $\emptyset$...), or even if the above stated is actually valid, so any comments clarifying the matter asked above would be much appreciated!

Answer 1

If you are working with a form of first-order logic where $\vdash \exists x (x = x)$, and if you moreover postulate the axiom scheme of separation, then you are correct that the null set axiom is redundant. Alternately, if you postulate the axiom of infinity, you get the empty set more directly.

For a look at the benefits and drawbacks of using first-order logic which assumes $\exists x (x = x)$, see this question. The bottom line is that first-order logic which does not automatically prove $\exists x (x = x)$ is complete for all models (including possibly empty models), while first-order logic which does prove $\exists x (x = x)$ is complete for non-empty models.