Foundational Dependencies

What This Page Is

TheoremPath covers content from basic set theory through frontier ML research. Different parts of the site rest on different axiomatic foundations. This page maps which foundational system each branch depends on.

This is not a philosophy page. It is a practical reference: if you want to know whether a result on this site uses the axiom of choice, this tells you.

The Short Version

Almost everything mathematical on this site implicitly assumes ZFC (Zermelo-Fraenkel set theory with the axiom of choice). The exceptions are:

• Algorithms and computability: Peano arithmetic suffices
• Finite combinatorics: Peano arithmetic suffices
• Logic and proof theory: Can be formalized in weaker systems

The axiom of choice is specifically needed for:

• Measure theory (existence of non-measurable sets, extension theorems)
• Functional analysis (Hahn-Banach, Banach-Alaoglu, Tychonoff)
• Probability theory (existence of conditional expectations in full generality)
• Some results in topology (well-ordering, Zorn's lemma arguments)

Choice has levels

Most of "elementary" analysis does not actually need full AC. It needs dependent choice (DC): given a relation $R$ such that for every $x$ there exists $y$ with $xRy$, there is a sequence $(x_n)$ with $x_nRx_{n+1}$. DC is what justifies "pick a sequence converging to the supremum" arguments. ZF + DC is strictly weaker than ZFC and is the honest level for sequential real analysis, sigma-finite measure theory, and most of the probability we care about. Full AC is used for non-constructive existence results on uncountable index sets (Hahn-Banach extensions, ultrafilters, Tychonoff over arbitrary product, Vitali sets).

Detailed Map

Peano Arithmetic Is Enough For

Definition

Peano-sufficient content

The following site content can be formalized using only Peano arithmetic (or conservative extensions of it):

• Sorting algorithms, graph algorithms, dynamic programming
• P vs NP, computability, halting problem
• Godel's incompleteness theorems (these are ABOUT Peano arithmetic)
• Finite combinatorics (counting, binomial coefficients)
• Basic number theory
• Lambda calculus, type theory (the syntax and reduction rules)
• SAT/SMT (the decision problems themselves)

ZF + DC Is Enough For

Definition

ZF+DC-sufficient content

These results hold in ZF + dependent choice. Pure ZF (no choice at all) is too weak for sequential analysis. DC is the right level for almost all real analysis on separable spaces and probability on standard Borel spaces:

• Real analysis on separable metric spaces (sequential compactness, Bolzano-Weierstrass, etc.)
• Sigma-finite measure theory (Caratheodory extension, Lebesgue measure on $\mathbb{R}^n$)
• Probability on countable or standard Borel sample spaces
• Sigma-finite Radon-Nikodym (this is a DC argument, not full AC)
• Linear algebra over finite-dimensional spaces (no choice at all)
• Convex optimization in finite dimensions (no choice at all)
• Neural network computations on finite tensors (no choice at all)

The Axiom of Choice Is Needed For

Definition

Choice-dependent content

These results on the site specifically require the axiom of choice (or equivalents like Zorn's lemma or the well-ordering theorem):

• Hahn-Banach theorem: extending linear functionals on infinite-dimensional spaces. The finite-dimensional version is choice-free.
• Banach-Alaoglu theorem: weak-* compactness of the dual unit ball on a non-separable space. The separable case is provable in ZF + DC.
• Tychonoff's theorem over arbitrary index sets. Tychonoff is equivalent to AC (Kelley, 1950). Countable products are fine in ZF + DC.
• Existence of non-measurable sets: Vitali sets, Banach-Tarski. Provably independent of ZF + DC (Solovay, 1970).
• Lebesgue decomposition beyond sigma-finite: the unrestricted Radon-Nikodym theorem on arbitrary measure spaces needs full AC. The sigma-finite version, which is what probability and statistics actually use, is a DC argument.
• Hamel bases for $\mathbb{R}$ over $\mathbb{Q}$ and similar uncountable-dimensional bases. These appear in pathological counterexamples, not in practical RKHS theory. Separable RKHS uses orthonormal bases, which are constructive.
• Well-ordering of the reals: used in transfinite induction proofs in descriptive set theory.

The infrastructure claim is narrower than it looks. Probability on standard Borel spaces, the spaces that show up in ML, lives entirely in ZF + DC. Full AC mainly enters when textbooks state results in maximum generality (arbitrary measure spaces, non-separable Banach spaces, uncountable products) that the rest of this site never invokes.

What Practitioners Should Know

Proposition

For ML practitioners, ZFC is invisible

Statement

All computations performed by ML systems (gradient descent, matrix multiplication, sampling, optimization) involve finite objects and can in principle be carried out without the axiom of choice. The axiom of choice enters through the mathematical theory used to analyze these computations, not the computations themselves.

Intuition

When you train a neural network, you are manipulating finite-dimensional vectors on a finite-precision computer. No axiom of choice is involved in the computation. But when you prove that SGD converges to a local minimum, or that the generalization gap is bounded, you may invoke measure theory, functional analysis, or probability theory results that depend on ZFC.

report a correction →

Connection to Lean and Formal Verification

Lean 4 is built on the Calculus of Inductive Constructions (CIC), which is a different foundational system from ZFC. CIC is constructive by default (no law of excluded middle) but Lean's Mathlib adds classical axioms: Classical.choice, propositional extensionality, and quotient types. Together these give Mathlib roughly the strength of ZFC.

If TheoremPath content were formalized in Lean:

• Algorithms, type theory, and finite-dimensional linear algebra would work in pure constructive CIC.
• Real analysis would invoke Classical.choice (used in Mathlib's Mathlib.Topology.MetricSpace.Basic and Mathlib.Analysis.Normed.Module.HahnBanach.Extension).
• Sigma-finite measure theory (Mathlib.MeasureTheory.Decomposition.RadonNikodym) compiles with classical axioms but the underlying argument is at DC strength.
• The constructive subset of Mathlib is large and growing; see the Mathlib4 axiom audit (#print axioms) to check what any specific theorem actually uses.

Reverse Mathematics

The precise way to ask "which axioms does theorem $T$ need" is reverse mathematics, which classifies theorems by the minimal subsystem of second-order arithmetic that proves them. The standard hierarchy is $\mathrm{RCA}_0 \subset \mathrm{WKL}_0 \subset \mathrm{ACA}_0 \subset \mathrm{ATR}_0 \subset \Pi^1_1\text{-CA}_0$. Most analysis on this site lives in $\mathrm{ACA}_0$ or below. Simpson's Subsystems of Second Order Arithmetic (2nd ed., 2009) is the canonical reference. This site does not classify theorems at this granularity, but the framework is the right one to consult when the AC-or-not question matters.

Summary

• ZFC is the default foundation for the mathematical content on this site, but most of it lives at the strictly weaker level of ZF + dependent choice.
• Peano arithmetic suffices for algorithms, computability, and finite combinatorics.
• Full AC is needed for infinite-dimensional Hahn-Banach, arbitrary Tychonoff, non-measurable sets, and the unrestricted Radon-Nikodym theorem.
• ML in practice uses sigma-finite measures on standard Borel spaces, where DC is sufficient.
• Computations are finite and use no choice. The theory about computations sometimes does.
• For exact axiom dependencies, the right framework is reverse mathematics; the right tool is #print axioms in Lean. This page is the practitioner-level summary, not the formal classification.

Exercises

ExerciseAdvanced

Problem

Which of the following results on this site require the axiom of choice? (a) The Bellman optimality equation. (b) The Hahn-Banach theorem. (c) The universal approximation theorem. (d) The Radon-Nikodym theorem. (e) Quicksort runs in O(n log n) expected time.

Hint

Reveal Solution

References

Canonical:

• Jech, Set Theory (3rd ed., 2003), Chapters 5-6 for the role of AC in analysis.
• Schechter, Handbook of Analysis and its Foundations (1996), Chapter 6 for choice-free analysis and the DC vs AC distinction.
• Simpson, Subsystems of Second Order Arithmetic (2nd ed., 2009), the canonical reverse-mathematics reference.
• Howard and Rubin, Consequences of the Axiom of Choice (1998), for the precise logical strength of specific theorems.

Background:

• Enderton, Elements of Set Theory (1977), Chapters 1-6.
• Halmos, Naive Set Theory (1960), Chapters 1-25.
• Munkres, Topology (2nd ed., 2000), Chapter 1 (set theory review) and Section 37 (Tychonoff).
• Solovay, "A model of set-theory in which every set of reals is Lebesgue measurable," Annals of Mathematics 92 (1970), 1-56, for the independence of non-measurable sets.