Event Detail

During the last 20 years (though building upon pioneering ideas of G. Kreisel going back to the 50's) a new applied form of proof theory emerged that sometimes is referred to as "proof mining". 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 these logical methods provide a systematic approach to Tao's program of "hard analysis" and at the same time shed new light on some issues in the philosophy of mathematics.