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)

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)

ZFC Without Choice Is Enough For

Definition

ZF-sufficient content

These results hold in ZF (without the axiom of choice):

• Real analysis on separable spaces
• Countable measure theory
• Most of elementary probability (on countable sample spaces)
• Linear algebra over finite-dimensional spaces
• Convex optimization in finite dimensions
• Neural network computations (these are finite-dimensional)

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 (functional analysis core)
• Banach-Alaoglu theorem: weak-* compactness of the dual unit ball
• Tychonoff's theorem: products of compact spaces are compact
• Existence of non-measurable sets: Vitali sets (measure theory)
• Radon-Nikodym theorem in full generality (sigma-finite is enough, but the general case needs more)
• Existence of conditional expectations as random variables (measure-theoretic probability)
• Zorn's lemma arguments in RKHS theory and kernel methods
• Well-ordering used in transfinite induction proofs

In practice, the axiom of choice is used so pervasively in analysis and probability that avoiding it would require rewriting most of the mathematical infrastructure.

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.

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 including choice.

If TheoremPath content were formalized in Lean, the constructive core (algorithms, type theory, basic definitions) would work without classical axioms. The analysis and probability content would require Classical.choice and Decidable instances.

Summary

• ZFC is the implicit foundation for all mathematical content on this site
• Peano arithmetic suffices for algorithms, computability, and finite combinatorics
• The axiom of choice is specifically needed for functional analysis, measure theory, and probability
• Computations are finite and don't need choice; the theory about computations does
• This distinction rarely matters in practice but is important for formal verification

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 (2003), for the role of choice in analysis

• Schechter, Handbook of Analysis and its Foundations (1996), for choice-free analysis

• Enderton, Elements of Set Theory (1977), Chapters 1-6

• Halmos, Naive Set Theory (1960), Chapters 1-25

• Munkres, Topology (2000), Chapter 1 (set theory review)