Axiom of choice

In mathematics, the axiom of choice, abbreviated AC or AoC, is an axiom of set theory. Informally put, the axiom of choice says that given any collection of non-empty sets, one can identify another set containing one element chosen from each set, even if the collection is infinite. Formally, the axiom establishes existence rather than a construction; it states that for every set \(I\) and every \(I\)-indexed family \((S_i)_{i \in I}\) of nonempty sets, there exists an \(I\)-indexed set \((x_i)_{i \in I}\) of elements of \(\cup_{i\in I}S_i\) such that \(x_i \in S_i\) for every \(i \in I\). The axiom of choice was formulated in 1904 by Ernst Zermelo in order to formalize his proof of the well-ordering theorem.

In many cases, a set created by choosing elements can be made without invoking the axiom of choice, particularly if the number of sets from which to choose the elements is finite (in which induction can be applied), or if a canonical rule on how to choose the elements is available, some distinguishing property that happens to hold for exactly one element in each set. An illustrative example is sets picked from the natural numbers. From such sets, one may always select the smallest number, e.g. given the sets {{4, 5, 6}, {10, 12}, {1, 400, 617, 8000}}, the set containing each smallest element is {4, 10, 1}. In this case, "select the smallest number" is a choice function. Even if infinitely many sets are collected from the natural numbers, it will always be possible to form a choice function from choosing the smallest element from each set to produce a set; the axiom of choice is not needed here. On the other hand, for the collection of all non-empty subsets of the real numbers, there is no known canonical rule by which one can choose one element from each of these subsets. In that case, the axiom of choice must be invoked to construct the desired choice function.

Bertrand Russell coined an analogy: for any (even infinite) collection of unordered pairs of shoes, one can pick out the left shoe from each pair to obtain an appropriate collection (i.e. set) of shoes; this makes it possible to define a choice function without using the axiom of choice. However, for an infinite collection of unordered pairs of socks (assumed to have no distinguishing features such as being a left sock rather than a right sock), there is no natural (i.e., canonical) way of choosing one sock from each pair, so one must appeal to the axiom of choice to construct the desired choice function.

Although originally controversial, the axiom of choice is now used without reservation by most mathematicians, and is included in the standard form of axiomatic set theory, Zermelo-Fraenkel set theory with the axiom of choice (ZFC). One motivation for this is that a number of generally accepted mathematical results, such as Tychonoff's theorem, require the axiom of choice for their proofs. Contemporary set theorists also study axioms that are not compatible with the axiom of choice, such as the axiom of determinacy. While some varieties of constructive mathematics avoid the axiom of choice, others embrace it.

A choice function (also called selector or selection) is a function \(f\), defined on a collection \(X\) of nonempty sets, such that for every set \(A\) in \(X\), \(f(A)\) is an element of \(A\). With this concept, the axiom can be stated:

Axiom, For any set \(X\) of nonempty sets, there exists a choice function \(f\) that is defined on \(X\) and maps each set of \(X\) to an element of that set.

Formally, this may be expressed as follows:

\[\forall X \left[ \varnothing \in X \lor \exist f \left[ \mathrm{dom} \ f = X \land \forall A \in X \left[ f\left(A\right) \in A \right] \right] \right].\]

Each choice function on a family \(X\) of nonempty sets is an element of the Cartesian product of the sets in \(X\), and vice versa. Therefore, an equivalent form of the axiom of choice is:

This form implies a more general form where the Cartesian product is of a general indexed family of sets (which may contain duplicates), since one can always select the same element from duplicate factors.

In this article and other discussions of the axiom of choice the following abbreviations are common:

• AC, the axiom of choice. More rarely, AoC is used.
• ZF, Zermelo-Fraenkel set theory omitting the axiom of choice.
• ZFC, Zermelo-Fraenkel set theory, extended to include the axiom of choice.

There are many other equivalent statements of the axiom of choice. These are equivalent in the sense that, in the presence of other basic axioms of set theory, they imply the axiom of choice and are implied by it.

One variation avoids the use of choice functions by, in effect, replacing each choice function with its range:

This can be formalized in first-order logic as:

\[\begin{aligned} \forall x (& \\ &\exists e (e \in x \and \lnot\exists y (y \in e)) \or \\ &\exists a \, \exists b \, \exists c \, (a \in x \and b \in x \and c \in a \and c \in b \and \lnot(a = b)) \or \\ &\exists c \, \forall e \, (e \in x \implies \exists a \, (a \in e \and a \in c \and \forall b \, ((b \in e \and b \in c) \implies a = b)))) \end{aligned}\]

Note that \(P \or Q \or R\) is logically equivalent to \((\lnot P \and \lnot Q) \implies R\). In English, this first-order sentence reads:

This guarantees for any partition of a set \(X\) the existence of a subset \(C\) of \(X\) containing exactly one element from each part of the partition.

Another equivalent axiom only considers collections \(X\) that are essentially powersets of other sets:

Condensed: the full section is in Wikipedia.

Until the late 19th century, the axiom of choice was often used implicitly, although it had not yet been formally stated. For example, after having established that the set X contains only non-empty sets, a mathematician might have said "let F(s) be one of the members of s for all s in X" to define a function F. In general, it is impossible to prove that F exists without the axiom of choice, but this seems to have gone unnoticed until Zermelo.

The existence of a choice function for a finite collection of nonempty sets can be proved by the principle of finite induction, without appealing to the axiom of choice. The proof uses the fact that, given a single nonempty set ⁠\(A\)⁠, first-order logic allows choosing some concrete ⁠\(a \in A\)⁠. However, since a proof in first-order logic must be finite, one cannot make an infinite number of choices with first-order logic alone.

Another case where the axiom of choice is not needed is when there exists an explicit rule that gives a canonical choice function. For example, if each member of the collection ⁠\(X\)⁠ is a nonempty subset of the natural numbers, then one such explicit rule is to choose the smallest element of each ⁠\(A \in X\)⁠. The canonical choice function that maps each ⁠\(A \in X\)⁠ to its smallest element can again be constructed in ZF without the axiom of choice.

In general, if the union of all sets in ⁠\(X\)⁠ can be well-ordered, then a choice function for ⁠\(X\)⁠ can be constructed without using the axiom of choice. Note that it does not suffice that each ⁠\(A \in X\)⁠ can be well-ordered, since the axiom of choice may be needed to choose a canonical well-ordering for each ⁠\(A\)⁠ anyway.

As an example where the axiom of choice is required, let ⁠\(X\)⁠ be set of all non-empty subsets of the real numbers. Choosing the least element from each set no longer works, because some subsets of the real numbers do not have least elements. For example, the open interval ⁠\((0,1)\)⁠ does not have a least element: if ⁠\(x\)⁠ is in ⁠\((0,1)\)⁠, then so is ⁠\(x/2\)⁠, and ⁠\(x/2\)⁠ is always strictly smaller than ⁠\(x\)⁠. This strategy fails here because the natural order of real numbers is not a well-order.

If there exists a different ordering of the real numbers which is a well-ordering, then applying the least-element strategy with respect to that ordering would give a choice function for ⁠\(X\)⁠. Conversely, if there exists a choice function for ⁠\(X\)⁠, then the proof of the well-ordering theorem would show that a well-ordering of the real numbers does exist.

Let ⁠\(S\)⁠ be the unit circle, and ⁠\(G\)⁠ be the group consisting of all rational rotations (i.e., rotations by angles which are rational multiples of ⁠\(\pi\)⁠). Since ⁠\(G\)⁠ is countable while ⁠\(S\)⁠ is uncountable, ⁠\(S\)⁠ must break up into uncountably many orbits under the action of ⁠\(G\)⁠.

Using the axiom of choice, we could pick a single point from each orbit, obtaining an uncountable subset ⁠\(X\)⁠ of ⁠\(S\)⁠ with the property that all of its translates by ⁠\(G\)⁠ are disjoint from ⁠\(X\)⁠. The set of those translates partitions the circle into a countable collection of pairwise disjoint sets, which are all pairwise congruent. The set ⁠\(X\)⁠ will be non-measurable for any rotation-invariant countably additive measure on ⁠\(S\)⁠: if ⁠\(X\)⁠ has zero measure, countable additivity would imply that the whole circle has zero measure. If ⁠\(X\)⁠ has positive measure, countable additivity would show that the circle has infinite measure.

Applying a similar construction to the three-dimensional ball can result in a set that is non-measurable even for any rotation-invariant finitely additive measure, as shown by the Banach-Tarski paradox.

A proof requiring the axiom of choice may establish the existence of an object without canonically defining the object in the language of set theory. For example, while the axiom of choice implies that there is a well-ordering of the real numbers, there are models of set theory with the axiom of choice in which no individual well-ordering of the reals is definable. Similarly, although a subset of the real numbers that is not Lebesgue measurable can be proved to exist using the axiom of choice, it is consistent that no such set is definable.

The axiom of choice asserts the existence of these intangibles (objects that are proved to exist, but which cannot be constructed in any canonical way), which may conflict with some philosophical principles. Because there is no canonical well-ordering of all sets, a construction that relies on a well-ordering may not produce a canonical result, even if a canonical result is desired (as is often the case in category theory). This has been used as an argument against the use of the axiom of choice.

Another argument against the axiom of choice is that it implies the existence of objects that may seem counterintuitive. One example is the Banach-Tarski paradox, which says that it is possible to decompose the 3-dimensional solid unit ball into finitely many pieces and, using only rotations and translations, reassemble the pieces into two solid balls each with the same volume as the original. The pieces in this decomposition, constructed using the axiom of choice, are non-measurable sets.

Despite these seemingly paradoxical results, most mathematicians accept the axiom of choice as a valid principle for proving new results in mathematics. But the debate is interesting enough that it is considered notable when a theorem in ZFC (ZF plus AC) is logically equivalent (with just the ZF axioms) to the axiom of choice, and mathematicians look for results that require the axiom of choice to be false, though this type of deduction is less common than the type that requires the axiom of choice to be true.

Theorems of ZF hold true in any model of that theory, regardless of the truth or falsity of the axiom of choice in that particular model. The implications of choice below, including weaker versions of the axiom itself, are listed because they are not theorems of ZF. The Banach-Tarski paradox, for example, is neither provable nor disprovable from ZF alone: it is impossible to construct the required decomposition of the unit ball in ZF, but also impossible to prove there is no such decomposition. Such statements can be rephrased as conditional statements, for example, "If AC holds, then the decomposition in the Banach-Tarski paradox exists." Such conditional statements are provable in ZF when the original statements are provable from ZF and the axiom of choice.

As discussed above, in the classical theory of ZFC, the axiom of choice enables nonconstructive proofs in which the existence of a type of object is proved without an explicit canonical construction of an instance of this type. In fact, in set theory and topos theory, Diaconescu's theorem shows that the axiom of choice implies the law of excluded middle. The principle is thus not available in constructive set theory, where non-classical logic is employed.

The situation is different when the principle is formulated in Martin-Löf type theory. There and higher-order Heyting arithmetic, the appropriate statement of the axiom of choice is (depending on approach) included as an axiom or provable as a theorem. A cause for this difference is that the axiom of choice in type theory does not have the extensionality properties that the axiom of choice in constructive set theory does. The type theoretical context is discussed further below.

Different choice principles have been thoroughly studied in the constructive contexts and the principles' status varies between different school and varieties of the constructive mathematics. Some results in constructive set theory use the axiom of countable choice or the axiom of dependent choice, which do not imply the law of the excluded middle. Errett Bishop, who is notable for developing a framework for constructive analysis, argued that an axiom of choice was constructively acceptable, saying

Although the axiom of countable choice in particular is commonly used in constructive mathematics, its use has also been questioned.

It has been known since as early as 1922 that the axiom of choice may fail in a variant of ZF with urelements, through the technique of permutation models introduced by Abraham Fraenkel and developed further by Andrzej Mostowski. The basic technique can be illustrated as follows: Let x_n and y_n be distinct urelements for n=1, 2, 3..., and build a model where each set is symmetric under the interchange x_n ↔ y_n for all but a finite number of n. Then the set X = {{x₁, y₁}, {x₂, y₂}, {x₃, y₃}, ...} can be in the model but sets such as {x₁, x₂, x₃, ...} cannot, and thus X cannot have a choice function.

In 1938, Kurt Gödel showed that the negation of the axiom of choice is not a theorem of ZF by constructing an inner model (the constructible universe) that satisfies ZFC, thus showing that ZFC is consistent if ZF itself is consistent. In 1963, Paul Cohen employed the technique of forcing, developed for this purpose, to show that, assuming ZF is consistent, the axiom of choice itself is not a theorem of ZF. He did this by constructing a much more complex model that satisfies ZF¬C (ZF with the negation of AC added as axiom) and thus showing that ZF¬C is consistent. Cohen's model is a symmetric model, which is similar to permutation models, but uses "generic" subsets of the natural numbers (justified by forcing) in place of urelements.

Together these results establish that the axiom of choice is logically independent of ZF. The assumption that ZF is consistent is harmless because adding another axiom to an already inconsistent system cannot make the situation worse. Because of independence, the decision whether to use the axiom of choice (or its negation) in a proof cannot be made by appeal to other axioms of set theory. It must be made on other grounds.

One argument in favor of using the axiom of choice is that it is convenient because it allows one to prove some simplifying propositions that otherwise could not be proved. Many theorems provable using choice are of an elegant general character: the cardinalities of any two sets are comparable, every nontrivial unital ring has a maximal ideal, every vector space has a basis, every connected graph has a spanning tree, and every product of compact spaces is compact, among many others. Frequently, the axiom of choice allows generalizing a theorem to "larger" objects. For example, it is provable without the axiom of choice that every vector space of finite dimension has a basis, but the generalization to all vector spaces requires the axiom of choice. Likewise, a finite product of compact spaces can be proven to be compact without the axiom of choice, but the generalization to infinite products (Tychonoff's theorem) requires the axiom of choice.

The axiom of choice is not the only significant statement that is independent of ZF. For example, the generalized continuum hypothesis (GCH) is not only independent of ZF, but also independent of ZFC. However, ZF plus GCH implies AC, making GCH a strictly stronger claim than AC, even though they are both independent of ZF.

Condensed: the full section is in Wikipedia.

The axiom of constructibility and the generalized continuum hypothesis each imply the axiom of choice and are strictly stronger than it. In class theories such as Von Neumann-Bernays-Gödel set theory and Morse-Kelley set theory, there is an axiom called the axiom of global choice that is stronger than the axiom of choice for sets because it also applies to proper classes. The axiom of global choice follows from the axiom of limitation of size. Tarski's axiom, which is used in Tarski-Grothendieck set theory and states (in the vernacular) that every set belongs to some Grothendieck universe, is stronger than the axiom of choice.

There are important statements that, assuming the axioms of ZF but neither AC nor ¬AC, are equivalent to the axiom of choice (that is, their truth values in ZF, while undecidable, are the same as that of AC). The most important among them are Zorn's lemma and the well-ordering theorem. In fact, Zermelo initially introduced the axiom of choice in order to formalize his proof of the well-ordering theorem.

Condensed: the full section is in Wikipedia.

Several results in category theory invoke the axiom of choice for their proof. These results might be weaker than, equivalent to, or stronger than the axiom of choice, depending on the strength of the technical foundations. For example, if one defines categories in terms of sets, that is, as sets of objects and morphisms (usually called a small category), then there is no category of all sets, and so it is difficult for a category-theoretic formulation to apply to all sets. On the other hand, other foundational descriptions of category theory are considerably stronger, and an identical category-theoretic statement of choice may be stronger than the standard formulation, à la class theory, mentioned above.

Examples of category-theoretic statements which require choice include:

• Every small category has a skeleton.
• If two small categories are weakly equivalent, then they are equivalent.
• Every continuous functor on a small-complete category which satisfies the appropriate solution set condition has a left adjoint (the Freyd adjoint functor theorem).