The Axiom of Choice

1. Introducing the axiom

The Axiom of Choice (AC) is the remaining axiom to be added to the set of Zermelo-Fraenkel axioms (ZF) making it the full theory ZFC. Zermelo introduced the Axiom of Choice as an intuitively correct axiom that proved Cantor's well-ordering principle. As such it was rapidly accepted: in some sense it fits the ideal for set theory very well. It is a set theoretic principle that expresses a suitable internal version of Skolem-functions, a standard simplifying device used in first-order logic. In other words the Axiom of Choice is a natural and rather powerful set-theoretic extension of a generally accepted principle in logic. However some mathematicians have been concerned about the non constructive nature of the Axiom of Choice and many of its consequences. For example, the Axiom of Determinacy is also a powerful set-theoretic extension of a generally accepted principle in logic, by the Axiom of Choice and the Axiom of Determinacy are incompatible with each other.

The Axiom of Choice is equivalent to Zorn's Lemma discussed at length in The Mathematics of Logic and also to Cantor's Well-Ordering principle. In particular Section 2.3 proves the equivalence of AC and Zorn's lemma in a naïve set theoretic setting, but this proof can easily be adapted to the axiomatic setting here. In fact Theorem 2.36 is a thinly disguised proof taking us from the Axiom of Choice to the Zorn's Lemma via the Well-Ordering Principle. This web page fills in a few necessary details for students wishing to study set theory from the axiomatic point of view.

2. The Axiom of Choice and its equivalents

The axiom of choice is the statement x ( y x y f y x f ( y ) y ) expressing the fact that if x is a set of nonempty sets there is a set function f selecting (choosing) an element from each y x .

It is sometimes thought that the problem with AC is the fact it makes arbitrary choices and it is a pity that this emphasis is put on the axiom by its name. In fact if x had some precisely specified number of elements (57 for example) then such an f could be obtained by the axioms of pair set and sum set and ordinary first order logic. The difficulty arises when one does not know in advance how many elements x has, particularly but not only if x is infinite, in which case an unknown number of arbitrary choices would seem to be required. This isn't possible in first-order logic, but is not stretching the imagination too far, and the Axiom of Choice specifies that there is a suitable choice function for x .

In fact we see from the last paragraph that it appears to be a very reasonable course to adopt the Axiom of Choice, as it is, it seems, only a mild extension of what is already possible in plain first-order logic. It has a strong simplifying effect, that is:

Proposition.

If x is a set of sets then there is a function f such that for all y x : z z y holds if and only if f ( y ) y .

Proof.

Let u x and x = { y x : y } . Let g be a choice function for x and f ( y ) = g ( y ) if y x and f ( y ) = u otherwise.

This characteristic property of choice functions that they simplify first-order formulas by removing a quantifier is the main idea of Skolem Functions. A choice function is slightly more than a Skolem function: it is given internally in set theory and is not just available externally in the metamathematics, and this again is another (related) reason why AC is a good axiom to adopt: it mimics a familiar logical principle within set theory itself, in line with the general motivation for set theory as being a mathematical theory of logical property.

The Well-Ordering principle (WO) is the statement that for every non-empty set x there is a well-ordering < on x . By a previous result this is equivalent to saying that every set is in one-to-one correspondence with some ordinal. It is reasonably straightforward to show directly from the Axiom of Choice that the Well-ordering principle holds.

Proposition.

Let x be a set. Then there is an ordinal α and a bijection f : α x .

Proof.

Let X = P ( x ) , the set of all nonempty subsets of x and let f : X x be a choice function. Then we may define by recursion on ordinals g ( α ) = f ( x { g ( β ) : β < α } ) up to some ordinal α 0 for which { g ( β ) : β < α 0 } = x . Then g : α 0 x is a bijection as required. If there is no such α 0 for which { g ( β ) : β < α 0 } = x we quickly get a contradiction, for let y = { u x : α g ( α ) = u } , the image of g . Then y is a set by separation, and the absence of α 0 as above shows that On = { g -1 ( u ) : u y } is a set by replacement. But we have already seen that the collection of all ordinals is not a set.

To get a well-ordering on x given a bijection g : α x just define u < v iff g -1 ( u ) g -1 ( v ) .

Conversely, going from the well-ordering principle to the axiom of choice, given a set x of nonempty sets and a well-ordering < on x it is easy to define a choice function, by choosing the < -least element each time.

The last of the three main equivalents of AC is Zorn's lemma. This is proved to be equivalent to AC in Section 2.3 of the book, and direct proofs showing it to be equivalent to WO are also straightforward to find. Zorn's lemma tends to be used more often in algebraic settings and other areas of mathematics where transfinite inductions and recursions are not so commonly used, but the well-ordering principle might also be applied in such cases.

3. Criticisms of the Axiom of Choice

The nonconstructive nature of AC has lead to some people rejecting it as an axiom, or at least carefully stating when it is and isn't required. The Well-Ordering principle illustrates the nonconstructive nature of the axiom of choice very well: even a familiar set such as the set of real numbers does not obviously have a well-order and certainly not one that can be defined or constructed. Now there are flavours of constructivism in mathematics which expect that some existence theorem that is provable should come with an explicit construction or definition of the object shown to exist, but there is no obvious necessity for mathematics have this nature. It is similar to the fact that the mathematical implication is adequate or even correct for ordinary mathematics despite being unlike the natural language implication because of the lack of any sense of causality: mathematical language and mathematical proofs in general are not necessarily the same as real world arguments, and this might actually be a bonus rather than a negative aspect of them. Similarly real world constructivism may not be appropriate to mathematics at all times.

But in fact the nonconstructive nature of AC is rather harder to pin down than it seems. Gödel showed that if ZF without Choice is consistent then so is the theory ZFC with Choice. His method was to construct a particular minimal definable substructure inside the universe of sets, called L. This was, if you like, an ultra-constructivist sort of definition. It turns out that in L, because of the very precise definable nature of the sets there, AC is true. In other words AC is true in L because of the constructions of the sets in L, and if AC is false in some other universe it is because the sets in that universe are already non-constructive in some sense. This suggests that it is arguable that the nonconstructive axiom is actually the power set axiom (which allows all subsets of a given set without specifying how they arise) rather than the Axiom of Choice itself.