Classical analysis in weak systems of finite type
Ulrich Kohlenbach, University of Aarhus
Abstract
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
-
discuss the range and limits of polynomially bounded analysis PBA,
-
the range and limits of PRA-reducible analysis PRedA detecting a
precise borderline between fragments of analysis which are
PRA-conservative and analytical principles which just go beyond the
strength of PRA,
-
introduce a new PA-conservative extension (of a finite type version
of) ACA_0 which is based on strong principles of uniform
boundedness.
click here for nicer ps format.