Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem

TL;DR

This paper develops a constructive framework for effective topological spaces, introduces Spreen spaces with a new separation property, and proves a purely constructive continuity theorem relating these spaces to regular spaces.

Contribution

It introduces Spreen spaces with a novel separation property and establishes a constructive continuity theorem linking these spaces to regular spaces.

Findings

Spreen spaces are plentiful in synthetic computability theory.

A new separation property for spaces is introduced.

A constructive continuity theorem for maps from Spreen spaces is proved.

Abstract

I take a constructive look at Dieter Spreen's treatment of effective topological spaces and the Kreisel-Lacombe-Shoenfield-Tseitin (KLST) continuity theorem. Transferring Spreen's ideas from classical computability theory and numbered sets to a constructive setting leads to a theory of topological spaces, in fact two of them: a locale-theoretic one embodied by the notion of $\sigma$-frames, and a pointwise one that follows more closely traditional topology. Spreen's notion of effective limit passing turns out to be closely related to sobriety, while his witnesses for non-inclusion give rise to a novel separation property - any point separated from an overt subset by a semidecidable subset is already separated from it by an open one. I name spaces with this property Spreen spaces, and show that they give rise to a purely constructive continuity theorem: every map from an overt Spreen space to a pointwise regular space is pointwise continuous. The theorem is easily proved, but finding non-trivial examples of Spreen spaces is harder. I show that they are plentiful in synthetic computability theory.