Such theories are typically obtained by requiring that quantifiers be bounded in the induction axiom or equivalent postulates (a bounded quantifier is of the form ∀x ≤ t or ∃x ≤ t, where t is a term not containing x).
The main purpose is to characterize one or another class of computational complexity in the sense that a function is provably total if and only if it belongs to a given complexity class.
Further, theories of bounded arithmetic present uniform counterparts to standard propositional proof systems such as Frege system and are, in particular, useful for constructing polynomial-size proofs in these systems.
The characterization of standard complexity classes and correspondence to propositional proof systems allows to interpret theories of bounded arithmetic as formal systems capturing various levels of feasible reasoning (see below).
The approach was initiated by Rohit Jivanlal Parikh[1] in 1971, and later developed by Samuel R. Buss.
Stephen Cook introduced an equational theory
(for Polynomially Verifiable) formalizing feasibly constructive proofs (resp.
consists of function symbols for all polynomial-time algorithms introduced inductively using Cobham's characterization of polynomial-time functions.
Axioms and derivations of the theory are introduced simultaneously with the symbols from the language.
The theory is equational, i.e. its statements assert only that two terms are equal.
Samuel Buss introduced first-order theories of bounded arithmetic
are first-order theories with equality in the language
(the number of digits in the binary representation of
allows to express polynomial bounds in the bit-length of the input.)
Bounded quantifiers are expressions of the form
is the set of sharply bounded formulas.
Bounded formulas capture the polynomial-time hierarchy: for any
coincides with the set of natural numbers definable by
(the standard model of arithmetic) and dually
consists of a finite list of open axioms denoted BASIC and the polynomial induction schema where
are precisely the functions computable in polynomial time.
The characterization can be generalized to higher levels of the polynomial hierarchy.
Theories of bounded arithmetic are often studied in connection to propositional proof systems.
Similarly as Turing machines are uniform equivalents of nonuniform models of computation such as Boolean circuits, theories of bounded arithmetic can be seen as uniform equivalents of propositional proof systems.
The connection is particularly useful for constructions of short propositional proofs.
can be equivalently expressed as a sequence of formulas
can be in turn formulated as a propositional tautology
(possibly containing new variables needed to encode the computation of the predicate
proves the so called reflection principle for Extended Frege system, which implies that Extended Frege system is the weakest proof system with the property from the theorem above: each proof system satisfying the implication simulates Extended Frege.
An alternative translation between second-order statements and propositional formulas given by Jeff Paris and Alex Wilkie (1985) has been more practical for capturing subsystems of Extended Frege such as Frege or constant-depth Frege.