Spreen 空间与综合 Kreisel-Lacombe-Shoenfield-Tseitin 定理

我从构造性视角考察 Dieter Spreen 对有效拓扑空间及 Kreisel-Lacombe-Shoenfield-Tseitin（KLST）连续性定理的处理。将 Spreen 的思想从经典可计算性理论与编号集转移到构造性设定中，会导出一种拓扑空间理论，事实上是两种：一种由 $\sigma$-frames 概念体现的局部ic 理论，以及一种更贴近传统拓扑的点态理论。Spreen 的有效极限传递概念被证明与 sober 性密切相关，而他的非包含性见证则引出了一种新颖的分离性质——任何被半可判定子集从可显见（overt）子集中分离出来的点，已然被一个开子集从该子集中分离出来。我将具有此性质的空间命名为 Spreen 空间，并证明它们引出一个纯粹的构造性连续性定理：从可显见 Spreen 空间到点点正则空间的每个映射都是点态连续的。该定理易于证明，但寻找 Spreen 空间的非平凡例子则更为困难。我展示了它们在综合可计算性理论中十分丰富。