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.
The Axiom of Choice and Zorn's lemma are equivalent
Statement
Over ZF, the Axiom of Choice (The Axiom of Choice) and Zorn's lemma (Zorn's lemma) are equivalent: each implies the other.
Facts & Assumptions
Given: The axioms of ZF.
The Axiom of Choice implies Zorn's lemma (Zorn's lemma).
Zorn's lemma implies the Axiom of Choice (Zorn's lemma implies the Axiom of Choice).
Proof
Assuming the Axiom of Choice, every nonempty poset in which each chain has an upper bound has a maximal element, which is Zorn's lemma.
Assuming Zorn's lemma, every family of nonempty sets has a choice function, which is the Axiom of Choice.
Each statement implies the other over ZF, so they are equivalent.
Remarks
- This is the item later pages cite when they want to use either form without re-arguing the passage between them. The ultrafilter lemma (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter ↗) uses the Zorn form; results about products of nonempty sets use the choice-function form.
- Equivalence is over ZF, and it is a genuine two-way implication proved here. It does not by itself decide whether either equivalent statement is a theorem of ZF.
- Because the two are equivalent, a theorem proved with Zorn's lemma costs at most the Axiom of Choice. The equivalence gives an upper bound on the proof, not a lower bound on the theorem. The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter ↗ is the standing example: the proof supplied here routes through Zorn, while The proved choice cost of the ultrafilter lemma ↗ deliberately makes no unproved claim about the least choice principle sufficient for the statement.
Depends on
Used by
- Choice, Zorn and well-ordering are equivalent Corollary
- The proved choice cost of the ultrafilter lemma Remark
- The proved choice ledger: hypotheses, equivalences, and upper bounds Remark
- Alexander's subbase lemma: if every cover by members of a fixed subbasis has a finite subcover then the space is compact; the proof is an application of Zorn's lemma Theorem
Dependency tree · two levels
9 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
- Encyclopedia of Mathematics, Zorn lemma (standard reference, not scraped)
- I. Khatchatourian, The Axiom of Choice (University of Toronto MAT327 notes) (standard reference, not scraped)
- Zorn's lemma (Wikipedia) (standard reference, not scraped)
- Axiom of choice (Wikipedia) (standard reference, not scraped)