An unexpected separation result in Linearly Bounded Arithmetic

The theories S i 1 ( α ) and T i 1 ( α ) are the analogues of Buss' relativized bounded arithmetic theories in the language where every term is bounded by a polynomial, and thus all definable functions grow linearly in length. For every i , a Σ b i +1 ( α )‐formula TOP i ( a ), which expresses a form of the total ordering principle, is exhibited that is provable in S i +1 1 ( α ), but unprovable in T i 1 ( α ). This is in contrast with the classical situation, where S i +1 2 is conservative over T i 2 w. r. t. Σ b i +1 ‐sentences. The independence results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)