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 (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. [2] and a number of other logicians.
Stephen Cook introduced an equational theory (for Polynomially Verifiable) formalizing feasibly constructive proofs (resp. polynomial-time reasoning). [3] 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. [4] Axioms of are universal sentences and contain all equations provable in . In addition, contains axioms replacing the induction axioms for open formulas.
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. Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "http://localhost:6011/en.wikipedia.org/v1/":): \sharp allows to express polynomial bounds in the bit-length of the input.) 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 (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 .
Buss (1986) proved that theorems of are witnessed by polynomial-time functions. [2]
Theorem (Buss 1986)
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.
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. [3]
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 (possibly containing new variables needed to encode the computation of the predicate ).
Theorem (Cook 1975)
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 (1985) has been more practical for capturing subsystems of Extended Frege such as Frege or constant-depth Frege. [5] [6]
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word ἀξίωμα (axíōma), meaning 'that which is thought worthy or fit' or 'that which commends itself as evident'.
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them. Any set that receives a classification is called arithmetical. The arithmetical hierarchy was invented independently by Kleene (1943) and Mostowski (1946).
In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.
In computational complexity theory, the polynomial hierarchy is a hierarchy of complexity classes that generalize the classes NP and co-NP. Each class in the hierarchy is contained within PSPACE. The hierarchy can be defined using oracle machines or alternating Turing machines. It is a resource-bounded counterpart to the arithmetical hierarchy and analytical hierarchy from mathematical logic. The union of the classes in the hierarchy is denoted PH.
In computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees.
In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.
In logic and theoretical computer science, and specifically proof theory and computational complexity theory, proof complexity is the field aiming to understand and analyse the computational resources that are required to prove or refute statements. Research in proof complexity is predominantly concerned with proving proof-length lower and upper bounds in various propositional proof systems. For example, among the major challenges of proof complexity is showing that the Frege system, the usual propositional calculus, does not admit polynomial-size proofs of all tautologies. Here the size of the proof is simply the number of symbols in it, and a proof is said to be of polynomial size if it is polynomial in the size of the tautology it proves.
In complexity theory, the Karp–Lipton theorem states that if the Boolean satisfiability problem (SAT) can be solved by Boolean circuits with a polynomial number of logic gates, then
Effective descriptive set theory is the branch of descriptive set theory dealing with sets of reals having lightface definitions; that is, definitions that do not require an arbitrary real parameter. Thus effective descriptive set theory combines descriptive set theory with recursion theory.
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.
In the study of formal theories in mathematical logic, bounded quantifiers are often included in a formal language in addition to the standard quantifiers "∀" and "∃". Bounded quantifiers differ from "∀" and "∃" in that bounded quantifiers restrict the range of the quantified variable. The study of bounded quantifiers is motivated by the fact that determining whether a sentence with only bounded quantifiers is true is often not as difficult as determining whether an arbitrary sentence is true.
In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.
In computational complexity theory, the language TQBF is a formal language consisting of the true quantified Boolean formulas. A (fully) quantified Boolean formula is a formula in quantified propositional logic where every variable is quantified, using either existential or universal quantifiers, at the beginning of the sentence. Such a formula is equivalent to either true or false. If such a formula evaluates to true, then that formula is in the language TQBF. It is also known as QSAT.
In set theory and mathematical logic, the Lévy hierarchy, introduced by Azriel Lévy in 1965, is a hierarchy of formulas in the formal language of the Zermelo–Fraenkel set theory, which is typically called just the language of set theory. This is analogous to the arithmetical hierarchy, which provides a similar classification for sentences of the language of arithmetic.
In mathematics, lifting theory was first introduced by John von Neumann in a pioneering paper from 1931, in which he answered a question raised by Alfréd Haar. The theory was further developed by Dorothy Maharam (1958) and by Alexandra Ionescu Tulcea and Cassius Ionescu Tulcea (1961). Lifting theory was motivated to a large extent by its striking applications. Its development up to 1969 was described in a monograph of the Ionescu Tulceas. Lifting theory continued to develop since then, yielding new results and applications.
In proof complexity, a Frege system is a propositional proof system whose proofs are sequences of formulas derived using a finite set of sound and implicationally complete inference rules. Frege systems are named after Gottlob Frege.
In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic, is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, xy, together with induction for formulas with bounded quantifiers.
In propositional calculus and proof complexity a propositional proof system (pps), also called a Cook–Reckhow propositional proof system, is a system for proving classical propositional tautologies.
In first-order arithmetic, the induction principles, bounding principles, and least number principles are three related families of first-order principles, which may or may not hold in nonstandard models of arithmetic. These principles are often used in reverse mathematics to calibrate the axiomatic strength of theorems.