One axiom. Nine ZFC properties as theorems. Every model finite. The Axiom of Finite Bounds determines the standard models 𝒱_n. Nine ZFC axioms — Foundation, Extensionality, Empty Set, Pairing, Union, Replacement, Separation, Power Set, and Choice — are proved as Bounded Fundamental Theorems, each constrained to interior elements. The Axiom of Infinity is the only ZFC axiom whose content BST denies.
The Axiom of Finite Bounds negates infinity and asserts a finite upper bound on set size. From this single commitment, the entire set-theoretic apparatus follows: nine ZFC axioms proved as theorems of the standard models.
ZFC distributes its foundational content across ten independent axioms. BST concentrates it in one. What ZFC assumes separately, BST derives from the single fact that the universe is a finite level of the cumulative hierarchy.
One axiom per candidate bound n. Each instance is a BFOL sentence. Each model satisfies exactly one instance.
All models finite. The bound is not an object of the theory. BST ⊢ φ iff φ is true in every standard model 𝒱_n.
Each built by iterated power set. The key structural fact: V_n = P(V_{n-1}). Every subset of V_{n-1} is an element of V_n. This is what makes all construction operations work.
The partition is a structural consequence of finiteness, not an additional axiom. Any finite structure with a membership relation has maximal elements — elements that nothing contains. The interior/ceiling partition is discovered in the model theory, not decreed by stipulation.
An element x ∈ V_n is interior if x ∈ V_{n-1} — equivalently, if it appears as a member of some set in the domain. All nine Bounded Fundamental Theorems apply to interior elements. These are the elements on which mathematics operates. In 𝒱₃: the 4 elements of V₂.
An element x ∈ V_n is a ceiling element if x ∈ V_n \ V_{n-1} — nothing in the domain contains it. Ceiling elements exist with definite cardinality but no BFT applies to them. They carry the bound. In 𝒱₃: the 12 elements of V₃ \ V₂.
Each holds in every 𝒱_n because V_n = P(V_{n-1}), which guarantees closure under set-forming operations for interior elements. All nine carry the interiority condition uniformly.
The single axiom from which all nine BFTs follow. Every set is finite. A metatheoretic upper bound on cardinality exists.
Every nonempty interior set has an ∈-minimal element. Rank descent in V_n makes membership acyclic — a finite DAG always has leaves.
Two interior sets with the same members are identical. Transitivity of V_n ensures all members are visible.
∅ is interior in every 𝒱_n with n ≥ 1. The empty set exists and has no members.
If a, b are interior, {a, b} exists. Because {a, b} ⊆ V_{n-1}, so {a, b} ∈ P(V_{n-1}) = V_n.
If F is interior, ⋃F exists. Members of members are at lower rank, already in V_{n-1}.
The image of an interior set under a functional formula mapping to interior elements exists. |image| ≤ |input|.
Any subset of an interior set defined by a BFOL formula exists. Subsets of interior sets are interior.
P(A) exists when 2^|A| fits in the model. Every interior set in the standard models satisfies this. Above the threshold, exponential growth exceeds the bound.
For any interior collection of nonempty sets, each member has an element in the domain. Transitivity guarantees this. No non-constructive principle required — choices by finite enumeration.
Directly negated by AFB. The root of the entire system change.
For sets near the bound, the power set exceeds the domain. Falls as a consequence of bounded finitude.
Over finite collections, Choice is provable by enumeration. Banach-Tarski vanishes with it.
Prevents infinite descending chains — pathologies that cannot arise when all sets are finite.
BST proves sentences ZFC refutes. ZFC proves sentences BST refutes. The two are model-theoretically incomparable — neither's models include the other's.
The nine properties are not independent features of set-theoretic reality. They are consequences of finiteness. The set theory is established. The bounded number systems, analysis, and applications belong to subsequent papers.
"The bound is the axiom. Everything else is structure." — Bounded Set Theory, Working Paper 2026