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

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.