Parameter free induction and provably total computable functions

AbstractWe study the classes of computable functions that can be proved to be total by means of parameter free Σn and Πn, induction schemata, IΣn− and IΠn−, over Kalmar elementary arithmetic. We give a positive answer to a question, whether the provably total computable functions of IΠ2− are exactly the primitive recursive ones, and show that the class of such functions for IΣ1 + IΠ2− coincides with the class of doubly recursive functions of Peter. We also characterize provably total computable functions of theories of the form IΠn + 1− and IΣn + IΠn + 1− for all n ⩾ 1, in terms of the fast growing hierarchy.These results are based on a precise characterization of IΣn− and IΠn− in terms of reflection principles and conservation results for local reflection principles obtained by techniques of modal provability logic. Using similar ideas we show that IΠn + 1− is conservative over IΣn− w.r.t. boolean combinations of Σn + 1 sentences, for n ⩾ 1, and obtain a number of results on the strength of bounded number of instances of parameter free induction schemata and complexity of their axiomatization