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.
The axiom of choice is the statement
expressing the fact that if is a set of nonempty sets there is a set function
selecting (choosing
) an element from each .
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 had some
precisely specified number of elements (57 for example) then such an
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
has, particularly but not only if 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 .
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 is a set of sets then there is a function such that for all : holds if and only if .
Proof.
Let and . Let be a choice function for and if and 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 there is a well-ordering on . 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 be a set. Then there is an ordinal and a bijection .
Proof.
Let , the set of all nonempty subsets of and let be a choice function. Then we may define by recursion on ordinals up to some ordinal for which . Then is a bijection as required. If there is no such for which we quickly get a contradiction, for let , the image of . Then is a set by separation, and the absence of as above shows that 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 given a bijection just define iff .
Conversely, going from the well-ordering principle to
the axiom of choice, given a set of nonempty sets
and a well-ordering on 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.
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.