Classical analysis in weak systems of finite type

Ulrich Kohlenbach, University of Aarhus


In the 70s S. Feferman introduced a mathematically strong system S=restricted(PA^omega)+QF-AC+mu for classical mathematics (and in particular analysis) and showed that S is conservative over Peano arithmetic PA. S is formulated in the language of arithmetic in all finite types (with induction restricted to arithmetical formulas) and based on a non-constructive mu-operator. The conservation proof uses Gödel's functional interpretation relative to mu. In this talk we survey some of our work which was stimulated by Feferman's paper: systems in the language of finite types allow a rather direct formalization of important analytical concepts and functional interpretation, because of its good behaviour with respect to the logical deduction rules (`modularity'), is a very useful tool to extract constructive data out of given proofs. For these data to be of mathematical relevance it is important to keep their numerical complexity low (in particular well below general alpha(< epsilon_0)-recursion). This led to the study of systems of finite type which still allow to formalize substantial parts of analysis, but which also guarantee the extractability of primitive recursive, elementary recursive and even polynomial data. In this talk we

click here for nicer ps format.