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.

About the speaker:

Ulrich Kohlenbach is a German mathematician and professor of mathematical logic at the Technische Universität Darmstadt. His research interests lie in proof theory. He is a leading expert in the field of proof mining. Kohlenbach was President of the German Association for Mathematical Logic and the Foundations of Exact Sciences (DVMLG) from 2008 to 2012, and President of the Association for Symbolic Logic from 2016 to 2018. He was the Dean of Department of Mathematics at the Technische Universität Darmstadt.

In 2011 he received the prestigious Kurt Gödel Research Prize Fellowship of the Kurt Gödel Society. He was an invited speaker at the 2018 International Congress of Mathematicians (Section: Logic and Foundations). He has published more than 90 research papers in mathematics and logic, and a book titled "Applied Proof Theory: Proof Interpretations and their Use in Mathematics" in the series of "Springer Monographs in Mathematics" in 2008. He is an advisory editor of Journal of Mathematical Logic, and a coordinating editor of Annals of Pure and Applied Logic.