The Axiom of Choice

Suppose you have infinitely many nonempty boxes, each containing some socks. You want to pick exactly one sock from each box simultaneously. Can this always be done? If the boxes come with a rule — say, "always take the leftmost sock" — the answer is obviously yes. But suppose the boxes hold real numbers with no distinguished order. Or suppose they hold arbitrary sets with no internal structure at all. Then it is far from clear that a single simultaneous selection can be specified. The Axiom of Choice (AC) asserts that it can, always. This holds for any family of nonempty sets. It does not matter how large the family is. It does not matter how little structure the sets possess. This assertion looks innocuous — even "obviously true." Yet it turns out to be logically independent of the other axioms of set theory. It cannot be proved from them. Its negation cannot be proved from them either. This is one of the most important discoveries in the foundations of mathematics. It shows that ordinary set-theoretic reasoning does not settle every reasonable-sounding question. Mathematicians face a genuine choice about which universe of sets to work in. AC matters because enormous swaths of mathematics quietly depend on it. Every vector space has a basis. Every ring has a maximal ideal. Every set can be well-ordered. Tychonoff's theorem holds for arbitrary products of compact spaces. All of these are equivalent to or consequences of AC. Without it, some of these statements provably fail. With it, they hold unconditionally. But so do some famously strange consequences. One example is the Banach–Tarski decomposition. This splits a ball into finitely many pieces. These pieces reassemble into two balls of the same size. This article gives the precise formal statement of AC. It is phrased in terms of choice functions and Cartesian products. The article proves its equivalence with the nonemptiness of infinite products. It discusses the theorem of Gödel and Cohen. This theorem establishes AC's independence from the Zermelo–Fraenkel axioms. The article situates AC among its most important reformulations. It previews Zorn's Lemma and the broader family of Equivalents and Consequences of Choice.

Key takeaways
  • AC says every family of nonempty sets has a choice function, selecting one element from each set simultaneously.
  • For finite families, AC is a theorem of The ZFC Axioms Overview; the content of AC is entirely about infinite families.
  • AC is equivalent to the statement that the Cartesian product of any family of nonempty sets is nonempty.
  • Gödel (1938) showed AC is consistent with ZF; Cohen (1963) showed ¬AC is consistent with ZF — so AC is independent of ZF.
  • Dropping AC breaks many familiar facts (every vector space has a basis, arbitrary products of compacts are compact), but AC also implies surprising consequences like Banach–Tarski.
  • Key idea: existence of an infinite simultaneous selection cannot in general be constructed — it must be postulated.

Where this lives today

AC (or its equivalents, foreshadowed here and developed under Equivalents and Consequences of Choice) underlies linear algebra's claim that every vector space has a basis, algebra's claim that every nonzero ring has a maximal ideal, and general topology's Tychonoff theorem that arbitrary products of compact spaces are compact. In Zorn's Lemma — the maximal-element reformulation of AC used constantly in algebra and analysis — the same existence-without-construction phenomenon appears in disguise, applied to partially ordered sets rather than families of nonempty sets directly. In measure theory and probability, AC produces the existence of non-measurable sets (e.g. Vitali sets) and the Banach–Tarski paradox, phenomena that vanish in "AC-free" models where every set of reals is Lebesgue measurable. In mathematical logic, AC (or fragments like Countable Choice or Dependent Choice) is needed to prove the compactness theorem and the equivalence of different formulations of first-order completeness in full generality. In computer science and constructive mathematics, the computational content of AC is scrutinized directly: type-theoretic foundations (e.g. Martin-Löf type theory) often validate a form of choice automatically (via the "axiom of choice is a theorem" phenomenon for dependent types), while other constructive frameworks explicitly reject unrestricted AC because it is non-computable in general — no algorithm outputs the required simultaneous selection for arbitrary families. In model theory and forcing constructions themselves (as in the independence theorem above), the presence or absence of AC is the primary dial set-theorists turn to build exotic models with prescribed cardinal-arithmetic or measure-theoretic behavior.

Ask the tutor: How does the Axiom of Choice translate into Zorn's Lemma, and why are they logically equivalent over ZF?

DefinitionChoice Function, and the Axiom of Choice

Let II be a set (an index set) and let {Ai}i∈I\{A_i\}_{i \in I} be an indexed family of sets, i.e. a function i↦Aii \mapsto A_i with domain II. Suppose Ai≠∅A_i \neq \varnothing for every i∈Ii \in I. A choice function for the family {Ai}i∈I\{A_i\}_{i\in I} is a function

f:I→⋃i∈IAif : I \to \bigcup_{i \in I} A_i

such that f(i)∈Aif(i) \in A_i for every i∈Ii \in I. Equivalently, treating {Ai}i∈I\{A_i\}_{i\in I} as a set F\mathcal{F} of nonempty sets (allowing repeated appearance to be handled via indexing), a choice function for F\mathcal{F} is a function f:F→⋃Ff : \mathcal{F} \to \bigcup \mathcal{F} with f(A)∈Af(A) \in A for every A∈FA \in \mathcal{F}.

Axiom of Choice (AC). For every family {Ai}i∈I\{A_i\}_{i \in I} of nonempty sets, there exists a choice function for the family. Formally:

∀I  ∀{Ai}i∈I  [(∀i∈I, Ai≠∅)→∃f(f:I→⋃i∈IAi ∧ ∀i∈I, f(i)∈Ai)].\forall I \; \forall \{A_i\}_{i\in I}\; \Big[ \big(\forall i \in I,\ A_i \neq \varnothing\big) \rightarrow \exists f \Big( f : I \to \bigcup_{i\in I} A_i \ \wedge\ \forall i \in I,\ f(i) \in A_i \Big) \Big].

The Cartesian product of the family {Ai}i∈I\{A_i\}_{i\in I} is defined as

∏i∈IAi:={f:I→⋃i∈IAi | ∀i∈I, f(i)∈Ai},\prod_{i\in I} A_i := \left\{ f : I \to \bigcup_{i\in I} A_i \ \middle|\ \forall i \in I,\ f(i)\in A_i \right\},

so that a choice function for {Ai}i∈I\{A_i\}_{i\in I} is precisely an element of ∏i∈IAi\prod_{i \in I} A_i.

Intuition

Think of II as a (possibly infinite, possibly uncountable) index set labeling a shelf of boxes, and AiA_i as the nonempty contents of box ii. A choice function is a single rule ff that, fed the label ii, hands back one item from box ii — and it must do this for every box at once, consistently, as a genuine function with domain all of II. When II is finite, this is not controversial: one can choose an element from A1A_1, then from A2A_2, and so on, in finitely many steps, and the Pairing, Union, and Replacement axioms let you assemble these finitely many choices into a single function. The trouble is genuinely infinitary. If II is infinite, "choose one element, then another, then another, forever" is not a finite procedure and does not by itself produce a set — the other axioms of ZF (Extensionality, Pairing, Union, Power Set, Infinity, Replacement, Separation, Foundation, Regularity) do not guarantee that the totality of all these choices, made "simultaneously," exists as a completed function. Whenever the sets AiA_i come equipped with some canonical rule — e.g., Ai⊆NA_i \subseteq \mathbb{N} nonempty, choose the least element by well-ordering of N\mathbb{N} — no extra axiom is needed, because the rule is an explicit definition of ff, and Separation/Replacement build ff for you. AC is needed exactly when no such uniform definable rule is available, e.g. when each AiA_i is an arbitrary nonempty subset of R\mathbb{R} with no distinguished point. The picture below shows finitely many boxes with an explicit rule (leftmost point) versus infinitely many "unstructured" boxes, where AC is invoked to assert — without giving an explicit recipe — that a simultaneous selection nonetheless exists.

Figure
Choice functions: definable rule vs. AC-postulated existence
Case 1: A_i ⊆ ℕ nonempty — choose least element (no AC needed) 3,7,9 2,4 5,6,8,11 f(i) = min(A_i) Case 2: A_i ⊆ ℝ nonempty, arbitrary — AC postulates f exists … (0, 1)\{1/2} irrationals ∩ [3,4] unmeasurable set ? ? ? AC: ∃ f with f(i) ∈ A_i for all i, though no explicit formula for f is given.

Definition recap and the product formulation

We now make precise the equivalence promised in the overview between AC and nonemptiness of arbitrary products.

TheoremAC ⟺ Nonemptiness of Arbitrary Products

The following two statements are equivalent, over the base theory ZF (Zermelo–Fraenkel set theory without Choice):

(1) (Axiom of Choice) For every family {Ai}i∈I\{A_i\}_{i \in I} of nonempty sets indexed by a set II, there is a choice function f:I→⋃i∈IAif: I \to \bigcup_{i\in I} A_i with f(i)∈Aif(i) \in A_i for all i∈Ii \in I.

(2) (Nonemptiness of products) For every family {Ai}i∈I\{A_i\}_{i\in I} of nonempty sets indexed by a set II, the Cartesian product ∏i∈IAi\prod_{i\in I} A_i is nonempty.

Proof

We show (1) ⇒\Rightarrow (2) and (2) ⇒\Rightarrow (1); together with the definitions this gives logical equivalence, working entirely within ZF (all constructions below use only Pairing, Union, Power Set, Separation, and Replacement, which are available in ZF).

(1⇒21 \Rightarrow 2). Assume AC and let {Ai}i∈I\{A_i\}_{i\in I} be a family of nonempty sets. By AC there is a choice function f:I→⋃i∈IAif : I \to \bigcup_{i\in I} A_i with f(i)∈Aif(i) \in A_i for every i∈Ii \in I. By definition, ∏i∈IAi\prod_{i \in I} A_i is exactly the set of functions g:I→⋃i∈IAig : I \to \bigcup_{i \in I} A_i such that g(i)∈Aig(i) \in A_i for all ii. Since ff satisfies this defining property, f∈∏i∈IAif \in \prod_{i\in I} A_i. Hence ∏i∈IAi≠∅\prod_{i\in I} A_i \neq \varnothing.

(2⇒12 \Rightarrow 1). Assume that every product of a family of nonempty sets is nonempty, and let {Ai}i∈I\{A_i\}_{i\in I} be an arbitrary family of nonempty sets. Form ∏i∈IAi\prod_{i \in I} A_i; by hypothesis it is nonempty, so it contains some element ff. By definition of the product, ff is a function with domain II satisfying f(i)∈Aif(i) \in A_i for every i∈Ii \in I. This ff is precisely a choice function for the family {Ai}i∈I\{A_i\}_{i\in I}. Since the family was arbitrary, AC holds. Both directions used only the definitions of "choice function" and "Cartesian product," which are formalizable in ZF using Separation (to carve out ⋃i∈IAi\bigcup_{i\in I} A_i inside a power set of I×⋃iAiI \times \bigcup_i A_i, itself formed via Union and Power Set applied to the AiA_i, which exist as a set-indexed family by Replacement) — no instance of Choice was smuggled in. Hence (1) and (2) are equivalent over ZF. ■\blacksquare

∎
LemmaAC restricted to finite index sets is a ZF theorem

If II is finite and {Ai}i∈I\{A_i\}_{i \in I} is a family of nonempty sets, then ZF alone (without AC) proves the existence of a choice function for the family.

Proof

By induction on n=∣I∣n = |I|. If n=0n = 0, I=∅I = \varnothing and the empty function f=∅f = \varnothing vacuously satisfies "f(i)∈Aif(i) \in A_i for all i∈Ii \in I," and it is a well-defined function I→⋃iAi=∅I \to \bigcup_{i} A_i = \varnothing (with codomain vacuously correct), so it is a choice function. This uses only the definition of function as a set of ordered pairs, available in ZF. Suppose the claim holds for index sets of size nn, and let I=I0∪{in}I = I_0 \cup \{i_n\} with ∣I0∣=n|I_0| = n and in∉I0i_n \notin I_0. By inductive hypothesis, ZF proves there is a choice function f0f_0 for {Ai}i∈I0\{A_i\}_{i \in I_0}. Since Ain≠∅A_{i_n} \neq \varnothing (given as a hypothesis of the family), by the axiom of Extensionality and the definition of ≠∅\neq \varnothing, there exists some element a∈Aina \in A_{i_n}; this existential instantiation for a single set is a direct application of first-order logic together with the hypothesis "Ain≠∅A_{i_n}\neq\varnothing," requiring no choice principle, since we are only asserting the existence of one witness for one set, not simultaneously for infinitely many. Define f=f0∪{(in,a)}f = f_0 \cup \{(i_n, a)\}; by Pairing and Union this is a set, and one checks directly it is a function on I0∪{in}=II_0 \cup \{i_n\} = I with f(i)∈Aif(i) \in A_i for all i∈Ii \in I. This completes the induction. ■\blacksquare

∎

This lemma is the precise sense in which AC "adds nothing" for finite families: the genuinely new content of AC is the assertion for infinite (in particular uncountable) index sets, where the inductive argument above has no finite stopping point and cannot be carried out by finitely many applications of "there exists a witness."

Worked examples

Example 1 — a family where no choice function is definable without AC. Let I=RI = \mathbb{R} and for each r∈Ir \in I let

Ar={S⊆Q:S is a nonempty bounded set with sup⁡S=r}.A_r = \{ S \subseteq \mathbb{Q} : S \text{ is a nonempty bounded set with } \sup S = r \}.

Each ArA_r is a set of sets of rationals whose supremum is exactly rr; since Q\mathbb{Q} is dense in R\mathbb{R}, for every real rr there exist nonempty bounded sets of rationals with supremum rr (e.g. an increasing sequence of rationals converging to rr from below, together possibly with rr itself if r∈Qr \in \mathbb{Q}), so Ar≠∅A_r \neq \varnothing for every rr. There is no uniform explicit definition in the ordinary sense picking out one specific element of ArA_r for each real rr simultaneously, because the elements of ArA_r are themselves arbitrary infinite subsets of Q\mathbb{Q} with no canonical "smallest" or "largest" one (unlike Example nonexistent-canonical-element cases such as subsets of N\mathbb{N}, where least element gives a definable choice). AC asserts nonetheless that a choice function ff with f(r)∈Arf(r) \in A_r for every r∈Rr \in \mathbb{R} exists as a set, even though no such ff can be written down by an explicit formula. This is the paradigmatic situation AC is designed to cover: existence without construction.

Example 2 — an explicit choice function requiring no AC, contrasted with a variant that does. Let I=NI = \mathbb{N} and let Bn={k∈Z:k≡n(mod7), k>0}B_n = \{ k \in \mathbb{Z} : k \equiv n \pmod{7},\ k > 0\} for each n∈{0,1,…,6}n \in \{0,1,\dots,6\}, extended periodically so I=NI = \mathbb{N} indexes BnB_n for n∈Nn \in \mathbb{N} via Bn:={k∈Z+:k≡(n  7)}B_n := \{k \in \mathbb{Z}^+ : k \equiv (n \bmod 7)\}. Each BnB_n is a nonempty subset of Z+\mathbb{Z}^+ (it is infinite, and nonempty since e.g. n  7n \bmod 7 itself, or 77 if the residue is 00, lies in it). Define f(n)=min⁡Bnf(n) = \min B_n. This uses the well-ordering of Z+\mathbb{Z}^+, a ZF-provable fact (every nonempty subset of N\mathbb{N} has a least element, by the definition of the natural numbers and induction), so ff is an explicit ZF-definable choice function; no AC is needed here. Now modify the family: let Cn=R∖{q1,…,qn}C_n = \mathbb{R} \setminus \{q_1, \dots, q_n\} for a fixed enumeration q1,q2,…q_1, q_2, \dots of Q\mathbb{Q} (which exists by ZF, since Q\mathbb{Q} is countable and this uses only one arbitrary enumeration, fixed once, not infinitely many simultaneous choices). Each CnC_n is nonempty (removing finitely many points from R\mathbb{R} leaves uncountably many). This still admits an explicit choice, e.g. f(n)=f(n) = the least element of Cn∩NC_n \cap \mathbb{N} that is not among q1,…,qnq_1,\dots,q_n — again ZF-definable via well-ordering of N\mathbb{N}, no AC needed. To manufacture a genuine AC-requiring case one must remove all definable handles, as in Example 1: index by an uncountable, unstructured parameter and choose from sets with no canonical distinguished point (no least element, no algebraic description), which is exactly why Example 1's family of "sets of rationals with given real supremum" — rather than subsets of N\mathbb{N} or finite modifications of R\mathbb{R} — is the right kind of example to show AC's necessity.

Independence from ZF

TheoremIndependence of AC from ZF (Gödel–Cohen)

Assume ZF is consistent (has a model). Then:

(a) (Gödel, 1938–1940) ZF + AC is consistent. That is, if ZF has a model, then ZF + AC has a model. Equivalently, ZF does not prove ¬AC\neg\mathrm{AC}.

(b) (Cohen, 1963) ZF + ¬\negAC is consistent. That is, if ZF has a model, then ZF + ¬\negAC has a model. Equivalently, ZF does not prove AC. Consequently, AC is independent of ZF: neither AC nor its negation is a theorem of ZF (assuming ZF is consistent).

Proof

We give the logical structure and the method of each half; a full construction of the models is a substantial undertaking belonging to advanced set theory (forcing and inner model theory), and is cited here as the standard result, with the proof technique named precisely, rather than reproduced in full — this is explicitly flagged as beyond the scope of this article, in accordance with the convention of citing landmark independence proofs by method.

(a) Gödel's constructible universe LL. Gödel defines, inside any model VV of ZF, a transitive class LL (the constructible universe) by transfinite recursion:

L0=∅,Lα+1=Def(Lα),Lλ=⋃α<λLα for limit λ,L=⋃α∈OrdLα,L_0 = \varnothing, \qquad L_{\alpha+1} = \mathrm{Def}(L_\alpha), \qquad L_\lambda = \bigcup_{\alpha<\lambda} L_\alpha \text{ for limit } \lambda, \qquad L = \bigcup_{\alpha \in \mathrm{Ord}} L_\alpha,

where Def(Lα)\mathrm{Def}(L_\alpha) is the set of subsets of LαL_\alpha definable over (Lα,∈)(L_\alpha, \in) by a first-order formula with parameters from LαL_\alpha. One proves, by induction on rank using the recursion theorem for well-founded relations (an inner model construction), that:

  • LL satisfies every axiom of ZF (Extensionality, Foundation, Pairing, Union, Power Set, Infinity, Separation, Replacement all relativize correctly to LL, a lengthy but mechanical verification);
  • LL satisfies a global well-ordering principle definable from the recursion itself (each LαL_\alpha is well-ordered compatibly with the construction, and every set in LL enters at some stage LαL_\alpha), yielding a definable well-ordering of LL;
  • a definable well-ordering of the universe of a model of ZF implies AC in that model, since one can then well-order any nonempty set AiA_i and choose its least element uniformly.

Hence L⊨ZF+ACL \models \mathrm{ZF} + \mathrm{AC}. If V⊨ZFV \models \mathrm{ZF}, then its constructible submodel LL also satisfies ZF (by the mechanical verification above) and additionally satisfies AC (by the definable well-ordering). Thus ZF consistent ⇒\Rightarrow ZF+AC consistent. Method: inner models (Gödel's constructibility).

(b) Cohen's forcing. Cohen starts from a countable transitive model MM of ZF and constructs a generic extension M[G]M[G] by adjoining a "generic" object GG built from a partially ordered set of forcing conditions, together with a genericity filter meeting all dense sets in MM (obtained via a Rasiowa–Sikorski style enumeration argument, since MM is countable). The key technical results (the Forcing Theorem) show:

  • M[G]M[G] satisfies all axioms of ZF, because the forcing relation ⊩\Vdash is definable in MM and one verifies, axiom by axiom, that ZF's axioms are forced;
  • by choosing the forcing poset to adjoin infinitely many "indiscernible" generic reals (or generic subsets) with no definable way to distinguish or select among them — e.g. Cohen's original construction adjoins an infinite set of "generic" reals permuted by a group of automorphisms of the forcing poset, and passes to the submodel of sets fixed by finite-support automorphisms (the Fraenkel–Mostowski–Cohen method, adapted from permutation models to genuine ZF models via forcing) — one arranges that in M[G]M[G] there is an infinite family of nonempty sets (e.g. an indexed family related to that generic set of reals) admitting no choice function;
  • hence M[G]⊨ZF+¬ACM[G] \models \mathrm{ZF} + \neg\mathrm{AC}.

Thus ZF consistent ⇒\Rightarrow ZF+¬\negAC consistent. Method: forcing with a symmetric submodel.

Conclusion. By (a), if ZF is consistent then so is ZF+AC, so ZF cannot prove ¬\negAC (else ZF+AC would prove a contradiction, making ZF+AC — hence ZF, by (a)'s construction sitting inside any model of ZF — inconsistent, contradicting consistency of ZF+AC). By (b), symmetrically, ZF cannot prove AC. Hence AC is independent of ZF. ■\blacksquare This proof is non-circular: it does not invoke AC anywhere in the meta-theoretic construction of LL or of M[G]M[G] as ZF-models; both constructions are carried out in ZF (or a weak fragment of it) applied to an assumed model, exactly the technique required to prove an independence result.

∎
CorollaryAC is not a theorem of ZF, nor is its negation

If ZF is consistent, AC is neither provable nor refutable from the ZF axioms alone; equivalently, ZF + AC and ZF + ¬\negAC are both consistent theories, and the choice of whether to adopt AC is a genuine axiomatic decision, not a matter that follows from more basic set-theoretic principles.

Proof

Immediate restatement of the Theorem's conclusion, by the standard equivalence (in a consistent, sufficiently strong theory TT) between "TT does not prove φ\varphi" and "T+¬φT + \neg\varphi is consistent," and symmetrically for ¬φ\neg\varphi. Both directions were established in the Theorem. ■\blacksquare

∎
CounterexampleWhy "nonempty sets" cannot be replaced by "sets" (empty sets break AC trivially) — and why "arbitrary" cannot be dropped in favor of "definable"

The nonemptiness hypothesis on each AiA_i cannot be dropped: if some Ai0=∅A_{i_0} = \varnothing, there can be no function ff with f(i0)∈Ai0=∅f(i_0) \in A_{i_0} = \varnothing, since no element lies in ∅\varnothing at all — the very statement "f(i0)∈∅f(i_0) \in \varnothing" is unsatisfiable regardless of any choice principle. So the theorem's hypothesis "Ai≠∅A_i \neq \varnothing for every ii" is not a cosmetic simplification; it is logically indispensable, and this is a ZF-level fact requiring no independence discussion at all. More substantively, consider weakening AC to "Definable Choice": for every family {Ai}i∈I\{A_i\}_{i \in I} of nonempty sets such that some first-order formula φ(i,x)\varphi(i, x) (with parameters in a fixed countable set) picks out, for each ii, a unique x∈Aix \in A_i with φ(i,x)\varphi(i,x), there is a choice function. This weakened principle is in fact a theorem of ZF (via Separation and Replacement applied to the formula φ\varphi), and it is strictly weaker than full AC. To see the gap is real, consider the family from Worked Example 1: Ar={S⊆Q:sup⁡S=r}A_r = \{S \subseteq \mathbb{Q} : \sup S = r\} for r∈Rr \in \mathbb{R}. In a model of ZF + ¬\negAC constructed via Cohen's method restricted to reals with no definable well-ordering of R\mathbb{R} (such models exist by part (b) of the independence theorem, adapted to give "R\mathbb{R} has no well-ordering" as the failure of choice), there is no formula φ(r,S)\varphi(r,S) uniformly picking out a single S∈ArS \in A_r for every real rr — because any such uniform definable rule would, combined with the well-ordering of Q\mathbb{Q}'s finite subsets by length-then-lexicographic order, yield a definable well-ordering of R\mathbb{R} itself, contradicting the construction of that model. Hence "Definable Choice" is a strictly weaker, genuinely different, and provable-in-ZF principle, while full AC — quantifying over all families, definable or not — is not provable in ZF. This exhibits precisely why "arbitrary" in the statement of AC cannot be replaced by "definable" without changing the theorem's content.

Scope, edge cases & common traps

SituationWhat holdsNeeds AC?
II finiteChoice function existsNo (ZF, by induction)
II countably infinite, each Ai⊆NA_i \subseteq \mathbb{N}Choice function exists (take min)No (ZF; well-ordering of N\mathbb{N})
II countably infinite, each AiA_i arbitrary nonempty setChoice function existence is not ZF-provable in generalYes, in general (Countable Choice, a strictly weaker fragment of AC, is independent of ZF too)
II arbitrary, each AiA_i nonempty subset of a fixed well-ordered setChoice function exists (take least element)No (well-ordering supplies the rule)
II arbitrary, each AiA_i arbitrary nonempty set, no canonical structureChoice function existenceYes — this is exactly the content of full AC
Product of family of nonempty sets is nonemptyEquivalent to AC (proved above)Yes, in general

The mathematician behind it

Origins · 1 minErnst Zermelo and how this was discovered
EZ
Ernst Zermelo
1871–1953 · Foundations of set theory, Göttingen and Zurich

Ernst Zermelo formulated the Axiom of Choice explicitly in 1904 in order to prove that every set can be well-ordered — the Well-Ordering Theorem — settling a question Cantor had struggled with. His 1908 paper gave the first axiomatization of set theory (later extended by Fraenkel and Skolem into what is now ZFC), explicitly isolating AC as a distinct principle whose use, he argued, was already implicit throughout existing mathematical practice, even where mathematicians had not noticed they were invoking it.

History
- 1904 — Zermelo publishes his proof of the Well-Ordering Theorem, introducing AC explicitly as a needed principle.
- 1908 — Zermelo publishes the first axiomatic system for set theory, with AC as one axiom among several.
- 1922 — Fraenkel and Skolem independently strengthen Zermelo's system with Replacement, yielding ZF (and ZFC with AC included).
- 1938–1940 — Gödel constructs LL and proves ZF + AC is consistent relative to ZF.
- 1963 — Paul Cohen invents forcing and proves ZF + ¬\negAC is consistent relative to ZF, establishing full independence.
Is the Axiom of Choice "true"?

Truth of an independent axiom is not settled by proof from more basic principles — that is exactly what independence means. Mathematicians generally accept AC as part of the standard axiom system ZFC because it is intuitively plausible, indispensable for large parts of ordinary mathematics (algebra, analysis, topology), and known to be consistent relative to ZF by Gödel's theorem, so adopting it introduces no new risk of contradiction beyond that already present in ZF itself. Some areas (measure theory, constructive mathematics, computer science) deliberately work without full AC, or with weaker choice principles, because AC's nonconstructive consequences (like non-measurable sets) are undesirable there. So "true" is best replaced by "adopted, for good structural reasons, in the standard foundational convention."

Why isn't AC just provable from Zermelo's other axioms?

Because the other ZF axioms (Extensionality, Pairing, Union, Power Set, Infinity, Separation, Replacement, Foundation) only ever assert the existence of sets built by explicit, definable operations from given sets — unions, subsets carved out by a formula, images under definable functions, and so on. None of them provide a mechanism to assemble an infinite, simultaneous, uniform selection across a family with no shared definable selection rule. Gödel's and Cohen's model constructions make this precise: there exist models of ZF (Cohen's symmetric extensions) where some infinite family of nonempty sets genuinely has no choice function at all, showing the other axioms are simply too weak to force one into existence.

What is the difference between AC, Countable Choice, and Dependent Choice?

Full AC applies to families indexed by an arbitrary set, of arbitrary cardinality. Countable Choice (CC) restricts to countably infinite index sets. Dependent Choice (DC) is a further principle allowing recursively dependent choices (each choice may depend on the previous ones) along N\mathbb{N}-many steps. The strict implications AC⇒DC⇒CC\mathrm{AC} \Rightarrow \mathrm{DC} \Rightarrow \mathrm{CC} hold in ZF, and each implication is known to be strict (there are models separating them), so these are genuinely different strengths of choice principle, useful for calibrating exactly how much choice a given theorem (e.g. "every sequentially continuous function is continuous," which needs only CC) actually requires.

Does AC follow from, or imply, the Continuum Hypothesis?

No — AC and the Continuum Hypothesis (CH) are logically independent of each other as well as each independently independent of ZF. Cohen's forcing techniques (the same method used to show ZF + ¬AC is consistent) also show ZF + AC + ¬CH is consistent, and Gödel's constructible universe LL satisfies ZF + AC + CH. So all four combinations of (AC or ¬AC) with (CH or ¬CH) are separately realizable as consistent extensions of ZF, meaning neither principle decides the other.

What is a concrete "everyday" consequence of AC that mathematicians use constantly?

The statement "every vector space has a basis" is a direct and well-known equivalent-strength consequence of AC (indeed, "every vector space has a basis" is provably equivalent to AC over ZF). Without AC, it is consistent that some vector space (for instance, R\mathbb{R} regarded as a vector space over Q\mathbb{Q}) has no basis at all. Similarly "every ring has a maximal ideal," used throughout commutative algebra, is a Zorn's-Lemma consequence of AC and can fail without it.

Is AC needed to prove that every surjection has a right inverse (a section)?

Yes, in general, and this is one of the cleanest reformulations of AC. If g:X→Yg : X \to Y is a surjection, a right inverse is a function h:Y→Xh : Y \to X with g(h(y))=yg(h(y)) = y for all y∈Yy \in Y; constructing hh amounts to choosing, for each yy, some preimage h(y)∈g−1({y})h(y) \in g^{-1}(\{y\}), i.e. a choice function for the family {g−1({y})}y∈Y\{g^{-1}(\{y\})\}_{y \in Y} of nonempty sets. This statement ("every surjection has a section") is in fact equivalent to AC over ZF, and is often the most memorable way category-theoretically minded readers first encounter the axiom.

Why does Banach–Tarski need AC, and should that make us suspicious of AC?

The Banach–Tarski decomposition partitions a solid ball into finitely many pieces that can be reassembled (using only rigid motions) into two balls congruent to the original; the pieces constructed are necessarily non-measurable, and their existence relies on AC applied to orbits of a free group action on the sphere with no definable selection rule. It is a genuine, provable theorem of ZFC, not a paradox in the sense of an outright contradiction — it only seems paradoxical because it conflicts with intuitions about volume that implicitly assume measurability. Whether this should make one suspicious of AC is a matter of mathematical taste; most working mathematicians accept it as an acceptable price for the vastly larger convenience AC provides elsewhere.

Before this

Where this leads