Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Choice, Zorn and well-ordering are equivalent
Statement
Over ZF the following three statements are equivalent:
(1) the Axiom of Choice (The Axiom of Choice);
(2) Zorn's lemma;
(3) the well-ordering theorem, that every set can be well ordered.
Facts & Assumptions
Given: The axioms of ZF. Each implication below is itself a theorem of ZF, so what is established here is an equivalence proved in ZF, with no appeal to any further principle. Read it exactly that way: it says that ZF proves each of (1), (2), (3) to follow from the others, and it does not say that any of the three is itself a theorem of ZF. Which of them ZF proves outright is a separate, metamathematical question, and the answer, conditional on the consistency of ZF, is none of them; that is recorded among this page's false statements and in the remarks below.
The Axiom of Choice implies that every set can be well ordered (The well-ordering theorem).
If every set can be well ordered then the Axiom of Choice holds (The well-ordering theorem implies the Axiom of Choice).
The Axiom of Choice and Zorn's lemma are equivalent over ZF (The Axiom of Choice and Zorn's lemma are equivalent).
The Axiom of Choice is the statement that every family of nonempty sets has a choice function (The Axiom of Choice).
Proof
Assuming (1), every set can be well ordered, which is (3).
Assuming (3), every family of nonempty sets has a choice function, which is (1).
Statements (1) and (3) therefore imply each other over ZF and are equivalent.
Statements (1) and (2) are equivalent over ZF by [L3].
Equivalence is transitive, so (1), (2) and (3) are equivalent over ZF.
Remarks
What this licenses. Any later result may be proved with whichever of the three forms is convenient, at exactly the same cost. Applications that build an object stage by stage naturally use (3) through Transfinite recursion; applications that maximise something naturally use (2); applications about products of nonempty sets use (1).
What is not proved here. That any of the three is independent of ZF. That requires Gödel's constructible universe for the consistency of the Axiom of Choice with ZF (Gödel 1938: ZF does not refute the Axiom of Choice ‡) and Cohen's forcing for the consistency of its negation (Cohen 1963: ZF does not prove the Axiom of Choice ‡), neither of which this library contains: both are recorded with references and are not proved anywhere here. The honest conditional statements are FALSE: Zorn's lemma is a theorem of ZF and FALSE: the well-ordering theorem is a theorem of ZF.
Strictly weaker principles get no information from this. The equivalence says nothing about the ultrafilter lemma, dependent choice or countable choice. Each of those is, if ZF is consistent, strictly weaker than the Axiom of Choice: not provable in ZF, and not strong enough to recover AC. Those separations are external metamathematical results, established by forcing and by permutation models, quoted from references and proved nowhere in this library; the consistency hypothesis cannot be dropped and cannot be proved inside ZF. Every theorem in this library that uses one of the weaker principles must say which, and the ledger, with the sources, is The choice ledger: what costs the Axiom of Choice and what does not.
Historical note. Zermelo proved (1) implies (3) in 1904, Kuratowski and Zorn isolated (2) in 1922 and 1935, and the circle of equivalences was standard by the 1940s. The choice-free content of the theory of well-orders, by contrast, was settled earlier: Hartogs proved in 1915 that cardinal comparability implies (3), which is what makes Hartogs: an ordinal that does not inject into a given set a choice-free theorem worth isolating.
Depends on
Used by
- FALSE: the well-ordering theorem is a theorem of ZF False statement
- The choice ledger: what costs the Axiom of Choice and what does not Remark
- Comparability of arbitrary sets, that any two sets admit an injection one way or the other, is equivalent to the Axiom of Choice Theorem
- Tarski: the Axiom of Choice is equivalent to the statement that A × A ≈ A for every infinite set A, so extending Hessenberg's theorem from the alephs to arbitrary sets is exactly as strong as choice Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 20 results over 5 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Axiom of choice (Wikipedia) (standard reference, not scraped)
- Well-ordering theorem (Wikipedia) (standard reference, not scraped)
- The Well-Ordering Problem (Open Logic Project) (standard reference, not scraped)
- The Axiom of Choice (Stanford Encyclopedia of Philosophy) (standard reference, not scraped)