Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
Hostname: page-component-66644f4456-q629f Total loading time: 0 Render date: 2025-02-13T03:41:33.573Z Has data issue: true hasContentIssue false

Proof interpretations and majorizability

Published online by Cambridge University Press:  01 March 2011

By
Fernando Ferreira
Edited by
Françoise Delon ,
Ulrich Kohlenbach ,
Penelope Maddy  and
Frank Stephan
Françoise Delon
Affiliation:
UFR de Mathématiques
Ulrich Kohlenbach
Affiliation:
Technische Universität, Darmstadt, Germany
Penelope Maddy
Affiliation:
University of California, Irvine
Frank Stephan
Affiliation:
National University of Singapore
Get access

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 - 81
Publisher: Cambridge University Press
Print publication year: 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

[1] Y., Akama, S., Berardi, S., Hayashi, and U., Kohlenbach, 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] J., Avigad and S., Feferman, Gödel's functional (“Dialectica”) interpretation, Handbook of Proof Theory (S. R., Buss, editor), Studies in Logic and the Foundations of Mathematics, vol. 137, North Holland, Amsterdam, 1998, pp. 337–405.Google Scholar
[3] J., Avigad and H., Towsner, Functional interpretation and inductive definition, The Journal of Symbolic Logic, vol. 74 (2009), pp. 1100–1120.Google Scholar
[4] M., Bezem, 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] W., Burr, A Diller-Nahm-style functional interpretation of KPω, Archive for Mathematical Logic, vol. 39 (2000), pp. 599–604.Google Scholar
[6] J., Diller and W., Nahm, 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] P., Engrácia and F., Ferreira, The bounded functional interpretation of the double negation shift, to appear in The Journal of Symbolic Logic.
[8] F., Ferreira, 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: Thomas, Strahm.Google Scholar
[9] F., Ferreira, On a new functional interpretation (abstract), The Bulletin of Symbolic Logic, vol. 14 (2008), pp. 128–129.Google Scholar
[10] F., Ferreira, 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: Sergei, Artemov, Matthias, Baaz and Harvey, Friedman.Google Scholar
[11] F., Ferreira and A., Nunes, Bounded modified realizability, The Journal of Symbolic Logic, vol. 71 (2006), pp. 329–346.Google Scholar
[12] F., Ferreira and P., Oliva, Bounded functional interpretation, Annals of Pure and Applied Logic, vol. 135 (2005), pp. 73–112.Google Scholar
[13] F., Ferreira, Bounded functional interpretation and feasible analysis, Annals of Pure and Applied Logic, vol. 145 (2005), pp. 115–129.Google Scholar
[14] J., Gaspar, Factorization of the Shoenfield-like bounded functional interpretation, Notre Dame Journal of Formal Logic, vol. 50 (2009), pp. 53–60.Google Scholar
[15] P., Gerhardy and U., Kohlenbach, General logical metatheorems for functional analysis, Transactions of the American Mathematical Society, vol. 360 (2008), pp. 2615–2660.Google Scholar
[16] K., Gödel, Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines Mathematischen Kolloquiums, vol. 4 (1933), pp. 34–38.Google Scholar
[17] K., Gödel, Ü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] K., Gödel, On an extension of finitary mathematics which has not yet been used, 1972, Published in [19], pages 271–280. Revised version of [17].
[19] K., Gödel, Collected Works, vol. II, (S., Feferman, editor), Oxford University Press, Oxford, 1990.Google Scholar
[20] W. A., Howard, Hereditarily majorizable functionals of finite type, Metamathematical investigation of intuitionistic Arithmetic and Analysis (A. S., Troelstra, editor), Lecture Notes in Mathematics, vol. 344, Springer, Berlin, 1973, pp. 454–461.Google Scholar
[21] S. C., Kleene, On the interpretation of intuitionistic number theory, The Journal of Symbolic Logic, vol. 10 (1945), pp. 109–124.Google Scholar
[22] S. C., Kleene, Countable functionals, Constructivity in Mathematics (A., Heyting, editor), North Holland, Amsterdam, 1959, pp. 81–100.Google Scholar
[23] U., Kohlenbach, 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] U., Kohlenbach, 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] U., Kohlenbach, Pointwise hereditary majorization and some applications, Archive for Mathematical Logic, vol. 31 (1992), pp. 227–241.Google Scholar
[26] U., Kohlenbach, 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] U., Kohlenbach, Analysing proofs in analysis, Logic: from Foundations to Applications (W., Hodges, M., Hyland, C., Steinhorn, and J., Truss, editors), Oxford University Press, 1996, pp. 225–260.Google Scholar
[28] U., Kohlenbach, 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] U., Kohlenbach, Relative constructivity, The Journal of Symbolic Logic, vol. 63 (1998), pp. 1218–1238.Google Scholar
[30] U., Kohlenbach, On the no-counterexample interpretation, The Journal of Symbolic Logic, vol. 64 (1999), pp. 1491–1511.Google Scholar
[31] U., Kohlenbach, Intuitionistic choice and restricted classical logic, Mathematical Logic Quarterly, vol. 47 (2001), pp. 455–460.Google Scholar
[32] U., Kohlenbach, Foundational and mathematical uses of higher types, Reflections on the Foundations of Mathematics: Essay in Honor of Solomon Feferman (W., Sieg et al., editors), Lecture Notes in Logic, vol. 15, A. K. Peters, 2002, pp. 92–116.Google Scholar
[33] U., Kohlenbach, Some logical metatheorems with applications in functional analysis, Transactions of the American Mathematical Society, vol. 357 (2005), pp. 89–128.Google Scholar
[34] U., Kohlenbach, Proof interpretations and the computational content of proofs in mathematics, Bulletin of the EATCS, vol. 93 (2007), pp. 143–173.Google Scholar
[35] U., Kohlenbach, Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics, Springer, Berlin, 2008.Google Scholar
[36] U., Kohlenbach, Effective bounds from proofs in abstract functional analysis, New Computational Paradigms: Changing Conceptions of What is Computable (S. B., Cooper, B., Löwe, and A., Sorbi, editors), Springer Verlag, to appear.
[37] U., Kohlenbach and P., Oliva, 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] U., Kohlenbach and T., Streicher, Shoenfield is Gödel after Krivine, Mathematical Logic Quarterly, vol. 53 (2007), pp. 176–179.Google Scholar
[39] G., Kreisel, On the interpretation of non-finitist proofs, part I, The Journal of Symbolic Logic, vol. 16 (1951), pp. 241–267.Google Scholar
[40] G., Kreisel, Interpretation of analysis by means of constructive functionals of finite types, Constructivity in Mathematics (A., Heyting, editor), North Holland, Amsterdam, 1959, pp. 101–128.Google Scholar
[41] G., Kreisel, On weak completeness of intuitionistic predicate logic, The Journal of Symbolic Logic, vol. 27 (1962), pp. 139–158.Google Scholar
[42] H., Luckhardt, Extensional Gödel Functional Interpretation: A Consistency Proof of Classical Analysis, Lecture Notes in Mathematics, vol. 306, Springer, Berlin, 1973.Google Scholar
[43] P., Oliva, Unifying functional interpretations, Notre Dame Journal of Formal Logic, vol. 47 (2006), pp. 263–290.Google Scholar
[44] C., Parsons, On a number theoretic choice schema and its relation to induction, Intuitionism and Proof Theory (J., Myhill, A., Kino, and R. E., Vesley, editors), North-Holland, 1970, pp. 459–473.Google Scholar
[45] J. R., Shoenfield, Mathematical Logic, Addison-Wesley Publishing Company, 1967, Republished in 2001 by AK Peters.Google Scholar
[46] S. G., Simpson, Subsystems of Second Order Arithmetic, Perspectives in Mathematical Logic, Springer, Berlin, 1999.Google Scholar
[47] C., Spector, 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 (F. D. E., Dekker, editor), vol. 5, AMS, Providence, Rhode Island, 1962, pp. 1–27.Google Scholar
[48] T., Strahm (editor), Gödel's dialectica Interpretation, dialectica, vol. 62 (2008), pp. 145–290.Google Scholar
[49] W., Tait, Intentional interpretations of functionals of finite type I, The Journal of Symbolic Logic, vol. 32 (1967), pp. 198–212.Google Scholar
[50] T., Tao, 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] T., Tao, 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] A. S., Troelstra (editor), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol. 344, Springer, Berlin, 1973.Google Scholar
[53] A. S., Troelstra, Introductory note to [17] and [18], 1990, Published in [19], pages 214–241.
[54] A. S., Troelstra, Realizability, Handbook of Proof Theory (S. R., Buss, editor), Studies in Logic and the Foundations of Mathematics, vol. 137, North Holland, Amsterdam, 1998, pp. 408–473.Google Scholar
[55] A. S., Troelstra and D., van Dalen, Constructivism in Mathematics. An Introduction, Studies in Logic and the Foundations of Mathematics, vol. 121, North Holland, Amsterdam, 1988.Google Scholar
[56] M., Yasugi, Intuitionistic analysis and Gödel's interpretation, Journal of the Mathematical Society of Japan, vol. 15 (1963), pp. 101–112.Google Scholar

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×