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.