The engine of everything. Two tools — bounded induction and bounded recursion — drive every construction in the bounded framework. This paper derives them from BST, defines the arithmetic operations, proves the complete algebraic identities, and develops elementary number theory through unique factorisation. It also addresses the self-grounding question: whether the arithmetic can evaluate the logic that defines the set theory that constructs it. The paper argues yes (Theorem 8.1) — but the application to the wider programme is still pending.
The proof tool. Every algebraic identity, every order property, every number-theoretic result in the bounded framework is proved by BI-BST. It is finite iteration: apply a step function k times from a base case. Interior inheritance guarantees interiority at every step — verify once, use everywhere.
The computational tool. Every recursive definition — addition, multiplication, exponentiation, every algorithm — is a BR-BST construction. Derived from BI-BST, not assumed independently. Each step produces a definite interior element. The construction is effective: iterate the step function k times.
Addition is defined by BR-BST directly. Multiplication uses addition. Exponentiation uses multiplication. This is iterated recursion — each level is a BR-BST construction using the previous level's function as its step.
BR-BST with g = m, h(n, v) = S(v). Each step computes a successor — one application of BFT 4 and BFT 5. Exact when m + n is interior.
BR-BST with g = 0, h(n, v) = v + m. The step function uses addition, which was itself defined by BR-BST. First instance of iterated recursion.
BR-BST with g = 1, h(n, v) = v × m. The step function uses multiplication, which uses addition. Three nested levels of BR-BST. Exact when m^n is interior.
No precision parameters, no approximation, no families indexed by k. Each identity is simply true of ℕ_B(k) for all interior elements. Every proof is a direct application of BI-BST.
Divisibility, primality, GCD, Bezout's identity, Euclid's lemma, and unique factorisation — all developed within ℕ_B(k) using only BI-BST, BR-BST, and BFTs 1, 4, 5, 7. Every result is exact.
For any m and nonzero d in ℕ_B(k), there exist unique q, r with m = d × q + r and r < d. Proved by SBI-BST.
gcd(m, n) exists and is computable by iterated division. Terminates in finitely many steps because remainders decrease strictly.
For any m, n in ℕ_B(k), there exist a, b such that gcd(m, n) = a × m + b × n. Extended Euclidean algorithm by BR-BST.
If a prime p divides m × n, then p divides m or p divides n. Proved from Bezout — the same argument Euclid gave, 2300 years ago.
Every integer ≥ 2 in ℕ_B(k) has a unique prime factorisation. Existence by SBI-BST (descending divisor chains), uniqueness by Euclid's lemma.
Every nonempty subset of ℕ_B(k) has a least element. From BFT 1 (Foundation) — the finite domain makes this a structural consequence.
The paper argues that the bounded arithmetic can evaluate any BFOL sentence in any standard model by direct computation (Theorem 8.1). If this holds under application to the wider programme, the dependency chain becomes self-supporting: the logic defines the set theory, the set theory constructs the arithmetic, and the arithmetic evaluates the logic. This application is still pending.
Theorem 8.1 argues that for any specific BFOL sentence φ and any specific standard model 𝒱_n, the bounded arithmetic can determine whether 𝒱_n ⊨ φ by direct computation. This is not a soundness theorem — it is a computation. The application of this result to the wider programme's dependency chain is still pending.
BST proves every specific finite instance of results like Ackermann, Goodstein, and Paris-Harrington. What it cannot prove is the universal quantification across all naturals. For elementary number theory, finite algebra, combinatorics, and experimental physics, this boundary is irrelevant.
All of elementary number theory. All algebraic identities. All combinatorics with fixed parameters. The self-grounding (Theorem 8.1) — evaluating a BFOL sentence of quantifier depth d is recursion of depth d, which is fixed for each specific sentence. Every result in this paper.
Ackermann totality, Goodstein's theorem, Paris-Harrington. Every specific finite instance is provable in BST. The universal statement is not. The gap is precisely identified: recursion of variable depth, where the depth depends on the input. The boundary is named exactly and honestly.
Bounded induction, bounded recursion, the arithmetic operations, the algebraic identities, elementary number theory through unique factorisation. Every result is Type I. Every construction is exact. The self-grounding argument (Theorem 8.1) is stated — its application to the wider programme is the next step.
"Every result in this paper is Type I. The precision parameters on ℕ_B(k) are not approximations to values in some external framework of higher precision. There is no such framework." — Bounded Arithmetic, Working Paper 2026