Applied Proof Theory: Proof Interpretations and their Use in Mathematics
This book gives an introduction to so-called proof interpretations, more speci?cally various forms of realizability and functional interpretations, and their use in mat- matics. Whereas earlier treatments of these techniques(e. g. [366, 266, 122, 369, 7]) emphasize foundational and logical issues the focus of this book is on applications of the methods to extract new effective information such as computable uniform boundsfrom given(typically ineffective)proofs. This line of research, which has its roots in G. Kreisel’s pioneering work on ‘unwinding of proofs’ from the 50’s, has in more recent years developed into a ?eld of mathematical logic which has been called (suggested by D. Scott) ‘proof mining’. The areas where proof mining based onproofinterpretationshasbeenappliedmostsystematically arenumericalanalysis and functional analysis and so the book concentrates on those. There are also some extractions of effective information from proofs (guided by logic) in number theory (G. Kreisel,H. Luckhardt,seee. g. [249, 268, 267, 122]) and algebra (G. Kreisel, C. Delzell, H. Lombardi, T. Coquand and others, see e. g. [252, 84, 77, 74, 76]). H- ever, here mainly methodsfromstructural prooftheory such as Herbrand’stheorem, ?-substitution and cut-elimination are used and we will refer to the literature for more information on these results. In this book two kinds of systems play an important role: those with full induction and variants with induction for purely existential formulas (whose central role has been singled out in the context of so-called reverse mathematics, ). Further (still weaker) fragments are brie?y discussed in comments and referred to in the literature.
First book on the subject at all