Bounded arithmetic is a collective name for a family of weak subtheories of Peano arithmetic. Such theories are typically obtained by requiring that quantifiers be bounded in the induction axiom or equivalent postulates. The main purpose is to characterize one or another class of computational complexity in the sense that a function is provably totalif 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. The approach was initiated by Rohit Jivanlal Parikh in 1971, and later developed by Samuel R. Buss. and a number of other logicians.
Theories
Cook's theory
introduced an equational theory formalizing feasibly constructive proofs. The language of 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. A popular extension of is a theory, an ordinary first-order theory. Axioms of are universal sentences and contain all equations provable in. In addition, contains axioms replacing the induction axioms for open formulas.
Buss's theories
introduced first-order theories of bounded arithmetic. are first-order theories with equality in the language, where the function is intended to designate and is. Bounded quantifiers are expressions of the form,, where is a term without an occurrence of. A bounded quantifier is sharply bounded if has the form of for a term. A formula is sharply bounded if all quantifiers in the formula are sharply bounded. The hierarchy of and formulas is defined inductively: is the set of sharply bounded formulas. is the closure of under bounded existential and sharply bounded universal quantifiers, and is the closure of under bounded universal and sharply bounded existential quantifiers. Bounded formulas capture the polynomial-time hierarchy: for any, the class coincides with the set of natural numbers definable by in and dually. In particular,. The theory consists of a finite list of open axioms denoted BASIC and the polynomial induction schema where.
Buss's witnessing theorem
Buss proved that theorems of are witnessed by polynomial-time functions.
Theorem Assume that, with. Then, there exists a -function symbol such that.
Moreover, can -define all polynomial-time functions. That is, -definable functions in are precisely the functions computable in polynomial time. The characterization can be generalized to higher levels of the polynomial hierarchy.
Correspondence to propositional proof systems
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. It is often easier to prove a theorem in a theory of bounded arithmetic and translate the first-order proof into a sequence of short proofs in a propositional proof system than to design short propositional proofs directly in the propositional proof system. The correspondence was introduced by S. Cook. Informally, a statement can be equivalently expressed as a sequence of formulas. Since is a coNP predicate, each can be in turn formulated as a propositional tautology .
Theorem Assume that, where. Then tautologies have polynomial-size Extended Frege proofs. Moreover, the proofs are constructible by a polynomial-time function and proves this fact.
Further, 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 has been more practical for capturing subsystems of Extended Frege such as Frege or constant-depth Frege.
