arnold beckmann's pages
An Unexpected Separation Result in Linearly Bounded Arithmetic
File: PDFFile
Author: Arnold Beckmann and Jan Johannsen
Title: An Unexpected Separation Result in Linearly Bounded Arithmetic
Journal: Math. Log. Quart. 2005, 51: 191200
DOI: 10.1002/malq.200410019
Abstract:
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}(α)
, 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.