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)

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)

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.

We construct models of the integers, to yield: witnessing, independence and separation results for weak systems of bounded induction.

We define and study a new restricted consistency notion RCon ∗ for bounded arithmetic theories T 2 j . It is the strongest ∀ Π 1 b -statement over S 2 1 provable in T 2 j , similar to Con in Krajíček and Pudlák, 29) or RCon in Krajı́ček and Takeuti 107). The advantage of our notion over the others is that RCon ∗ can directly be used to construct models of T 2 j . We apply this by (...) proving preservation theorems for theories of bounded arithmetic of the following well-known kind: The ∀ Π 1 b -separation of bounded arithmetic theories S 2 i from T 2 j is equivalent to the existence of a model of S 2 i which does not have a Δ 0 b -elementary extension to a model of T 2 j . More specific, let M ⊨ Ω 1 nst denote that there is a nonstandard element c in M such that the function n ↦ 2 log c is total in M . Let BLΣ 1 b be the bounded collection schema for Σ 1 b -formulas. We obtain the following preservation results: the ∀ Π 1 b -separation of S 2 i from T 2 j is equivalent to the existence of 1. a model of S 2 i +Ω 1 nst which is 1 b -closed w.r.t. T 2 j , 2. a countable model of S 2 i + BLΣ 1 b without weak end extensions to models of T 2 j. (shrink)

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)

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)

Dynamic ordinal analysis is ordinal analysis for weak arithmetics like fragments of bounded arithmetic. In this paper we will define dynamic ordinals – they will be sets of number theoretic functions measuring the amount of sΠ b 1(X) order induction available in a theory. We will compare order induction to successor induction over weak theories. We will compute dynamic ordinals of the bounded arithmetic theories sΣ b n (X)−L m IND for m=n and m=n+1, n≥0. Different dynamic ordinals lead to (...) separation. In this way we will obtain several separation results between these relativized theories. We will generalize our results to further languages extending the language of bounded arithmetic. (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)

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)

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)

Let H be a proof system for quantified propositional calculus (QPC). We define the Σqj-witnessing problem for H to be: given a prenex Σqj-formula A, an H-proof of A, and a truth assignment to the free variables in A, find a witness for the outermost existential quantifiers in A. We point out that the Σq1-witnessing problems for the systems G*1and G1 are complete for polynomial time and PLS (polynomial local search), respectively. We introduce and study the systems G*0 and G0, (...) in which cuts are restricted to quantifier-free formulas, and prove that the Σqj-witnessing problem for each is complete for NC1. Our proof involves proving a polynomial time version of Gentzen’s midsequent theorem for G*0 and proving that G0-proofs are TC0-recognizable. We also introduce QPC systems for TC0 and prove witnessing theorems for them. We introduce a finitely axiomatizable second-order system VNC1 of bounded arithmetic which we prove isomorphic to Arai’s first order theory AID + Σb0-CA for uniform NC1. We describe simple translations of VNC1 proofs of all bounded theorems to polynomial size families of G*0 proofs. From this and the above theorem we get alternative proofs of the NC1 witnessing theorems for VNC1 and AID. (shrink)

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)

Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations. Explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.