Models of Intuitionistic Set Theories over Partial Combinatory Algebras

  • Michael Rathjen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3959)


This paper presents two types of realizability models for intuitionistic set theories. The point of departure for every notion of realizability will be a domain of computation, called a partial combinatory algebra, PCA. To put it roughly, the role of a PCA in the first type of realizability is to furnish a concrete instantiation of the Brouwer-Heyting-Kolmogorov interpretation of the logical connectives. In a sense, partial combinatory algebras can lay claim to be of equal importance to models of intuitionistic set theory as partial orderings are to forcing models of classical set theory.

Among other things, these models can be used to extract computational information from proofs. Their main employment here, however, will be to provide consistency, equiconsistency, and independence results. Relinquishing classical logic can bring forth considerable profits. It allows for axiomatic freedom in that one can adopt new axioms that are true in realizability models but utterly false classically.


Classical Logic Type Theory Intuitionistic Logic Logical Connective Choice Principle 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aczel, P.: The type theoretic interpretation of constructive set theory: Choice principles. In: Troelstra, A.S., van Dalen, D. (eds.) The L.E.J. Brouwer Centenary Symposium, pp. 1–40 North Holland, Amsterdam (1982)Google Scholar
  2. 2.
    Aczel, P., Rathjen, M.: Notes on constructive set theory, Technical Report 40, Institut Mittag-Leffler The Royal Swedish Academy of Sciences (2001),
  3. 3.
    Barendregt, H.P.: The Lambda Calculus: It’s Syntax and Semantics. North Holland, Amsterdam (1981)Google Scholar
  4. 4.
    Barwise, J.: Admissible Sets and Structures. Springer, Heidelberg (1975)zbMATHGoogle Scholar
  5. 5.
    Beeson, M.: Foundations of Constructive Mathematics. Springer, Heidelberg (1985)zbMATHGoogle Scholar
  6. 6.
    Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis, Naples (1984)Google Scholar
  7. 7.
    McCarty, D.C.: Realizability and recursive mathematics, PhD thesis, Oxford University, p. 281 (1984)Google Scholar
  8. 8.
    Myhill, J.: Constructive set theory. Journal of Symbolic Logic 40, 347–382 (1975)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Rathjen, M.: Realizability for constructive Zermelo-Fraenkel set theory. In: Väänänen, J., Stoltenberg-Hansen, V. (eds.) Proceedings of the Logic Colloquium (2003) (to appear)Google Scholar
  10. 10.
    Rathjen, M.: Choice principles in constructive and classical set theories. In: Chatzidakis, Z., Koepke, P., Pohlers, W. (eds.) Logic Colloquium 2002. Lecture Notes in Logic, vol. 27, Association for Symbolic Logic (2002) (to appear)Google Scholar
  11. 11.
    Rathjen, M.: The disjunction and other properties for constructive Zermelo-Fraenkel set theory. Journal of Symbolic Logic, 1233–1254 (2005)Google Scholar
  12. 12.
    Rathjen, M.: Constructive set theory and Brouwerian principles. Journal of Universal Computer Science, 2008–2033 (2005)Google Scholar
  13. 13.
    Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, vol. I, II North Holland, Amsterdam (1988)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Michael Rathjen
    • 1
    • 2
  1. 1.Department of MathematicsOhio State UniversityColumbusUSA
  2. 2.Department of Pure MathematicsUniversity of LeedsLeedsUK

Personalised recommendations