Abstract
We propose a realizability interpretation of a system for quantifier free arithmetic which is equivalent to the fragment of classical arithmetic without nested quantifiers, which we call EM 1-arithmetic. We interpret classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the “environment” and with each other. With respect to known constructive interpretations of classical arithmetic, the present one differs under many respects: for instance, the interpretation is compositional in a strict sense; in particular the interpretation of (the analogous of) the cut rule is the plain composition of functionals. As an additional remark, any two quantifier-free formulas provably equivalent in classical arithmetic have the same realizer.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Akama, Y., Berardi, S., Hayashi, S., Kohlenbach, U.: An arithmetical hierarchy of the law of excluded middle and related principles. In: Proc. of LICS 2004, pp. 192–201 (2004)
Berardi, S., de’ Liguoro, U.: A Calculus of Realizers for EM1 Arithmetic (Full Version). Technical report, Università di Torino (2008), http://www.di.unito.it/~stefano/RealWFA.pdf
Coquand, T.: A semantics of evidence for classical arithmetic. J. Symb. Log. 60, 325–337 (1995)
Criscuolo, G., Minicozzi, E., Trautteur, G.: Limiting recursion and the arithmetic hierarchy. ITA 9(1), 5–12 (1975)
Friedman, H.: Classically and intuitionistically provably recursive functions. In: Scott, D.S., Muller, G.H. (eds.) Higher Set Theory. LNM, vol. 699, pp. 21–28. Springer, Heidelberg (1978)
Gold, E.M.: Limiting recursion. J. Symb. Log. 30, 28–48 (1965)
Griffin, T.G.: The formulae-as-types notion of control. In: Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL 1990, San Francisco, CA, USA, January 17–19, pp. 47–57. ACM Press, New York (1990)
Hayashi, S.: Mathematics based on incremental learning, excluded middle and inductive inference. Theor. Comp. Sci. 350, 125–139 (2006)
Hilbert, D., Bernays, P.: Grundlagen der Mathematik, vol. II. Springer, Heidelberg (1970)
Krivine, J.-L.: Dependent choice, ‘quote’ and the clock. Theor. Comput. Sci. 308, 259–276 (2003)
Mints, G.: Strong termination for the epsilong substitution method. J. Symb. Log. 61(4), 1193–1205 (1996)
Moser, G., Zach, R.: The epsilon calculus and herbrand complexity. Studia Logica 82(1), 133–155 (2006)
Murthy, C.R.: An evaluation semantics for classical proofs. In: Proc. of LICS 1991, pp. 96–107 (1991)
Parigot, M.: Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In: LPAR, pp. 190–201 (1992)
Schubert, L.K.: Iterated limiting recursion and the program minimalization problem. J. of Ass. Comp. Mach. 21(3), 436–445 (1974)
van Dalen, D., Troelstra, A.: Constructivism in Mathematics, vol. I. North-Holland, Amsterdam (1988)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berardi, S., de’Liguoro, U. (2008). A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract). In: Kaminski, M., Martini, S. (eds) Computer Science Logic. CSL 2008. Lecture Notes in Computer Science, vol 5213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87531-4_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-87531-4_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87530-7
Online ISBN: 978-3-540-87531-4
eBook Packages: Computer ScienceComputer Science (R0)