Accessible Recursive Functions (going back 20 years)

Professor Stan Wainer, University of Leeds. Part of the proofs, constructions and computations seminar series.

The class of all recursive functions fails to possess a natural hierarchical structure, generated predicatively "from within".  On the other hand, many (proof theoretically significant) sub-recursive classes do. We attempt to measure the limit of predicative generation in this context, by classifying and characterizing those (predicatively terminating) recursive functions which can be successively defined according to an autonomy condition of the form: Allow recursions only over well-orderings which have already been "coded" at previous levels. The question is "How can a recursion code a well-ordering?". The answer lies in Girard's theory of dilators, but is reworked here in a quite different and simplified form specific to our purpose. The "accessible" recursive functions thus generated turn out to be those provably recursive in Pi^1_1-CA_0.