100 years of Zermelo's axiom of choice: What was the problem with it? (2006)

Foundations, Categories, and the Role of AC

• One framing: ZFC’s axiom of choice (AC) is equivalent to “every surjection in Set splits” (admits a section), unlike in Top where many surjections lack continuous splittings.
• Independence results are presented as: besides Set (ZFC), there are other categories/models (ZF without AC, NFU, constructive systems) where some surjections don’t split, and that is just “a different game.”
• Category theory is seen as a way to compare such “games” via functors, without insisting on a single absolute notion of set-theoretic truth.

Formalism vs Constructivism vs Platonism

• One camp emphasizes axioms as “rules of a game”: results like “there are more reals than naturals” are true relative to classical ZF(C), not absolute eternal verities.
• Others push back, arguing that there are many consistent set theories (e.g. ones where the reals are countable or uncountable), and what’s eternal is that these systems have the consequences they do; which one we treat as “the” reals is historically contingent.
• Platonist voices insist there are objective mathematical truths beyond provability, invoking Gödel and real-world analogies (innocent people wrongly convicted).
• Constructivists stress that existence should mean “there is a construction/computation,” and uncountability is better understood as self-reference/limits of computation than as “more things.”

Cantor’s Diagonal, Countability, and Alternative Systems

• Discussion of variants of Cantor’s argument: in some systems (NFU, certain constructive schools) key steps fail or are reinterpreted, so one can accept diagonalization yet not conclude “more reals than naturals.”
• Russian constructivism: internally, the function space N→Bool can again be “uncountable” in an internal sense, even though externally only countably many computable functions exist.
• NFU + additional axioms can make the continuum countable or uncountable; in such settings the (un)countability of reals is independent.
• Several comments emphasize the need to distinguish “truth in a model” vs “provability from axioms.”

Induction, Choice, and Proof Strength

• Dropping induction (Peano → Robinson arithmetic) yields more models and weaker proof power; proofs can become exponentially longer.
• Countable choice and induction are seen as relatively uncontroversial; the tension is with uncountable choice, which leads to nonconstructive and counterintuitive results.
• AC is linked to nonconstructive existence proofs and to the law of excluded middle in intuitionistic settings.

Constructive AC, Type Theory, and HoTT

• In constructive type theory, the “naïve” reading of AC (Π–Σ distribution) is trivial and not the classical AC.
• Martin-Löf’s setoid-based reading recovers something like classical AC via an extensional choice function; that’s where strength enters.
• In Homotopy Type Theory, AC is reformulated using propositional truncation; Zermelo-style global choice is too strong and clashes with univalence.
• On HoTT as foundations: logicians and type theorists see it as a major conceptual advance; some mainstream mathematicians are skeptical of its practical payoff so far.

Explaining the Axiom of Choice and Its Consequences

• Multiple ELI5-style explanations:
  • AC asserts the existence of a “choice function” picking one element from each set in an arbitrary family (possibly infinitely many, no canonical rule).
  • Equivalent formulation: the Cartesian product of a family of nonempty sets is nonempty.
  • Russell’s socks vs shoes: shoes have a canonical left/right rule; indistinguishable socks require AC.
• Banach–Tarski is cited as a dramatic consequence: decomposing a ball into finitely many non-measurable pieces and reassembling into two balls of the same size, relying crucially on AC and pathological, nonconstructible sets.