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. S₂ corresponds to polynomial time. 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 Σ₁ᵇ)
S₂ = ⋃ᵢ S₂ⁱ

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

Correspondence:

S₂¹ ↔ polynomial time (Σ₁ᵇ-definable functions = P)
T₂¹ ↔ polynomial time (with LIND)
Weaker theories ↔ smaller classes (NC, L, etc.)

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

Symbols.

Symbol	Unicode	Name	Meaning
≤	U+2264	Bounded	Within bound
\|x\|	—	Length	Bit length (log)
Σᵢᵇ	—	Bounded Σ	Hierarchy level
PIND	—	Poly induction	Length induction
LIND	—	Length induction	On \|x\|
S₂ⁱ	—	Buss theory	i-th level
⌊x/2⌋	—	Half	Divide by 2

Metatheory. Bounded arithmetic is finitely axiomatizable. 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.