Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

A realizability interpretation for classical analysis


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 ∀xyA(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.


  1. 1.

    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

  2. 2.

    Schwichtenberg, H.: The Handbook of Mathematical Logic. Proof theory: Some aspects of cut-elimination, North-Holland, 1977 pp. 867–895

  3. 3.

    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

  4. 4.

    Kreisel, G.: Interpretation of Analysis by means of Functionals of Finite Type. Constructivity in Mathematics. A. Heyting, North-Holland, 1959, pp. 101–128

  5. 5.

    Kreisel, G.: On Weak Completeness of Intuitionistic Predicate Logic. J. Symb. Logic. 27, 139–158 (1962)

  6. 6.

    Dragalin, A.G.: New forms of realizability and Markov’s rule (Russian). Doklady, 251, 534–537, (1980)

  7. 7.

    Friedman, H.: Higher Set Theory, Classically and Intuitionistically Provably Recursive Functions, Springer, 1978, 669, Springer Lecture Notes, 21–27

Download references

Author information

Correspondence to Henry Towsner.

Additional information

Mathematics Subject Classification (2000): 03F35,03F05

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Towsner, H. A realizability interpretation for classical analysis. Arch. Math. Logic 43, 891–900 (2004).

Download citation


  • Classical Analysis
  • Realizability Interpretation
  • Classical Proof
  • Existential Formula
  • Recursive Type