A complete formal foundation for mathematics from a single axiom. Not a restriction on mathematics — a clarification of what mathematics is about. The logic, the set theory, the arithmetic, the full apparatus of real analysis, and the Millennium Problems, constructed from the ground up without any appeal to completed infinite totalities.
This paper constructs a complete formal foundation for mathematics from a single axiom: the Axiom of Finite Bounds (AFB), which asserts that every set has a finite cardinality bounded by some metatheoretic natural number.
The construction proceeds in strict order of logical dependence. The axiom forces a discipline on the logic used to reason about it: quantification must be bounded, because unrestricted quantification over a potentially infinite domain is semantically incoherent when no such domain is admitted. That discipline is Bounded First-Order Logic (BFOL). Within BFOL, the set-theoretic axioms of BST are built. On top of BST, the complete bounded number chain is constructed, and the full apparatus of real analysis is recovered over the bounded reals ℝ_B(k).
This is not a philosophical challenge to infinity. It is a formal construction — with proofs — of everything that mathematics needs, without positing infinite objects that cannot be constructed or observed.
Each stage builds on the last. The first establishes the formal foundations. The second develops the mathematics. The third applies the completed system to physics and open problems.
BFOL, primitive ordinals, and AFB are not separable — they arrive as a unified commitment. The logic provides the language. Primitive ordinals give content to "bounded by n." AFB states the constraint. The seven axioms of BST are built on top.
The full mathematical programme. Ordinals, induction, functions, the complete number chain through ℂ_B(k⁴), real and complex analysis. Every major classical theorem classified in four categories.
The formal core applied to physics and the Millennium Problems. Extrapolations — not formal developments — but grounded in the completed system of Stages I and II.
The Axiom of Infinity required no justification beyond declaration. Its negation requires exactly the same. But where the original merely asserted infinity and derived consequences, AFB asserts finitude and constructs mathematics — with proofs — from the ground up.
"There exists a completed infinite set containing all natural numbers simultaneously — as a finished object, not a process."
"No completed infinite set exists. There is a finite upper bound on the size of sets — metatheoretically fixed, unknown in magnitude, potentially unimaginably large."
Four ZFC axioms fall away — not by ad hoc removal but as direct formal consequences of AFB. What remains is a clean, paradox-free system that supports the full development of Parts V through IX.
The single foundational commitment from which all else follows. Every set is finite. A metatheoretic upper bound on cardinality exists. This axiom drives every downstream consequence — the fall of Power Set, the redundancy of Choice, and the irrelevance of Foundation all follow from here.
Two sets are equal iff they have the same members. Purely definitional. Survives without modification.
There exists a set with no members. Zero members is the smallest finite number. Fully compatible with finite bounds.
For any two finite sets, there exists a finite set containing exactly those two. Finiteness made explicit where ZFC left it implicit.
The union of finitely many finite sets is finite. Exactly what all concrete applications require.
Any definable subset of a finite set is finite. Carve sub-collections by any property — the subset cannot exceed the whole.
A finitely expressible function on a finite set produces a finite image. Inputs, functions, and outputs stay finite throughout.
Directly negated and replaced by AFB. The root of the entire system change.
For any set near the finite bound B, the power set (2ⁿ elements) necessarily exceeds B. Falls as a consequence of bounded finitude.
Over finite collections, Choice is provable by bounded induction — it becomes a theorem, not an axiom. Banach–Tarski vanishes with it.
Prevents infinite descending membership chains — pathologies that cannot arise when all sets are finite. The axiom did no independent work.
Prior finitist programs either overstated what was lost or understated it. This paper gives a precise four-category classification of how classical theorems relate to BST. Every major affected theorem is placed in a category — with justification.
Classical theorems provable in BST with explicit precision bounds. The BST version is strictly more informative than the classical version — it names the bound rather than asserting mere existence.
Theorems about finite structures provable directly in BST, without modification. The full sweep of concrete mathematics that working mathematicians and physicists actually use.
Theorems that require completed infinite totalities, uncountable Choice, or objects BST does not posit. Absent not by oversight but because the objects they concern do not exist under AFB.
Three universal statements that sit exactly at the boundary of what finite induction can reach. Every specific instance is provable. The universal collection is not. This gap is real, and it is named precisely.
The narrow gap — Category D — is real and is not softened. Three universal statements at the edge of finite induction sit beyond what BST can reach universally, though every specific instance is provable. Everything else that classical mathematics proves either falls into A, B, or C. The Category C losses are real but concern objects with no finite interpretation and no correspondence to physical observation. The gains are substantial: explicit cardinalities, explicit quantifier ranges, paradox-free analysis, and Choice and Foundation as theorems rather than axioms.
Seven problems. One million dollars each. The central finding: no problem simply dissolves. Each either survives intact, transforms into a finite-field or discrete analog of comparable depth, or splits into a finite part (available) and an analytic part (requiring continuous or smooth-manifold structure). The pattern is evidence that the filter is tracking something real.
The core intuition is inherently finite: real computational tasks involve finite inputs, finite algorithms, finite resources. The asymptotic formulation (input size → ∞) is a convenience for unifying infinitely many finite questions. Under finite bounds, this becomes a family of concrete questions about bounded computational resources. The fundamental insight — that verification can be easier than solution — does not depend on infinity at all.
The classical statement concerns cohomology classes on complex projective varieties — objects defined within continuous geometry. Under BST, the primary analog is the Tate Conjecture over finite fields: an equally deep question about algebraic cycles and Galois representations, fully available within BST. A second analog — a bounded Hodge conjecture over ℂ_B(k⁴) — is now also formulated, using bounded simplicial cohomology over finite simplicial complexes.
The classical statement requires infinite series and analytic continuation. The finite-field analog was proved by Weil and Deligne (1974). The prime-counting connection survives in a BST-available reformulation. Additionally, a truncated zeta function ζ_B(s, k) over ℂ_B(k⁴) is now computable within BST — a numerical investigation tool for the empirical distribution of zeros of finite truncations.
Physicists know experimentally that the mass gap exists. The Millennium Problem exists because the infinite framework of QFT cannot prove what observation already confirms. Under BST, Yang–Mills becomes a question about lattice gauge theory on finite graphs. Crucially, the gauge group SU(N)_B(k⁴) — N×N matrices over ℂ_B(k⁴) satisfying M†M = I within precision — is now formally recoverable within BST, bridging the lattice formulation to the group-theoretic structure of the continuum theory.
The problem presupposes continuous spatial domains and infinite differentiability. Computational fluid dynamics on finite grids already produces excellent results for engineering applications. Under BST, the question becomes: do bounded-domain discrete Navier–Stokes equations on a finite grid with bounded initial conditions produce bounded solutions? The physical phenomenon is finite. The difficulty may be an artifact of continuous idealisation.
The arithmetic content — counting rational points on elliptic curves — is fundamentally finite and computational. BST supports the full arithmetic theory of elliptic curves over finite fields. The conjecture as formulated invokes L-functions defined via infinite series and analytic continuation: that part requires infinite analytic machinery. The finite arithmetic phenomenon is real and deep; the analytic formulation of the connection is not available.
Proved by Perelman in 2003 via Ricci flow — smooth manifolds, continuous time evolution, infinite differentiability. The proof does not transfer to BST as written. The geometric insight — the topological characterisation of the three-sphere — has discrete analogs in combinatorial topology, and BST supports simplicial complexes and finite triangulations. The classical proof cannot be transplanted; a discrete analog of the geometric content can be pursued.
Part X applies the formal core of Parts I–IX to physical questions as an exploratory extrapolation. The argument: infinity enters physics as calculational scaffolding from which finite results are extracted — not as an indispensable component of physical ontology. The crises appear exactly where infinite mathematics is pushed beyond what it was built to do.
Feynman diagrams routinely produce infinite values. An elaborate procedure subtracts infinity from infinity to obtain finite answers — answers that then agree with observation to twelve decimal places. The finite answers were always there. The infinities were introduced by the infinite framework.
Vacuum energy predicted by QFT exceeds the observed value by a factor of roughly 10¹²⁰. The divergence appears only when integration extends over an infinite range of momenta. A finite cutoff at the Planck scale — which BST motivates naturally — resolves it.
Where curvature and density become infinite. Physicists interpret these as signals that the theory has exceeded its domain — not as physical predictions. A finite underlying structure prevents them structurally, not by additional axioms.
The Bekenstein-Hawking bound — that the information content of a region is proportional to its surface area — is structurally parallel to AFB's metatheoretic bound on set cardinality. BST provides a formal framework that accommodates this bound naturally, without adding it as a separate constraint.
Zermelo's 1908 axiom did not appear from nowhere. The assumption had shaped Western thought since before Socrates. Prior programs correctly identified symptoms — but each stopped before the root cause.
Proposes the apeiron — the boundless — as the fundamental principle underlying reality. The first recorded assertion that infinity is a foundational feature of existence. It was not argued for. It was declared.
Draws the distinction between potential and actual infinity — accepting the former, rejecting the latter. A distinction that shaped mathematical thought for two millennia. But potential infinity defers the problem rather than resolving it: a domain that grows without limit is infinite in everything but name.
Bishop Berkeley attacks Newton's infinitesimals. The critique was largely ignored. Calculus worked. But Berkeley had identified, nearly three centuries ago, the same foundational discomfort this paper addresses — that mathematical machinery producing correct results is not the same as mathematical machinery grounded in coherent foundations.
What Anaximander declared as metaphysics, Zermelo encodes as mathematics. The Axiom of Infinity gives the boundless a formal address within rigorous set theory. The assumption does not become more justified by becoming more precise. It becomes harder to question.
Seeks to prove consistency of infinite mathematics using finite methods. Correctly identifies the problem — but aims to vindicate infinity rather than replace it. Stopped by Gödel's incompleteness theorems, which showed the programme cannot succeed on its own terms.
Insists that mathematical objects must be constructively specified. Recovers a large portion of analysis constructively. Stopped at: no formal bounding axiom, potential infinity retained, real analysis incomplete without classical principles.
Rejects not just completed infinities but sufficiently large finite numbers. Correctly identifies that the infinite assumption is an assumption. Stopped at: no systematic development of bounded mathematics, informal rather than formal, no recovery of real analysis.
The four stopping points are addressed in turn: the foundational package is complete (BFOL + AFB + BST); the Burali-Forti problem for bounded theories is solved; the bounded reals are constructed with the full analytic apparatus; and the accounting is precise. The result is a rigorous, self-contained alternative foundation for finite mathematics, with every tradeoff stated at the level of precision the mathematics demands.
Eleven parts. Three stages. One axiom. The paper constructs Bounded First-Order Logic, states AFB, builds the seven axioms of BST, solves the Burali-Forti problem for bounded theories, develops two induction schemas, builds function theory without Power Set, constructs the full bounded number chain through ℂ_B(k⁴), recovers real and complex analysis, applies the system to physics and the Millennium Problems, and gives a four-category accounting of every classical theorem. Every tradeoff is stated at the level of precision the mathematics demands.
The formal proofs are open on GitHub — verified Isabelle/HOL and Coq scaffolds, MIT licensed. Contributions and scrutiny welcome.
"The result is not a complete solution to every problem in foundations. It is a rigorous and self-contained alternative foundation for finite mathematics, with every tradeoff stated at the level of precision the mathematics demands." — The Axiom of Finite Bounds, Working Paper 2026