How do I get the existence of a set in ZFC following Jech?

Solution 1:

The symbol $\emptyset$ is not part of the formal language of ZFC, so from the strictest viewpoint the subformula "$\emptyset \in S$" is not even syntactically valid in ZFC.

One way to handle that problem is to prove there is a set that has no members, as Brian M. Scott indicates, and then make a definitional expansion of ZFC to add a constant symbol $\emptyset$ for this set.

Another way to handle it, without making a definitional expansion, is to just mentally replace "$\emptyset \in S$" with something like "$(\exists z)[(\forall w)[\lnot (w \in z)] \land z \in S]$". Obviously this makes the axiom much harder to read, so writing $\emptyset \in S$ is a convenient abbreviation.

This same issue comes up in many formal settings: when someone uses a symbol that is not in the formal language, but where you know the intended definition for the symbol, you can simply interpret the formula as an abbreviation for a longer formula that does not use the symbol. For example, the definition in $\{z \in \mathbb{N} : z\text{ is even}\}$ is not a formula of ZFC, but it is an abbreviation for $(\exists w \in \mathbb{N})[z = w + w]$, which in turn is an abbreviation for a much longer formula that does not include the symbols "+" or "$\mathbb{N}$". In most settings the author will not comment much on this sort of thing unless it is unclear that there is a definition in the language of set theory or unless it matters which specific definition is used.

Solution 2:

You can replace $\emptyset$ with $\{ x\in S: x\neq x\}$ in the axiom of infinity, because of the separation axiom. This way, the axiom of infinity implies the existence of all sets all by itself.

Solution 3:

The usual formalizations of first-order logic implicitly assume a non-empty domain of discourse. Knowing that, one can argue informally as follows: let $D$ be any set, and let $E=\{x\in D:x\ne x\}$. The existence of $E$ follows from comprehension, and it’s not hard to prove that $\forall x(x\notin E)$.