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.

A well-known result states that, over basic Kalmar elementary arithmetic EA, the induction schema for ∑n formulas is equivalent to the uniform reflection principle for ∑n + 1 formulas . We show that fragments of arithmetic axiomatized by various forms of induction rules admit a precise axiomatization in terms of reflection principles as well. Thus, the closure of EA under the induction rule for ∑n formulas is equivalent to ω times iterated ∑n reflection principle. Moreover, for k < ω, k (...) times iterated ∑n reflection principle over EA precisely corresponds to the extension of EA by k nested applications of ∑n induction rule.The above relationship holds in greater generality than just stated. In fact, we give general formulas characterizing in terms of iterated reflection principles the extension of any given theory by k nested applications of ∑n or Πn induction rules. In particular, the closure of a theory T under just one application of ∑1 induction rule is equivalent to T together with ∑1 reflection principle for each finite Π2 axiomatized subtheory of T.These results have closely parallel ones in the theory of subrecursive function classes. The rules under study correspond, in a canonical way, to natural closure operators on the classes of provably recursive functions. Thus, ∑1 induction rule precisely corresponds to the primitive recursive closure operator, and ∑1 collection rule, introduced below, corresponds to the elementary closure operator. (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.

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 show that the quantified propositional proof systems Gi are polynomially equivalent to their restricted versions that require all cut formulas to be prenex Σqi . Previously this was known only for the treelike systems G*i. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

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 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 investigate the possibility to characterize (multi)functions that are-definable with smalli(i= 1, 2, 3) in fragments of bounded arithmeticT2in 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 areand-definable in the theoriesand.(2) New characterizations of (multi)functions that areand-definable in the theory.(3) A new non-conservation result: the theoryis not-conservative over the theory.To prove that the theoryis not-conservative over the theory, we present two examples of a-principle separating the two (...) theories:(a) the weak pigeonhole principle WPHP(a2,f, g) formalizing that no functionfis a bijection betweena2andawith the inverseg,(b) the iteration principle Iter(a, R, f) formalizing that no functionfdefined on a strict partial order ({0,…, a},R) can have increasing iterates. (shrink)

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)

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

Let Iπ2 denote the fragment of Peano Arithmetic obtained by restricting the induction scheme to parameter free Π2Π2 formulas. Answering a question of R. Kaye, L. Beklemishev showed that the provably total computable functions of Iπ2 are, precisely, the primitive recursive ones. In this work we give a new proof of this fact through an analysis of certain local variants of induction principles closely related to Iπ2. In this way, we obtain a more direct answer to Kaye's question, avoiding the (...) metamathematical machinery needed for Beklemishev's original proof.Our methods are model-theoretic and allow for a general study of Iπn+1 for all n≥0n≥0. In particular, we derive a new conservation result for these theories, namely that Iπn+1 is πn+2 -conservative over IΣn for each n≥1n≥1. (shrink)

We prove the following theorem: Let φ be a formula in the language of the theory PA− of discretely ordered commutative rings with unit of the form ∃yφ′ with φ′ and let ∈ Δ0 and let fφ: ℕ → ℕ such that fφ = y iff φ′ & < xK). Here I ∏math image1− denotes the theory PA− plus the scheme of induction for formulas φ of the form ∀yφ′ with φ′ ∈ Δ0.