Abstract
Just as forcing, or Boolean-valued models, produce a model of ZF (when the meta-theory is, or the ground model satisfies, ZF), so do Heyting-valued models satisfy IZF, which stands for Intuitionistic ZF, the standard constructive re-working of the ZF axioms. In this paper, a variant model is introduced (with truth values the Heyting algebra of open sets of a topological space), along with a correspondingly revised forcing or satisfaction relation. Such a model is shown to satisfy only a fragment of IZF. Natural properties of the underlying topological space are shown to imply stronger closure properties of the model. (It is impossible, except in trivial cases, for Power Set to be satisfied.) This semantics generalizes the second model of [9], which is the current semantics for the special case of the underlying topological space being \({\mathbb R}\).
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
Aczel, P.: The type theoretic interpretation of constructive set theory. In: MacIntyre, A., Pacholski, L., Paris, J. (eds.) Logic Colloquium 1977, pp. 55–66. North-Holland, Amsterdam (1978)
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.: The type theoretic interpretation of constructive set theory: inductive definitions. In: Marcus, R.B., et al. (eds.) Logic, Methodology and Philosophy of Science VII, pp. 17–49. North-Holland, Amsterdam (1986)
Aczel, P., Rathjen, M.: Notes on constructive set theory, Technical Report 40, 2000/2001. Mittag-Leffler Institute, Sweden (2001)
Fourman, M.P., Scott, D.S.: Sheaves and Logic. In: Fourman, M.P., Mulvey, C.J., Scott, D.S. (eds.) Applications of Sheaves. Lecture Notes in Mathematics, vol. 753, pp. 302–401. Springer, Heidelberg (1979)
Grayson, R.J.: Heyting-valued models for intuitionistic set theory. In: Fourman, M.P., Mulvey, C.J., Scott, D.S. (eds.) Applications of Sheaves. Lecture Notes in Mathematics, vol. 753, pp. 402–414. Springer, Heidelberg (1979)
Grayson, R.J.: Heyting-valued semantics. In: Lolli, G., Longo, G., Marcja, A. (eds.) Logic Colloquium 1982. Studies in Logic and the Foundations of Mathematics, vol. 112, pp. 181–208. North-Holland, Amsterdam (1984)
Lubarsky, R.: CZF and Second Order Arithmetic. Annals of Pure and Applied Logic 141, 29–34 (2006)
Lubarsky, R., Rathjen, M.: On the constructive Dedekind reals. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 349–362. Springer, Heidelberg (2007); Also Logic and Analysis, vol. 1, pp. 131–152 (2008)
MacLane, S., Moerdijk, I.: Sheaves in Geometry and Logic. Springer, New York (1992)
McCarty, D.: Realizability and recursive mathematics. Ph.D. thesis, Oxford University (1984), also Carnegie-Mellon University Technical Report CMU-CS-84-131
Mostowski, A.W.: Proofs of non-deducibility in intuitionistic functional calculus. JSL 13, 204–207 (1948)
Scott, D.S.: Extending the topological interpretation to intuitionistic analysis I. Compos. Math. 20, 194–210 (1968)
Scott, D.S.: Extending the topological interpretation to intuitionistic analysis II. In: Myhill, J., Kino, A., Vesley, R.E. (eds.) Intuitionism and Proof Theory, pp. 235–255. North-Holland, Amsterdam (1970)
Stone, M.H.: Topological representations of distributive lattices and Brouwerian logics. Casopis Pro Pestvovani Mathematiky a Fysiki Cast Matematicka 67, 1–25 (1937)
Tarski, A.: Der Aussagenkalkül and die Topologie. Fundam. Math. 31, 103–134 (1938)
Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics – An Introduction, vol. II. In: Studies in Logic and the Foundations of Mathematics, vol. 123. North-Holland, Amsterdam (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lubarsky, R.S. (2008). Topological Forcing Semantics with Settling. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2009. Lecture Notes in Computer Science, vol 5407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92687-0_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-92687-0_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-92686-3
Online ISBN: 978-3-540-92687-0
eBook Packages: Computer ScienceComputer Science (R0)