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 \ne \emptyset$ for every $i \in I$, then $\prod_{i \in I} X_i \ne \emptyset$. 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.

• This is an axiom, not a theorem, and it is deliberately not derived here. Assume ZF is consistent. Then AC is independent of the axioms of Zermelo–Fraenkel set theory: Gödel (1938) showed that ZF, if consistent, cannot refute it (Gödel 1938: ZF does not refute the Axiom of Choice ‡), and Cohen (1963) showed that ZF, if consistent, cannot prove it (Cohen 1963: ZF does not prove the Axiom of Choice ‡). The consistency hypothesis is not decoration and cannot be dropped: an inconsistent ZF proves everything, AC included, so both halves of the independence would fail. Nor can the hypothesis be discharged inside ZF. Both directions also require machinery (the constructible universe and forcing) that this library does not yet contain, so both are recorded with references rather than proved. FALSE: Zorn's lemma is a theorem of ZF ↗ carries the same consistency assumption explicitly in its Given; The choice ledger: what costs the Axiom of Choice and what does not ↗ records the weaker choice principles.
• 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 choice ledger: what costs the Axiom of Choice and what does not ↗. What the ultrafilter lemma costs: a choice principle strictly weaker than AC ↗ carries the narrower question of what the ultrafilter lemma costs, and on cited authority, and under the hypothesis that ZF is consistent, places that principle strictly between ZF and AC.