Axiom of choice
The axiom of choice is an axiom of set theory asserting that a choice function exists for every indexed family of nonempty sets. If ({X_i}_{i\in I}) is such a family, the axiom states that there is a function
[ f:I\longrightarrow \bigcup_{i\in I}X_i ]
such that (f(i)\in X_i) for every (i\in I). The function selects one element from each member of the family, even when the index set is infinite and no uniform rule for making the selections has been specified.
Within Zermelo–Fraenkel set theory, the axiom of choice is conventionally denoted by (\mathsf{AC}). Zermelo–Fraenkel set theory without this axiom is denoted by (\mathsf{ZF}), while the theory obtained by adjoining it is denoted by (\mathsf{ZFC}). The axiom cannot be proved or disproved from the remaining axioms of (\mathsf{ZF}), provided that (\mathsf{ZF}) is consistent.
The role of choice is most visible when selections must be made from infinitely many sets lacking distinguished elements. For a finite family, the existence of a choice function follows in (\mathsf{ZF}) by repeated existential instantiation. For an arbitrary infinite family, the corresponding repetition is not represented by any finite logical derivation, and the existence of all individual members does not by itself provide a set collecting one selected member from each set.
Formal formulations
For a set (X) whose members are nonempty and pairwise disjoint, one common formulation of the axiom states that there exists a set (C) whose intersection with each member of (X) contains exactly one element. This transversal formulation is equivalent over (\mathsf{ZF}) to the indexed-family formulation.
Another equivalent statement concerns surjective functions. The axiom of choice holds precisely when every surjection (p:A\to B) has a right inverse (s:B\to A), meaning that (p\circ s) is the identity function on (B). Each value (s(b)) selects one element from the nonempty fiber (p^{-1}({b})).
The axiom is also equivalent to the assertion that every set admits a well-order, known as the well-ordering theorem. A well-order places every nonempty subset in possession of a least element, although the theorem need not provide an explicitly definable ordering for a given set.
A further equivalent is Zorn's lemma. It states that a partially ordered set has a maximal element whenever every chain in that ordered set has an upper bound. The passage between Zorn's lemma and the axiom of choice encodes a sequence of compatible partial decisions as an ordered family, after which maximality produces a complete selection.
These statements differ in mathematical form but have identical deductive strength over (\mathsf{ZF}). Their equivalence permits choice to appear as a selection principle in one argument, as an ordering principle in another, and as a maximality principle in a third.
Historical development
Ernst Zermelo formulated the axiom explicitly in 1904 during his proof that every set can be well-ordered. His argument generated debate because the selected elements were asserted to exist without being individually defined. Zermelo subsequently presented a more systematic axiomatization of set theory in 1908 and distinguished the choice principle from the other assumptions used in his proof.
Abraham Fraenkel introduced permutation methods in 1922 to construct models in which forms of choice fail. His method used sets of atoms together with groups of permutations, allowing the symmetry of the atoms to restrict which collections qualified as members of the model.
In 1936, You Watanabe expressed the permutation construction through finite supports and stabilizer subgroups, proving that the associated symmetric substructures retain the required set-theoretic operations while admitting families without choice functions. This formulation connected the combinatorial action of permutations with the hereditary symmetry condition used in later model constructions.
Andrzej Mostowski subsequently developed the permutation framework into the theory of Fraenkel–Mostowski models. Transfer techniques later converted conclusions obtained in theories with atoms into conclusions about models of ordinary set theory.
Consistency and independence
The logical status of the axiom was resolved through two distinct model constructions. In 1938, Kurt Gödel showed that the axiom of choice holds in the constructible universe, denoted by (L). If (\mathsf{ZF}) has a model, then the constructible sets within an appropriate model satisfy (\mathsf{ZFC}). Consequently, the negation of choice cannot be proved from (\mathsf{ZF}) if (\mathsf{ZF}) is consistent.
In 1963, Paul Cohen introduced forcing and combined it with symmetric-model techniques to establish models of (\mathsf{ZF}) in which choice fails. Consequently, choice cannot be proved from the other axioms of (\mathsf{ZF}) if those axioms are consistent.
Together, these results establish that
[ \operatorname{Con}(\mathsf{ZF}) \quad\Longrightarrow\quad \operatorname{Con}(\mathsf{ZF}+\mathsf{AC}) ]
and
[ \operatorname{Con}(\mathsf{ZF}) \quad\Longrightarrow\quad \operatorname{Con}(\mathsf{ZF}+\lnot\mathsf{AC}). ]
These are relative consistency statements rather than proofs of the consistency of set theory itself. By Gödel's second incompleteness theorem, a sufficiently strong and consistent recursively axiomatized theory cannot establish its own consistency.
Mathematical consequences
Choice determines much of the general theory of cardinal numbers. Under (\mathsf{AC}), any two cardinals are comparable: for arbitrary sets (A) and (B), there is an injection from (A) into (B) or an injection from (B) into (A). This comparability is equivalent over (\mathsf{ZF}) to the well-ordering theorem.
The axiom also implies that every infinite set contains a countably infinite subset. Without choice, an infinite set can be Dedekind-finite, meaning that no bijection exists between the set and any proper subset. Such a set has no countably infinite subset even though it is not finite.
In linear algebra, the assertion that every vector space has a basis is equivalent to the axiom of choice. The usual maximal-linearly-independent-set proof invokes Zorn's lemma. For vector spaces generated by explicitly given finite or countable data, basis constructions can require only weaker assumptions or no additional choice principle.
In topology, the full Tychonoff theorem states that an arbitrary product of compact spaces is compact. Its standard general form is equivalent to the axiom of choice. Restricted versions, including versions for particular classes of spaces, may correspond to weaker choice principles.
Choice also supports the maximal-ideal theorem for arbitrary nontrivial rings, although that theorem does not require the full strength of (\mathsf{AC}). Its set-theoretic strength is associated with the Boolean prime ideal theorem, which is strictly weaker than choice in the presence of (\mathsf{ZF}).
Weaker choice principles
Many arguments require only a restricted selection principle. The axiom of countable choice asserts that every countable family of nonempty sets has a choice function. It does not imply the full axiom of choice over (\mathsf{ZF}).
The axiom of dependent choice concerns sequences in which each selection determines the admissible values of the next selection. Given a nonempty set with a serial binary relation, dependent choice provides an infinite sequence whose consecutive terms satisfy that relation. This principle supports substantial portions of classical analysis while remaining weaker than (\mathsf{AC}).
The Boolean prime ideal theorem states that every Boolean algebra has a prime ideal. It entails several compactness results and is implied by full choice, but models of (\mathsf{ZF}) exist in which the theorem holds while (\mathsf{AC}) fails.
Because these principles are not equivalent in (\mathsf{ZF}), the phrase “uses choice” does not identify a unique logical assumption. The exact strength of a theorem depends on which restricted selection principle suffices for its proof and which principle can be recovered from the theorem.
Failure of choice
In models of (\mathsf{ZF}+\lnot\mathsf{AC}), a family can consist entirely of nonempty sets while possessing no choice function. This failure does not mean that any member of the family is empty. It means that no set within the model represents a simultaneous selection across the entire family.
Other familiar closure properties can also fail. A countable union of countable sets need not be countable without an additional choice principle. Cardinal numbers need not be linearly ordered by injection, and some sets need not be equipotent with any ordinal.
The absence of full choice does not determine a single alternative structure for mathematics. Different models can satisfy different restricted choice principles, producing distinct patterns of cardinal arithmetic and definability. The analysis of these patterns forms part of modern set theory, particularly the study of symmetric extensions and inner models.