Choice ledger for this page: ${\omega }_1$ exists in ZF, and the boundedness theorem does not

This item is bookkeeping, in the manner of The proved choice ledger: hypotheses, equivalences, and upper bounds: it records what each result on this page costs, so that a later page quoting one of them knows what it is inheriting. Nothing is proved here that is not proved elsewhere.

Free: everything about ordinal arithmetic. Ordinal $+$, $\cdot$ and ${\alpha }^{\beta }$ are defined by transfinite recursion along the ordinals, and recursion spends Replacement and no choice; the values are unique at every stage, so nothing is ever selected. Monotonicity, associativity, left distributivity, subtraction, division with remainder, the exponent laws, the Cantor normal form and the agreement with the Peano operations on $\omega$ are all theorems of ZF.

Free: the existence of ${\omega }_1$. This is worth stating loudly, because it is the point at which readers most often expect a choice principle to appear. ${\omega }_1$ is defined as the Hartogs number $\mathrm{\aleph }(\omega )$ (The first uncountable ordinal ${\omega }_1:=\mathrm{\aleph }(\omega )$), and Hartogs: an ordinal that does not inject into a given set is a theorem of ZF. Its construction collects the order types of the well-ordered subsets of $\mathbb{N}$; the well-ordering arrives as part of each datum rather than being chosen for each subset, and the passage from that class to a set of ordinals is Replacement. Consequently ${\omega }_1$ is uncountable, every ordinal below it is at most countable, it is a cardinal and a limit ordinal, and its existence is a theorem of ZF — that ${\omega }_1$ is uncountable, that every ordinal below it is at most countable, that it is a cardinal and that it is a limit ordinal — is choice free in full.

Not free: boundedness of at most countable subsets of ${\omega }_1$. Assuming countable choice: every at most countable subset of ${\omega }_1$ is bounded below ${\omega }_1$, so no at most countable subset of ${\omega }_1$ is cofinal in it, and a supremum of at most countably many at most countable ordinals is at most countable takes the Axiom of Countable Choice (The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)) as a standing hypothesis, and spends it at exactly one step: the appeal to Countable unions of at most countable sets, assuming ${\mathrm{A}\mathrm{C}}_{\omega }$, which selects one enumeration of each of countably many at most countable sets at once. Every consequence of the boundedness theorem inherits that cost, including the statement that no at most countable subset of ${\omega }_1$ is cofinal in it. The exact ${\mathrm{A}\mathrm{C}}_{\omega }$ hypothesis is therefore part of those results and may not be silently replaced by “choice-free” or by full AC. The local ledger The proved choice ledger: hypotheses, equivalences, and upper bounds makes no unproved reverse-implication claim.

A standing warning for later pages. Any argument that builds a counterexample on the ordinal space below ${\omega }_1$ and uses "a countable family of ordinals below ${\omega }_1$ has a bound below ${\omega }_1$" is spending ${\mathrm{A}\mathrm{C}}_{\omega }$, whether or not it says so. Pages that use the boundedness theorem must carry the hypothesis forward into their own statements.