Premium
An unexpected separation result in Linearly Bounded Arithmetic
Author(s) -
Beckmann Arnold,
Johannsen Jan
Publication year - 2005
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200410019
Subject(s) - mathematics , bounded function , independence (probability theory) , discrete mathematics , propositional variable , polynomial , arithmetic , combinatorics , intermediate logic , computer science , mathematical analysis , artificial intelligence , statistics , description logic
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)