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

The Axiom of Countable Choice, written $\mathrm{AC}_\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 (Finite, countably infinite, countable, uncountable) has a choice function.

• 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} = \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)$.

• $\mathrm{AC}_\omega$ is strictly weaker than the Axiom of Choice (The Axiom of Choice): AC implies it immediately, since AC applies to every family, while it is consistent with ZF that $\mathrm{AC}_\omega$ holds and AC fails. It is also strictly stronger than what ZF proves: it is consistent with ZF that $\mathrm{AC}_\omega$ fails, as Cohen's first model shows, since an infinite set of reals with no countably infinite subset (Cohen's first model: an infinite Dedekind-finite set of reals ‡) is already a failure of $\mathrm{AC}_\omega$; the Feferman-Levy model (The Feferman-Levy model: the reals as a countable union of countable sets ‡) is a second witness. Both statements are conditional on the consistency of ZF and are external results, established by forcing and by permutation models; they are recorded here with references and are not proved in this library, which contains neither technique. Of the two, only the failure of $\mathrm{AC}_\omega$ is recorded in this library's catalogue of unproved results; the separation of $\mathrm{AC}_\omega$ from AC in the other direction is quoted from the references alone.

• Dependent choice sits between them. The Axiom of Dependent Choice (DC) says that if $R$ is a relation on a nonempty set $X$ such that every $x \in X$ has some $y$ with $x \mathbin{R} y$, then there is a sequence $(x_n)_{n \in \mathbb{N}}$ with $x_n \mathbin{R} x_{n+1}$ for all $n$. In ZF, $\mathrm{AC} \Rightarrow \mathrm{DC} \Rightarrow \mathrm{AC}_\omega$; both implications are theorems of ZF, and neither is proved here. That neither reverses is a pair of relative-consistency results of the same kind as in the previous bullet: if ZF is consistent, then so are ZF + DC + (not AC) and ZF + $\mathrm{AC}_\omega$ + (not DC). Both are established by forcing and by permutation models, are quoted here from the references rather than proved, and cannot be stated without the consistency hypothesis; so "DC is strictly between AC and $\mathrm{AC}_\omega$" is shorthand for those two conditional statements and is never used here as a standalone assertion. DC is the principle that legitimises "choose $x_0$, then choose $x_1$ depending on $x_0$, and so on"; $\mathrm{AC}_\omega$ only legitimises countably many independent choices made at once.

• Being an axiom, $\mathrm{AC}_\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{AC}_\omega$ assumes it and flags the exact step that spends it, and FALSE: countable unions of countable sets are countable is a theorem of ZF records that the assumption cannot be removed.

• Every result proved on this page other than Countable unions of at most countable sets, assuming $\mathrm{AC}_\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. The false statements at the end of the page are not all of that kind, and the claim above does not cover them: two of the three refute a ZF-provability claim only under the hypothesis that ZF is consistent, quoting an external independence result rather than proving it, and they say so in their own Facts.