Axiom of Choice

Statement

Axiom of Choice (AC): For any set $A$ of nonempty sets there exists a choice function $f : A \to \bigcup A$ satisfying $f(S) \in S$ for every $S \in A$.

The three statements below are equivalent (provably so in ZF without Choice):

1. AC — choice functions exist.
2. Zorn's Lemma — every chain-bounded nonempty poset has a maximal element.
3. Well-Ordering Theorem — every set can be well-ordered.

Visualization

Choice from a family of shoes vs. socks:

Hilbert's informal picture: for infinitely many pairs of shoes, you can choose the left shoe from each pair without AC (it is a definable rule). For infinitely many pairs of socks (identical), you need AC — there is no rule to distinguish elements, so you must postulate the choice function.

Zorn ↔ AC (one direction):

Given a collection $\mathcal{F}$ of functions (partial choice functions on subsets of $A$), ordered by extension, every chain has an upper bound (their union). By Zorn there is a maximal partial choice function $f^*$; if its domain were not all of $A$, we could extend it (using a single choice), contradicting maximality. So $f^*$ is a full choice function.

Equivalences and Consequences

Consequence	Proof route
Every vector space has a basis	Zorn on the poset of linearly independent sets
Every ring has a maximal ideal	Zorn on proper ideals ordered by inclusion
Every field has an algebraic closure	Zorn + transfinite extension
Tychonoff's TheoremTychonoff's Theorem$$\prod_{i \in I} X_i \text{ compact} \iff \forall i,\; X_i \text{ compact}$$An arbitrary product of compact spaces is compact in the product topologyRead more →	AC (Tychonoff ↔ AC)
Zorn's LemmaZorn's Lemma$$\text{every chain bounded} \implies \exists\text{ maximal element}$$If every chain in a nonempty poset has an upper bound, the poset has a maximal element.Read more →	Direct equivalence with AC
Well-ordering of $\mathbb{R}$	WOT (non-constructive, AC equivalent)

Proof Sketch (Zorn $\Rightarrow$ AC)

1. Let $A = \{S_i\}$ be a family of nonempty sets. Consider the poset $\mathcal{P}$ of all partial choice functions: pairs $(B, f)$ with $B \subseteq A$ and $f : B \to \bigcup A$, $f(S) \in S$ for all $S \in B$.
2. Order $\mathcal{P}$ by $(B, f) \le (B', f')$ iff $B \subseteq B'$ and $f' \restriction_B = f$.
3. Every chain $(B_\alpha, f_\alpha)$ in $\mathcal{P}$ has upper bound $(\bigcup B_\alpha, \bigcup f_\alpha)$ (compatible functions on a chain have a consistent union).
4. By Zorn's lemma, there exists a maximal $(B^*, f^*)$.
5. If $B^* \neq A$, pick $S \in A \setminus B^*$ and any $x \in S$; extend $f^*$ to $B^* \cup \{S\}$ by $f^*(S) = x$ — contradicting maximality. Hence $B^* = A$ and $f^*$ is a total choice function.

Connections

• Zorn's LemmaZorn's Lemma$$\text{every chain bounded} \implies \exists\text{ maximal element}$$If every chain in a nonempty poset has an upper bound, the poset has a maximal element.Read more → — direct equivalence; Zorn is often the most convenient form for algebra
• Well-Ordering TheoremWell-Ordering Theorem$$\forall X,\ \exists\, \le_X,\ (X, \le_X) \text{ is well-ordered}$$Every set can be well-ordered: given AC, every set admits a relation under which every nonempty subset has a minimum.Read more → — equivalent to AC; implies every cardinal is an aleph
• Tychonoff's TheoremTychonoff's Theorem$$\prod_{i \in I} X_i \text{ compact} \iff \forall i,\; X_i \text{ compact}$$An arbitrary product of compact spaces is compact in the product topologyRead more → — product of compact spaces is compact; equivalent to AC in full generality
• Cantor's TheoremCantor's Theorem$$|X| < |2^X|$$Every set is strictly smaller than its power set: |X| < |2^X| for any set X.Read more → — cardinality strict inequalities hold independently of AC, but cardinal arithmetic relies on AC for linearity of $\le_\text{card}$

import Mathlib.Order.Zorn
import Mathlib.Logic.Choice

/-- The Axiom of Choice is a global axiom in Lean/Mathlib via `Classical.choice`.
    Every nonempty type has an element. -/
theorem choice_nonempty {α : Sort*} [h : Nonempty α] : α :=
  Classical.choice h

/-- Zorn's lemma in Mathlib (`zorn_le`) is proved from `Classical.choice`.
    Direction: Zorn ⊢ for any chain-bounded nonempty poset, a maximal element exists. -/
theorem zorns_lemma_from_choice {α : Type*} [PartialOrder α]
    (h : ∀ c : Set α, IsChain (· ≤ ·) c → BddAbove c) : ∃ m : α, IsMax m :=
  zorn_le h

/-- One direction of AC ↔ Zorn: existence of choice functions.
    For a family of nonempty sets (here modelled as a type with Nonempty instances),
    Classical.choice provides the choice function definitionally. -/
theorem ac_choice_function {ι : Type*} (S : ι → Type*) [∀ i, Nonempty (S i)] :
    ∃ f : ∀ i, S i, True :=
  ⟨fun i => Classical.choice (inferInstance), trivial⟩