Recursive inequalities in applied proof theory
Appears in collection : Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométrique
Applied proof theory is an area of research that uses ideas and techniques from proof theory to produce new results in 'mainstream' mathematics and computer science. While the field has historical roots in Hilbert's program, where it aligns with the much broader effort to give a computational meaning to mathematical proofs, its emergence as a powerful area of applied logic only started in the early 2000s with the research of Kohlenbach and his collaborators. This talk aims to accomplish two things. Firstly, I seek to give a brief overview of the main ideas behind applied proof theory without assuming any prior background in the area. Secondly, within this context, I want to present some recent results which have focused on abstract convergence properties of sequences of real numbers that satisfy certain recursive inequalities. I argue that recursive inequalities present us with a unifying framework for viewing many convergence proofs in the literature, and propose what I believe to be some fascinating possibilities for future work, involving stochastic convergence, computer formalized mathematics and automated reasoning.
