We define theories of bounded arithmetic, whose definable functions and relations are exactly those in certain complexity classes. Based on a recursion-theoretic characterization of NC in Clote , the first-order theory TNC, whose principal axiom scheme is a form of short induction on notation for nondeterministic polynomial-time computable relations, has the property that those functions having nondeterministic polynomial-time graph Θ such that TNC x y Θ are exactly the functions in NC, computable on a parallel random-access machine in (...) polylogarithmic parallel time with a polynomial number of processors.0 We then define three theories of weak second-order arithmetic which respectively characterize relations in the classes of alternating logarithmic time, logspace and nondeterministic logspace. (shrink)

This book presents an up-to-date, unified treatment of research in bounded arithmetic and complexity of propositional logic, with emphasis on independence proofs and lower bound proofs. The author discusses the deep connections between logic and complexity theory and lists a number of intriguing open problems. An introduction to the basics of logic and complexity theory is followed by discussion of important results in propositional proof systems and systems of bounded arithmetic. More advanced topics are then treated, (...) including polynomial simulations and conservativity results, various witnessing theorems, the translation of bounded formulas (and their proofs) into propositional ones, the method of random partial restrictions and its applications, direct independence proofs, complete systems of partial relations, lower bounds to the size of constant-depth propositional proofs, the method of Boolean valuations, the issue of hard tautologies and optimal proof systems, combinatorics and complexity theory within bounded arithmetic, and relations to complexity issues of predicate calculus. Students and researchers in mathematical logic and complexity theory will find this comprehensive treatment an excellent guide to this expanding interdisciplinary area. (shrink)

In this paper we introduce a system AID of bounded arithmetic. The main feature of AID is to allow a form of inductive definitions, which was extracted from Buss’ propositional consistency proof of Frege systems F in Buss 3–29). We show that AID proves the soundness of F , and conversely any Σ 0 b -theorem in AID yields boolean sentences of which F has polysize proofs. Further we define Σ 1 b -faithful interpretations between AID+Σ 0 b (...) -CA and a quantified theory QALV of an equational system ALV in Clote 57–106). Hence ALV also proves the soundness of F. (shrink)

T i 2 = S i +1 2 implies ∑ p i +1 ⊆ Δ p i +1 ⧸poly. S 2 and IΔ 0 ƒ are not finitely axiomatizable. The main tool is a Herbrand-type witnessing theorem for ∃∀∃ П b i -formulas provable in T i 2 where the witnessing functions are □ p i +1.

We characterize the collapse of Buss' bounded arithmetic in terms of the provable collapse of the polynomial time hierarchy. We include also some general model-theoretical investigations on fragments of bounded arithmetic.

We study search problems and reducibilities between them with known or potential relevance to bounded arithmetic theories. Our primary objective is to understand the sets of low complexity consequences of theories Si2 and Ti2 for a small i, ideally in a rather strong sense of characterization; or, at least, in the standard sense of axiomatization. We also strive for maximum combinatorial simplicity of the characterizations and axiomatizations, eventually sufficient to prove conjectured separation results. To this end two techniques (...) based on the Herbrand's theorem are developed. They characterize/axiomatize Σb1-consequences of Σb2-definable search problems, while the method based on the more involved concept of characterization is easier and gives more transparent results. This method yields new proofs of Buss' witnessing theorem and of the relation between PLS and Σb1, and also an axiomatization of Σb1. (shrink)

Over 25 years ago, the first author conjectured in [15] that the existence of arbitrarily large primes is provable from the axioms I Δ₀(π) + def(π), where π(x) is the number of primes not exceeding x, IΔ₀(π) denotes the theory of Δ₀ induction for the language of arithmetic including the new function symbol π, and de f(π) is an axiom expressing the usual recursive definition of π. We prove a modified version in which π is replaced by a more (...) general function ξ that counts some of the primes below x (which primes depends on the values of parameters in ξ), and has the property that π is provably Δ₀(ξ) definable. (shrink)

The bounded arithmetic theory S2 is finitely axiomatized if and only if the polynomial hierarchy provably collapses. If T2i equals S2i + 1 then T2i is equal to S2 and proves that the polynomial time hierarchy collapses to ∑i + 3p, and, in fact, to the Boolean hierarchy over ∑i + 2p and to ∑i + 1p/poly.

In 'On interpretations of arithmetic and set theory', Kaye and Wong proved the following result, which they considered to belong to the folklore of mathematical logic.

THEOREM 1 The first-order theories of Peano arithmetic and Zermelo-Fraenkel set theory with the axiom of infinity negated are bi-interpretable.

In this note, I describe a theory of sets that is bi-interpretable with the theory of bounded arithmetic IDelta0 + exp. Because of the weakness of this theory of sets, I cannot straightforwardly (...) adapt Kaye and Wong's interpretation of the arithmetic in the set theory. Instead, I am forced to produce a different interpretation. (shrink)

In this paper, we study bounded versions of some model-theoretic notions and results. We apply these results to the context of models of bounded arithmetic theories as well as some related complexity questions. As an example, we show that if the theory \(\rm S_2 ^1(PV)\) has bounded model companion then \(\rm NP=coNP\). We also study bounded versions of some other related notions such as Stone topology.

We develop approximate counting of sets definable by Boolean circuits in bounded arithmetic using the dual weak pigeonhole principle (dWPHP(PV)), as a generalization of results from [15]. We discuss applications to formalization of randomized complexity classes (such as BPP, APP, MA, AM) in PV₁ + dWPHP(PV).

We investigate the possibility to characterize (multi) functions that are Σ b i -definable with small i (i = 1, 2, 3) in fragments of bounded arithmetic T 2 in terms of natural search problems defined over polynomial-time structures. We obtain the following results: (1) A reformulation of known characterizations of (multi)functions that are Σ b 1 - and Σ b 2 -definable in the theories S 1 2 and T 1 2 . (2) New characterizations of (multi)functions (...) that are Σ b 2 - and Σ b 3 -definable in the theory T 2 2 . (3) A new non-conservation result: the theory T 2 2 (α) is not ∀Σ b 1 (α)-conservative over the theory S 2 2 (α). To prove that the theory T 2 2 (α) is not ∀Σ b 1 (α)-conservative over the theory S 2 2 (α), we present two examples of a Σ b 1 (α)-principle separating the two theories: (a) the weak pigeonhole principle WPHP (a 2 , f, g) formalizing that no function f is a bijection between a 2 and a with the inverse g, (b) the iteration principle Iter (a, R, f) formalizing that no function f defined on a strict partial order ( $\{0,\dots,a\}$ , R) can have increasing iterates. (shrink)

The elementary arithmetic operations +,·,≤\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${+,\cdot,\le}$$\end{document} on integers are well-known to be computable in the weak complexity class TC0, and it is a basic question what properties of these operations can be proved using only TC0-computable objects, i.e., in a theory of bounded arithmetic corresponding to TC0. We will show that the theory VTC0 extended with an axiom postulating the totality of iterated multiplication proves induction for quantifier-free formulas in (...) the language ⟨+,·,≤⟩\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\langle{+,\cdot,\le}\rangle}$$\end{document}, and more generally, minimization for Σ0b\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\Sigma_{0}^{b}}$$\end{document} formulas in the language of Buss’s S2. (shrink)

We formalize the construction of Paterson’s variant of the Ajtai–Komlós–Szemerédi sorting network of logarithmic depth in the bounded arithmetical theory , under the assumption of the existence of suitable expander graphs. We derive a conditional p-simulation of the propositional sequent calculus in the monotone sequent calculus.

We study variants of Buss’s theories of bounded arithmetic axiomatized by induction schemes disallowing the use of parameters, and closely related induction inference rules. We put particular emphasis on \ induction schemes, which were so far neglected in the literature. We present inclusions and conservation results between the systems and \ of a new form), results on numbers of instances of the axioms or rules, connections to reflection principles for quantified propositional calculi, and separations between the systems.

We develop an arithmetical theory and its variant , corresponding to “slightly nonuniform” . Our theories sit between and , and allow evaluation of log-depth bounded fan-in circuits under limited conditions. Propositional translations of -formulas provable in admit L-uniform polynomial-size Frege proofs.

We prove some independence results for the bounded arithmetic theoryR 2 0 , and we define a class of functions that is shown to be an upper bound for the class of functions definable by a certain restricted class of ∑ 1 b in extensions ofR 2 0.

We define a theory of two-sort bounded arithmetic whose provably total functions are exactly those in ${\mathcal{F}_{LOGCFL}}$ by way of a generalized quantifier that expresses computations of SAC 1 circuits. The proof depends on Kolokolova’s conditions for the connection between the provable capture in two-sort theories and descriptive complexity.

We consider the problem whether the $\forall \Sigma _{1}^{b}$ theorems of the fragments $T_{2}^{a}$ form a strictly increasing hierarchy. We shall show a link to some results about the lengths of proofs in predicate logic that supports the conjecture that the hierarchy is strictly increasing.

We investigate the problem how to lift the non - $\forall \Sigma^b_1(\alpha)$ - conservativity of $T^2_2(\alpha)$ over $S^2_2(\alpha)$ to the expected non - $\forall \Sigma^b_i(\alpha)$ - conservativity of $T^{i+1}_2(\alpha)$ over $S^{i+1}_2(\alpha)$ , for $i > 1$ . We give a non-trivial refinement of the “lifting method” developed in [4,8], and we prove a sufficient condition on a $\forall \Sigma^b_1(f)$ -consequence of $T_2(f)$ to yield the non-conservation result. Further we prove that Ramsey's theorem, a $\forall \Sigma^b_1(\alpha)$ - formula, is not provable (...) in $T^1_2(\alpha)$ , and that $\forall \Sigma^b_j(\alpha)$ - conservativity of $T^{i+1}_2(\alpha)$ over $T^{i}_2(\alpha)$ implies $\forall \Sigma^b_j(\alpha)$ - conservativity of the whole $T_2(\alpha)$ over $T^{i}_2(\alpha)$ , for any $j \geq 2$. (shrink)

This paper presents proof that Buss's S22 can prove the consistency of a fragment of Cook and Urquhart's PV from which induction has been removed but substitution has been retained. This result improves Beckmann's result, which proves the consistency of such a system without substitution in bounded arithmetic S12. Our proof relies on the notion of "computation" of the terms of PV. In our work, we first prove that, in the system under consideration, if an equation is proved (...) and either its left- or right-hand side is computed, then there is a corresponding computation for its right- or left-hand side, respectively. By carefully computing the bound of the size of the computation, the proof of this theorem inside a bounded arithmetic is obtained, from which the consistency of the system is readily proven. This result apparently implies the separation of bounded arithmetic because Buss and Ignjatović stated that it is not possible to prove the consistency of a fragment of PV without induction but with substitution in Buss's S12. However, their proof actually shows that it is not possible to prove the consistency of the system, which is obtained by the addition of propositional logic and other axioms to a system such as ours. On the other hand, the system that we have considered is strictly equational, which is a property on which our proof relies. (shrink)

V i 2 ⊢A iff for some term t :S i 2 ⊢ “2 i exists→ A”, a bounded first-order formula, i ≥1. V i 2 is not Π b 1 -conservative over S i 2 . Any model of V 2 not satisfying Exp satisfies the collection scheme BΣ 0 1 . V 1 3 is not Π b 1 -conservative over S 2.

We prove that PTCN cannot be a model of U12. This implies that there exists a first order sentence of bounded arithmetic which is provable in U12 but does not hold in PTCN.

We show how to formalize approximate counting via hash functions in subsystems of bounded arithmetic, using variants of the weak pigeonhole principle. We discuss several applications, including a proof of the tournament principle, and an improvement on the known relationship of the collapse of the bounded arithmetic hierarchy to the collapse of the polynomial-time hierarchy.

The bounded arithmetic theories R2i, S2i, and T2i are closely connected with complexity theory. This paper is motivated by the questions: what are the Σi+1b-definable multifunctions of R2i? and when is one theory conservative over another? To answer these questions we consider theories , and where induction is restricted to prenex formulas. We also define which has induction up to the 0 or 1-ary L2-terms in the set τ. We show and and for . We show that the (...) -multifunctions of are FPΣip and that those of are FPΣip. For -definability we get FPΣi+k+1p for all these theories. Write for the set of terms 2min,t) where ℓ is a finite product of terms in τ and tL2. We prove and we show - INDτ provided τO2. This gives a proof theoretic proof that S2iΔi+1b-LIND and -LLIND solving an open problem. For τO2, we define using weak replacement axioms and show . We show if or if or if where τ′ has an unbounded term then PH=B. We separate PΣip from PΣip for behaved ℓ and deduce theory separations. We lastly introduce a notion of a model separating two theories and derive some consequences. (shrink)

We describe a method of forcing against weak theories of arithmetic and its applications in propositional proof complexity.

We will give a two-sort system which axiomatizes winning strategies for the combinatorial game Node Kayles. It is shown that our system captures alternating polynomial time reasonings in the sense that the provably total functions of the theory corresponds to those computable in APTIME. We will also show that our system is equivalently axiomatized by Sprague–Grundy theorem which states that any Node Kayles position is provably equivalent to some NIM heap.

We formalize the notion of Herbrand Consistency in an appropriate way for bounded arithmetics, and show the existence of a finite fragment of IΔ0 whose Herbrand Consistency is not provable in IΔ0. We also show the existence of an IΔ0-derivable Π1-sentence such that IΔ0 cannot prove its Herbrand Consistency.

The theories Si1 and Ti1 are the analogues of Buss' relativized bounded arithmetic theories in the language where every term is bounded by a polynomial, and thus all definable functions grow linearly in length. For every i, a Σbi+1-formula TOPi, which expresses a form of the total ordering principle, is exhibited that is provable in Si+11 , but unprovable in Ti1. This is in contrast with the classical situation, where Si+12 is conservative over Ti2 w. r. t. (...) Σbi+1-sentences. The independence results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems. (shrink)

Let PLω be the provability logic of IΔ0 + ω1. We prove some containments of the form L ⊆ PLω < Th(C) where L is the provability logic of PA and Th(C) is a suitable class of Kripke frames.

The purpose of this note is to show that the independence results for sharply bounded arithmetic of Takeuti [4] and Tada and Tatsuta [3] can be obtained and, in case of the latter, improved by the model-theoretic method developed by the author in [2].

The complexity class of [Formula: see text]-polynomial local search problems is introduced and is used to give new witnessing theorems for fragments of bounded arithmetic. For 1 ≤ i ≤ k + 1, the [Formula: see text]-definable functions of [Formula: see text] are characterized in terms of [Formula: see text]-PLS problems. These [Formula: see text]-PLS problems can be defined in a weak base theory such as [Formula: see text], and proved to be total in [Formula: see text]. Furthermore, (...) the [Formula: see text]-PLS definitions can be skolemized with simple polynomial time functions, and the witnessing theorem itself can be formalized, and skolemized, in a weak base theory. We introduce a new [Formula: see text]-principle that is conjectured to separate [Formula: see text] and [Formula: see text]. (shrink)

We give combinatorial and computational characterizations of the NP search problems definable in the bounded arithmetic theories $T_{2}^{2}$ and $T_{3}^{2}$.

A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1) Feasible (...) interpolation theorems for the following proof systems: (a) resolution (b) a subsystem of LK corresponding to the bounded arithmetic theory S 2 2 (α) (c) linear equational calculus (d) cutting planes. (2) New proofs of the exponential lower bounds (for new formulas) (a) for resolution ([15]) (b) for the cutting planes proof system with coefficients written in unary ([4]). (3) An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory S 2 2 (α). In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle. (shrink)

We investigate the theory IΔ 0 + Ω 1 and strengthen [Bu86. Theorem 8.6] to the following: if NP ≠ co-NP. then Σ-completeness for witness comparison formulas is not provable in bounded arithmetic. i.e. $I\delta_0 + \Omega_1 + \nvdash \forall b \forall c (\exists a(\operatorname{Prf}(a.c) \wedge \forall = \leq a \neg \operatorname{Prf} (z.b))\\ \rightarrow \operatorname{Prov} (\ulcorner \exists a(\operatorname{Prf}(a. \bar{c}) \wedge \forall z \leq a \neg \operatorname{Prf}(z.\bar{b})) \urcorner)).$ Next we study a "small reflection principle" in bounded arithmetic. (...) We prove that for all sentences φ $I\Delta_0 + \Omega_1 \vdash \forall x \operatorname{Prov}(\ulcorner \forall y \leq \bar{x} (\operatorname{Prf} (y. \overline{\ulcorner \varphi \urcorner}) \rightarrow \varphi)\urcorner).$ The proof hinges on the use of definable cuts and partial satisfaction predicates akin to those introduced by Pudlak in [Pu86]. Finally, we give some applications of the small reflection principle, showing that the principle can sometimes be invoked in order to circumvent the use of provable Σ-completeness for witness comparison formulas. (shrink)

For all i ≥ 1, Ti+11 is not ∀Σb2-conservative over Ti1.

Samuel R. Buss and Aleksandar Ignjatović. Unprovability of Consistency Statements in Fragments of Bounded Arithmetic.

We show that length initial submodels of S12 can be extended to a model of weak second order arithmetic. As a corollary we show that the theory of length induction for polynomially bounded second order existential formulae cannot define the function division.

We prove two conservation results involving a generalization of the principle of strict ${\Pi^1_1}$ -reflection, in the context of bounded arithmetic. In this context a separation between the concepts of bounded set and binary sequence seems to emerge as fundamental.