Consider a deceptively simple computational task: write a program that verifies the statement every non-empty bounded subset of the reals has a least upper bound. The challenge is not algorithmic—it is expressive. The completeness axiom quantifies over subsets, not elements, and this single quantifier crosses a foundational boundary that has shaped seventy years of automated reasoning research.

First-order logic, despite its decidability properties and elegant model theory, cannot capture this statement faithfully. Any first-order axiomatization of the reals admits non-standard models containing infinitesimals, as Skolem demonstrated. To formalize mainstream mathematics—real analysis, topology, category theory—we need machinery that quantifies over predicates and functions, not merely individuals.

This is the domain of higher-order logic and dependent type theory. Proof assistants like Coq, Lean, Isabelle/HOL, and Agda implement different solutions to the same fundamental problem: how do we mechanize a language expressive enough to encode mathematics while keeping proof checking decidable? The answers diverge in interesting ways. The Calculus of Inductive Constructions treats propositions as types and proofs as programs. Classical HOL adds simple types to Church's lambda calculus. ZFC-based systems like Mizar embed everything in set theory. Each choice has consequences for what mathematics looks natural, what proofs look like, and what automation becomes feasible.

First-order logic permits quantification only over individuals in a domain. We can write ∀x. P(x), but we cannot directly write ∀P. ∀x. P(x) → P(x)—the second universal quantifier ranges over predicates, not elements. This restriction is not arbitrary; it is what gives first-order logic its desirable metatheoretic properties: completeness (Gödel 1929), compactness, and the Löwenheim-Skolem theorems.

The cost of these properties is expressiveness. The induction principle for natural numbers, in its mathematical form, states that for every property P, if P(0) and P(n) → P(n+1), then ∀n. P(n). First-order Peano Arithmetic approximates this with an axiom schema—one axiom for each first-order definable predicate. But there are uncountably many predicates over the naturals and only countably many first-order formulas, so the schema captures only a fragment. Non-standard models slip through the gap.

Real analysis fares worse. The least upper bound property, Dedekind completeness, and the Archimedean property all require second-order quantification for categorical axiomatization. Tarski's first-order theory of real closed fields is decidable and beautiful, but it cannot express that every continuous function on a closed interval attains its maximum—the statement involves quantification over functions.

Category theory presents another obstacle. Defining a functor requires speaking about all morphisms between objects, and natural transformations require quantifying over functors. Without higher-order machinery, large swaths of modern mathematics become circumlocutory at best, inexpressible at worst.

This expressiveness gap is precisely what proof assistants must bridge. The architectural decisions of systems like Coq and Lean—dependent types, universe hierarchies, impredicative propositions—are direct engineering responses to the limitations Gödel and Skolem identified nearly a century ago.

Takeaway

The choice between first-order and higher-order logic is not academic taste—it determines which mathematical statements can even be written down, let alone proved.

The Calculus of Inductive Constructions, underlying Coq and conceptually close to Lean's type theory, identifies propositions with types and proofs with terms inhabiting those types. A proof of A ∧ B is literally a pair (a, b) where a : A and b : B. Dependent types allow the type of a term to depend on a value—the type Vec n A of length-n vectors over A is parameterized by n : Nat. This lets us encode mathematical structures with their invariants built into their types.

Higher-order logic in the Church tradition, implemented by Isabelle/HOL and HOL Light, takes a more conservative approach. It extends typed lambda calculus with a distinguished type of booleans and quantifiers over arbitrary types. There are no dependent types and no universe hierarchy—just simple types and polymorphism. This restraint yields powerful automation: HOL Light's tiny kernel is roughly 400 lines, and its decision procedures handle real arithmetic and large fragments of analysis efficiently.

Set-theoretic foundations, exemplified by Mizar and the Metamath project, embed mathematics in first-order ZFC. Higher-order quantification is recovered by quantifying over sets that represent predicates or functions. The advantage is fidelity to mathematical practice—working mathematicians implicitly use ZFC—and the ability to leverage classical set-theoretic constructions directly.

The tradeoffs are substantive. CIC offers computational content: proofs of constructive statements are programs that can be extracted and executed. HOL offers automation maturity and a smaller trusted kernel. ZFC offers cultural continuity with informal mathematics. Quotients are natural in HOL via the Hilbert epsilon operator, painful in pure CIC, and trivial in set theory. Inductive types are primitive in CIC but require encoding elsewhere.

No foundation dominates. The Univalent Foundations program, formalized in homotopy type theory, suggests that even our notion of equality—a settled matter in HOL and ZFC—admits foundational reconsideration.

Takeaway

Every foundation is a bet about which mathematical concepts deserve primitive status; the cost of that bet appears in every subsequent proof.

The Feit-Thompson Odd Order Theorem, formalized in Coq by Gonthier's team over six years, demonstrates what dependent type theory can sustain. The proof spans 170,000 lines and required developing extensive algebraic infrastructure—the mathematical components library—because group theory, character theory, and Galois theory had to be built from foundations. The dependent types proved essential for managing the intricate algebraic structures.

Flyspeck, Hales's formalization of the Kepler conjecture, used HOL Light and Isabelle. The choice was pragmatic: the proof relied heavily on nonlinear real arithmetic and interval computations where HOL Light's decision procedures excelled. The project completed in 2014 after eleven years, validating both the original proof and the foundational choice.

The Lean Mathematical Library, mathlib, has emerged as the largest unified formalization effort, containing over a million lines covering algebra, analysis, topology, and category theory. Its success rests on Lean's type class mechanism, which automates the inference of algebraic structures, and on aggressive refactoring discipline. The recent formalization of the Liquid Tensor Experiment by Scholze and collaborators demonstrated that even cutting-edge research mathematics is now mechanically verifiable.

Isabelle/HOL hosts the Archive of Formal Proofs, with over 800 entries spanning algorithms, logic, and mathematics. The HOL approach trades expressiveness for automation; Sledgehammer integrates external automated theorem provers, often discharging routine goals that would require manual work in dependently typed systems.

These projects reveal that foundational choices have downstream engineering consequences measured in years of human effort. Yet they also show convergence: mathlib increasingly resembles a structured library independent of Lean's specifics, and translation efforts between Coq, Lean, and Isabelle suggest a future where foundational commitments become less binding.

Takeaway

Formalized mathematics is becoming infrastructure, not merely demonstration—and the foundational debates that once seemed philosophical now have empirical answers measured in lines of verified code.

The expressiveness required to formalize mathematics is not a luxury—it is the minimum entry fee. First-order logic, for all its metatheoretic beauty, cannot bear the weight of analysis, topology, or category theory in their natural form. Higher-order systems answer this need, but they do so through different architectural commitments that ripple through every subsequent definition and proof.

What emerges from comparing CIC, HOL, and set-theoretic foundations is not a winner but a map. Each foundation optimizes for different mathematical activities: computation and constructive content, automation and small kernels, or cultural continuity with informal practice. The choice shapes which proofs feel natural and which feel like fighting the system.

For AI reasoning systems, this history offers a sobering lesson. Expressive power and automated tractability stand in fundamental tension. The proof assistant community has spent decades negotiating this tradeoff, and the resulting systems represent some of the most sophisticated reasoning infrastructure ever built—worth studying carefully as we design the next generation of machine reasoners.