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
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
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
References
[1] , , , and , An arithmetical hierarchy of the law of excluded middle and related principles, Proceedings of the 19th Annual IEEE Symposium on Logic and Computer Science, vol. 117, IEEE Press, 2004, pp. 192–201.Google Scholar
[2] and , Gödel's functional (“Dialectica”) interpretation, Handbook of Proof Theory (, editor), Studies in Logic and the Foundations of Mathematics, vol. 137, North Holland, Amsterdam, 1998, pp. 337–405.Google Scholar
[3] and , Functional interpretation and inductive definition, The Journal of Symbolic Logic, vol. 74 (2009), pp. 1100–1120.Google Scholar
[4] , Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals, The Journal of Symbolic Logic, vol. 50 (1985), pp. 652–660.Google Scholar
[5] , A Diller-Nahm-style functional interpretation of KPω, Archive for Mathematical Logic, vol. 39 (2000), pp. 599–604.Google Scholar
[6] and , Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen, Archive für mathematische Logik und Grundlagenforschung, vol. 16 (1974), pp. 49–66.Google Scholar
[7] and , The bounded functional interpretation of the double negation shift, to appear in The Journal of Symbolic Logic.
[8] , A most artistic package of a jumble of ideas, dialectica, vol. 62 (2008), pp. 205–222, Special Issue: Gödel's dialectica Interpretation. Guest editor: .Google Scholar
[9] , On a new functional interpretation (abstract), The Bulletin of Symbolic Logic, vol. 14 (2008), pp. 128–129.Google Scholar
[10] , Injecting uniformities into Peano arithmetic, Annals of Pure and Applied Logic, vol. 157 (2009), pp. 122–129, Special Issue: Kurt Gödel Centenary Research Prize Fellowships. Editors: , and .Google Scholar
[11] and , Bounded modified realizability, The Journal of Symbolic Logic, vol. 71 (2006), pp. 329–346.Google Scholar
[12] and , Bounded functional interpretation, Annals of Pure and Applied Logic, vol. 135 (2005), pp. 73–112.Google Scholar
[13] , Bounded functional interpretation and feasible analysis, Annals of Pure and Applied Logic, vol. 145 (2005), pp. 115–129.Google Scholar
[14] , Factorization of the Shoenfield-like bounded functional interpretation, Notre Dame Journal of Formal Logic, vol. 50 (2009), pp. 53–60.Google Scholar
[15] and , General logical metatheorems for functional analysis, Transactions of the American Mathematical Society, vol. 360 (2008), pp. 2615–2660.Google Scholar
[16] , Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines Mathematischen Kolloquiums, vol. 4 (1933), pp. 34–38.Google Scholar
[17] , Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, dialectica, vol. 12 (1958), pp. 280–287, Reprinted with an English translation in [19].Google Scholar
[18] , On an extension of finitary mathematics which has not yet been used, 1972, Published in [19], pages 271–280. Revised version of [17].
[20] , Hereditarily majorizable functionals of finite type, Metamathematical investigation of intuitionistic Arithmetic and Analysis (, editor), Lecture Notes in Mathematics, vol. 344, Springer, Berlin, 1973, pp. 454–461.Google Scholar
[21] , On the interpretation of intuitionistic number theory, The Journal of Symbolic Logic, vol. 10 (1945), pp. 109–124.Google Scholar
[22] , Countable functionals, Constructivity in Mathematics (, editor), North Holland, Amsterdam, 1959, pp. 81–100.Google Scholar
[23] , Theorie der majorisierbaren und stetigen Funktionale und ihre Anwendung bei der Extraktion von Schranken aus inkonstruktiven Beweisen: Effektive Eindeutigkeitsmodule bei besten Approximationen aus ineffektiven Beweisen, Ph.D. thesis, Frankfurt, pp. xxii+278, 1990.
[24] , Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization, The Journal of Symbolic Logic, vol. 57 (1992), pp. 1239–1273.Google Scholar
[25] , Pointwise hereditary majorization and some applications, Archive for Mathematical Logic, vol. 31 (1992), pp. 227–241.Google Scholar
[26] , Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation, Annals of Pure and Applied Logic, vol. 64 (1993), pp. 27–94.Google Scholar
[27] , Analysing proofs in analysis, Logic: from Foundations to Applications (, , , and , editors), Oxford University Press, 1996, pp. 225–260.Google Scholar
[28] , Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals, Archive for Mathematical Logic, vol. 36 (1996), pp. 31–71.Google Scholar
[29] , Relative constructivity, The Journal of Symbolic Logic, vol. 63 (1998), pp. 1218–1238.Google Scholar
[30] , On the no-counterexample interpretation, The Journal of Symbolic Logic, vol. 64 (1999), pp. 1491–1511.Google Scholar
[31] , Intuitionistic choice and restricted classical logic, Mathematical Logic Quarterly, vol. 47 (2001), pp. 455–460.Google Scholar
[32] , Foundational and mathematical uses of higher types, Reflections on the Foundations of Mathematics: Essay in Honor of Solomon Feferman ( et al., editors), Lecture Notes in Logic, vol. 15, A. K. Peters, 2002, pp. 92–116.Google Scholar
[33] , Some logical metatheorems with applications in functional analysis, Transactions of the American Mathematical Society, vol. 357 (2005), pp. 89–128.Google Scholar
[34] , Proof interpretations and the computational content of proofs in mathematics, Bulletin of the EATCS, vol. 93 (2007), pp. 143–173.Google Scholar
[35] , Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics, Springer, Berlin, 2008.Google Scholar
[36] , Effective bounds from proofs in abstract functional analysis, New Computational Paradigms: Changing Conceptions of What is Computable (, , and , editors), Springer Verlag, to appear.
[37] and , Proof mining: a systematic way of analysing proofs in mathematics, Proceedings of the Steklov Institute of Mathematics, vol. 242 (2003), pp. 136–164.Google Scholar
[38] and , Shoenfield is Gödel after Krivine, Mathematical Logic Quarterly, vol. 53 (2007), pp. 176–179.Google Scholar
[39] , On the interpretation of non-finitist proofs, part I, The Journal of Symbolic Logic, vol. 16 (1951), pp. 241–267.Google Scholar
[40] , Interpretation of analysis by means of constructive functionals of finite types, Constructivity in Mathematics (, editor), North Holland, Amsterdam, 1959, pp. 101–128.Google Scholar
[41] , On weak completeness of intuitionistic predicate logic, The Journal of Symbolic Logic, vol. 27 (1962), pp. 139–158.Google Scholar
[42] , Extensional Gödel Functional Interpretation: A Consistency Proof of Classical Analysis, Lecture Notes in Mathematics, vol. 306, Springer, Berlin, 1973.Google Scholar
[43] , Unifying functional interpretations, Notre Dame Journal of Formal Logic, vol. 47 (2006), pp. 263–290.Google Scholar
[44] , On a number theoretic choice schema and its relation to induction, Intuitionism and Proof Theory (, , and , editors), North-Holland, 1970, pp. 459–473.Google Scholar
[45] , Mathematical Logic, Addison-Wesley Publishing Company, 1967, Republished in 2001 by AK Peters.Google Scholar
[46] , Subsystems of Second Order Arithmetic, Perspectives in Mathematical Logic, Springer, Berlin, 1999.Google Scholar
[47] , Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics, Recursive Function Theory: Proceedings of Symposia in Pure Mathematics (, editor), vol. 5, AMS, Providence, Rhode Island, 1962, pp. 1–27.Google Scholar
[48] (editor), Gödel's dialectica Interpretation, dialectica, vol. 62 (2008), pp. 145–290.Google Scholar
[49] , Intentional interpretations of functionals of finite type I, The Journal of Symbolic Logic, vol. 32 (1967), pp. 198–212.Google Scholar
[50] , The correspondence principle and finitary ergodic theory, Essay posted August 30, 2008. Available at: http://terrytao.wordpress.com/2008/08/30/the-correspondence-principle-and-finitary-ergodic-theory/.
[51] , Soft analysis, hard analysis, and the finite convergence principle, Structure and Randomness: Pages from Year One of a Mathematical Blog, AMS, 2008, pp. 17–29.Google Scholar
[52] (editor), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol. 344, Springer, Berlin, 1973.Google Scholar
[53] , Introductory note to [17] and [18], 1990, Published in [19], pages 214–241.
[54] , Realizability, Handbook of Proof Theory (, editor), Studies in Logic and the Foundations of Mathematics, vol. 137, North Holland, Amsterdam, 1998, pp. 408–473.Google Scholar
[55] and , Constructivism in Mathematics. An Introduction, Studies in Logic and the Foundations of Mathematics, vol. 121, North Holland, Amsterdam, 1988.Google Scholar
[56] , Intuitionistic analysis and Gödel's interpretation, Journal of the Mathematical Society of Japan, vol. 15 (1963), pp. 101–112.Google Scholar