Buss's first-order theories
Samuel Buss introduced first-order theories of bounded arithmetic .[2] are first-order theories with equality in the language , where the function is intended to designate (the number of digits in the binary representation of ) and is . (Note that , i.e. allows to express polynomial bounds in the bit-length of the input.) Bounded quantifiers are expressions of the form :=\exists x(x\leq t\wedge \dots )}
, :=\forall x(x\leq t\rightarrow \dots )}
, 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 (the standard model of arithmetic) and dually . In particular, .
The theory consists of a finite list of open axioms denoted BASIC and the polynomial induction schema
where .