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 introduce multifunction algebras B i τ where τ is a set of 0 or 1-ary terms used to bound recursion lengths. We show that if for all ℓ ∈ τ we have ℓ ∈ O then B i τ = FP Σ i−1 p , those multifunctions computable in polynomial time with at most O )) queries to a Σ i−1 p witness oracle for ℓ ∈ τ and p a polynomial. We use our algebras to obtain independence results (...) in bounded arithmetic. In particular, we show if S 2 i proves Σ j b = PH for some j⩾i then S 2 i ≼ B S 2 . This implies if P NP ≠ P NP then S 2 1 does not prove the polynomial hierarchy collapses. We then consider a subtheory, Z , of the well-studied bounded arithmetic theory S 2 = ∪ i S 2 i . Using our algebras we establish the following properties of this theory: Z cannot prove the polynomial hierarchy collapses. In fact, even Z+ Π ̂ 0 b -consequences of S 2 cannot prove the hierarchy collapses. If Z ⊆ S 2 i for any i then the polynomial hierarchy collapses. If Z proves the polynomial hierarchy is infinite then for all i , S 2 i ⊢ Σ i p ≠ Π i p. (shrink)

The paper establishes lower bounds on the provability of.

This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.

This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.

It is well known that S12 cannot prove the injective weak pigeonhole principle for polynomial time functions unless RSA is insecure. In this note we investigate the provability of the surjective weak pigeonhole principle in S12 for provably weaker function classes.

The use of $Nepomnja\check{s}\check{c}i\check{i}'s$ Theorem in the proofs of independence results for bounded arithmetic theories is investigated. Using this result and similar ideas, it is shown that at least one of S1 or TLS does not prove the Matiyasevich-Robinson-Davis-Putnam Theorem. It is also established that TLS does not prove a statement that roughly means nondeterministic linear time is equal to co-nondeterministic linear time. Here S1 is a conservative extension of the well-studied theory IΔ0 and TLS is a theory for LOGSPACE (...) reasoning. (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)

In this paper we provide a new arithmetic characterization of the levels of the og-time hierarchy . We define arithmetic classes equation image and equation image that correspond to equation image-LOGTIME and equation image-LOGTIME, respectively. We break equation image and equation image into natural hierarchies of subclasses equation image and equation image. We then define bounded arithmetic deduction systems equation image′ whose equation image-definable functions are precisely B. We show these theories are quite strong in that LIOpen proves for any (...) fixed m that equation image, TAC, a theory that is slightly stronger than equation image′ whose equation image-definable functions are LH, proves LH is not equal to equation image-TIME for any m> 0, where 2s ∈L, s ∈ ω, and TAC proves LH ≠ equation image for all k and m. We then show that the theory TAC cannot prove the collapse of the polynomial hierarchy. Thus any such proof, if it exists, must be argued in a stronger systems than ours. (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)