Elementary arithmetic

Abstract. There is a very simple way in which the safe/normal variable discipline of Bellantoni-Cook recursion (1992) can be imposed on arithmetical theories like PA: quantify over safes and induct on normals. This weakens the theory severely, so that the provably recursive functions become more realistically computable (slow growing rather than fast growing). Earlier results of Leivant (1995) are re-worked and extended in this new context, giving proof-theoretic characterizations (according to the levels of induction used) of complexity classes between Grzegorczyk's E2 and E3. This is a contribution to the search for syntactically simple theories, without explicitly-imposed bounds on quantifiers as in Buss [3], whose provably recursive functions form "more feasible" complexity classes (than for example the primitive recursive functions). We develop a quite different, alternative treatment of Leivant's results in [6], where ramified inductions over N are cleverly us...

• Type: Journal
• Year: 2005
• Where: APAL
• Authors: Geoffrey E. Ostrin, Stanley S. Wainer
• Keywords: APAL 2005, Proof-theoretic Characterizations, Recursive Functions, Variable Discipline