An unexpected separation result in Linearly Bounded Arithmetic - Arnold Beckmann (MLQ, 2005)
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 TOPi(α) , 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.