The Axiom of Choice

The Axiom of Choice (AC) is the following statement.

Every family of nonempty sets has a choice function (Choice function).

Written out: for every set $\mathcal{F}$ all of whose members are nonempty, there exists a function $g$ with domain $\mathcal{F}$ satisfying $g(S)\in S$ for all $S\in \mathcal{F}$.

An equivalent formulation is that a product of nonempty sets is nonempty: if $X_i\mathrm{\ne }\mathrm{\varnothing }$ for every $i\in I$, then ${\prod }_{i\in I}{X}_i\mathrm{\ne }\mathrm{\varnothing }$. Here ${\prod }_{i\in I}{X}_i$ is the set of functions $f$ with domain $I$ such that $f(i)\in X_i$ for every $i\in I$; when a family of nonempty sets is indexed by itself, such an $f$ is precisely a choice function for it.

Choice function

• This is an axiom, not a theorem. The results on this page prove equivalences and consequences from AC; they do not assume an independence theorem in order to define or use it. The proved choice ledger: hypotheses, equivalences, and upper bounds ↗ records only the implications and proof costs established by local results.
• Being an axiom, AC carries no well-definedness obligation, which is why this item has no justified_by.
• The case of a family listed by a natural number, which is the finite case once finiteness is defined, is a theorem of ZF and needs no axiom (Every natural-number-indexed list of nonempty sets has a choice function on its family of values ↗). AC is exactly the extension of that theorem to arbitrary index sets, and the gap between the two is not a matter of degree: Russell's shoes and socks ↗ exhibits the difference concretely.
• "ZFC" abbreviates ZF together with AC. A result that invokes AC should say so where it is stated, so that a reader can tell which theorems are choice-free; that bookkeeping is the purpose of The proved choice ledger: hypotheses, equivalences, and upper bounds ↗. The proved choice cost of the ultrafilter lemma ↗ records the narrower, locally proved upper bound for the ultrafilter lemma. Its exact reverse implications wait for the later Boolean-algebra and symmetric-model development.