Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem (Q7022901)

This paper is a contribution to synthetic computability theory (SCT), a variety of constructive mathematics. The author provides a constructive treatment of Spreen's notion of an effective topological space and \textit{D. Spreen}'s generalisation of the Kreisel, Lacombe, Shoenfield and Tseitin theorem (KLST) on effective pointwise continuity of effective functions found in [J. Symb. Log. 63, No. 1, 185--221 (1998; Zbl 0915.03038)].\N\NFollowing an introduction, the author describes Rosolini's dominance in Section 2, the notion of semidecidability associated to an open set within SCT. The notion of an overt space, which is dual to a compact space, is defined through semidecidability. Two variants of countably based topological spaces are introduced in Section 3, \(\sigma\)-frames and pointwise bases. It is shown classically that in the effective topos there is a countable pointwise base that is not a countable base for a \(\sigma\)-frame. Sober spaces are defined in the context of \(\sigma\)-frames, and it is shown that a complete separable metric space is sober, that the hypothesis that every separable metric space is sober implies LPO and that the Scott topology of an \(\omega\)-algebraic \(\omega\)-cpo is sober. The author also gives an equational characterisation of \(\sigma\)-frame homomorphisms. In order to constructivise the standard KLST theorem, the author defines pointwise regular spaces and the so-called Spreen spaces. He then proves the synthetic KLST theorem, according to which, a map from an overt Spreen space to a regular space is pointwise continuous. In Sections 4 and 5, the author shows that within SCT, or the effective topos, there is a rich supply of Spreen spaces. Namely, he proves that a countably based sober space is a Spreen space, from which the classic KLST theorem follows.