Ulrich Kohlenbach

Title: Proof Interpretations, "Hard Analysis" and Ergodic Theory

Abstract: Building upon pioneering ideas of G. Kreisel,
going back to the 50's, a new applied form of proof theory emerged
during the last 20 year. Here the emphasis is on applications of
so-called proof interpretations to concrete mathematical proofs
with the aim of extracting effective bounds as well as new
uniformity results from prima facie ineffective proofs.
This has led to new results in number theory, approximation
theory, nonlinear analysis, geodesic geometry and ergodic theory
as well as the development of logical metatheorems that explain
these results as instances of general logical phenomena. Specialized
to the examples discussed in T. Tao's recent essay "Soft analysis,
hard analysis, and the finite convergence principle" the logical
machinery yields very much the type of quantitative finitary
versions of analytical theorems as considered by Tao.
We will argue that such logical methods based on appropriate functional
interpretations provide a systematic approach to Tao's program of
"hard analysis".
We will also give a recent application (joint work with L. Leustean)
of proof mining to ergodic theory.