Book contents
- Frontmatter
- Contents
- Introduction
- Speakers and Titles
- Decorated linear order types and the theory of concatenation
- Cardinal preserving elementary embeddings
- Proof interpretations and majorizability
- Proof mining in practice
- Cardinal structure under AD
- Three lectures on automatic structures
- Pillay's conjecture and its solution—a survey
- Proof theory and meaning: On the context of deducibility
- Bounded super real closed rings
- Analytic combinatorics of the transfinite: A unifying Tauberian perspective
- References
Proof interpretations and majorizability
Published online by Cambridge University Press: 01 March 2011
- Frontmatter
- Contents
- Introduction
- Speakers and Titles
- Decorated linear order types and the theory of concatenation
- Cardinal preserving elementary embeddings
- Proof interpretations and majorizability
- Proof mining in practice
- Cardinal structure under AD
- Three lectures on automatic structures
- Pillay's conjecture and its solution—a survey
- Proof theory and meaning: On the context of deducibility
- Bounded super real closed rings
- Analytic combinatorics of the transfinite: A unifying Tauberian perspective
- References
Summary
Abstract. In the last fifteen years, the traditional proof interpretations of modified realizability and functional (dialectica) interpretation in finite-type arithmetic have been adapted by taking into account majorizability considerations. One of such adaptations, the monotone functional interpretation of Ulrich Kohlenbach, has been at the center of a vigorous program in applied proof theory dubbed proof mining. We discuss some of the traditional and majorizability interpretations, including the recent bounded interpretations, and focus on the main theoretical techniques behind proof mining.
Introduction. Functional interpretations were introduced half a century ago by Kurt Gödel in. Göodel's interpretation uses functionals of finite type and is an exact interpretation. It is exact in the sense that it provides precise witnesses of existential statements. Another example of an exact (functional) interpretation is Georg Kreisel's modified realizability. In the last fifteen years or so, there has been an interest in interpretations which are not exact, but only demand bounds for existential witnesses. These interpretations, when dealing with bounds for functionals of every type, are based on the majorizability notions of William Howard and Marc Bezem. This is the case with Ulrich Kohlenbach's monotone modified realizability and monotone functional interpretation, the bounded modified realizability of Fernando Ferreira and Ana Nunes, or the bounded functional interpretation of Ferreira and Paulo Oliva. There are, to be sure, other interpretations which also incorporate majorizability notions to a certain extent: for instance, the seminal Diller-Nahm interpretation, Wolfgang Burr's interpretation of KPω or the very recent interpretation of Jeremy Avigad and Henry Towsner which is able to provide a proof theoretic analysis of ID1.
- Type
- Chapter
- Information
- Logic Colloquium 2007 , pp. 32 - 81Publisher: Cambridge University PressPrint publication year: 2010