The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)

The Axiom of Countable Choice, written ${\mathrm{A}\mathrm{C}}_{\omega }$, is the following statement.

For every family $(X_n{)}_{n\in \mathbb{N}}$ of nonempty sets indexed by $\mathbb{N}$ there is a function $f$ with domain $\mathbb{N}$ such that $f(n)\in X_n$ for every $n\in \mathbb{N}$.

Equivalently, in the vocabulary of Choice function: every at most countable family of nonempty sets has a choice function.

Choice function

Finite, countably infinite, countable, uncountable

• The two formulations are equivalent, and the passage between them uses no choice. Given an at most countable family $\mathcal{F}$ of nonempty sets, either $\mathcal{F}=\mathrm{\varnothing }$, where the empty function is a choice function, or a surjection $s:\mathbb{N}\to \mathcal{F}$ exists (A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$); applying the indexed form to $X_n:=s(n)$ gives $f$ with $f(n)\in s(n)$, and $g(S):=f(\min \{n:s(n)=S\})$ is a choice function for $\mathcal{F}$, the minimum being canonical by The well-ordering principle. Conversely a choice function $g$ on the at most countable family $\{X_n:n\in \mathbb{N}\}$ gives $f(n):=g(X_n)$.

• AC implies countable choice. The Axiom of Choice (The Axiom of Choice) applies to the family of values of any sequence of nonempty sets; composing the resulting choice function with the sequence gives the function required above.

• Dependent choices and independent choices have different input data. Countable choice selects from a family fixed in advance. Dependent choice instead asks for a sequence following an entire relation, where the available successors depend on the preceding term. The later AC implies DC implies countable choice proves $\mathrm{A}\mathrm{C}\Rightarrow \mathrm{D}\mathrm{C}\Rightarrow {\mathrm{A}\mathrm{C}}_{\omega }$ in ZF. This remark makes no assertion about reversing either implication.

• A locally proved failure comparison appears later. Relative consistency of the Feferman–Levy choice failures over ZF ↗ proves the external implication from consistency of ZF to consistency of $\mathrm{Z}\mathrm{F}+\mathrm{\neg }{\mathrm{A}\mathrm{C}}_{\omega }$, together with the stated Feferman–Levy properties. Hence, if ZF is consistent, it cannot prove countable choice: a ZF proof would also hold in that consistent extension. This is a conditional consistency comparison, not an assertion that countable choice fails in the present development.

• Being an axiom, ${\mathrm{A}\mathrm{C}}_{\omega }$ carries no well-definedness obligation, which is why this item has no justified_by. Its role in this library is bookkeeping: Countable unions of at most countable sets, assuming ${\mathrm{A}\mathrm{C}}_{\omega }$ assumes it and flags the exact step that spends it. No necessity claim is inferred from that proof.

• Every result proved on this page other than Countable unions of at most countable sets, assuming ${\mathrm{A}\mathrm{C}}_{\omega }$ is a theorem of ZF alone. In particular Every subset of an at most countable set is at most countable, A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$, The Schröder-Bernstein theorem, $\mathbb{Q}$ is countably infinite, Cantor's theorem: $A\prec \mathcal{P}(A)$ and $\mathbb{R}$ is uncountable (Cantor's nested intervals, 1874) are choice free, and each says so.