How a Point-free Constructive Version of the Uryshon Metrization Theorem Can Turn a Collection Into a Set

Giovanni Curi

In the context of Type Theory the question often arises whether (the collection of points of) a given mathematical space (such as the Continuum, the spaces L(A) of linear functionals from a semi-normed space A to the reals,...) can be presented as a Set (Data Type) or not. Here we show that some topological conditions can be isolated which, if satisfied, allow to give a positive answer. The result is obtained by basing on the framework of Formal Topology (see [Sa87], [Sa99]), here conceived as a constructive and predicative presentation of point-free topology (Locale Theory, see e.g. [J82]) which can be phrased within Per Martin-Löf’s Type Theory ([ML84], [NPS90]; see also [SV98]).

We first introduce the notion of metric formal topology and prove that it is adequate as a point-free axiomatization of the notion of metric space. A predicative formulation of the topological concept of complete regularity is then provided, and the point-free constructive analogue of Uryshon’s metrization theorem (stating that a (completely) regular topological space with a countable base is metrizable) is derived. This metrization result leads to a characterization of the points of (a wide subclass of) compact regular formal topologies with a countable base and, more in general, of locally compact completely regular formal topologies with a countable base: points are shown to coincide with particular subsets of basic neighbourhoods (entirely defined by first-order conditions) in which neighbourhoods of arbitrarily small diameter can be found. It is then easily proved that if a space can be represented via a (locally) compact (completely) regular formal topology with a countable base, the collection of its points can be indexed by a set. We will say that such a space admits a domain. In particular, the Continuum, the n-dimensional Euclidean space, Cantor space, and a wide subclass of the class of topologies giving rise to the spaces L(A) of linear functionals from a semi-normed space A to the reals, admit a domain.

[J82] P. T. Johnstone, Stone Spaces, Cambridge University Press, 1982.

[ML84] P. Martin-Löf, Intuitionistic Type Theory. Studies in Proof Theory. Lecture Notes, 1. (Bibliopolis), Napoli, 1984.

[NPS90] B.Nordstrom, K. Peterson, J. Smith, Programming in Martin-Löf’s Type Theory (Clarendon Press), Oxford, 1990.

[Sa87] G. Sambin, “Intuitionistic formal spaces - a first communication”, in Mathematical Logic and its Applications, D. Skordev, ed. Plenum, New York - London 1987, 187-204

[Sa99] G. Sambin, “Formal topology and domains”, proceedings of the Workshop on Domains IV, Informatik-Bericht Nr. 99-01, Universität-GH Siegen, 1999.

[SV98] G. Sambin, S. Valentini, “Building up a toolbox for Martin-Löf’s type theory: subset theory”. In: Twenty-Five years of Constructive Type Theory. Proceedings of a Congress held in Venice, October 1995, G. Sambin and J. Smith eds., Oxford University Press, 1998, pp. 221-244.

Address: Dipartimento di Matematica “Roberto Magari”, Via del Capitano, 15 - 53100 Siena, Italy

E-mail: gcuri@math.unipd.it