Bounded Arithmetic

Origin. Buss introduced bounded arithmetic (S₂, 1986). Weak fragments of Peano arithmetic. Quantifiers bounded: ∀x≤t and ∃x≤t. Proof-theoretic characterization of complexity classes. Foundation for proof complexity and feasible mathematics.

Models. Arithmetic with resource bounds. PA: unbounded quantification, full induction. Bounded: quantifiers relativized to terms, limited induction. It is S₂¹, the first level, that corresponds to polynomial time; the union S₂ climbs the polynomial hierarchy level by level. Weaker systems for smaller classes. Separating theories = separating complexity classes.

Formalism.

Bounded quantifiers:

• ∀x≤t. φ(x) means ∀x. (x≤t → φ(x))
• ∃x≤t. φ(x) means ∃x. (x≤t ∧ φ(x))

Hierarchy of bounded formulas:

• Σ₀ᵇ = Π₀ᵇ: sharply bounded (∀x≤|t|, ∃x≤|t|)
• Σᵢ₊₁ᵇ: ∃x≤t. Πᵢᵇ
• Πᵢ₊₁ᵇ: ∀x≤t. Σᵢᵇ

Buss's theories:

• S₂ⁱ: Σᵢᵇ-PIND (polynomial induction on Σᵢᵇ)
• T₂ⁱ: Σᵢᵇ-IND (ordinary induction on Σᵢᵇ)
• S₂ = ⋃ᵢ S₂ⁱ, T₂ = ⋃ᵢ T₂ⁱ
• The two interleave: S₂ⁱ ⊆ T₂ⁱ ⊆ S₂ⁱ⁺¹, and no inclusion is known to be strict.

PIND: φ(0) ∧ ∀x.(φ(⌊x/2⌋) → φ(x)) → ∀x.φ(x) (Polynomial induction: halving instead of predecessor)

LIND is the third form, induction along the length: φ(0) ∧ ∀x.(φ(x) → φ(x+1)) → ∀x.φ(|x|). Over the base theory Σᵢᵇ-LIND and Σᵢᵇ-PIND are equivalent, so LIND is a presentation of S₂ⁱ — it is not what distinguishes T₂ⁱ, which is defined by full IND.

Correspondence:

• S₂¹ ↔ polynomial time: the Σ₁ᵇ-definable functions of S₂¹ are exactly FP (Buss 1986)
• S₂ⁱ ↔ the i-th level: Σᵢᵇ-definable functions are FP^{Σᵖ_{i−1}} = □ᵖᵢ, so S₂ as a whole tracks PH, not P
• T₂¹ ↔ PLS, not polynomial time: the Σ₁ᵇ-definable multifunctions of T₂¹ are exactly the projections of polynomial local search problems (Buss–Krajíček 1994)
• Beckmann–Buss (2009) extend this upward, characterizing T₂^{k+1} by Πᵖ_k-PLS
• Weaker theories ↔ smaller classes (NC, L, etc.)

PLS is a genuine strengthening, not a restatement of P. A PLS problem is a neighbourhood function together with a cost that strictly decreases; a solution is a local optimum, guaranteed to exist because the cost cannot descend forever, but reachable only by following the descent, which may take exponentially many steps. That is exactly the extra power ordinary induction gives over halving induction — T₂¹ proves a totality that S₂¹ witnesses only if PLS ⊆ FP.

Witnessing theorems: If S₂¹ ⊢ ∀x.∃y≤t.φ(x,y) where φ ∈ Σ₁ᵇ, then witness computable in P.

Symbols.

Metatheory. Each level is finitely axiomatizable — every S₂ⁱ and T₂ⁱ has a finite axiomatization (Buss) — but whether the union S₂ is finitely axiomatizable is open, and the two claims must not be run together. The question is not incidental: S₂ is finitely axiomatizable exactly when the hierarchy collapses to some finite level, so a proof of finite axiomatizability would be a proof of collapse. Krajíček, Pudlák and Takeuti (1991) settled the relativized case negatively — S₂(α) is not finitely axiomatizable, so the relativized hierarchy does not collapse — and their witnessing theorem gives T₂ⁱ = S₂ⁱ⁺¹ ⟹ Σᵖ_{i+1} ⊆ Δᵖ_{i+1}/poly, a non-uniform collapse rather than an outright one. Definable functions = complexity class. Proof complexity: short proofs ↔ feasible witnessing. Separation of bounded arithmetics open (implies P≠NP type results). Conservation results between levels.

Applies to. Proof complexity. Feasible mathematics. Cryptography foundations. Complexity theory. Formal verification. Foundations of algorithms.

Limitations. Separations unproven (linked to open problems). Technical and specialized. Not standard logic education. Multiple competing systems. Connection to practical verification indirect. Requires complexity theory background.

© 2026 Lingenic LLC