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. The conservation results run the other way and are exact: T₂ⁱ ⊆ S₂ⁱ⁺¹, and S₂ⁱ⁺¹ is ∀Σᵇ_{i+1}-conservative over T₂ⁱ (Buss), so the interleaving is tight rather than merely inclusive. Parikh (1971) supplies the reason the theories stay feasible: in a theory all of whose axioms are bounded, a provable ∀x∃y φ with φ bounded can always be reproved with the existential bounded by a term. Translation into propositional logic makes proof complexity the same subject — S₂ⁱ proofs become polynomial-size G_i proofs and Cook's PV corresponds to Extended Frege — and lower bounds transfer back: Ajtai (1988) showed the pigeonhole principle is unprovable in bounded arithmetic with a new predicate, which with the later exponential lower bounds for constant-depth Frege makes unprovability and circuit lower bounds two readings of one result.

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

Limitations. Exponentiation is not total in S₂: by Parikh's theorem every provably total function is bounded by a term of the language, so ∀x∃y (y = 2^x) is unprovable and no long sequence coding is available without adding Ω₁ or exp. The theories are too weak to certify even the weakest arithmetic — Wilkie and Paris (1987) showed I∆₀ + Ω₁ does not prove Con(Q) — and by Gödel's second theorem none of them proves its own consistency. Induction is confined to bounded formulas, so any property whose definition needs an unbounded quantifier is outside the schema. Nothing in the subject separates anything: S₂ⁱ ⊊ T₂ⁱ ⊊ S₂ⁱ⁺¹ is open at every level, and the correspondence with complexity classes means a separation would settle a major open problem, so the theories inherit rather than resolve those questions. The correspondence itself is with function classes and witnessing, not with decision-class separations, so results about provability yield conditional, not absolute, complexity information.

© 2026 Lingenic LLC