The proved choice ledger: hypotheses, equivalences, and upper bounds

This ledger records only conclusions established by local proofs. It separates an assumption actually used by an argument from a claim about the weakest possible assumption, which usually needs additional model theory.

Equivalent formulations proved over ZF. The Axiom of Choice, Zorn's lemma, and the assertion that every set can be well ordered are equivalent by The Axiom of Choice and Zorn's lemma are equivalent and Choice, Zorn and well-ordering are equivalent. Thus a proof using any one of them may be translated into a proof using either of the others. This is an equivalence statement; it does not itself prove an independence result.

Where the supplied proofs spend full choice. Zorn's lemma uses The Axiom of Choice to select a strict upper bound for every chain that has no maximal member. Its structural fixed-point core, Bourbaki–Witt fixed point theorem, is choice-free. The well-ordering theorem then obtains a well-order through Zorn. The proof that every vector space has a basis similarly extends an independent set by Zorn (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 $\mathrm{span}(S)=V$, there is a basis $B$ of $V$ with $L\subseteq B\subseteq S$, Every vector space has a basis). These routes establish AC as a sufficient hypothesis; they do not establish that every consequence needs AC.

Weaker hypotheses remain distinct in this ledger. Countable choice and dependent choice are separately stated principles (The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$), The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain). A theorem using one must carry that exact assumption in its statement and proof. This item does not assert any unproved reverse implication or nonimplication among them.

Choice-free substitutes. Hartogs: an ordinal that does not inject into a given set gives, for every set $A$, an ordinal that does not inject into $A$, without comparing arbitrary sets. Comparability of well-orders compares already supplied well-orders without choosing well-orders for arbitrary sets. Transfinite induction and recursion likewise operate on a supplied well-order. These results are not weakened by the fact that assigning $\mathrm{\mid }A\mathrm{\mid }$ to an arbitrary set requires a well-orderability hypothesis.

The later constructibility, forcing, Boolean-algebra, and symmetric-model pages are responsible for proving relative consistency and strictness claims. Until then, recorded external results are targets, never dependencies of this ledger or of any other Foundations item.