Douglas S. Bridges: TBA in Constructive Theory of Apartness Spaces

The theory of apartness spaces, a counterpart of the classical one of proximity spaces, provides one entry to a purely constructive (i.e. developed with intuitionistic logic and CZF set theory or ML type theory) study of topology. The canonical example of apartness spaces are metric spaces, locally convex spaces, and, more generally, uniform spaces. The general theory of apartness and its specialisation to uniform spaces has been studied extensively since 2000, and is expounded in detail in [1].

In this talk we first present the basic notions of apartness between sets and of uniform structures, and point out the connection between point-set apartness spaces and neighbourhood spaces. We then introduce u-neighbourhood structures, which lie somewhere between topological and uniform neighbourhood structures. It turns out that every reasonable apartness space X has an associated apartness relation ⋈ _w induced by a u-neighbourhood structure. Classically, that associated structure is induced by the unique totally bounded uniform structure that induces the original apartness on X. Although there is no possibility of proving, in general, that ⋈ _w is induced constructively by a uniform structure, it is always induced by a u-neighbourhood structure.

The mysterious ‘TBA’ in the title of the talk derives from the fact that there is a natural definition of total boundedness for u-neighbourhood spaces, enabling us to examine the computationally useful notion of totally bounded apartness (TBA) outside the context of a uniform space.

Reference

[1] D.S. Bridges and L.S.Vîţă, Apartness and Uniformity: A Constructive Development, in: CiE series Theory and Applications of Computability, Springer Verlag, Heidelberg, 2011.