Title: Proof Theory: From the Foundations of Mathematics to Applications in Core Mathematics

Speaker: Prof.Ulrich Kohlenbach (Technical University of Darmstadt,Germany)

Time: 2021-03-09  16:00-18:00

ZOOMID: 676 8585 0217   Password: 20210309

Abstract: During the last two decades a systematic program of 'proof mining' emerged as a new applied form of proof theory and has successfully been applied to a number of areas of core mathematics. This program has its roots in Georg Kreisel's pioneering ideas of 'unwinding of proofs' going back to the 1950's who asked for a‘shift of emphasis’in proof theory away from issues of mere consistency of mathematical theories ('Hilbert's program') to the question 'What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?' We are primarily concerned with the extraction of hidden finitary and combinatorial content from proofs that make use of infinitary noneffective principles. The main logical tools for this are so-called interpretation. Logical meta-theorems based on such interpretations have been applied with particular success in the context of nonlinear analysis including fixed point theory, ergodic theory, continuous optimization, game theory and abstract Cauchy problems. The combinatorial content can manifest itself both in explicit effective bounds as well as uniformity results. In this talk we will outline the general background of this logic-based approach and its origin in research on the foundations of mathematics and indicate some recent applications in the context of nonlinear analysis.