Abstract.
Formal topologies are today an established topic in the development of constructive mathematics. One of the main tools in formal topology is inductive generation since it allows to introduce inductive methods in topology. The problem of inductively generating formal topologies with a cover relation and a unary positivity predicate has been solved in [CSSV]. However, to deal both with open and closed subsets, a binary positivity predicate has to be considered. In this paper we will show how to adapt to this framework the method used to generate inductively formal topologies with a unary positivity predicate; the main problem that one has to face in such a new setting is that, as a consequence of the lack of a complete formalization, both the cover relation and the positivity predicate can have proper axioms.
Similar content being viewed by others
References
Coquand, T., Sambin, G., Smith, J., Valentini, S.: Inductively generated formal topologies. Ann. Pure and Applied Logic, 124 (1–3), 71–106 (2003)
Engelking, R.: General Topology. Polish Scientific Publisher, Warszawa, 1977
Martin-Löf, P.: Intuitionistic Type Theory, notes by G. Sambin of a series of lectures given in Padua. Bibliopolis, Naples, 1984
Negri, S., Valentini, S.: Tychonoff’s theorem in the framework of formal topologies. J. Symbolic Logic, 62 (4), 1315–1332 (1997)
Sambin, G.: Some points in formal topology. Topology in computer science (Schlo Dagstuhl, 2000). Theoretical Computer Science, 305 (1–3), 347–408 (2003)
Sambin, G., Gebellato, S.: A preview of the basic picture: a new perspective on formal topology. Proceedings of the Annual Meeting of the Types Working Group “Types ‘98”, T. Altenkirch and W. Naraschewski and B. Reus (eds.), Springer Lecture Notes in Computer Science, 1999, pp. 194–207
Sambin, G. with Gebellato, S., Martin-Löf, P., Capretta, V.: The basic picture. To appear
Sambin, G., Valentini, S.: Building up a tool-box for Martin-Löf intuitionistic type theory. In: Twenty-five years of Constructive Type Theory, G. Sambin and J. Smith (eds.), Oxford logic guides 36, 221–244 (1998)
Valentini, S.: The problem of completeness of formal topologies with a binary positivity predicate and their inductive generation. http://www.math.unipd.it/∼silvio
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Valentini, S. The problem of the formalization of constructive topology. Arch. Math. Logic 44, 115–129 (2005). https://doi.org/10.1007/s00153-004-0243-1
Received:
Revised:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00153-004-0243-1