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.

We prove that the boundedness theorem of generalized recursion theory can be derived from the ω-completeness theorem for number theory. This yields a proof of the boundedness theorem which does not refer to the analytical hierarchy theorem.

We prove some independence results for the bounded arithmetic theoryR 2 0 , and we define a class of functions that is shown to be an upper bound for the class of functions definable by a certain restricted class of ∑ 1 b in extensions ofR 2 0.

We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic fixed (...) point theories which are conservative extensions of HA.6. 6. Proof theoretic strengths of classical fixed points theories.7. 7. An equivalence between transfinite induction rule and iterated reflection schema over IΣn.8. 8. Derivation lengths of finite rewrite rules reducing under lexicographic path orders and multiply recursive functions.Each section can be read separately in principle. (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 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)