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 prove the following results: (i) PV proves NP ⊆ P/poly iff PV proves coNP ⊆ NP/O(1). (ii) If PV proves NP ⊆ P/poly then PV proves that the Polynomial Hierarchy collapses to the Boolean Hierarchy. (iii) $S_{2}^{1}$ proves NP ⊆ P/poly iff $S_{2}^{1}$ proves coNP ⊆ NP/O(log n). (iv) If $S_{2}^{1}$ proves NP ⊆ P/poly then $S_{2}^{1}$ proves that the Polynomial Hierarchy collapses to PNP[log n]. (v) If $S_{2}^{2}$ proves NP ⊆ P/poly then $S_{2}^{2}$ proves that the Polynomial Hierarchy (...) collapses to PNP. Motivated by these results we introduce a new concept in proof complexity: proof systems with advice, and we make some initial observations about them. (shrink)

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.

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.

This paper will introduce the notion of a naming convention and use this paradigm to both develop a new version of the Second Incompleteness Theorem and to describe when an axiom system can partially evade the Second Incompleteness Theorem.

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 give a new characterization of the strict $$\forall {\Sigma^b_j}$$ sentences provable using $${\Sigma^b_k}$$ induction, for 1 ≤ j ≤ k. As a small application we show that, in a certain sense, Buss’s witnessing theorem for strict $${\Sigma^b_k}$$ formulas already holds over the relatively weak theory PV. We exhibit a combinatorial principle with the property that a lower bound for it in constant-depth Frege would imply that the narrow CNFs with short depth j Frege refutations form a strict hierarchy with (...) j, and hence that the relativized bounded arithmetic hierarchy can be separated by a family of $$\forall {\Sigma^b_1}$$ sentences. (shrink)

We prove that the sharply bounded arithmetic T02 in a language containing the function symbol ⌊x /2y⌋ is equivalent to PV1.

In this paper we naturally define when a theory has bounded quantifier elimination, or is bounded model complete. We give several equivalent conditions for a theory to have each of these properties. These results provide simple proofs for some known results in the model theory of the bounded arithmetic theories like CPV and PV1. We use the mentioned results to obtain some independence results in the context of intuitionistic bounded arithmetic. We show that, if the intuitionistic theory of polynomial induction (...) on strict $\Pi_2^{b}$ formulas proves decidability of $\Sigma_1^b$ formulas, then P=NP. We also prove that, if the mentioned intuitionistic theory proves ${\rm LMIN}(\Sigma_{1}^{b})$ , then P=NP. (shrink)

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.

Let be the fragment of elementary Peano arithmetic in which induction is restricted to -formulas. More than three decades ago, Parsons showed that the provably total functions of are exactly the primitive recursive functions. In this paper, we observe that Parsons' result is a consequence of Herbrand's theorem concerning the -consequences of universal theories. We give a self-contained proof requiring only basic knowledge of mathematical logic.

Using nonstandard methods we construct a model of an induction scheme called inside a "resource" of the form is a Turing machine of code is calculated in less than , where means the length of the binary expansion of and are nonstandard parameters in a model of . As a consequence we obtain a model theoretic proof of a witnessing theorem for this theory by functions computable in time , a result first obtained by Buss, Krajícek, and Takeuti using proof (...) theory. (shrink)

The purpose of this paper is to survey the correspondence between bounded arithmetic and propositional proof systems. In addition, it also contains some new results which have appeared as an extended abstract in the proceedings of the conference TAMC 2008 [11].Bounded arithmetic is closely related to propositional proof systems; this relation has found many fruitful applications. The aim of this paper is to explain and develop the general correspondence between propositional proof systems and arithmetic theories, as introduced by Krajíček and (...) Pudlák [46]. Instead of focusing on the relation between particular proof systems and theories, we favour a general axiomatic approach to this correspondence. In the course of the development we particularly highlight the role played by logical closure properties of propositional proof systems, thereby obtaining a characterization of extensions of EF in terms of a simple combination of these closure properties (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim). (shrink)

Conservative subtheories of $${{R}^{1}_{2}}$$ and $${{S}^{1}_{2}}$$ are presented. For $${{S}^{1}_{2}}$$, a slight tightening of Jeřábek’s result (Math Logic Q 52(6):613–624, 2006) that $${T^{0}_{2} \preceq_{\forall \Sigma^{b}_{1}}S^{1}_{2}}$$ is presented: It is shown that $${T^{0}_{2}}$$ can be axiomatised as BASIC together with induction on sharply bounded formulas of one alternation. Within this $${\forall\Sigma^{b}_{1}}$$ -theory, we define a $${\forall\Sigma^{b}_{0}}$$ -theory, $${T^{-1}_{2}}$$, for the $${\forall\Sigma^{b}_{0}}$$ -consequences of $${S^{1}_{2}}$$. We show $${T^{-1}_{2}}$$ is weak by showing it cannot $${\Sigma^{b}_{0}}$$ -define division by 3. We then consider what (...) would be the analogous $${\forall\hat\Sigma^{b}_{1}}$$ -conservative subtheory of $${R^{1}_{2}}$$ based on Pollett (Ann Pure Appl Logic 100:189–245, 1999. It is shown that this theory, $${{T}^{0,\left\{2^{(||\dot{id}||)}\right\}}_{2}}$$, also cannot $${\Sigma^{b}_{0}}$$ -define division by 3. On the other hand, we show that $${{S}^{0}_{2}+open_{\{||id||\}}}$$ -COMP is a $${\forall\hat\Sigma^{b}_{1}}$$ -conservative subtheory of $${R^{1}_{2}}$$. Finally, we give a refinement of Johannsen and Pollett (Logic Colloquium’ 98, 262–279, 2000) and show that $${\hat{C}^{0}_{2}}$$ is $${\forall\hat\Sigma^{b}_{1}}$$ -conservative over a theory based on open cl-comprehension. (shrink)

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)

We formulate schemes and of the “typical” ∀∑ 1 b -sentences that are provable in T 2 1, respectively T 2 2. As an application, we reprove a recent result of Buss and Krajíček which describes witnesses for the ∀∑ 1 b -sentences provable in T 2 1 in terms of solutions to PLS-problems.

We study the long-standing open problem of giving$\forall {\rm{\Sigma }}_1^b$separations for fragments of bounded arithmetic in the relativized setting. Rather than considering the usual fragments defined by the amount of induction they allow, we study Jeřábek’s theories for approximate counting and their subtheories. We show that the$\forall {\rm{\Sigma }}_1^b$Herbrandized ordering principle is unprovable in a fragment of bounded arithmetic that includes the injective weak pigeonhole principle for polynomial time functions, and also in a fragment that includes the surjective weak pigeonhole (...) principle for FPNPfunctions. We further give new propositional translations, in terms of random resolution refutations, for the consequences of$T_2^1$augmented with the surjective weak pigeonhole principle for polynomial time functions. (shrink)

We introduce a class of models of the bounded arithmetic theoryPV n . These models, which are generated by their tally part, have a curious feature: they have end-extensions or satisfyB∑ n b only in case they are closed under exponentiation. As an application, we show that if then the polynomial hierarchy does not collapse.

Let g be a map defined as the Nisan–Wigderson generator but based on an NP ∩ coNP -function f. Any string b outside the range of g determines a propositional tautology τb expressing this fact. Razborov [27] has conjectured that if f is hard on average for P/poly then these tautologies have no polynomial size proofs in the Extended Frege system EF. We consider a more general Statement that the tautologies have no polynomial size proofs in any propositional proof system. (...) This is equivalent to the statement that the complement of the range of g contains no infinite NP set. We prove that Statement is consistent with Cook' s theory PV and, in fact, with the true universal theory T PV in the language of PV. If PV in this consistency statement could be extended to "a bit" stronger theory then Razborov's conjecture would follow, and if TPV could be added too then Statement would follow. We discuss this problem in some detail, pointing out a certain form of reflection principle for propositional logic, and we introduce a related feasible disjunction property of proof systems. (shrink)

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 formulate schemes and of the “typical” ∀∑ 1 b -sentences that are provable in T 2 1 , respectively T 2 2 . As an application, we reprove a recent result of Buss and Krajíček which describes witnesses for the ∀∑ 1 b -sentences provable in T 2 1 in terms of solutions to PLS-problems.

This paper defines natural hierarchies of function and relation classes □i,kc and Δi,kc, constructed from parallel complexity classes in a manner analogous to the polynomial-time hierarchy. It is easily shown that □i−1,kp □c,kc □i,kp and similarly for the Δ classes. The class □i,3c coincides with the single-valued functions in Buss et al.'s class , and analogously for other growth rates. Furthermore, the class □i,kc comprises exactly the functions Σi,kb-definable in Ski−1, and if Tki−1 is Σi,kb-conservative over Ski−1, then □i,kp is (...) completely parallelizable. All functions in □i,kc are Σi,kb-definable in Rki; this suffices to show that if the known Σi,kb conservativity between R3i and S3i−1 extends to R2i and S2i−1, then NC = NC1 relative to an oracle in PH. We prove a KPT-style witnessing theorem for Ski using constantly many rounds of □i,kc interactive computation, and thus show that if Ski ≡ Rki+1 then the bounded arithmetic hierarchy collapses, provably in Ski. (shrink)

We consider tautologies formed form a pseudo-random number generator, defined in Krajicek [11] and in Alekhnovich et al. [2]. We explain a strategy of proving their hardness for Extended Frege systems via a conjecture about bounded arithmetic formulated in Krajicek [11]. Further we give a purely finitary statement, in the form of a hardness condition imposed on a function, equivalent to the conjecture. This is accompanied by a brief explanation, aimed at non-specialists, of the relation between prepositional proof complexity and (...) bounded arithmetic. (shrink)

We introduce a second-order system V1-Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Grädel's 35) second-order Horn characterization of P. Our system has comprehension over P predicates , and only finitely many function symbols. Other systems of polynomial-time reasoning either allow induction on NP predicates , and hence are more powerful than our system , or use Cobham's theorem to introduce function symbols for all polynomial-time functions . We prove that our system is equivalent to QPV and Zambella's P-def. (...) Using our techniques, we also show that V1-Horn is finitely axiomatizable, and, as a corollary, that the class of Σ1b consequences of S21 is finitely axiomatizable as well, thus answering an open question. (shrink)

The question of whether the bounded arithmetic theories and are equal is closely connected to the complexity question of whether is equal to. In this paper, we examine the still open question of whether the prenex version of,, is equal to. We give new dependent choice‐based axiomatizations of the ‐consequences of and. Our dependent choice axiomatizations give new normal forms for the ‐consequences of and. We use these axiomatizations to give an alternative proof of the finite axiomatizability of and to (...) show new results such as is finitely axiomatized and that there is a finitely axiomatized theory,, containing and contained in. On the other hand, we show that our theory for splits into a natural infinite hierarchy of theories. We give a diagonalization result that stems from our attempts to separate the hierarchy for. (shrink)

We prove that if the linear-time and polynomial-time hierarchies coincide, then every model of Π1 + ¬Ω1has a proper end-extension to a model of Π1, and so Π1 + ¬Ω ⊢ BΣ1. Under an even stronger complexity-theoretic assumption which nevertheless seems hard to disprove using present-day methods, Π1 + ¬Exp ⊢ BΣ1. Both assumptions can be modified to versions which make it possible to replace Π1 by IΔ0as the base theory.We also show that any proof that IΔ0+ ¬Exp does not (...) prove a given finite fragment of BΣ1has to be “nonrelativizing”, in the sense that it will not work in the presence of an arbitrary oracle. (shrink)

We consider tautologies formed from a pseudo-random number generator, defined in Krajíček [11] and in Alekhnovich et al. [2]. We explain a strategy of proving their hardness for Extended Frege systems via a conjecture about bounded arithmetic formulated in Krajíček [11]. Further we give a purely finitary statement, in the form of a hardness condition imposed on a function, equivalent to the conjecture.

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.

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 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.

A polynomial time ultrapower is a structure given by the set of polynomial time computable functions modulo some ultrafilter. They model the universal theory \ of all polynomial time functions. Generalizing a theorem of Hirschfeld :111–126, 1975), we show that every countable model of \ is isomorphic to an existentially closed substructure of a polynomial time ultrapower. Moreover, one can take a substructure of a special form, namely a limit polynomial time ultrapower in the classical sense of Keisler Ultrafilters across (...) mathematics, contemporary mathematics vol 530, pp 163–179. AMS, New York, 1963). Using a polynomial time ultrapower over a nonstandard Herbrand saturated model of \ we show that \ is consistent with a formal statement of a polynomial size circuit lower bound for a polynomial time computable function. This improves upon a recent result of Krajíček and Oliveira, 2017). (shrink)

Motivated by the problem of finding finite versions of classical incompleteness theorems, we present some conjectures that go beyond NP ≠ coNP. These conjectures formally connect computational complexity with the difficulty of proving some sentences, which means that high computational complexity of a problem associated with a sentence implies that the sentence is not provable in a weak theory, or requires a long proof. Another reason for putting forward these conjectures is that some results in proof complexity seem to be (...) special cases of such general statements and we want to formalize and fully understand these statements. Roughly speaking, we are trying to connect syntactic complexity, by which we mean the complexity of sentences and strengths of the theories in which they are provable, with the semantic concept of complexity of the computational problems represented by these sentences. -/- We have introduced the most fundamental conjectures in our earlier works. Our aim in this article is to present them in a more systematic way, along with several new conjectures, and prove new connections between them and some other statements studied before. (shrink)

When restricted to proving $\Sigma _{i}^{q}$ formulas, the quantified propositional proof system $G_{i}^{\ast}$ is closely related to the $\Sigma _{i}^{b}$ theorems of Buss's theory $S_{2}^{i}$ . Namely, $G_{i}^{\ast}$ has polynomial-size proofs of the translations of theorems of $S_{2}^{i}$ , and $S_{2}^{i}$ proves that $G_{i}^{\ast}$ is sound. However, little is known about $G_{i}^{\ast}$ when proving more complex formulas. In this paper, we prove a witnessing theorem for $G_{i}^{\ast}$ similar in style to the KPT witnessing theorem for $T_{2}^{i}$ . This witnessing theorem (...) is then used to show that $S_{2}^{i}$ proves $G_{i}^{\ast}$ is sound with respect to $\Sigma _{i+1}^{q}$ formulas. Note that unless the polynomial-time hierarchy collapses $S_{2}^{i}$ is the weakest theory in the s₂ hierarchy for which this is true. The witnessing theorem is also used to show that $G_{i}^{\ast}$ is p-equivalent to a quantified version of extended-Frege for prenex formulas. This is followed by a proof that Gi p-simulates $G_{i+1}^{\ast}$ with respect to all quantified propositional formulas. We finish by proving that S₂ can be axiomatized by $S_{2}^{1}$ plus axioms stating that the cut-free version of $G_{0}^{\ast}$ is sound. All together this shows that connection between $G_{i}^{\ast}$ and $S_{2}^{i}$ does not extend to more complex formulas. (shrink)