Elementary Computable Topology

Abstract

We revise and extend the foundation of computable topology in the framework of Type-2 theory of effectivity, TTE, where continuity and computability on finite and infinite sequences of symbols are defined canonically and transferred to abstract sets by means of notations and representations. We start from a computable topological space, which is a T0-space with a notation of a base such that intersection is computable, and define a number of multi-representations of the points and of the open, the closed and the compact sets and study their properties and relations. We study computability of boolean operations. By merely requiring "provability" of suitable relations (element, non-empty intersection, subset) we characterize in turn computability on the points, the open sets (!), computability on the open sets, computability on the closed sets, the compact sets(!), and computability on the compact sets. We study modifications of the definition of a computable topological space that do not change the derived computability concepts. We study subspaces and products and compare a number of representations of the space of partial continuous functions. Since we are operating mainly with the base elements, which can be considered as regions for points ("pointless topology"), we study to which extent these regions can be filled with points (completions). We conclude with some simple applications including Dini's Theorem as an example.