Wolfram Pohlers

In this paper we revisit our contribution to Lecture Note 897 and present a computation of the prooftheoretic ordinals of formal theories for iterated inductive definitions together with a characterization of their provably recursive functions. The techniques used here differ essentially from the original ones. Sections 1–5 contain a general survey of the connections between recursion theoretic and proof theoretic ordinals and roughly recap some basic facts on iterated inductive definitions. Beginning with Sect. 6 the paper becomes more technical. After introducing the semi–formal system for iterated inductive definition and the necessary ordinals we compute the ordinal spectrum of the formal theory for iterated inductive definitions and characterize their provably total functions in terms of a subrecursive hierarchy. The last section briefly discusses the foundational aspects of the paper.

Apologies. The purpose of the following talk is to give an overview of the present state of aims, methods and results in Pure Proof Theory. Shortage of time forces me to concentrate on my very personal views. This entails that I will emphasize the work which I know best, i.e., work that has been done in the triangle Stanford, Munich and Münster. I am of course well aware that there are as important results coming from outside this triangle and I apologize for not displaying these results as well.Moreover the audience should be aware that in some points I have to oversimplify matters. Those who complain about that are invited to consult the original papers.1.1. General. Proof theory startedwithHilbert's Programme which aimed at a finitistic consistency proof for mathematics.By Gödel's Theorems, however, we know that we can neither formalize all mathematics nor even prove the consistency of formalized fragments by finitistic means. Inspite of this fact I want to give some reasons why I consider proof theory in the style of Gentzen's work still as an important and exciting field of Mathematical Logic. I will not go into applications of Gentzen's cut-elimination technique to computer science problems—this may be considered as applied proof theory—but want to concentrate on metamathematical problems and results. In this sense I am talking about Pure Proof Theory.Mathematicians are interested in structures. There is only one way to find the theorems of a structure. Start with an axiom system for the structure and deduce the theorems logically. These axiom systems are the objects of proof-theoretical research. Studying axiom systems there is a series of more or less obvious questions.