Set Theory Jottings 16. Axioms of ZFC

Prev TOC Next

The Axioms of ZFC

The language of ZF (ℒ(ZF)) consists of basic first-order syntax, with a single binary predicate symbol ∈. Here is a list of the axioms, with a tag-line (an imprecise description) for each.

Extensionality:

Every set is determined by its elements.

Foundation:

All sets are built up in levels by starting with the empty set.

Pairs:

There is a set whose elements are any two given sets. (Or any one set.)

Union:

For every set, there is a set consisting of the union of its elements.

Power Set:

For every set, there is a set consisting of all its subsets.

Infinity:

There is an infinite set.

Replacement:

Given a set and a rule for replacing its elements, there is a set consisting of all these replacements.

Choice:

Given a set of pairwise disjoint nonempty sets, there is a set containing exactly one element from each of them.

Two more axioms:

Null Set:

There is a set with no elements.

Separation:

Given a set and a property, there is a set consisting of all the elements satisfying the property.

These are redundant. The version of Replacement we adopt implies Separation; Null Set follows from Pairs plus Separation. But they are historically important, and help understand ZFC.

Now for the formal, or at least more formal, statements. (I discussed “vernacular” in post 15. Recall that t̄ stands for stands for a list (t₁,…,t_n).)

Extensionality:

∀z(z∈x↔z∈y)→x=y

Using the defined symbol ⊆ (defined as ∀z(z∈x→z∈y)), we could also write this as “x⊆y∧y⊆x→x=y’’.

Foundation:

∀x(∃y∈x)(y∩x=∅)

Of course, ∩ and ∅ are defined terms, and (∃y∈x) is vernacular. Here is Foundation without using them:

∀x∃y(y∈x∧∀u(¬(u∈x∧u∈y)))

People sometimes call this Regularity. Foundation says there is an ∈-minimal element of x, that is, a y∈x none of whose elements belong to x. If that were false, we’d have an infinite descending chain x∋y₁∋y₂∋…. (Possibly it could end in a loop, i.e., y_m=y_n for some m<n.) But such an x is not “built up from ∅’’.

Foundation has an equivalent statement: There are no infinite descending ∈-chains. To prove this equivalence, you need Choice. The version above (due to von Neumann) avoids this issue, and is simpler to express.

Pairs:

∀x ∀y ∃z(z={x,y})

or without the defined term {x,y}:

∀x ∀y ∃z∀u(u∈z ↔(u=x∨u=y))

Since x=y is not excluded, this also covers singletons.

Null Set:

∃x∀y(¬y∈x)

Union:

∀x ∃u(u=⋃_y∈xy)

or without the defined term ⋃

∀x ∃u ∀z(z∈u ↔∃y(z∈y∧y∈x))

In other words, the elements of the union are the elements of the elements of the original set.

Power Set:

∀x∃p∀s(s∈p↔s⊆x)

Or in other words, p={s : s⊆x}, just the kind of set-builder definition that was uncritically accepted before the paradoxes. The power set of x is denoted 𝒫(x). Without the defined term s⊆x:

∀x∃p∀s(s∈p↔∀y(y∈s →y∈x))

Infinity:

∃w(∅∈w∧∀x(x∈w→x∪{x}∈w))

We mentioned earlier the von Neumann representation for natural numbers: 0={∅}, 1={0}, 2={0,1}, etc. This axiom insures the existence of a set containing all the von Neumann natural numbers. I leave the vernacular-free expression of Infinity as an exercise for the fastidious.

Separation (sometimes called Subset) isn’t a single axiom, but an axiom schema. We have an instance of the schema for each formula φ(y,t̄). For any set x and any choice of values c̄ for t̄, the instance says there is a set of all elements y of x satisfying φ(y,c̄).

Separation:

∀t̄ ∀x ∃s∀y(y∈s↔y∈x∧φ(y,t̄))

Separation justifies the use of the set-builder notation s={y∈x:φ(y,t̄)}.

Replacement (sometimes called Substitution) is also an axiom schema, with an instance for each formula φ(y,z,t̄). Suppose for some particular choice t̄=c̄, the formula φ(y,z,t̄) defines z as a partial function φ° of y: Given y, there is at most one z making φ(y,z,c̄) true. Then the range of φ° on any set x is a set.
Replacement:

∀t̄∀x(∀y ∃_≤1z φ(y,z,t̄) →∃w(w={φ°(y):y∈x}))

But the set-builder term is not justifiable by Separation. Eliminating it gives:

	∀t̄∀x[∀y∃≤1zφ(y,z,t̄)
	→∃w∀z(z∈w↔(∃y∈x)φ(y,z,t̄))]

And we can eliminate ∃_≤1z and ∃y∈x. We replace ∃_≤1z with this:

∀u∀v(φ(y,u,t̄)∧φ(y,v,t̄)→u=v)

and (∃y∈x)φ(y,z,t̄) with

∃y(y∈x ∧φ(y,z,t̄))

This version of Replacement demands only that φ° be a partial function, not necessarily total. You can derive Separation from it. If φ(y,t̄) is the separating property, then let ψ(y,z,t̄) (for a particular t̄=c̄) define the partial function ψ°(y)=y when φ(y,c̄) is true, and undefined when φ(y,c̄) is false. Then applying ψ° to x gives the subset we want. Some authors use the “total” version of Replacement, and include Separation in their list of axioms.

Choice (AC) was the scene for major philosophical combat early in the 20th century, as we’ve seen. It’s easier to express than Replacement.

Choice:

	∀x[(∀y∈x)y≠∅∧ (∀y∈x)(∀z∈x)(y≠z→y∩z=∅)
	→∃c(∀y∈x)#(c∩y)=1]

Eliminating some vernacular should be routine by now: y≠∅, y∩z=∅. As for #(c∩y)=1, this becomes

∃u(u∈c∩y∧∀v(v∈c∩y→v=u))

where of course u∈c∩y is formally u∈c∧u∈y, likewise for v.

Another version of Choice does not require disjointness. It’s easy to express formally once you have the machinery of ordered pairs, and thus functions as sets of ordered pairs. It says: for every set x whose elements are all nonempty sets, there is a so-called choice function c such that c(y)∈y for all y∈x.

Unlike every other “set existence” axiom of ZFC, we can’t define c with set-builder notation, or indeed give any other explicit description of the choice function. We’ve seen how this lead to much distrust of AC. In 1938, Gödel showed if ZF is consistent, then ZFC is too. That calmed things down somewhat. I’ve cited Moore’s book before on the history of the Axiom of Choice.

Prev TOC Next