递归定理 - 版本历史

Jake：/* SRT 与计算复杂性理论 */

2026-09-20T00:43:41Z

SRT 与计算复杂性理论

Jake：/* 存在性与可构造性的分野 */

2026-09-18T02:51:29Z

存在性与可构造性的分野

Jake：/* 存在性与可构造性的分野 */

2026-09-18T02:51:09Z

存在性与可构造性的分野

Jake：/* SRT 与计算复杂性理论 */

2026-09-18T02:47:54Z

SRT 与计算复杂性理论

Jake：/* Myhill定理：创造集 = 完备集 */

2026-09-18T02:38:51Z

Myhill定理：创造集 = 完备集

Jake：/* 通用序数记号系统ω_1^{CK} */

2026-09-18T02:36:08Z

通用序数记号系统ω_1^{CK}

2026年9月18日 (五) 02:35 Jake

2026-09-18T02:35:47Z

Jake：/* Rice-Shapiro 定理（1956） */

2026-09-18T02:34:29Z

Rice-Shapiro 定理（1956）

Jake：/* Rice定理（1951） */

2026-09-18T02:29:25Z

Rice定理（1951）

Jake：/* 超算术集与有效描述集合论 */

2026-09-18T02:22:47Z

超算术集与有效描述集合论

@@ 第832行： / 第832行： @@
 ==== SRT 与计算复杂性理论 ====
-在[[复杂性理论]]中，递归定理主要扮演'''证明工具'''的角色。[[复杂性类]]的许多分离与结构定理采用"带时钟的对角化"：让机器检查并躲开自己（或更早的机器）的行为；当这种自躲藏需要程序援引自己的代码时，严格化的抓手正是 SRT。这类证明有一个内禀的时序难题：对角化机器要躲开的对象可能就是它自己（或自己的更早版本），而它必须在对方"提交行为"之后才能可靠地反着做——处理这一难题的技术称为'''延迟对角化'''（delayed diagonalization），其源头是 Breidbart 的"[[分裂递归集]]"构造显式调用递归定理<ref name="breidbart1978">'''Breidbart, S. (1978).''' ''On splitting recursive sets''. Journal of Computer and System Sciences 17: 56–64.【复杂性类对角化中显式使用递归定理的"延迟构造"源头】</ref>；其思想后来被 Schmidt 统一为"[[复杂性类的递归论结构]]"定理，推论包括：除非 [[NP = P]]，[[NP]] 不等于 [[P]] 与 NP 完全类之并这类"[[可递归呈现类]]"的非平凡并<ref name="schmidt1985">'''Schmidt, D. (1985).''' ''The recursion-theoretic structure of complexity classes''. Theoretical Computer Science 38: 143–156. doi:10.1016/0304-3975(85)90217-8.【复杂性类对角化定理的递归论统一；推论：除非 NP=P，NP ≠ P ∪ {NP完全类}】</ref>。延迟对角化由此成为分离复杂性类的标准武器——本质上，它是"带时钟的对角线"对自引用时序的形式化处理。
+在[[复杂性理论]]中，递归定理主要扮演'''证明工具'''的角色。[[复杂性类]]的许多分离与结构定理采用"带时钟的对角化"：让机器检查并躲开自己（或更早的机器）的行为；当这种自躲藏需要程序援引自己的代码时，严格化的抓手正是 SRT。这类证明有一个内禀的时序难题：对角化机器要躲开的对象可能就是它自己（或自己的更早版本），而它必须在对方"提交行为"之后才能可靠地反着做——处理这一难题的技术称为'''[[延迟对角化]]'''（delayed diagonalization）。这一思想的源头可以追溯到 Breidbart 的"[[分裂递归集]]"构造显式调用递归定理<ref name="breidbart1978">'''Breidbart, S. (1978).''' ''On splitting recursive sets''. Journal of Computer and System Sciences 17: 56–64.【复杂性类对角化中显式使用递归定理的"延迟构造"源头】</ref>，后来被 Schmidt 统一为"[[复杂性类的递归论结构]]"定理，推论包括：除非 [[NP = P]]，[[NP]] 不等于 [[P]] 与 NP 完全类之并这类"[[可递归呈现类]]"的非平凡并<ref name="schmidt1985">'''Schmidt, D. (1985).''' ''The recursion-theoretic structure of complexity classes''. Theoretical Computer Science 38: 143–156. doi:10.1016/0304-3975(85)90217-8.【复杂性类对角化定理的递归论统一；推论：除非 NP=P，NP ≠ P ∪ {NP完全类}】</ref>。延迟对角化由此成为分离复杂性类的标准武器——本质上，它是"带时钟的对角线"对自引用时序的形式化处理。
 在[[曼纽尔·布卢姆|Blum]]的机器无关复杂性理论中，SRT 与对角化结合产生了一批"存在性"结果。代表性的一例：Helm 与 Young 回答了 Blum 的一个问题——存在这样的可计算函数，任何为它"换上更快的程序"的尝试都要付出程序尺寸爆炸的代价，且刻画这一代价的增长函数快于任何递归函数<ref name="helmyoung1971">'''Helm, J.; Young, P. (1971).''' ''On size vs. efficiency for programs admitting speed-ups''. Journal of Symbolic Logic 36.【回答 Blum 的问题：加速必然伴随尺寸爆炸，代价函数增长快于任何递归函数】</ref>。"加速与简洁不可兼得"由此成为定理而非格言。

@@ 第844行： / 第844行： @@
 '''工具一：[[Kolmogorov复杂性]]与[[DNR度]]。'''相对化之后 SRT 何时失效，有一个精确刻画：<math>A</math> 能算 DNR 函数当且仅当 <math>A</math> 是 [[autocomplex]] 的<ref name="kjos2011">'''Kjos-Hanssen, B.; Merkle, W.; Stephan, F. (2011).''' ''Kolmogorov complexity and the recursion theorem''. Transactions of the American Mathematical Society 363(10): 5465–5480. doi:10.1090/S0002-9947-2011-05306-7.【SRT 相对化失效的刻画：A 能计算 DNR 函数 ⟺ A autocomplex；会议版为 STACS 2006, LNCS 3884, 149–161】</ref>。换个角度看，这条定理把"自指是否可用"从一个全有全无的定性事实，变成了一个由环境（oracle）标定的'''可测量、可分级、可缺失'''的复杂性量——DNR 度的层级就是"自指损坏程度"的标尺。
-'''工具二（工程终点）：哥德尔机。'''Schmidhuber 把"资源有界的自引用"推到了最雄心勃勃的形式<ref name="schmidhuber2003">'''Schmidhuber, J. (2003).''' ''Gödel machines: self-referential universal problem solvers making provably optimal self-improvements''. arXiv:cs/0309048【正式版本见 LNCS 3394 (2005), 1–23 及 Springer《Artificial General Intelligence》(2006)；IDSIA 技术报告 IDSIA-19-03】</ref>：机器的初始代码包含自身硬件、环境、效用函数乃至整个初始软件的公理化描述，一个基于 [[Levin通用搜索]]的偏置最优证明搜索器（BIOPS）持续寻找证明——'''一旦证明某个对自身代码的改写能提升未来效用，就立即改写（包括改写证明搜索器本身）'''。由于改写前必须证明"继续搜索其他改写不值当"，每次自改进都是全局最优的，没有局部极值。它的边界同样是哥德尔式的：只能改写"在形式系统内可证明有用"的部分，超出可证明范围的好处再大也拿不到。这条工程谱系与上文的[[#自省程序与自省式自改进程序|自省程序]]一脉相承：自省程序"知道自己的有界执行轨迹"，哥德尔机则"能证明地改写自己的任何部分"——自指从存在性工具，最终长成了资源有界的自改进机制<ref name="zhang2026" />。
+'''工具二（工程终点）：[[哥德尔机]]。'''Schmidhuber 把"资源有界的自引用"推到了最雄心勃勃的形式<ref name="schmidhuber2003">'''Schmidhuber, J. (2003).''' ''Gödel machines: self-referential universal problem solvers making provably optimal self-improvements''. arXiv:cs/0309048【正式版本见 LNCS 3394 (2005), 1–23 及 Springer《Artificial General Intelligence》(2006)；IDSIA 技术报告 IDSIA-19-03】</ref>：机器的初始代码包含自身硬件、环境、效用函数乃至整个初始软件的公理化描述，一个基于 [[Levin通用搜索]]的偏置最优证明搜索器（BIOPS）持续寻找证明——'''一旦证明某个对自身代码的改写能提升未来效用，就立即改写（包括改写证明搜索器本身）'''。由于改写前必须证明"继续搜索其他改写不值当"，每次自改进都是全局最优的，没有局部极值。它的边界同样是哥德尔式的：只能改写"在形式系统内可证明有用"的部分，超出可证明范围的好处再大也拿不到。这条工程谱系与上文的[[#自省程序与自省式自改进程序|自省程序]]一脉相承：自省程序"知道自己的有界执行轨迹"，哥德尔机则"能证明地改写自己的任何部分"——自指从存在性工具，最终长成了资源有界的自改进机制<ref name="zhang2026" />。
 ==== KRT 可以被分级 ====

@@ 第844行： / 第844行： @@
 '''工具一：[[Kolmogorov复杂性]]与[[DNR度]]。'''相对化之后 SRT 何时失效，有一个精确刻画：<math>A</math> 能算 DNR 函数当且仅当 <math>A</math> 是 [[autocomplex]] 的<ref name="kjos2011">'''Kjos-Hanssen, B.; Merkle, W.; Stephan, F. (2011).''' ''Kolmogorov complexity and the recursion theorem''. Transactions of the American Mathematical Society 363(10): 5465–5480. doi:10.1090/S0002-9947-2011-05306-7.【SRT 相对化失效的刻画：A 能计算 DNR 函数 ⟺ A autocomplex；会议版为 STACS 2006, LNCS 3884, 149–161】</ref>。换个角度看，这条定理把"自指是否可用"从一个全有全无的定性事实，变成了一个由环境（oracle）标定的'''可测量、可分级、可缺失'''的复杂性量——DNR 度的层级就是"自指损坏程度"的标尺。
-'''工具二（工程终点）：哥德尔机。'''Schmidhuber 把"资源有界的自引用"推到了最雄心勃勃的形式<ref name="schmidhuber2003">'''Schmidhuber, J. (2003).''' ''Gödel machines: self-referential universal problem solvers making provably optimal self-improvements''. arXiv:cs/0309048【正式版本见 LNCS 3394 (2005), 1–23 及 Springer《Artificial General Intelligence》(2006)；IDSIA 技术报告 IDSIA-19-03】</ref>：机器的初始代码包含自身硬件、环境、效用函数乃至整个初始软件的公理化描述，一个基于 Levin 通用搜索的偏置最优证明搜索器（BIOPS）持续寻找证明——'''一旦证明某个对自身代码的改写能提升未来效用，就立即改写（包括改写证明搜索器本身）'''。由于改写前必须证明"继续搜索其他改写不值当"，每次自改进都是全局最优的，没有局部极值。它的边界同样是哥德尔式的：只能改写"在形式系统内可证明有用"的部分，超出可证明范围的好处再大也拿不到。这条工程谱系与上文的[[#自省程序与自省式自改进程序|自省程序]]一脉相承：自省程序"知道自己的有界执行轨迹"，哥德尔机则"能证明地改写自己的任何部分"——自指从存在性工具，最终长成了资源有界的自改进机制<ref name="zhang2026" />。
+'''工具二（工程终点）：哥德尔机。'''Schmidhuber 把"资源有界的自引用"推到了最雄心勃勃的形式<ref name="schmidhuber2003">'''Schmidhuber, J. (2003).''' ''Gödel machines: self-referential universal problem solvers making provably optimal self-improvements''. arXiv:cs/0309048【正式版本见 LNCS 3394 (2005), 1–23 及 Springer《Artificial General Intelligence》(2006)；IDSIA 技术报告 IDSIA-19-03】</ref>：机器的初始代码包含自身硬件、环境、效用函数乃至整个初始软件的公理化描述，一个基于 [[Levin通用搜索]]的偏置最优证明搜索器（BIOPS）持续寻找证明——'''一旦证明某个对自身代码的改写能提升未来效用，就立即改写（包括改写证明搜索器本身）'''。由于改写前必须证明"继续搜索其他改写不值当"，每次自改进都是全局最优的，没有局部极值。它的边界同样是哥德尔式的：只能改写"在形式系统内可证明有用"的部分，超出可证明范围的好处再大也拿不到。这条工程谱系与上文的[[#自省程序与自省式自改进程序|自省程序]]一脉相承：自省程序"知道自己的有界执行轨迹"，哥德尔机则"能证明地改写自己的任何部分"——自指从存在性工具，最终长成了资源有界的自改进机制<ref name="zhang2026" />。
 ==== KRT 可以被分级 ====

@@ 第836行： / 第836行： @@
 在[[曼纽尔·布卢姆|Blum]]的机器无关复杂性理论中，SRT 与对角化结合产生了一批"存在性"结果。代表性的一例：Helm 与 Young 回答了 Blum 的一个问题——存在这样的可计算函数，任何为它"换上更快的程序"的尝试都要付出程序尺寸爆炸的代价，且刻画这一代价的增长函数快于任何递归函数<ref name="helmyoung1971">'''Helm, J.; Young, P. (1971).''' ''On size vs. efficiency for programs admitting speed-ups''. Journal of Symbolic Logic 36.【回答 Blum 的问题：加速必然伴随尺寸爆炸，代价函数增长快于任何递归函数】</ref>。"加速与简洁不可兼得"由此成为定理而非格言。
-更微妙的是，我们能否把 SRT 本身复杂性化？如果把编号限制到多项式时间的程序族上，SRT 还成立吗？困难出在证明的两个枢纽操作上：通用模拟在 P-时间世界里没有多项式时间版本（万能解释器本身要超线性时间），s-m-n 实例化（把参数写死）也会放大运行时间。因此对一般的多项式时间编号，'''带时间界的 SRT 不成立'''；不过 Kleene 1938 年的直接证明不经过通用程序，所以某些没有通用程序的子递归系统仍保有递归定理。一句话主旋律：'''自指免费，高效自指昂贵'''——不动点的"存在"有保证，"存在得节省"没有。
+更微妙的是，我们能否把 SRT 本身复杂性化？如果把编号限制到多项式时间的程序族上，SRT 还成立吗？困难出在证明的两个枢纽操作上：通用模拟在 P-时间世界里没有多项式时间版本（万能解释器本身要超线性时间），s-m-n 实例化（把参数写死）也会放大运行时间。因此对一般的多项式时间编号，'''带时间界的 SRT 不成立'''；不过 Kleene 1938 年的直接证明不经过通用程序，所以某些没有通用程序的子递归系统仍保有递归定理。一句话主旋律：'''自指免费，高效自指则昂贵'''——不动点的"存在"有保证，"节省地存在"则没有。
 ==== 存在性与可构造性的分野 ====

@@ 第758行： / 第758行： @@
 * '''[[Myhill定理]]（Myhill 1955）'''：每个创造集都是 r.e.-完备的；两个概念重合<ref name="myhill1955">Myhill, J., & Shepherdson, J. C. (1955). Effective operations on partial recursive functions. ''Zeitschrift für mathematische Logik und Grundlagen der Mathematik'', 1, 310–317.</ref><ref name="rogers1967" /><ref name="moschovakis2010" />.
-'''证明中 SRT 的关键一步'''：想把任意 r.e. 集 B 归约到创造集 A，需要构造一个程序 <math>z</math>，使得"若 <math>x\in B</math>，则 <math>z</math> 枚举出<math>\{u(z)\}</math>；否则 <math>z</math> 枚举空集"——'''<math>z</math> 的定义里用到了 <math>z</math> 自己的编号'''（<math>u(z)</math> 是生产反例的程序作用于 <math>z</math>）。这正是 SRT 合法化的自指；没有这个自指，证明无法闭合。由此 Rogers 还得到推论：'''所有创造集在"可计算的重新命名"意义下完全相同（两两递归同构）'''——从可计算性角度看它们"长得一模一样"<ref name="rogers1967" />。
+'''证明中用到了 SRT 的关键一步'''：想把任意 r.e. 集 B 归约到创造集 A，需要构造一个程序 <math>z</math>，使得"若 <math>x\in B</math>，则 <math>z</math> 枚举出<math>\{u(z)\}</math>；否则 <math>z</math> 枚举空集"——'''<math>z</math> 的定义里用到了 <math>z</math> 自己的编号'''（<math>u(z)</math> 是生产反例的程序作用于 <math>z</math>）。这正是 SRT 合法化的自指；没有这个自指，证明无法闭合。由此 Rogers 还得到推论：'''所有创造集在"可计算的重新命名"意义下完全相同（两两递归同构）'''——从可计算性角度看它们"长得一模一样"<ref name="rogers1967" />。
 ==== 有效运算的连续性：Myhill–Shepherdson 与 KLS–Čeĭnin 定理 ====

@@ 第641行： / 第641行： @@
   '''"You need a number z? You got it!"（你需要一个这样的数 z？给你！）'''<ref name="moschovakis2010" />
-==== 通用序数记号系统ω_1^{CK}====
+==== 通用序数记号系统ω_1^CK====
 这是 SRT '''最初的'''应用（见 [[#起源：一篇研究"序数记号"的 6 页短文|3.1]]）。回顾[[#起源：一篇研究"序数记号"的 6 页短文|§3.1]] 的背景：[[序数记号系统]]给可数序数指派自然数代号，使得 0 / 后继 / 极限这三种构建可以被机械地（可计算的）判定，前驱与[[柯西序列|基本序列]]都可被机械地（计算地）取出。在进入定理之前，我们先把本节反复用到的几个概念交代清楚（"序数"本身的背景见 [[#起源：一篇研究"序数记号"的 6 页短文|§3.1]] 的背景框）：

@@ 第580行： / 第580行： @@
 * 证明：取 <math>\theta(v)</math> = "<math>v</math> 不可证"，由不动点引理得 <math>\sigma\iff\text{"}\sigma\text{不可证"}</math>。若<math>\sigma</math> 可证，则它说的是真话（我不可证），矛盾；若 <math>\neg\sigma</math> 可证，则"<math>\sigma</math> 可证"，又矛盾。于是 <math>\sigma</math> 与 <math>\neg\sigma</math> 都不可证——不完备定理成立。把 <math>\theta</math> 换成 [[J. Barkley Rosser|Rosser]] 的精巧变体，还能去掉"<math>\omega</math>-一致性"这个额外假设，得到 [[Rosser 强化]]<ref name="godel1931" /><ref name="moschovakis2010" />。
-* '''[[Myhill定理]]（1955）'''：[[罗宾逊算术]] Q 的任何一致、可公理化扩张 <math>T</math>，其定理集都是'''[[创造集]]'''（见 [[#Myhill定理：创造集 = 完备集|§5.8.5.3]]），从而是 r.e.-完备的<ref name="moschovakis2010" />.
+* '''[[Myhill定理]]（1955）'''：[[罗宾逊算术]] Q 的任何一致、可公理化扩张 <math>T</math>，其定理集都是'''[[创造集]]'''（见 [[#Myhill定理：创造集 = 完备集|§5.8.5.2]]），从而是 r.e.-完备的<ref name="moschovakis2010" />.
 合起来我们可以得到一个惊人结论：所有足够强的一致公理化理论（[[皮亚诺算术]]、[[ZFC公理系统]]<math>\ldots\ldots</math>）都自动满足不动点引理的条件，因而都不完备、不可判定；而且任意两个这样的理论，其定理集在递归同构意义下完全相同<ref name="moschovakis2010" />。
@@ 第737行： / 第737行： @@
 可判定、可枚举这类词只能作用于自然数集合，索引集正是那道翻译层——它把"程序行为问题"转写成 <math>\mathbb{N}</math> 的子集，之后才能问"这个性质能判定吗、能枚举吗"。两个要点：其一，此类性质必须'''只看行为、不看代码'''（同一函数的两个不同编号在 A 中必须同真同假），否则退化为平凡的代码分析。
-与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 [[#Myhill定理：创造集 = 完备集|5.8.5.3]]）。
+与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 [[#Myhill定理：创造集 = 完备集|5.8.5.2]]）。
 ===== [[Rice定理]]（1951） =====

←上一版本		2026年9月18日 (五) 02:34的版本
第751行：		第751行：

	'''注（SRT 捷径，非本质）'''：[[莱斯定理\|Rice 定理]]也可用 SRT 三行证完：设 <math>A</math> 可计算，取变换规则 <math>f(x) =</math>"<math>x\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 <math>m</math> 使 <math>\phi_m = \phi_{f(m)}</math>。若 <math>m\in A</math>，则 <math>f(m)\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；<math>m\notin A</math> 同理。这条证明虽短，却是'''事后捷径'''——它没有揭示 Rice 定理与停机问题的血缘，而后者（上面的归约）才是定理的标准证明与本质机制<ref name="rogers1967" />。		'''注（SRT 捷径，非本质）'''：[[莱斯定理\|Rice 定理]]也可用 SRT 三行证完：设 <math>A</math> 可计算，取变换规则 <math>f(x) =</math>"<math>x\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 <math>m</math> 使 <math>\phi_m = \phi_{f(m)}</math>。若 <math>m\in A</math>，则 <math>f(m)\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；<math>m\notin A</math> 同理。这条证明虽短，却是'''事后捷径'''——它没有揭示 Rice 定理与停机问题的血缘，而后者（上面的归约）才是定理的标准证明与本质机制<ref name="rogers1967" />。
−
−	~~===== Rice-Shapiro 定理（1956） =====~~
−
−	Rice 定理回答"'''能否'''判定"；[[莱斯-夏皮罗定理\|Rice-Shapiro 定理]]进一步刻画"'''何时能半判定'''"——把注意力从"A 是否可计算"收窄到"A 自身何时是 r.e. 的"：
−
−	设 <math>A = \{ e :W_e \in \mathcal{A}\}</math> 是索引集。<math>A</math> 是 r.e. 的，'''当且仅当''' <math>\mathcal{A}</math> 是"有限可生成"的：存在一个可计算列举的有限集列 <math>\mathcal{S} = \{S_0,S_1,S_2,\ldots</math>}，使得 <math>W\in \mathcal{A}</math> ⟺ <math>\mathcal{S}</math>中存在某个 <math>S_i \subseteq W</math>。
−
−	含义：一个行为性质若能'''被枚举地识别'''（索引集 r.e.），它就必须由'''有限证据'''决定——W 一旦包含某个预列的有限集 <math>S_i</math>，性质即成立；反之，性质成立也只需某个有限子集作证。"能识别 ⟹ 只依赖有限信息"这一半是紧致性式的论证（若性质的成立只靠无限多证据，枚举过程就永远等不到决定性的一刻）；"有限可生成 ⟹ 可枚举"那一半是直接列举。两个方向都与 SRT 无关。
−
−	Rice-Shapiro 不是 SRT 的推论，而是索引集理论中独立的结构定理，并且它比 Rice 定理更强——由它可以推出 Rice 定理：若非平凡索引集 A 可计算，则 A 与补集都是 r.e. 索引集，Rice-Shapiro 给 <math>\mathcal{A}</math> 与其补类都套上"有限可生成"；而有限可生成自动蕴含"超集仍在类中"，把两个类里各自的成员并起来，就得到同时属于两类的一个 r.e. 集，矛盾。可见在"识别程序性质"的问题上，真正的母定理是 Rice-Shapiro 而非 SRT<ref name="rogers1967" /><ref name="soare1987" />。

	===== [[Myhill定理]]：[[创造集]] = [[完备集]] =====		===== [[Myhill定理]]：[[创造集]] = [[完备集]] =====

@@ 第741行： / 第741行： @@
 ===== [[Rice定理]]（1951） =====
-'''[[Rice定理|莱斯定理]]'''：程序行为的任何'''非平凡'''性质都不可判定。精确地说：设 <math>\mathcal{A}</math> 是某类部分可计算函数，既非空也非全体，则它的索引集 <math>A = \{ e : \phi_e \in \mathcal{A}\}</math> 不是可计算集（更不是递归集）。
+'''[[Rice定理|莱斯(Rice)定理]]'''：程序行为的任何'''非平凡'''性质都不可判定。精确地说：设 <math>\mathcal{A}</math> 是某类部分可计算函数，既非空也非全体，则它的索引集 <math>A = \{ e : \phi_e \in \mathcal{A}\}</math> 不是可计算集（更不是递归集）。
 * '''证明思路（停机归约——教科书标准路线，不依赖 SRT）'''：
@@ 第750行： / 第750行： @@
 * 直觉：任何非平凡的"行为分类"都把停机问题吸收为自己内部的一个子问题——你若想机械地给每个程序的行为贴标签，就不得不先回答"程序 <math>x</math> 停在自己身上吗"，而那正是不可判定的对角线问题<ref name="rice1953">'''Rice, H. G. (1953).''' Classes of recursively enumerable sets and their decision problems. ''Transactions of the AMS'', 74, 358–366.【Rice 定理原始论文】【§[[#通用序数记号系统与|5.8.5.1]]】</ref>.
-'''注（SRT 捷径，非本质）'''：[[莱斯定理|Rice 定理]]也可用 SRT 三行证完：设 <math>A</math> 可计算，取变换规则 <math>f(x) = "x <math>\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 <math>m</math> 使 <math>\phi_m = \phi_{f(m)}</math>。若 <math>m\in A</math>，则 <math>f(m)\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；<math>m\notin A</math> 同理。这条证明虽短，却是'''事后捷径'''——它没有揭示 Rice 定理与停机问题的血缘，而后者（上面的归约）才是定理的标准证明与本质机制<ref name="rogers1967" />。
+'''注（SRT 捷径，非本质）'''：[[莱斯定理|Rice 定理]]也可用 SRT 三行证完：设 <math>A</math> 可计算，取变换规则 <math>f(x) =</math>"<math>x\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 <math>m</math> 使 <math>\phi_m = \phi_{f(m)}</math>。若 <math>m\in A</math>，则 <math>f(m)\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；<math>m\notin A</math> 同理。这条证明虽短，却是'''事后捷径'''——它没有揭示 Rice 定理与停机问题的血缘，而后者（上面的归约）才是定理的标准证明与本质机制<ref name="rogers1967" />。
 ===== Rice-Shapiro 定理（1956） =====

@@ 第713行： / 第713行： @@
 ==== 超算术集与有效描述集合论 ====
-'''背景'''：在自然数的集合（数学分析的对象）上，可以用"[[二阶量词]]"分层：<math>\Sigma^1_1</math> 集是"存在一个实数使得某个可计算性质成立"的集合（由[[存在量词]]定义的集合），<math>\Pi^1_1</math> 是其对偶（由二阶的[[全称量词]]定义的集合），<math>\Delta^1_1 = \Sigma^1_1 \cap \Pi^1_1</math> 是"两面都可定义"的集合——可类比为[[分析学]]中"既可开逼近又可闭逼近"的集合。
+'''背景'''：在自然数的集合（数学分析的对象）上，可以用"[[二阶量词]]"分层：<math>\Sigma^1_1</math> 集是"存在一个实数使得某个可计算性质成立"的集合（由[[存在量词]]构成的命题定义的集合），<math>\Pi^1_1</math> 是其对偶（由二阶的[[全称量词]]构成的命题定义的集合），<math>\Delta^1_1 = \Sigma^1_1 \cap \Pi^1_1</math> 是"两面都可定义"的集合——可类比为[[分析学]]中"既可开逼近又可闭逼近"的集合。
 * '''Kleene 定理（1955）'''：自然数的集合 A 是 <math>\Delta^1_1</math> 的，当且仅当 A 是[[超算术]]的（HYP）<ref name="kleene1955">Kleene, S. C. (1955). On the forms of the predicates in the theory of constructive ordinals (second paper). ''American Journal of Mathematics'', 77, 405–428.【<math>\Delta^1_1</math> = 超算术集合（HYP）的原始定理出处（§[[#超算术集与有效描述集合论|5.8.4]]）】</ref><ref name="moschovakis2010" />。
-这把可计算性理论（HYP，由机器和序数定义）与[[描述集合论]]（<math>\Delta^1_1</math>，由投影/量化定义）两大传统焊接在一起，是 Kleene 获 1983 年 AMS Steele 奖的核心成果之一。证明的两个引理（[[Kleene's O]] 是 <math>\Pi^1_1</math> 集、且是 <math>\Pi^1_1</math> 中"最复杂"的完备集）都靠 SRT 沿良基树作[[有效超限递归]]建立<ref name="moschovakis2010" />.
+这把可计算性理论（HYP，由机器和序数定义）与[[描述集合论]]（<math>\Delta^1_1</math>，由投影/量化定义）两大传统焊接在一起，是 Kleene 获 1983 年 [[AMS Steele奖]]的核心成果之一。证明的两个引理（[[Kleene's O]] 是 <math>\Pi^1_1</math> 集、且是 <math>\Pi^1_1</math> 中"最复杂"的完备集）都靠 SRT 沿良基树作[[有效超限递归]]建立<ref name="moschovakis2010" />.
 在此基础上，SRT 向实数空间（[[贝尔空间|Baire 空间]]，即自然数无穷序列的空间）推广后，成为'''[[有效描述集合论]]'''的引擎，三个代表性结果：
-# '''[[Suslin–Kleene定理]]'''：[[博雷尔集|Borel 集]]（从开集出发经可数次并、交、补生成的集合）与 <math>\Delta^1_1</math> 集之间可以可计算地互译。它同时蕴含经典 [[米哈伊尔·苏斯林|Suslin]] 定理（<math>\Delta^1_1 = Borel</math>）和上述 Kleene 定理，是两大传统的汇合点<ref name="moschovakis2010" />；
+# '''[[Suslin–Kleene定理]]'''：[[博雷尔集|Borel 集]]（从开集出发经可数次并、交、补生成的集合）与 <math>\Delta^1_1</math> 集之间可以可计算地互译。它同时蕴含经典 [[Suslin定理]]（<math>\Delta^1_1 = Borel</math>）和上述 Kleene 定理，是两大传统的汇合点<ref name="moschovakis2010" />；
-# '''[[赋范归纳定理]]'''（Moschovakis 1974）：对带有良好"秩函数"结构的归纳定义，其最小/最大不动点保持在相应的可定义层级内。它的证明使用"关系版 SRT"（不动点代码 <math>\varepsilon</math>* 使自己的每个后继元组都由自己的前段定义）。这可视为对 Kleene 1944 年错误（见 [[#一个值得铭记的教训|3.3]]）的"正确打开方式"：SRT 只给某个不动点，要拿到'''最小'''不动点需要额外的秩结构<ref name="moschovakis2010" />；
+# '''[[赋范归纳定理]]'''（Moschovakis 1974）：对带有良好"[[秩函数]]"结构的归纳定义，其最小/最大不动点保持在相应的可定义层级内。它的证明使用"关系版 SRT"（不动点代码 <math>\varepsilon</math>* 使自己的每个后继元组都由自己的前段定义）。这可视为对 Kleene 1944 年错误（见 [[#一个值得铭记的教训|3.3]]）的"正确打开方式"：SRT 只给某个不动点，要拿到'''最小'''不动点需要额外的秩结构<ref name="moschovakis2010" />；
-# '''[[编码引理]]'''（Moschovakis 1970）：在 ZF+DC+AD（确定性公理，一个与大[[基数]]理论相关的集合论假设）下，若[[连续统]]可满射到基数 <math>\kappa</math>，则可满射到 <math>\kappa</math> 的幂集。证明通过'''带参数的 SRT'''作有效超限递归——SRT 由此进入基数算术这一纯集合论领域；它还是 '''[[Jackson 定理]]'''（1989：在 AD 下，三型存在量词的 Kleene 序数恰好等于'''最小的弱不可达基数'''）的基本工具——这是连接高类型递归论与大基数理论的最惊人结果之一<ref name="moschovakis2010" />。
+# '''[[编码引理]]'''（Moschovakis 1970）：在 ZF+DC+AD（确定性公理，一个与大[[基数]]理论相关的集合论假设）下，若[[连续统]]可满射到[[基数]] <math>\kappa</math>，则可满射到 <math>\kappa</math> 的幂集。证明通过'''带参数的 SRT'''作有效超限递归——SRT 由此进入基数算术这一纯集合论领域；它还是 '''[[Jackson 定理]]'''（1989：在 AD 下，三型存在量词的 Kleene 序数恰好等于'''最小的弱不可达基数'''）的基本工具——这是连接高类型递归论与大基数理论的最惊人结果之一<ref name="moschovakis2010" />。
 此外，Kleene 1940 年代为直觉主义数学（拒绝排中律的构造性数学）构造的'''可实现性（realizability）'''中，[[bar递归定义]]、[[bar归纳]]与[[连续性原理]]的验证也本质地使用 SRT 的各种形式<ref name="moschovakis2010" />。