### arnold beckmann's pages

## Ordinal Notations and Well-Orderings in Bounded Arithmetic

**File:** PDF-File

**Author:** Arnold Beckmann, Samuel R. Buss, Chris Pollett

**Title:** Ordinal Notations and Well-Orderings in Bounded Arithmetic

**Journal:** Ann.Pur.Appl.Logic 2003, **120**: 197-223

**DOI:** 10.1016/S0168-0072(02)00066-0

**Abstract:**
Ordinal notations and provability of well-foundedness
have been a central
tool in the study of the consistency strength and computational
strength of formal theories of arithmetic. This development began
with Gentzen's consistency proof for Peano arithmetic based on the
well-foundedness of ordinal notations up to
ε_{0}
.
Since the work of Gentzen, ordinal notations and provable
well-foundedness have been studied extensively for many other formal
systems, some stronger and some weaker than Peano arithmetic.
In the present paper, we investigate the provability and non-provability
of well-foundedness of ordinal notations in very weak theories of
bounded arithmetic, notably the theories
S
i
2
and
T
i
2
with
1 ≤ i ≤ 2
.
We prove several results about the provability of well-foundedness
for ordinal notations; our main results state that for the usual
ordinal notations for ordinals below
ε_{0}
and
Γ_{0}
,
the theories
T
i
2
and
S
2
2
can prove
the ordinal
Σ
b
1
- minimization principle over a
bounded domain.
PLS
is the class of functions computed by a
polynomial local search to minimize a cost function.
It is a corollary of our theorems that the cost function can
be allowed to take on ordinal values below
Γ_{0}
, without increasing the class
PLS
.