Structure and definability in general bounded arithmetic theories Original Research Article

The bounded arithmetic theories View the MathML source, and View the MathML source are closely connected with complexity theory. This paper is motivated by the questions: what are the View the MathML source-definable multifunctions of View the MathML source? and when is one theory conservative over another? To answer these questions we consider theories View the MathML source, and View the MathML source where induction is restricted to prenex formulas. We also define View the MathML source which has induction up to the 0 or 1-ary View the MathML source-terms in the set τ. We show View the MathML source and View the MathML source and for View the MathML source. We show that the View the MathML source-multifunctions of View the MathML source are View the MathML source and that those of View the MathML source are View the MathML source. For View the MathML source-definability we get View the MathML source for all these theories. Write View the MathML source for the set of terms View the MathML source where ℓ is a finite product of terms in τ and View the MathML source. We prove View the MathML source and we show View the MathML source- INDτ provided View the MathML source. This gives a proof theoretic proof that View the MathML source-LIND and View the MathML source-LLIND solving an open problem. For View the MathML source, we define View the MathML source using weak replacement axioms and show View the MathML source. We show if View the MathML source or if View the MathML source or if View the MathML source where τ′ has an unbounded term then View the MathML source. We separate View the MathML source from View the MathML source for behaved ℓ and deduce theory separations. We lastly introduce a notion of a model separating two theories and derive some consequences.