Axiom of Empty Set superfluous in ZF?

[honestrosewater]

Only some versions of the ZF axioms include an axiom stating that an empty set exists. According to mathworld, the Axiom of the Empty Set (AES) follows from the Axiom of Infinity (AI) and Axiom of Separation (AS), via \exists x (x = x) and \emptyset = \{y : y \not= y\}. I guess they think the AI states that a set exists? But the AI is defined inductively, and the empty set serves as its only basis. Here's the AI:

\exists x (\emptyset \in x \ \wedge \ \forall y (y \in x \rightarrow \cup \{y, \{y\}\} \in x))

The AI doesn't say the empty set exists. It seems to me to be, well, like a proof by weak induction without a basis. It only says that an infinite set exists provided that an empty set exists. No? I'm confused.

Edit: haha, though I guess without the empty set, the set that AI says exists has no extension, so... ouch, my head.

 

[D H]

I agree. It seems to me that the existence of the empty set \emptyset needs to be predicated before one use the empty set in the axiom of infinity,

\exists x (\emptyset \in x \ \wedge \ \forall y (y \in x \rightarrow \cup \{y, \{y\}\} \in x))

The Wikipedia ZF article does include the empty set as an axiom.

 

[Hurkyl]

Or at the very least, the AI needs to assert the existence of the empty set in its statement. One book I've checked out states that it is using:

\emptyset \in v_0[/itex]<br /> <br /> as an abbreviation for<br /> <br /> \exists v_1 \forall v_2 [ \neg v_2 \in v_1 \wedge v_1 \in v_0 ]<br /> <br /> in its statement of the AI.<br /> <br /> <br /> But, you can conclude the existence of the empty set merely from \exists x: P, for any relation P.

 

[honestrosewater]

Or at the very least, the AI needs to assert the existence of the empty set in its statement. One book I've checked out states that it is using:

\emptyset \in v_0[/itex]<br /> <br /> as an abbreviation for<br /> <br /> \exists v_1 \forall v_2 [ \neg v_2 \in v_1 \wedge v_1 \in v_0 ]<br /> <br /> in its statement of the AI.

Ah, okay then.<br /> <blockquote data-attributes="" data-quote="" data-source="" class="bbCodeBlock bbCodeBlock--expandable bbCodeBlock--quote js-expandWatch"> <div class="bbCodeBlock-content"> <div class="bbCodeBlock-expandContent js-expandContent "> But, you can conclude the existence of the empty set merely from \exists x: P, for any relation P. </div> </div> </blockquote>Yeah, this is what I was thinking. If it&#039;s already assumed that your domain is non-empty (as a logical presupposition, I suppose), the empty set is a subset of every set, so you can just use AS to get it -- but you don&#039;t need the AI.<br /> <br /> OOHH, I think I read their <i>and</i> wrong. They say,<br /> <blockquote data-attributes="" data-quote="" data-source="" class="bbCodeBlock bbCodeBlock--expandable bbCodeBlock--quote js-expandWatch"> <div class="bbCodeBlock-content"> <div class="bbCodeBlock-expandContent js-expandContent "> Itô includes an Axiom of the empty set, which can be gotten from (6) [AI] and (3) [AS], via \exists x(x = x) and \emptyset = \{x : x \not= x\}. </div> </div> </blockquote>I thought they meant (6) and (3) together, but they meant from (6) (by just including AES in AI) or from (3) (with the additional assumption that the domain is non-empty).

 

[Hurkyl]

No, I think you read it right the first time. Given the existence of some set, you use the axiom of subsets to produce the empty set. The axiom of infinity is the only axiom (aside from the axiom of the empty set) that unconditionally asserts the existence of a set.

A proof might look like:

Ex:Px (Axiom of infinity -- for the right P)
Ex:Px and Ey:Az: z in y <--> (z in x and Fz) (Axiom of subsets -- F is the relation that is always false)
Ex:Px and Ey:Az: not z in y
Ex:Ey:Az: not z in y
Ey:Az: not z in y

(I think I've gotten that right -- I don't think I've ever had to formally derive something like this involving quantifiers)


Of course, since the axiom of infinity is usually stated to assert the existence of the empty set directly, you could get it that way. (I wonder if there's a different way to state AI that doesn't do so?)

 

[honestrosewater]

No, I think you read it right the first time. Given the existence of some set, you use the axiom of subsets to produce the empty set.

Right, and I mean that the formal language and logical calculus with which your theory is built might be able to grant you the existence of a set (or whatever kind of object the members of your domain are). If your language L is a first-order language with equality and your calculus is a sound, complete, first-order calculus, \forall x (x = x) is logically true (satisfied by every L-valuation, i.e., holds in every L-structure) and provable (deducible from the empty set, i.e., a theorem of every L-theory). If you require the domain of an L-structure to be non-empty, (\forall x (\phi)) \rightarrow (\exists x (\phi)), so you have \exists x (x = x) before you even start adding any extralogical bits. Yes? Bleh, I need a break; my brain's fried.

The axiom of infinity is the only axiom (aside from the axiom of the empty set) that unconditionally asserts the existence of a set.
...
(I wonder if there's a different way to state AI that doesn't do so?)

AFAIK, there are only three ways to define a set (or class) S:

1) Extension -- name all members of S.
2) Intension -- name a definite property that all members of S have.
3) Induction/Recursion

a) basis clause -- name at least one member of S.
b) induction clause -- give rule(s) to get more members from those in (a) -- if x is in S, then x' is in S.
c) extremal clause -- says that nothing else is in S.​

Extension won't work for infinite sets. As long as the infinite set that the AI claims exists is defined inductively/recursively, you need a set to serve as the basis. Unless a set can serve as its own basis (and I don't think it can, will consider), your 'first' set cannot be defined recursively -- you need to already have another set, whatever it is and however you get it. Maybe you can define AI's infinite set by intension.

 

[Hurkyl]

The axiom of infinity doesn't define a set, by that criterion! (No extremal clause)

Ah, I remember now: you can write an axiom that asserts the existence of a set S, and a function f:S-->S where f is injective, but not surjective.

But I think this is useless from a practical point of view. (I don't think you can construct a model of the natural numbers)

There is a nice logical condition defining ordinals... ah, here it is:

Ord x <--> x is transitive and well-ordered. (WRT membership)

I think I can use these as a basis for an empty-set-free axiom of infinity!

AI': There exists a set S such that:
(1) There exists a function f:S-->S that is injective and not surjective
(2) S is transitive (WRT membership)
(3) S is well-ordered (WRT membership)

I don't think I've assumed the existence of the empty set, and I think this axiom should suffice to construct the naturals.

 

[honestrosewater]

The axiom of infinity doesn't define a set, by that criterion! (No extremal clause)

I'm sure your mother is very proud of you. Yeah, the extremal clause usually goes without saying. I was just trying to be thorough.

So I did a quick search for confirmation and the first book that I checked, Set Theory by Kenneth Kunen, which doesn't include the AES, includes \exists x (x = x) as Axiom 0, noting

This axiom says that our universe [a.k.a. domain] is non-void. Under most developments of formal logic, this is derivable from the logical axioms and thus redundant to state here, but we do so for emphasis.

Ah, I remember now: you can write an axiom that asserts the existence of a set S, and a function f:S-->S where f is injective, but not surjective.

But I think this is useless from a practical point of view. (I don't think you can construct a model of the natural numbers)

There is a nice logical condition defining ordinals... ah, here it is:

Ord x <--> x is transitive and well-ordered. (WRT membership)

I think I can use these as a basis for an empty-set-free axiom of infinity!

AI': There exists a set S such that:
(1) There exists a function f:S-->S that is injective and not surjective
(2) S is transitive (WRT membership)
(3) S is well-ordered (WRT membership)

I don't think I've assumed the existence of the empty set, and I think this axiom should suffice to construct the naturals.

I don't know about ordinals yet (I skip around a lot), but in order for f to not be surjective, there must exist some x in S that isn't in the range of f, yes? That is, it seems that you still need to posit another set before you can get this infinite one. (That's all that I meant, BTW -- that you might need some set, not necessarily the empty set.)

 

[Hurkyl]

I'm just happy I could state the AI without assuming the empty set.