We present a realizability interpretation for classical analysis–an association of a term to every proof so that the terms assigned to existential formulas represent witnesses to the truth of that formula. For classical proofs of Π2 sentences ∀x∃yA(x,y), this provides a recursive type 1 function which computes the function given by f(x)=y iff y is the least number such that A(x,y).
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Avigad, J.: A realizability interpretation for classical arithmetic. In Buss and Hájek and Pudlák, Logic Colloquium ‘98. Lecture Notes in Logic 13, 57–90, (2000) AK Peters
Schwichtenberg, H.: The Handbook of Mathematical Logic. Proof theory: Some aspects of cut-elimination, North-Holland, 1977 pp. 867–895
Troelstra, A.S.: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer. With contributions by A.S. Troelstra, C.A. Smoryński, J.I. Zucker and W.A. Howard, 1973
Kreisel, G.: Interpretation of Analysis by means of Functionals of Finite Type. Constructivity in Mathematics. A. Heyting, North-Holland, 1959, pp. 101–128
Kreisel, G.: On Weak Completeness of Intuitionistic Predicate Logic. J. Symb. Logic. 27, 139–158 (1962)
Dragalin, A.G.: New forms of realizability and Markov’s rule (Russian). Doklady, 251, 534–537, (1980)
Friedman, H.: Higher Set Theory, Classically and Intuitionistically Provably Recursive Functions, Springer, 1978, 669, Springer Lecture Notes, 21–27
Mathematics Subject Classification (2000): 03F35,03F05
About this article
Cite this article
Towsner, H. A realizability interpretation for classical analysis. Arch. Math. Logic 43, 891–900 (2004). https://doi.org/10.1007/s00153-004-0233-3
- Classical Analysis
- Realizability Interpretation
- Classical Proof
- Existential Formula
- Recursive Type