Elementary arithmetic (Q1772782)

The paper under review is a contribution to the search for syntactically simple theories, without explicitely imposed bounds on quantifiers, whose provably recursive functions form ``more feasible'' complexity classes. A quite different, alternative treatment of Leivant's results is developed. The characterization is extended to the first level of exponential complexity in the hierarchy between Grzegorczyk's \(E^{2}\) and \(E^{3}\). The emphasis is on cut elimination in ``traditional'' theories based on unary numerals, so complexity in the end is measured in terms of the numerical input itself rather than its binary length.