更改

'''[[Kreisel–Lacombe–Shoenfield–Čeĭnin定理]]（1957/1962）'''：作用在全函数上的可计算变换必然是'''连续'''的——输出在任何点的值只依赖输入函数的有限个值；而且可用确定性图灵机实现<ref name="moschovakis2010" />。

'''[[Kreisel–Lacombe–Shoenfield–Čeĭnin定理]]（1957/1962）'''：作用在全函数上的可计算变换必然是'''连续'''的——输出在任何点的值只依赖输入函数的有限个值；而且可用确定性图灵机实现<ref name="moschovakis2010" />。

[[尤里·切宁|Čeĭnin]] 的版本——"构造度量空间之间的每个可计算算子都是有效连续的"——是俄罗斯'''构造性分析'''学派（用可计算性重新奠基数学分析）的中心结果之一<ref name="moschovakis2010" />。证明中 SRT 出现两次，用法与上述如出一辙。

[[尤里·切宁|Čeĭnin]] 的版本——"构造度量空间之间的每个可计算算子都是有效连续的"——是俄罗斯'''[[构造性分析]]'''学派（用可计算性重新奠基数学分析）的中心结果之一<ref name="moschovakis2010" />。证明中 SRT 出现两次，用法与上述如出一辙。

此外，Rogers 用 SRT 证明了 '''[[Blum定理]]'''：任意两个"通用部分函数"（即[[解释器]]）都只差一个可计算的重新编号（递归同构）——编号系统在"重新命名"意义下本质唯一<ref name="rogers1967" />.

此外，Rogers 用 SRT 证明了 '''[[Blum定理]]'''：任意两个"[[通用部分函数]]"（即[[解释器]]）都只差一个可计算的重新编号（递归同构）——编号系统在"重新命名"意义下本质唯一<ref name="rogers1967" />.

=== Solovay 可证性逻辑 ===

=== Solovay 可证性逻辑 ===