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 give combinatorial and computational characterizations of the NP search problems definable in the bounded arithmetic theories $T_{2}^{2}$ and $T_{3}^{2}$.

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 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 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 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 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 present a simple propositional proof system which consists of a single axiom schema and a single rule, and use this system to construct a sequence of combinatorial tautologies that, when added to any Frege system, p-simulates extended-Frege systems.