| Description: The Null Set Axiom of ZF
set theory: there exists a set with no
elements. Axiom of Empty Set of [Enderton] p. 18. In some textbooks,
this is presented as a separate axiom; here we show it can be derived
from Separation ax-sep 3438. This version of the Null Set Axiom tells us
that at least one empty set exists, but does not tells us that it is
unique - we need the Axiom of Extensionality to do that (see
zfnuleu 3442).
This proof, suggested by Jeff Hoffman (3-Feb-2008), does not require the
set existence axiom ax-9 1307, unlike some empty set existence proofs
(such as the remark in [Kunen] p. 11).
However, it uses ax-4 1319, which
also presupposes the existence of at least one set, i.e it does not hold
in a "free logic" valid in empty domains. Theorem ax4 1318,
which shows
the redundancy of ax-4 1319, depends on ax-9 1307
for its proof. See
axnulALT 3443 for a similar proof directly from ax-rep 3428.
This theorem should not be referenced by any proof (except snex 3492
below). Instead, use ax-nul 3445 below so that the uses of the Null
Set
Axiom can be more easily identified. |