The choice ledger: what costs the Axiom of Choice and what does not

This item is bookkeeping, not mathematics: it records what each statement in the neighbourhood of the Axiom of Choice actually costs, so that later pages can state honestly which of their theorems are choice-free. Nothing here is proved that is not proved elsewhere in the library, and everything cited without a link is flagged as such.

Equivalent to the Axiom of Choice over ZF.

• Zorn's lemma and the well-ordering theorem. Both equivalences are proved in this library, in The Axiom of Choice and Zorn's lemma are equivalent and Choice, Zorn and well-ordering are equivalent. Each of these two statements costs exactly the Axiom of Choice, no more and no less. A theorem proved with one of them costs at most the Axiom of Choice, which is an upper bound and not a lower one: the theorem may well follow from something strictly weaker, and the ultrafilter lemma below is exactly that case.
• Tychonoff's theorem, that a product of compact spaces is compact. The implication from the Axiom of Choice is the familiar one; the converse is Kelley 1950. Not proved here, and worth a warning when it is: Kelley's original argument needs a repair, supplied by Schechter, and without the repair it yields only the Boolean prime ideal theorem (Schechter 2006: Kelley's cofinite proof yields BPI, not the Axiom of Choice ‡).
• Every vector space has a basis. The implication from the Axiom of Choice is a routine application of Zorn's lemma, and it is proved here, in Every vector space has a basis by way of Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if $L \subseteq S \subseteq V$ with $L$ independent and $\operatorname{span}(S) = V$, there is a basis $B$ of $V$ with $L \subseteq B \subseteq S$. The converse is a hard theorem of Blass, 1984, which is not proved here and is quoted on the authority of the references. The equivalence itself is recorded in the library, in Does Hahn-Banach yield a Hamel basis for $\mathbb{R}$ over $\mathbb{Q}$? (open) ‡, where it fixes the upper endpoint of an open question about the strength of Hahn-Banach.
• Cardinal comparability, that for any two sets one injects into the other. This is Hartogs 1915, and the full equivalence with the Axiom of Choice is now proved here, in Comparability of arbitrary sets, that any two sets admit an injection one way or the other, is equivalent to the Axiom of Choice ↗, by way of the construction of Hartogs: an ordinal that does not inject into a given set.

Strictly weaker than the Axiom of Choice.

Each of the following is a genuine choice principle: not provable in ZF (assuming ZF consistent), yet strictly weaker than the Axiom of Choice.

• The ultrafilter lemma, that every filter extends to an ultrafilter, equivalently the Boolean prime ideal theorem. The Axiom of Choice implies it, that implication being the one thing here this library does prove; it is not provable in ZF (Feferman 1965, Feferman 1965: ZF does not prove that a free ultrafilter on the naturals exists ‡), and it does not imply the Axiom of Choice (Halpern and Levy 1971, Halpern and Lévy 1971: the Boolean prime ideal theorem does not imply the Axiom of Choice ‡). Both of those are external results, recorded and not proved here. The proof given here (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter) runs through Zorn's lemma, so it pays full price for a statement that costs strictly less: exactly the overpayment set out in What the ultrafilter lemma costs: a choice principle strictly weaker than AC, and the reason a cost may not be read off a proof.
• Dependent choice (DC), that if every element of a nonempty set $X$ stands in a relation $R$ to some element of $X$, then for every $a \in X$ there is a sequence $(x_n)_{n \in \mathbb{N}}$ in $X$ with $x_0 = a$ and $x_n \mathbin{R} x_{n+1}$ for every $n$ (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain). The prescribed starting point belongs to the statement: deleting the clause $x_0 = a$ gives a formally weaker principle, which that item records as an immediate consequence and does not derive DC back from, so the two are not interchangeable here. What DC delivers is an $\mathbb{N}$-indexed sequence, not a chain in this library's sense (Chain in a poset, a totally ordered subset of a poset): $R$ need not be an order at all, and the terms need not be distinct. Implied by the Axiom of Choice, and implies countable choice; neither implication reverses, which is a relative-consistency result and so holds under the standing assumption that ZF is consistent. It is the principle quietly used whenever a sequence is built by picking each term in terms of the previous one. The two non-reversals are external results that this library does not prove; it records them, with their sources, in The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain.
• Countable choice ($\mathrm{AC}_\omega$), choice functions for countable families. Implied by dependent choice, and still not a theorem of ZF: Cohen's first model contains an infinite set of reals with no countably infinite subset (Cohen's first model: an infinite Dedekind-finite set of reals ‡), which is already a failure of $\mathrm{AC}_\omega$.

These three are not ranked on a line, and none of them is "the weakest". The only implications among them PROVABLE IN ZF are $\mathrm{DC} \Rightarrow \mathrm{AC}_\omega$ and its consequences; the ultrafilter lemma is incomparable with dependent choice and with countable choice alike, neither implying nor implied by either. Every non-implication in that sentence is a relative-consistency result, quoted from the references and conditional on the consistency of ZF: what is established is that ZF, if consistent, does not prove the missing implications, never that they are outright false. Those incomparabilities are quoted from the references, not recorded here. So a theorem must be labelled with the principle it actually uses, never with a position on a scale, and a phrase like "the weakest of the three" is simply not available.

Choice-free, and deliberately so.

• Hartogs: an ordinal that does not inject into a given set: for every set $A$ there is a least ordinal that does not inject into $A$. This is the ZF substitute for cardinal comparability, and its whole value is that it needs no choice.
• Comparability of well-orders: any two well-orders are comparable. Comparability of arbitrary sets is equivalent to the Axiom of Choice; comparability of well-orders is free.
• Transfinite induction, transfinite recursion, the assignment of order types, and the Burali-Forti theorem are all theorems of ZF. Transfinite recursion spends Replacement, and that is the only axiom beyond the basic ones it needs; the standard confusion on this point is recorded as FALSE: transfinite induction and recursion need the Axiom of Choice.
• Rigidity of well-orders (Rigidity of well-orders) is the structural reason for all of this: the witnessing isomorphisms are unique, so they never have to be chosen.

Where this library spends choice.

Full choice is spent at one step inside Zorn's lemma, and directly in some results that do not route through Zorn; more than one result assumes it, and there are a second and a third, weaker principle each assumed elsewhere. All four facts belong in the ledger.

• One step inside Zorn, and direct uses besides. The Axiom of Choice is used at a single step of the proof of Zorn's lemma (Zorn's lemma), to select a strict upper bound for every chain at once; the fixed point theorem underlying it (Bourbaki–Witt fixed point theorem) is choice-free. Most results in this library that assume full choice reach it through that step, but not all: some apply the Axiom of Choice directly instead, for example A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice ↗, which uses it to obtain a point of an arbitrary product of nonempty sets without routing through Zorn's lemma.
• The results that assume full choice. Zorn's lemma itself is the first of them: its statement takes the Axiom of Choice as a standing hypothesis, which is why the step above lives inside it. On this page: the well-ordering theorem (The well-ordering theorem), which takes the Axiom of Choice as a hypothesis; and the cardinality assignment of Cardinal (initial ordinal) and cardinality, which assumes it in order to well order an arbitrary set. That last one is easy to miss, because the property of being a cardinal is choice-free and only the attachment of $|X|$ to an arbitrary $X$ is not. The two equivalences The Axiom of Choice and Zorn's lemma are equivalent and Choice, Zorn and well-ordering are equivalent do not belong in this list: each is proved in ZF outright and assumes no choice principle, saying only that the statements it names imply one another. Elsewhere in the library, The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter is proved through Zorn's lemma and so also pays full price, although its statement costs strictly less; and the Hausdorff maximal principle, that every poset has a maximal chain, is drawn from Zorn as a consequence in The chains of a poset, ordered by inclusion, form a chain-complete poset and pays the same price, the chain-completeness verified there being free.
• A weaker principle, spent separately. Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$ and Assuming countable choice, every perfectly normal space is completely normal: separated sets in a normal space whose open sets are all $F_\sigma$ can be separated by disjoint open sets ↗ are each stated under countable choice (The Axiom of Countable Choice ($\mathrm{AC}_\omega$)) and flag the one step that spends it. That is not a use of the Axiom of Choice: $\mathrm{AC}_\omega$ is strictly weaker, so neither theorem may be relabelled choice-free or lumped in with the full-choice results above.
• A third principle below full AC. Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0,1]$, and conversely such a space is normal ↗ and Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a,b]$ extends continuously to the whole space, and this property characterises normality ↗ are each stated under dependent choice (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain), each applying dependent choice directly to a single relation on stage-tagged states to build an $\mathbb{N}$-indexed sequence of approximations; the standalone stagewise form Dependent choice along a sequence of relations: if $R_n$ is entire on $A$ for every $n$, then from any $a$ there is a sequence with $a_n \mathbin{R_n} a_{n+1}$ ↗ is a related construction that neither theorem cites. DC implies $\mathrm{AC}_\omega$ and neither reverses (recorded above), so this is a third, distinct cost: not the Axiom of Choice, and not interchangeable with the countable-choice results either, even though DC happens to imply enough to reprove them.

What is not proved anywhere here.

The independence of the Axiom of Choice from ZF. Gödel's 1938 constructible universe shows ZF cannot refute it (Gödel 1938: ZF does not refute the Axiom of Choice ‡); Cohen's 1963 forcing shows ZF cannot prove it (Cohen 1963: ZF does not prove the Axiom of Choice ‡). Both are external results requiring machinery this library does not yet contain, and both are conditional on the consistency of ZF. Every statement in the library that relies on them is written conditionally, as in FALSE: Zorn's lemma is a theorem of ZF and FALSE: the well-ordering theorem is a theorem of ZF. A reader who wants the unconditional version of those statements will not find it, here or anywhere.