Abstract
This note reexamines Spector’s remarkable computational interpretation of full classical analysis. Spector’s interpretation makes use of a rather abstruse recursion schema, so-called bar recursion, used to interpret the double negation shift DNS. In this note bar recursion is presented as a generalisation of a simpler primitive recursive functional needed for the interpretation of a finite (intuitionistic) version of DNS. I will also present two concrete applications of bar recursion in the extraction of programs from proofs of ∀ ∃-theorems in classical analysis.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Avigad, J.: Update procedures and the 1-consistency of arithmetic. Mathematical Logic Quarterly 48, 3–13 (2002)
Berger, U., Oliva, P.: Modified bar recursion and classical dependent choice. Lecture Notes in Logic 20, 89–107 (2005)
Gödel, K.: Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12, 280–287 (1958)
Kuroda, S.: Intuitionistische Untersuchungen der formalistischen Logik. Nagoya Mathematical Journal 3, 35–47 (1951)
Oliva, P.: Unifying functional interpretations. Notre Dame Journal of Formal Logic (to appear, 2006)
Spector, C.: Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In: Dekker, F.D.E. (ed.) Recursive Function Theory: Proc. Symposia in Pure Mathematics, vol. 5, pp. 1–27. American Mathematical Society, Providence, Rhode Island (1962)
Troelstra, A.S. (ed.): Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344. Springer, Berlin (1973)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Oliva, P. (2006). Understanding and Using Spector’s Bar Recursive Interpretation of Classical Analysis. In: Beckmann, A., Berger, U., Löwe, B., Tucker, J.V. (eds) Logical Approaches to Computational Barriers. CiE 2006. Lecture Notes in Computer Science, vol 3988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11780342_44
Download citation
DOI: https://doi.org/10.1007/11780342_44
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35466-6
Online ISBN: 978-3-540-35468-0
eBook Packages: Computer ScienceComputer Science (R0)