×

Heyting-valued interpretations for constructive set theory. (English) Zbl 1077.03038

Summary: We define and investigate Heyting-valued interpretations for Constructive Zermelo-Frankel set theory (CZF). These interpretations provide models for CZF that are analogous to Boolean-valued models for ZF and to Heyting-valued models for IZF. Heyting-valued interpretations are defined here using set-generated frames and formal topologies. As applications of Heyting-valued interpretations, we present a relative consistency result and an independence proof.

MSC:

03F65 Other constructive mathematics
03E70 Nonclassical and second-order set theories
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] P. Aczel, Extending the topological interpretation to Constructive Set Theory, Manuscript notes, 1977; P. Aczel, Extending the topological interpretation to Constructive Set Theory, Manuscript notes, 1977
[2] Aczel, P., The type theoretic interpretation of Constructive Set Theory, (MacIntyre, A.; Pacholski, L.; Paris, J., Logic Colloquium’77 (1978), North-Holland), 55-66
[3] P. Aczel, The type theoretic interpretation of Constructive Set Theory: choice principles, in: Troelstra and van Dalen [37]; P. Aczel, The type theoretic interpretation of Constructive Set Theory: choice principles, in: Troelstra and van Dalen [37]
[4] Aczel, P., The type theoretic interpretation of Constructive Set Theory: inductive definitions, (Barcan Marcus, R.; Dorn, G. J.W.; Weinegartner, P., Logic, Methodology and Philosophy of Science VII (1986), North-Holland), 17-49 · Zbl 0624.03044
[5] Aczel, P., On relating type theories and set theories, (Altenkirch, T.; Naraschewski, W.; Reus, B., Types for Proofs and Programs. Types for Proofs and Programs, Lecture Notes in Computer Science, vol. 1257 (2000), Springer) · Zbl 0944.03056
[6] Aczel, P.; Gambino, N., Collection principles in Dependent Type Theory, (Callaghan, P.; Luo, Z.; McKinna, J.; Pollack, R., Types for Proofs and Programs. Types for Proofs and Programs, Lecture Notes in Computer Science, vol. 2277 (2002), Springer), 1-23 · Zbl 1054.03036
[7] P. Aczel, M. Rathjen, Notes on Constructive Set Theory, Technical Report 40, Mittag-Leffler Institute, The Swedish Royal Academy of Sciences, 2001. Available from the first author’s web page at http://www.cs.man.ac.uk/ petera/papers.html; P. Aczel, M. Rathjen, Notes on Constructive Set Theory, Technical Report 40, Mittag-Leffler Institute, The Swedish Royal Academy of Sciences, 2001. Available from the first author’s web page at http://www.cs.man.ac.uk/ petera/papers.html
[8] G. Battilotti, G. Sambin, Pretopologies and a uniform presentation of sup-lattices, quantales and frames, Annals of Pure and Applied Logic (in press), doi: 10.1016/j.apal.2005.05.017; G. Battilotti, G. Sambin, Pretopologies and a uniform presentation of sup-lattices, quantales and frames, Annals of Pure and Applied Logic (in press), doi: 10.1016/j.apal.2005.05.017 · Zbl 1077.03036
[9] Bell, J. L., Boolean-valued Models and Independence Proofs in Set Theory (1977), Clarendon Press · Zbl 0371.02028
[10] Boileau, A.; Joyal, A., La logique des topos, Journal of Symbolic Logic, 46, 1, 6-16 (1981) · Zbl 0544.03035
[11] Coquand, T.; Palmgren, E., Intuitionistic choice and classical logic, Archive for Mathematical Logic, 39, 1, 53-74 (2000) · Zbl 0947.03078
[12] Coquand, T.; Sambin, G.; Smith, J. M.; Valentini, S., Inductively generated formal topologies, Annals of Pure and Applied Logic, 124, 1-3, 71-106 (2003) · Zbl 1070.03041
[13] Dragalin, A. G., Mathematical Intuitionism — Introduction to Proof Theory, Translations of Mathematical Monographs, vol. 67 (1980), American Mathematical Society · Zbl 0634.03054
[14] Escardó, M. H.; Simpson, A. K., A universal characterization of the closed Euclidean interval (extended abstract), (16th Annual IEEE Symposium on Logic in Computer Science (2001), IEEE Press), 115-125
[15] Feferman, S., Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis, (Kino, A.; Myhill, J.; Vesley, R. E., Intuitionism and Proof Theory (1970), North-Holland), 303-325 · Zbl 0218.02024
[16] M.P. Fourman, R.J. Grayson, Formal spaces, in: Troelstra and van Dalen [37]; M.P. Fourman, R.J. Grayson, Formal spaces, in: Troelstra and van Dalen [37]
[17] M.P. Fourman, J.M.E. Hyland, Sheaf models for analysis, in: Fourman et al. [18]; M.P. Fourman, J.M.E. Hyland, Sheaf models for analysis, in: Fourman et al. [18] · Zbl 0427.03028
[18] Applications of Sheaves, (Fourman, M. P.; Mulvey, C. J.; Scott, D. S., Lecture Notes in Mathematics, vol. 753 (1979), Springer)
[19] N. Gambino, Sheaf interpretations for generalised predicative intuitionistic theories, Ph.D. Thesis, Department of Computer Science, University of Manchester, 2002; N. Gambino, Sheaf interpretations for generalised predicative intuitionistic theories, Ph.D. Thesis, Department of Computer Science, University of Manchester, 2002
[20] Gambino, N., Presheaf models for constructive set theories, (Schuster, P.; Crosilla, L., From Sets and Types to Topology and Analysis (2005), Oxford University Press) · Zbl 1098.03072
[21] R.J. Grayson, Heyting-valued models for Intuitionistic Set Theory, in: Fourman et al. [18]; R.J. Grayson, Heyting-valued models for Intuitionistic Set Theory, in: Fourman et al. [18]
[22] Grayson, R. J., Forcing in intuitionistic systems without power-set, Journal of Symbolic Logic, 48, 3, 670-682 (1983) · Zbl 0595.03056
[23] Griffor, E. R.; Rathjen, M., The strength of some Martin-Löf type theories, Archive for Mathematical Logic, 33, 347-385 (1994) · Zbl 0819.03047
[24] Johnstone, P. T., Stone Spaces (1982), Cambridge University Press · Zbl 0499.54001
[25] Johnstone, P. T., The point of pointless topology, Bullettin of the American Mathematical Society, 8, 41-53 (1983) · Zbl 0499.54002
[26] Joyal, A.; Tierney, M., An extension of the Galois theory of Grothendieck, Memoirs of the American Mathematical Society, 309 (1984) · Zbl 0541.18002
[27] MacLane, S.; Moerdijk, I., Sheaves in Geometry and Logic — A First Introduction to Topos Theory (1992), Springer
[28] Moerdijk, I.; Palmgren, E., Wellfounded trees in categories, Annals of Pure and Applied Logic, 104, 189-218 (2000) · Zbl 1010.03056
[29] Moerdijk, I.; Palmgren, E., Type theories, toposes and Constructive Set Theory: predicative aspects of AST, Annals of Pure and Applied Logic, 114, 1-3, 155-201 (2002) · Zbl 0999.03061
[30] Rathjen, M.; Griffor, E. R.; Palmgren, E., Inaccessibility in Constructive Set Theory and Type Theory, Annals of Pure and Applied Logic, 94, 181-200 (1994) · Zbl 0926.03074
[31] Sambin, G., Intuitionistic formal spaces — A first communication, (Skordev, D., Mathematical Logic and its Applications (1987), Plenum), 87-204 · Zbl 1242.03087
[32] Sambin, G., Some points in formal topology, Theoretical Computer Science, 305, 1-3, 347-408 (2003) · Zbl 1044.54001
[33] Scedrov, A., Consistency and independence results in Intuitionistic Set Theory, (Richman, F., Constructive Mathematics. Constructive Mathematics, Lecture Notes in Mathematics, vol. 873 (1981), Springer), 54-86
[34] A. Scedrov, Independence of the fan theorem in the presence of continuity principles, in: Troelstra and van Dalen [37]; A. Scedrov, Independence of the fan theorem in the presence of continuity principles, in: Troelstra and van Dalen [37]
[35] Scedrov, A., Intuitionistic Set Theory, (Harrington, L. A.; Morley, M. D.; Scedrov, A.; Simpson, S. G., Harvey Friedman’s Research on the Foundations of Mathematics (1985), North-Holland), 257-284
[36] Simmons, H., A framework for topology, (MacIntyre, A.; Pacholski, L.; Paris, J., Logic Colloqiuum ’77 (1978), North-Holland), 239-251 · Zbl 0493.06005
[37] The L. E. J. Brouwer Centenary Symposium, (Troelstra, A. S.; van Dalen, D. (1982), North-Holland)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.