New definitions in the theory of Type 1 computable topological spaces

In 1957, Lacombe initiated a systematic study of the different possible notions of “computable topological spaces.” However, he interrupted this line of research, settling for the idea that “computably open sets should be computable unions of basic open sets.” We explain the limits of this approach, which in particular is not general enough to account for all spaces that admit a computable metric. We give a general notion of Type 1 computable topological space that does not rely on a notion of effective basis. Building on the work of Spreen, we show that the use of a formal inclusion relation should be systematized. We give the first general definition of the computable topology associated to a computable metric that does not rely on effective separability. This definition can be translated to other constructive settings, and its relevance goes beyond that of Type 1 computability. Finally, we give a new version of a theorem of Moschovakis, by showing that for an appropriate notion of effective basis, the “computably open sets” reduce to “computable unions of basic open sets” on computably separable spaces.