Proof theoretic complexity of low subrecursive classes (Q2752056)

In the paper under review a two-sorted version of Peano arithmetic is developed. Its proof-rules correspond to the normal/safe recursion schemes of Bellantoni and Cook. It is shown that 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 similar to earlier ones of Leivant are obtained -- they characterize classes \({\mathcal E}^{2}\) (in the existential fragment) and \({\mathcal E}^{3}\) (in the full theory) of the Grzegorczyk hierarchy.NEWLINENEWLINEFor the entire collection see [Zbl 0963.00029].