An unexpected separation result in Linearly Bounded Arithmetic

✍ Scribed by Arnold Beckmann; Jan Johannsen

• Publisher: John Wiley and Sons
• Year: 2005
• Tongue: English
• Weight: 170 KB
• Volume: 51
• Category: Article
• ISSN: 0044-3050
• DOI: 10.1002/malq.200410019

✦ Synopsis

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

The independence results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems.