[FOM] Of possible interest to Proof Theorists

[steve newberry]

"PROOF Theoretic Complexity of Low Subrecursive Classes"
Naim CAGMAN
Dept. of Mathematics, University of Gaziosmanpasa, Tokat, 60100, Turkey
Georey E. OSTRIN
CMAF, University of Lisbon, Lisbon, 1649-003, Portugal
Stanley S. WAINER
School of Mathematics, University of Leeds, Leeds, LS2 9JT, UK

Abstract. A two-sorted version of Peano Arithmetic is developed,
with proof-rules corresponding to the normal/safe recursion schemes of
Bellantoni and Cook. Classical methods of proof theory still apply,
but now the provably recursive functions are brought down to more
computationally realistic levels than in the single-sorted case, since the
bounding functions turn out to be \slow growing" rather than \fast
growing". Results very similar to earlier ones of Leivant are obtained
characterizing Grzegorczyk's classes E2 (in the existential fragment) and
E3 (in the full theory).