Some points in formal topology. (English) Zbl 1044.54001

It is now more than fifteen years since the appearance of the author’s ‘first communication’ on formal spaces, a constructive and predicative approach to general topology designed to be interpretable in Martin-Löf’s type theory.
The present paper has three main aims, which are developed in three broadly independent sections: first, to survey the progress that has been made since then in developing traditional notions of topology in the formal setting; secondly, to provide publicity for what the author calls ‘the basic picture’, which is a newer and more symmetric way of looking at the relationship between points and open sets, still under development by the author and S. Gebellato; and finally, in a section less mathematical and more philosophical in character, to present the author’s understanding of how and why one should seek to develop mathematics in a constructive context.


54A05 Topological spaces and generalizations (closure spaces, etc.)
03A05 Philosophical and critical aspects of logic and foundations
03F65 Other constructive mathematics
Full Text: DOI


[1] Abramsky, S.; Jung, A., Domain theory, (), 1-168
[2] G. Battilotti, G. Sambin, A uniform presentation of sup-lattices, quantales and frames by means of infinitary preordered sets, pretopologies and formal topologies, Preprint No. 19, Dipartimento di Matematica, Università di Padova, November 1993. · Zbl 1077.03036
[3] G. Battilotti, G. Sambin, Pretopologies and a uniform presentation of sup-lattices, quantales and frames, to appear. · Zbl 1077.03036
[4] Bishop, E., Foundations of constructive analysis, (1967), McGraw-Hill New York · Zbl 0183.01503
[5] E. Bishop, Schizophrenia in contemporary mathematics, in: M. Rosenblatt (Eds.), Errett Bishop: Reflections on Him and His Research, San Diego, CA, 1983, Contemporary Mathematics, Vol. 39, Amer. Math. Soc. Providence, RI, 1985, pp. 1-32.
[6] J. Cederquist, T. Coquand, Entailment relations and distributive lattices, in: Logic Colloquium ’98, Lecture Notes in Logic, Vol. 13, Association of Symbolic Logic, Springer, Berlin, 2000, pp. 127-139. · Zbl 0948.03056
[7] Cederquist, J.; Coquand, T.; Negri, S., The hahn – banach theorem in type theory, (), 57-72 · Zbl 0940.03069
[8] Coquand, T., An intuitionistic proof of Tychonoff’s theorem, J. symbolic logic, 57, 28-32, (1992) · Zbl 0764.03024
[9] Coquand, T.; Sadocco, S.; Sambin, G.; Smith, J., Formal topologies on the set of first-order formulae, J. symbolic logic, 65, 1183-1192, (2000) · Zbl 0965.03072
[10] T. Coquand, G. Sambin, J. Smith, S. Valentini, Inductively generated formal topologies, Ann. Pure Appl. Logic, to appear. · Zbl 1070.03041
[11] G. Curi, Analisi costruttiva nella teoria dei tipi: topologie formali con diametro e distanza, Tesi di laurea in Matematica, Università di Padova, July 1998.
[12] Curi, G., Metric spaces in type theory via formal topology, ()
[13] Curi, G., The points of (locally) compact regular formal topologies, () · Zbl 1011.54001
[14] G. Curi, Constructive metrizability in point-free topology, 2002, Theoret. Comput. Sci. · Zbl 1045.54002
[15] Engelking, R., Outline of general topology, (1968), North-Holland Amsterdam · Zbl 0157.53001
[16] Fourman, M.P.; Grayson, R.J., Formal spaces, (), 107-122 · Zbl 0537.03040
[17] S. Gebellato, G. Sambin, The essence of continuity (the Basic Picture, II), Preprint No. 27, Dipartimento di Matematica, Università di Padova, December 2001. · Zbl 0953.03069
[18] S. Gebellato, G. Sambin, Pointfree Continuity and Convergence, (the Basic Picture, II), Vol. IV, 2001, first draft. · Zbl 0953.03069
[19] S. Gebellato, G. Sambin, The basic picture as invariance under transfer along a relation, (the Basic Picture, II), Vol. V, 2002, first draft. · Zbl 0953.03069
[20] Girard, J., Linear logic, Theoret. comput. sci., 50, 1-102, (1987) · Zbl 0625.03037
[21] Johnstone, P.T., Stone spaces, (1982), Cambridge University Press Cambridge
[22] Kelley, J.L., General topology, (1955), van Nostrand New York · Zbl 0066.16604
[23] Maietti, M.E., About effective quotients in constructive type theory, (), 164-178 · Zbl 0943.03053
[24] Maietti, M.E.; Valentini, S., Can you add power-sets to martin-Löf’s intuitionistic set theory?, Math. logic quart., 45, 521-532, (1999) · Zbl 0935.03071
[25] Martin-Löf, P., Notes on constructive mathematics, (1970), Almqvist & Wiksell Stockholm · Zbl 0273.02021
[26] P. Martin-Löf, Constructive Mathematics and Computer Programming, in: L. Cohen, J. Łoš, H. Pfeiffer, K. Podowski (Eds.), Logic, Methodology and Philosophy of Science, Vol. VI, North-Holland, Amsterdam, 1982, pp. 153-175.
[27] P. Martin-Löf, Intuitionistic type theory. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980, Bibliopolis, Napoli, 1984.
[28] Negri, S.; Soravia, D., The continuum as a formal space, Arch. math. logic, 38, 423-447, (1999) · Zbl 0936.03060
[29] Negri, S.; Valentini, S., Tychonoff’s theorem in the framework of formal topologies, J. symbolic logic, 62, 1315-1332, (1997) · Zbl 0893.03023
[30] Nordström, B.; Petersson, K.; Smith, J.M., Programming in martin-Löf’s type theory, an introduction, (1990), Oxford University Press Oxford
[31] Pratt, V., Chu spaces and their interpretation as concurrent objects, (), 392-405
[32] Sambin, G., Intuitionistic formal spaces—a first communication, (), 187-204
[33] Sambin, G., Pretopologies and completeness proofs, J. symbolic logic, 60, 861-878, (1995) · Zbl 0839.03022
[34] Sambin, G., Formal topology and domains, () · Zbl 0962.68098
[35] Sambin, G., Steps towards a dynamic constructivism, (), 261-284
[36] G. Sambin, The Basic Picture, a structure for topology, (the Basic Picture, II), I, Preprint No. 26, Dipartimento di Matematica, Università di Padova, December 2001.
[37] G. Sambin, Basic topologies, formal topologies, formal spaces, (the Basic Picture, II), III, in preparation. · Zbl 1187.54010
[38] Sambin, G.; Gebellato, S., A preview of the basic picture: a new perspective on formal topology, (), 194-207 · Zbl 0953.03069
[39] Sambin, G.; Valentini, S., Building up a toolbox for martin-Löf’s type theory: subset theory, (), 221-244 · Zbl 0930.03091
[40] Sambin, G.; Valentini, S.; Virgili, P., Constructive domain theory as a branch of intuitionistic pointfree topology, Theoret. comput. sci., 159, 319-341, (1996) · Zbl 0871.68063
[41] Scott, D.S., Domains for denotational semantics, (), 577-613
[42] Sigstam, I., Formal spaces and their effective presentations, Arch. math. logic, 34, 211-246, (1995) · Zbl 0829.03026
[43] M.B. Smyth, Topology, in: S. Abramsky, D.M. Gabbay, T.S.E. Taibaum (Eds.), Handbook of Logic in Computer Science, Vol. 1, Clarendon Press, Oxford, 1992, pp. 641-761.
[44] B. Solito, Gli operatori di interno e di chiusura da un punto di vista costruttivo. Tesi di Laurea in Matematica, Università di Padova, October 1998.
[45] D. Soravia, Numeri reali e analisi costruttiva nel contesto delle topologie formali. Tesi di Laurea in Matematica, Università di Padova, July 1995.
[46] Valentini, S., The forget-restore principle: a paradigmatic example, (), 275-283 · Zbl 0937.03069
[47] Valentini, S., A Cartesian closed category in martin-Löf’s intuitionistic type theory, Theoret. comput. sci., 290, 189-219, (2002) · Zbl 1018.68078
[48] Vickers, S., Topology via logic, Cambridge tracts in theoretical computer science, Vol. 5, (1989), Cambridge University Press Cambridge · Zbl 0668.54001
[49] Weihrauch, K.; Schreiber, U., Embedding metric spaces into Cpo’s, Theoret. comput. sci., 16, 5-24, (1981) · Zbl 0485.68040
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.