Well-behaved principles alternative to bounded induction

We introduce some Pi(1)-expressible combinatorial principles which may be treated as axioms for some bounded arithmetic theories. The principles, denoted Sk(Sigma(n)(b), length log(k)) and Sk(Sigma(n)(b), depth log(k)) (where 'Sk' stands for 'Skolem'), are related to the consistency of Sigma(n)(b) induction: for instance, they provide models for Sigma(n)(b) induction. However, the consistency is expressed indirectly, via the existence of evaluations for sequences of terms. The evaluations do not have to satisfy Sigma(n)(b) induction, but must determine the truth value of Sigma(n)(b) statements. Our principles have the property that Sk(Sigma(n)(b), depth log(k)) proves Sk(Sigma(n+1)(b), length log(k)). Additionally, Sk(Sigma(n)(b), length log(k-2)) proves Sk(Sigma(n+1)(b), length log(k)). Thus, some provability is involved where conservativity is known in the case of Sigma(n)(b) induction on an initial segment and induction for higher Sigma(m)(b) classes on smaller segments. (C) 2004 Elsevier B.V. All rights reserved.