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: ZF proves each of (1), (2), and (3) to follow from the others. The equivalence alone does not say that ZF proves any one of them outright.
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. No independence conclusion follows from an equivalence proof. Establishing models in which the equivalent principles hold or fail belongs to the later constructibility, forcing, and symmetric-model pages and is not a premise of this item.
Other principles get no information from this. The equivalence says nothing about the ultrafilter lemma, dependent choice, or countable choice. Every theorem using one of those principles must state the actual hypothesis; the locally established implication ledger is The proved choice ledger: hypotheses, equivalences, and upper bounds.
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
- The proved choice ledger: hypotheses, equivalences, and upper bounds 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 · two levels
13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on 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)