Most presentations of ZF seem to be incomplete
A minor technical issue with ZF (and other set theories such as Morse-Kelley) is that if one isn't careful, the axioms will admit degenerate model, in which there are no sets at all. The axiom of pairing is typical here:
If $x$ and $y$ are sets, then $\{x, y\}$ is also a set
If there aren't any sets, then the axiom is vacuous.
Some presentations get around this with an explicit axiom of the empty set:
$$\exists x.\forall y. y\notin x$$
From this, we know there's at least one empty set; from extensionality we can can prove that it's unique, and this justifies assigning a symbol $\varnothing$ to it. (Kelley's original presentation of MK has instead an axiom “there exists a set”, and this, plus specification, is enough to prove the existence of the empty set.) Then pairing and union and specification get us a universe of other sets. Fine.
But many presentations omit the axiom of the empty set. Instead, they claim, the axiom of infinity asserts the existence of a set $\omega$, and with specification we can get $\varnothing$ as a subset of $\omega$.
But it seems to me that this approach doesn't actually work. The axiom of infinity states: $$\exists S. (\varnothing\in S) \land (\forall y\in S. y\cup\{y\}\in S)$$
If we're using the axiom of infinity to prove the existence of the empty set, then at this point the symbol $\varnothing$ doesn't refer to anything, and is meaningless, and we have no business using it in the axiom.
The symbol “$\varnothing$” also appears in the axiom of regularity, but there it isn't so problematic, because it only appears in the context “$x=\varnothing$”. By this we actually mean “$\lnot\exists y. y\in x$”, so the issue is merely sloppy notation. But for the axiom of infinity the problem is deeper and it seems to me it can't be fixed notationally, because the axiom of infinity demands that “$\varnothing$” denote an actual object.
Both the Wikipedia presentation of ZF (which claims to follow Kunen) and the Mathworld presentation (claims to follow Jech) have this defect.
I'm not trying to suggest that set theory itself is flawed; the issue is a minor technical one and is easily resolved by including an axiom of the empty set or even an axiom that asserts the existence of some set. My question is whether the typical presentation of set theory is defective. Or perhaps there is no defect and my understanding is deficient?
Solution 1:
If you remember correctly, the symbol $\varnothing$ does not appear in the language of set theory. It is syntactic sugar. In reality it masks the following:
$$\exists z(\forall w(w\notin z))$$
In particular, it posits the existence of a set which is empty. The same goes for $\cup$ and $\{y\}$ that you've used in the statement of the axiom of infinity.
But, and here's the thing, at the end of the day, mathematics, including set theory, is done by humans for other humans. So we need this syntactic sugar, otherwise everything becomes overly formal and annoying, which makes it also somewhat inaccessible for newcomers.
Solution 2:
You're missing a bit of context: in which logic you're establishing your ZF presentation? It is usually done in first order logic, where you can prove the logical theorem $\exists x(x=x)$, therefore, "there exists a set" which you can use for further constructions. For example, in Hilbert's calculus, the formula is just a shortcut for $\lnot\forall x(x\ne x)$, and it is easy to prove (by contradiction) using universal instantiation.
Of course, there are logics (such as inclusive logic) which do allow for empty domains of discourse, but those are usually more complicated (i.e. have more special cases) and surely not "default" for presentation of ZF. In such logics, "there exists a set" must be taken as a non-logical axiom, since it doesn't follow logically. But if you do that, the question arises, why not simply use first-order logic, if you're postulating away the only option this more complicated logic gives you? :-)
Solution 3:
This is similar to Asaf Karagila’s answer:
Let’s start more generally: Whenever we have some formula $\phi$ with free variable $x$ in some language and we can prove $\exists! x. \phi$ in some theory, we can extend the language by a new constant symbol $c$ (representing the unique $x$ making $\phi$ valid) and add the axiom $\forall x. (x = c \leftrightarrow \phi)$ to get a (basically) equivalent theory that allows us to talk about $c$.
To demonstrate this equivalence, we need to provide a way to transform formulas in the extended language (i.e. containing $c$) into formulas without $c$ such that the new theory proves a sentence with $c$ if and only if the original theory proves the transformed sentence without $c$.
We do this by induction over the structure of formulas. I won’t do everything here, but for a relation symbol $R$, we replace $R(c, t_1, \dots, t_n)$ (with terms $t_1, \dots, t_n$ not containing $c$, say) by $\forall x. (\phi \rightarrow R(x, t_1, \dots, t_n))$. You can do very similar things if $c$ is hidden deeper inside a term or appears in multiple positions.
Note that you can perform the transformation from the last paragraph even when you don’t have a proof of $\exists!x. \phi$ (yet). This is what happens in the presentation of the axiom of infinity. You perform this transformation with $\phi := \forall y. \neg(y \in x)$ and $c := \varnothing$. Your axiom becomes $$ \exists S. (\forall x. ((\forall y. \neg(y \in x)) \rightarrow x \in S)) \wedge (\forall y \in S. y \cup \{ y \} \in S) $$ (where technically, you would need to perform a very similar process for $\{ y \}$ and $\cup$ as well). This is now a perfectly fine axiom (not using $\varnothing$) that still ensures the existence of a set (an infinite set even). From this, you can prove the existence of the empty set (i.e. the necessary sentence $\exists! x. \phi$), justifying the introduction of the symbol a posteriori.
Of course, the introduction of the notation is somewhat circular if done this way, but from a purely logical point of view, nothing circular is going on.