Inductive definitions over a predicative arithmetic (Q2566072)

The paper begins with a brief survey of work by Ostrin and Wainer on the development of the theory EA(I;O), alternative to Leivant's, which codifies the basic principles of predicative arithmetic. The main part is devoted to a Buchholz-style proof-theoretical investigation of the theory ID\(_{1}\)(I;O) of (non-iterated) inductive definitions over predicative arithmetic. It is shown that no matter which inductive definitions are added (even Kleene's \({\mathcal O}\)), its strength, in terms of provably recursive functions, is never greater than PA. Thus PA is recaptured as the predicative theory of one inductive definition.