An unexpected separation result in Linearly Bounded Arithmetic

Mathematical Logic Quarterly 51 (2):191-200 (2005)
  Copy   BIBTEX


The theories Si1 and Ti1 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 Σbi+1-formula TOPi, which expresses a form of the total ordering principle, is exhibited that is provable in Si+11 , but unprovable in Ti1. This is in contrast with the classical situation, where Si+12 is conservative over Ti2 w. r. t. Σbi+1-sentences. The independence results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems



    Upload a copy of this work     Papers currently archived: 76,168

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles


Added to PP

28 (#418,389)

6 months
1 (#448,551)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Structure and definability in general bounded arithmetic theories.Chris Pollett - 1999 - Annals of Pure and Applied Logic 100 (1-3):189-245.
Dynamic ordinal analysis.Arnold Beckmann - 2003 - Archive for Mathematical Logic 42 (4):303-334.

Add more references