Abstract
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.
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.
Similar content being viewed by others
References
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)
Aczel, P., Rathjen, M.: Notes on constructive set theory, Technical Report 40, Institut Mittag-Leffler The Royal Swedish Academy of Sciences (2001), http://www.ml.kva.se/preprints/archive2000-2001.php
Barendregt, H.P.: The Lambda Calculus: It’s Syntax and Semantics. North Holland, Amsterdam (1981)
Barwise, J.: Admissible Sets and Structures. Springer, Heidelberg (1975)
Beeson, M.: Foundations of Constructive Mathematics. Springer, Heidelberg (1985)
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis, Naples (1984)
McCarty, D.C.: Realizability and recursive mathematics, PhD thesis, Oxford University, p. 281 (1984)
Myhill, J.: Constructive set theory. Journal of Symbolic Logic 40, 347–382 (1975)
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)
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)
Rathjen, M.: The disjunction and other properties for constructive Zermelo-Fraenkel set theory. Journal of Symbolic Logic, 1233–1254 (2005)
Rathjen, M.: Constructive set theory and Brouwerian principles. Journal of Universal Computer Science, 2008–2033 (2005)
Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, vol. I, II North Holland, Amsterdam (1988)
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
Rathjen, M. (2006). Models of Intuitionistic Set Theories over Partial Combinatory Algebras. In: Cai, JY., Cooper, S.B., Li, A. (eds) Theory and Applications of Models of Computation. TAMC 2006. Lecture Notes in Computer Science, vol 3959. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11750321_5
Download citation
DOI: https://doi.org/10.1007/11750321_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34021-8
Online ISBN: 978-3-540-34022-5
eBook Packages: Computer ScienceComputer Science (R0)