3,094
个编辑
更改
无编辑摘要
两条之中，第二递归定理尤为重要，它是数学中对[[自指]]（self-reference）现象最简洁、最有力的统一陈述：它只有一步对角线证明 `<math>c = S(e, e)</math>`（<math>S</math> 是"把程序的部分输入写死、生成新程序"的[[柯里化操作]]，详见 §2.3），却统一了从[[罗素悖论]]（1901）、[[Gödel不完备定理]]（1931）、[[Turing停机问题]]（1936）、[[von Neumann 自复制自动机]]（1948）到今天的[[Quine程序]]（1960s）等全部自指现象——它们本质上是同一种对角线/自指结构的不同化身（详 §5.7）。
两条之中，第二递归定理尤为重要，它是数学中对[[自指]]（self-reference）现象最简洁、最有力的统一陈述：它只有一步对角线证明 `<math>c = S(e, e)</math>`（<math>S</math> 是"把程序的部分输入写死、生成新程序"的[[柯里化操作]]，详见 §2.3），却统一了从[[罗素悖论]]（1901）、[[Gödel不完备定理]]（1931）、[[Turing停机问题]]（1936）、[[von Neumann 自复制自动机]]（1948）到今天的[[Quine程序]]（1960s）等全部自指现象——它们本质上是同一种对角线/自指结构的不同化身（详 §5.7）。
[[文件:自指家族.png|替代=自指家族|缩略图|图1：六个经典自指现象——[[Cantor对角线]]（1891）、[[Russell悖论]]（1901）、[[Gödel不完备定理]]（1931）、[[Turing停机问题]]（1936）、[[von Neumann自复制]]（1948）、[[Quine]]（[[自打印程序]]，1960s）——都源于同一种对角线/自指原理；Kleene 第二递归定理是这一原理最一般的陈述。]]
[[文件:自指家族.png|替代=自指家族|缩略图|图1：六个经典自指现象——[[Cantor对角线]]（1891）、[[Russell悖论]]（1901）、[[Gödel不完备定理]]（1931）、[[Turing停机问题]]（1936）、[[von Neumann自复制]]（1948）、[[Quine]]（[[自打印程序]]，1960s）——都源于同一种对角线/自指原理；Kleene 第二递归定理是这一原理最一般的陈述。]]
== 总览：两个定理各说了什么 ==
== 总览：两个定理各说了什么 ==
|}
|}
![两种[[不动点]]](figures/fig3_two_fixedpoints.png)
'''图2'''：两个定理的"不动点"含义截然不同——左：函数 <math>\phi</math> 经变换 <math>\Psi</math> 后变回 <math>\phi</math>（函数层面）；右：程序 n 经变换 f 后变成另一个程序 f(n)（通常 f(n) <math>\neq n</math>），但 <math>\phi_n = \phi_{f(n)}</math>（'''代码变了，行为不变'''）。§2.5 对此有详细辨析。
'''图2'''：两个定理的"不动点"含义截然不同——左：函数 <math>\phi</math> 经变换 <math>\Psi</math> 后变回 <math>\phi</math>（函数层面）；右：程序 n 经变换 f 后变成另一个程序 f(n)（通常 f(n) <math>\neq n</math>），但 <math>\phi_n = \phi_{f(n)}</math>（'''代码变了，行为不变'''）。§2.5 对此有详细辨析。
第二递归定理被 Moschovakis 称为 '''"令人惊叹的"（amazing）'''——他的综述标题就叫 ''Kleene's Amazing Second Recursion Theorem''<ref name="moschovakis2010" />；计算机科学家 Neil Jones 称之为'''"可计算性的瑞士军刀"（A Swiss Pocket Knife for Computability）'''〔转引自 Kiselyov, §1〕。它的一行证明看似只是个小技巧，却支撑了从 Gödel 不完备定理到序数理论、从程序自复制到有效描述集合论的庞大理论大厦（详见第五、六节）。
第二递归定理被 [[Yiannis N. Moschovakis|Moschovakis]] 称为 '''"令人惊叹的"（amazing）'''——他的综述标题就叫 ''Kleene's Amazing Second Recursion Theorem''<ref name="moschovakis2010" />；计算机科学家 Neil Jones 称之为'''"可计算性的瑞士军刀"（A Swiss Pocket Knife for Computability）'''〔转引自 Kiselyov, §1〕。它的一行证明看似只是个小技巧，却支撑了从 [[哥德尔|Gödel]] 不完备定理到[[序数]]理论、从程序自复制到有效[[描述集合论]]的庞大理论大厦（详见第五、六节）。
---
---
=== 通用程序（解释器） ===
=== 通用程序（解释器） ===
存在一台"通用机器"：给它输入 (e, x)，它就'''模拟'''编号 e 的程序在输入 x 上的运行。这就是今天的'''解释器 / 虚拟机'''思想，Turing 1936 年的通用图灵机是它的首个化身。用记号写就是：存在程序 i 使得 <math>\phi_i(e, x) = \phi_e(x)</math>。<ref name="rogers1967" />
存在一台"通用机器"：给它输入 (e, x)，它就'''模拟'''编号 e 的程序在输入 x 上的运行。这就是今天的'''解释器 / 虚拟机'''思想，Turing 1936 年的[[通用图灵机]]是它的首个化身。用记号写就是：存在程序 i 使得 <math>\phi_i(e, x) = \phi_e(x)</math>。<ref name="rogers1967" />
=== S-m-n 定理（柯里化 / 参数特化） ===
=== S-m-n 定理（柯里化 / 参数特化） ===
"不动点"在本文中出现于两个截然不同的层面，混淆它们是最常见的理解障碍：
"不动点"在本文中出现于两个截然不同的层面，混淆它们是最常见的理解障碍：
- '''函数层面的不动点'''（第一递归定理）：变换规则 <math>\Psi</math> 把函数 <math>\phi</math> 变成新函数 <math>\Psi(\phi)</math>；若 <math>\Psi(\phi) = \phi</math>（作为函数处处相等），<math>\phi</math> 就是 <math>\Psi</math> 的不动点。这与分析学中"f(x) = x 的解"同类。
- '''函数层面的不动点'''（[[#第一递归定理（FRT）|第一递归定理]]）：变换规则 <math>\Psi</math> 把函数 <math>\phi</math> 变成新函数 <math>\Psi(\phi)</math>；若 <math>\Psi(\phi) = \phi</math>（作为函数处处相等），<math>\phi</math> 就是 <math>\Psi</math> 的不动点。这与分析学中"f(x) = x 的解"同类。
- '''代码层面的不动点'''（第二递归定理）：变换规则 f 把程序编号 n 变成新编号 f(n)；'''注意 f(n) <math>\neq n</math> 通常成立'''——程序代码确实变了；但神奇的是，新程序 f(n) 和旧程序 n '''计算的函数相同'''：<math>\phi_n = \phi_{f(n)}</math>。所以"不动"的不是代码，而是'''代码的行为'''。Rogers 为此特意造了"'''不动点值'''（fixed-point value）"一词，强调它不是数值不动点<ref name="rogers1967" />。
- '''代码层面的不动点'''（第二递归定理）：变换规则 f 把程序编号 n 变成新编号 f(n)；'''注意 f(n) <math>\neq n</math> 通常成立'''——程序代码确实变了；但神奇的是，新程序 f(n) 和旧程序 n '''计算的函数相同'''：<math>\phi_n = \phi_{f(n)}</math>。所以"不动"的不是代码，而是'''代码的行为'''。[[Hartley Rogers, Jr|Rogers]] 为此特意造了"'''不动点值'''（fixed-point value）"一词，强调它不是数值不动点<ref name="rogers1967" />。
---
---
> Church 与 Kleene 在 1930 年代问了一个构造性问题：'''能不能给每个可数序数起一个"机械可读的代号"（自然数编码），使得仅凭代号就能机械地判断：这个序数是 0、是某个序数的后继（+1）、还是某个递增序列的极限？并且在后两种情况下能机械地取出前驱代号或序列代号？''' 满足这些条件的编码方案称为一个'''序数记号系统'''（Kleene 称之为 r-system）<ref name="kleene1938" />。
> Church 与 Kleene 在 1930 年代问了一个构造性问题：'''能不能给每个可数序数起一个"机械可读的代号"（自然数编码），使得仅凭代号就能机械地判断：这个序数是 0、是某个序数的后继（+1）、还是某个递增序列的极限？并且在后两种情况下能机械地取出前驱代号或序列代号？''' 满足这些条件的编码方案称为一个'''序数记号系统'''（Kleene 称之为 r-system）<ref name="kleene1938" />。
Kleene 在论文 §2 中建立了可计算函数的基本技术（编号、通用函数、§2.3 的 S 函数），然后在 §2 的最后'''顺手'''陈述并证明了一个当时没有名字的定理<ref name="kleene1938" />：
Kleene 在论文 §2 中建立了[[可计算函数]]的基本技术（编号、通用函数、§2.3 的 S 函数），然后在 §2 的最后'''顺手'''陈述并证明了一个当时没有名字的定理<ref name="kleene1938" />：
> '''若 <math>\psi(z, x)</math> 是任意可计算的部分函数，则存在一个数 f，使得 <math>\phi_f(x) = \psi(f, x)</math> 对所有 x 成立（等号含义：两边同时无定义，或同时有定义且相等）。'''
> '''若 <math>\psi(z, x)</math> 是任意可计算的部分函数，则存在一个数 f，使得 <math>\phi_f(x) = \psi(f, x)</math> 对所有 x 成立（等号含义：两边同时无定义，或同时有定义且相等）。'''
——这就是'''第二递归定理'''的原始形态。Moschovakis 称之为 Kleene 没有意识到自己发掘出的'''"小宝石"（little gem）'''<ref name="moschovakis2010" />；Kiselyov 则以"'''函数式珍珠'''（A Functional Pearl）"为题向函数式编程社区重新发掘了它<ref name="kiselyov" />。
——这就是'''第二递归定理'''的原始形态。Moschovakis 称之为 Kleene 没有意识到自己发掘出的'''"小宝石"（little gem）'''<ref name="moschovakis2010" />；Kiselyov 则以"'''函数式珍珠'''（A Functional Pearl）"为题向函数式编程社区重新发掘了它<ref name="kiselyov" />。
这个"小宝石"随即在论文 §3 被用于证明该文的主要结果：'''存在一个"通用"序数记号系统 <math>S_1</math>'''——任何其他合法记号系统能命名的序数，<math>S_1</math> 都能命名，且翻译过程本身是可计算的<ref name="kleene1938" />。这是"沿着序数逐层向上做递归定义"（后来称为'''有效超限递归'''，effective transfinite recursion）这一方法的首次应用。Kleene 由此构造出著名的'''记号系统 O（Kleene's O）'''，并证明存在最小的一个"不可命名"的序数——'''Church–Kleene 序数 <math>\omega_1^CK</math>'''，即可数序数中第一个无法被任何机械记号系统触及的序数<ref name="kleene1938" /><ref name="rogers1967" />。
这个"小宝石"随即在论文 §3 被用于证明该文的主要结果：'''存在一个"通用"序数记号系统 <math>S_1</math>'''——任何其他合法记号系统能命名的序数，<math>S_1</math> 都能命名，且翻译过程本身是可计算的<ref name="kleene1938" />。这是"沿着序数逐层向上做递归定义"（后来称为'''有效超限递归'''，effective transfinite recursion）这一方法的首次应用。Kleene 由此构造出著名的'''记号系统 O（Kleene's O）'''，并证明存在最小的一个"不可命名"的序数——'''Church–Kleene 序数 <math>\omega_1^CK</math>'''，即[[序数|可数序数]]中第一个无法被任何机械记号系统触及的序数<ref name="kleene1938" /><ref name="rogers1967" />。
=== 命名史 ===
=== 命名史 ===
=== 意义：递归定义的"存在性定理" ===
=== 意义：递归定义的"存在性定理" ===
第一递归定理的角色，类似于分析学中用[[不动点定理]]（如 Banach 压缩映像原理）证明微分方程'''解的存在性'''：它一劳永逸地保证"机械式递归定义必有可计算的解"，从此定义递归函数时无需逐个证明合法性。Rogers 指出，"递归定理"这个名字正来源于此——它是"解递归方程"的定理，类比[[集合论]]中沿序数递归定义函数的原理<ref name="rogers1967" />。Kleene 本人甚至把第一递归定理视为支持 '''Church–Turing 论题'''（"可计算 = 递归/图灵可计算"这一哲学论题）的最强证据之一：它表明"可计算函数"这个类恰好封闭于最一般的机械递归定义方式之下，不多也不少<ref name="moschovakis2010" />。
数学血统上，它是 '''Knaster–Tarski 不动点定理'''（序理论中"完备格上的单调映射必有不动点"）在"可计算"约束下的有效化版本<ref name="rogers1967" />。
数学血统上，它是 '''Knaster–Tarski 不动点定理'''（[[序理论]]中"[[完备格]]上的[[单调映射]]必有不动点"）在"可计算"约束下的有效化版本<ref name="rogers1967" />。
=== 与第二递归定理的关系 ===
=== 与第二递归定理的关系 ===
>
>
> - '''§5.2.1 Smullyan 双递归定理'''——SRT 的"联立化"推广：一次造出两个互相引用对方代码的程序（可推广到 k 个），是后续许多构造的通用工具；
> - '''§5.2.1 Smullyan 双递归定理'''——SRT 的"联立化"推广：一次造出两个互相引用对方代码的程序（可推广到 k 个），是后续许多构造的通用工具；
> - '''§5.2.2 Rogers 同构定理'''——SRT 的"编号独立性"推论：任意两个通用程序枚举之间必有保结构的可计算同构；
> - '''§5.2.2 Rogers 同构定理'''——SRT 的"编号[[独立性 (数学)|独立性]]"推论：任意两个[[通用图灵机|通用程序]]枚举之间必有保结构的可计算同构；
> - '''§5.2.3 Arslanov 完全性判据'''——相对化 SRT 的"刻画性"等价定理：一个 r.e. 集何时是 r.e.-完备的。
> - '''§5.2.3 Arslanov 完全性判据'''——相对化 SRT 的"刻画性"等价定理：一个 r.e. 集何时是 r.e.-完备的。
>
>
> 常被误归为 SRT 推论的 '''Rice 定理'''与 '''Rice-Shapiro 定理'''不在此列：Rice 的教科书证明是停机归约（对角线矛盾），Rice-Shapiro 是"有限可生成"的结构定理，两者都不依赖 SRT（SRT 至多为 Rice 提供一条事后捷径）。它们属于 r.e. '''索引集理论'''，与 SRT 的关系是"同源，但独立"——因此移至 §6.5，与真正依赖 SRT 的 Myhill 定理并置，以对照这两种不同关系。
> 常被误归为 SRT 推论的 '''Rice 定理'''与 '''Rice-Shapiro 定理'''不在此列：Rice 的教科书证明是停机[[归约 (数学)]]（对角线矛盾），Rice-Shapiro 是"有限可生成"的结构定理，两者都不依赖 SRT（SRT 至多为 Rice 提供一条事后捷径）。它们属于 r.e. '''索引集理论'''，与 SRT 的关系是"同源，但独立"——因此移至 §6.5，与真正依赖 SRT 的 [[#Myhill 定理：创造集 = 完备集|Myhill 定理]]并置，以对照这两种不同关系。
==== Smullyan 双递归定理（1959, 1961） ====
==== Smullyan 双递归定理（1959, 1961） ====
推广到 k 元：对任意 k 个全可计算函数 <math>g_1</math>, <math>\ldots</math>, <math>g_k</math>，存在 k 个程序 <math>m_1</math>, <math>\ldots</math>, <math>m_k</math> 使得 <math>\phi_{m_i}(x) = g_i(\langle m_1, \ldots, m_k\rangle, x)</math>。
推广到 k 元：对任意 k 个全可计算函数 <math>g_1</math>, <math>\ldots</math>, <math>g_k</math>，存在 k 个程序 <math>m_1</math>, <math>\ldots</math>, <math>m_k</math> 使得 <math>\phi_{m_i}(x) = g_i(\langle m_1, \ldots, m_k\rangle, x)</math>。
[[#Smullyan 双递归定理（1959, 1961）|双递归定理]]是后续许多重要构造的核心：① §6.3 介绍的"两层超算术构造"里，[[克利福德·斯佩克特|Spector]] 定理需要同时构造两个互相缠绕的函数；②Myhill-Shepherdson 定理（§6.6 简述）描述"如何用 r.e. 集作为其它 r.e. 集的有效操作"时也需要联立不动点；③某些停机问题的"相对化"证明也走双递归路线。<ref name="smullyan1961" /><ref name="rogers1967" />
==== Rogers 同构定理（1958） ====
==== Rogers 同构定理（1958） ====
直觉上：两个不同的程序编号系统乍看像不同的语言（一个把 quine 编号成 42，另一个编号成 100），但实质上说的是同一类对象；Rogers 定理说它们之间必有可计算的"翻译词典"，且词典严格保结构。
直觉上：两个不同的程序编号系统乍看像不同的语言（一个把 quine 编号成 42，另一个编号成 100），但实质上说的是同一类对象；Rogers 定理说它们之间必有可计算的"翻译词典"，且词典严格保结构。
证明思路：把"取 f(c) = 在另一编号系统下对应于 c 的程序编号"作为变换规则，对它套 SRT 得到不动点 c——c 就是翻译词典的种子；之后逐条验证它保 <math>\phi</math>、W 等价性。Rogers 同构定理常被引用作"程序编号系统的选择不影响可计算性理论"的根据——你可以挑任何合理的编号方式，得出的可计算性结论都一样。<ref name="rogers1967" />
证明思路：把"取 f(c) = 在另一编号系统下对应于 c 的程序编号"作为变换规则，对它套 SRT 得到不动点 c——c 就是翻译词典的种子；之后逐条验证它保 <math>\phi</math>、W 等价性。[[#Rogers 同构定理（1958）|Rogers 同构定理]]常被引用作"程序编号系统的选择不影响可计算性理论"的根据——你可以挑任何合理的编号方式，得出的可计算性结论都一样。<ref name="rogers1967" />
==== Arslanov 完全性判据（1981） ====
==== Arslanov 完全性判据（1981） ====
这里一下子出现了三个新名字，先逐个解释：
这里一下子出现了三个新名字，先逐个解释：
- '''r.e. 集合'''：见 §2.4。本词条统一用缩写 r.e.（recursively enumerable，递归可枚举）。
- '''r.e. 集合'''：见 §2.4。本词条统一用缩写 r.e.（recursively enumerable，[[递归可枚举集|递归可枚举]]）。
- '''r.e.-完全'''：r.e. 集合这个"复杂度类别"里"最硬核"的一档——任何别的 r.e. 集合 W 都能机械地归约到 C，判定"W 含 x"等价于"问 C"。
- '''r.e.-完全'''：r.e. 集合这个"复杂度类别"里"最硬核"的一档——任何别的 r.e. 集合 W 都能机械地归约到 C，判定"W 含 x"等价于"问 C"。
- '''Turing 归约 / W <math>\leq_T C</math> via <math>f_W</math>'''：A 能 '''Turing 归约'''到 B（记 A <math>\leq_T B</math>），意思是"只要允许把 B 当'''神谕机（oracle，下一条解释）'''——可以向它提任意多个 yes/no 问题并瞬时得到回答——A 就能被判定"。等式 W <math>\leq_T C</math> via <math>f_W</math> 即"编排提问方式的过程由可计算函数 <math>f_W</math> 给出，它把 x 改写成若干个向 C 的查询并综合出答案"。
- '''Turing 归约 / W <math>\leq_T C</math> via <math>f_W</math>'''：A 能 '''Turing 归约'''到 B（记 A <math>\leq_T B</math>），意思是"只要允许把 B 当'''神谕机（oracle，下一条解释）'''——可以向它提任意多个 yes/no 问题并瞬时得到回答——A 就能被判定"。等式 W <math>\leq_T C</math> via <math>f_W</math> 即"编排提问方式的过程由可计算函数 <math>f_W</math> 给出，它把 x 改写成若干个向 C 的查询并综合出答案"。
直觉上：[[R. R. Arslanov|Arslanov]] 判据说"装得下所有 r.e. 集合"等价于"对每个 r.e. 集合都有机械的相对化方式"——这和 SRT 中"对每个全可计算 f 都给出一个不动点"的相对化版本（relativized SRT）说的是同一件事：SRT 的相对化是说"对每个以 C 为'''神谕'''（oracle）可计算的 f，存在不动点 c"；Arslanov 判据说"对每个 W，存在以 C 为[[谕示机|神谕]]可计算的归约"。
Arslanov 判据在递归论里是教科书级工具：①用于证明 Gödel 不完备定理的算术陈述（"PA 不一致"这种陈述）的相对可计算性与停机问题同构；② 用于证明某些 r.e. 集"不可能被简化"。<ref name="arslanov1981" /><ref name="soare1987" />
Arslanov 判据在递归论里是教科书级工具：①用于证明 Gödel 不完备定理的算术陈述（"PA 不一致"这种陈述）的相对可计算性与停机问题同构；② 用于证明某些 r.e. 集"不可能被简化"。<ref name="arslanov1981" /><ref name="soare1987" />
> <math>\phi_f(x) = \phi_{S(e,e)}(x) = \phi_e(e, x) = \psi(S(e,e), x) = \psi(f, x)</math> ∎
> <math>\phi_f(x) = \phi_{S(e,e)}(x) = \phi_e(e, x) = \psi(S(e,e), x) = \psi(f, x)</math> ∎
第一步是 f 的定义；第二步是柯里化的定义（S(e,e) 就是"把 e 的第一个输入写死为 e"）；第三步是 e 的定义；第四步再回到 f 的定义。'''唯一实质操作是第三步前那个自应用 S(e,e)：让程序 e 作用于自己的编号。''' 这就是对角线方法——与 Cantor 证明实数不可数、Gödel 构造"本句不可证"、Turing 证明停机问题不可解是同一种技术。<ref name="kleene1938" /><ref name="rogers1967" />
第一步是 f 的定义；第二步是柯里化的定义（S(e,e) 就是"把 e 的第一个输入写死为 e"）；第三步是 e 的定义；第四步再回到 f 的定义。'''唯一实质操作是第三步前那个自应用 S(e,e)：让程序 e 作用于自己的编号。''' 这就是[[对角线论证|对角线方法]]——与 Cantor 证明实数不可数、Gödel 构造"本句不可证"、Turing 证明停机问题不可解是同一种技术。<ref name="kleene1938" /><ref name="rogers1967" />
==== 列表法（Cutland 1980）：把"对角线"画成一张表 ====
==== 列表法（Cutland 1980）：把"对角线"画成一张表 ====
上面的一行证明把对角线方法压缩到了极致——好处是直接，坏处是看不出"对角线"长什么样。Cutland 在《Computability》§2.3 (Theorem 2.3) 给出过一种更直观的'''列表法'''证明，'''用一张"行 = 枚举、列 = 位置"的二维表，把"对角线"和"沿对角线的循环"都画在纸面上'''。三步走。
上面的一行证明把对角线方法压缩到了极致——好处是直接，坏处是看不出"对角线"长什么样。[[奈杰尔·卡特兰|Cutland]] 在《Computability》§2.3 (Theorem 2.3) 给出过一种更直观的'''列表法'''证明，'''用一张"行 = 枚举、列 = 位置"的二维表，把"对角线"和"沿对角线的循环"都画在纸面上'''。三步走。
'''1. 把"所有可计算函数的枚举"摆成一张表'''
'''1. 把"所有可计算函数的枚举"摆成一张表'''
<math>\lambda</math> 演算（Church 1930 年代发明的、Lisp 等函数式语言的祖先）中有一个著名对象 '''Y 组合子'''：对任何函数 F，YF = F(YF)，即 Y 直接生产出 F 的不动点，纯函数式地实现递归——它让匿名函数也能"引用自己"。
<math>\lambda</math> 演算（Church 1930 年代发明的、Lisp 等函数式语言的祖先）中有一个著名对象 '''Y 组合子'''：对任何函数 F，YF = F(YF)，即 Y 直接生产出 F 的不动点，纯函数式地实现递归——它让匿名函数也能"引用自己"。
Kiselyov 在'''分阶段 <math>\lambda</math> 演算'''（staged lambda-calculus，区分"代码"与"值"两个阶段的现代元编程框架）中重构了第二递归定理，得出一个漂亮的结论：'''第二递归定理就是 Y 组合子的"带代码"推广'''——Y 组合子给出函数层面的不动点，SRT 给出"程序 + 自身代码"层面的不动点；当把"代码"取为平凡编码（程序即自身）时，SRT 的构造精确退化为 Y 组合子。<ref name="kiselyov" />
Kiselyov 在'''分阶段 <math>\lambda</math> 演算'''（staged lambda-calculus，区分"代码"与"值"两个阶段的现代元编程框架）中重构了第二递归定理，得出一个漂亮的结论：'''第二递归定理就是 Y 组合子的"带代码"推广'''——[[Y组合子]]给出函数层面的不动点，SRT 给出"程序 + 自身代码"层面的不动点；当把"代码"取为平凡编码（程序即自身）时，SRT 的构造精确退化为 Y 组合子。<ref name="kiselyov" />
这一视角澄清了 SRT 对计算机科学的意义：'''它陈述的是"任何合理的程序系统对自指构造封闭"，是把高阶操作（程序变换）降阶到数据层面（编号）的不动点原理'''——部分求值（partial evaluation）、编译器自举（bootstrapping）、宏系统的理论基础。
这一视角澄清了 SRT 对计算机科学的意义：'''它陈述的是"任何合理的程序系统对自指构造封闭"，是把高阶操作（程序变换）降阶到数据层面（编号）的不动点原理'''——部分求值（partial evaluation）、编译器自举（bootstrapping）、宏系统的理论基础。
=== 与其它不动点定理的关系 ===
=== 与其它不动点定理的关系 ===
SRT 衍生出许多重要推论（见 §5.2），但还有些定理与 SRT 的关系'''更微妙'''——它们与 SRT '''同源'''（都基于对角线 / 自指），却走的是独立证明路线，或者处于更高层的范畴论概括下。这里集中讨论两个最重要的"不动点定理"：Gödel 的不动点引理与 Lawvere 的范畴论不动点定理，重点说明 SRT 与它们的精确定位关系。
SRT 衍生出许多重要推论（见 §5.2），但还有些定理与 SRT 的关系'''更微妙'''——它们与 SRT '''同源'''（都基于对角线 / 自指），却走的是独立证明路线，或者处于更高层的[[范畴论]]概括下。这里集中讨论两个最重要的"不动点定理"：Gödel 的[[不动点引理]]与 [[F. William Lawvere|Lawvere]] 的范畴论不动点定理，重点说明 SRT 与它们的精确定位关系。
==== Gödel 不动点引理（对角引理） ====
==== Gödel 不动点引理（对角引理） ====
对任何包含足够算术的递归可公理化理论 T，对 T 中任何公式 <math>\phi(x)</math>，都存在一个"不动点句子"<math>\psi</math>，使得 T 证 <math>\psi</math> ↔ <math>\phi</math>(⌜<math>\psi</math>⌝)。它的证明手法（对角线替换）与 SRT 同源，但 Gödel 早在 1931 年就独立给出了完整论证，'''SRT 推不出 Gödel 自身的不完备定理'''——Gödel 不完备的全部内容（一致性、<math>\omega</math>-一致性、不可判定性三层）见 §5.7.4 的详述。
对任何包含足够算术的递归可公理化理论 T，对 T 中任何公式 <math>\phi(x)</math>，都存在一个"不动点句子"<math>\psi</math>，使得 T 证 <math>\psi</math> ↔ <math>\phi</math>(⌜<math>\psi</math>⌝)。它的证明手法（对角线替换）与 SRT 同源，但 Gödel 早在 1931 年就独立给出了完整论证，'''SRT 推不出 Gödel 自身的不完备定理'''——Gödel 不完备的全部内容（一致性、<math>\omega</math>-一致性、不[[可判定性]]三层）见 §5.7.4 的详述。
注：'''Gödel 不动点引理本身是 SRT 最干净、最纯粹的推论'''（既可以把 SRT 当证明工具来证它，也可以两边都用"自指 + 对角线"的同源手法独立证明）。它和 SRT 的关系是"同源、互为推论"；但 Gödel 不完备'''定理'''与 SRT 的关系另当别论，见 §5.7.4 的"双重身份"分析。
注：'''Gödel 不动点引理本身是 SRT 最干净、最纯粹的推论'''（既可以把 SRT 当证明工具来证它，也可以两边都用"自指 + 对角线"的同源手法独立证明）。它和 SRT 的关系是"同源、互为推论"；但 Gödel 不完备'''定理'''与 SRT 的关系另当别论，见 §5.7.4 的"双重身份"分析。
这一定理是 SRT 所在的整个"对角线 / 自指"现象的'''范畴论统一视角'''。它告诉我们：SRT 不是孤立的递归论怪事，而是任何"足够自指的计算系统"都会涌现出的通用结构。下面先用范畴论语言表述，再讲清它和 SRT 的接口。
这一定理是 SRT 所在的整个"对角线 / 自指"现象的'''范畴论统一视角'''。它告诉我们：SRT 不是孤立的递归论怪事，而是任何"足够自指的计算系统"都会涌现出的通用结构。下面先用范畴论语言表述，再讲清它和 SRT 的接口。
'''Lawvere 定理（标准陈述）'''：设 '''C''' 是一个 ''Cartesian 闭范畴''（Cartesian closed category，"对象 = 数据类型、态射 = 数据类型间可计算变换、函数空间本身也是对象、可以反复变换"的信息世界）。设 '''F: C <math>\to C</math>''' 是一个函子（"世界内部的一种自我变换"）。如果存在一个'''满射态射'''（surjective morphism，形象地说"覆盖了 F(A) 的全部出口"）
'''Lawvere 定理（标准陈述）'''：设 '''C''' 是一个 ''Cartesian 闭范畴''（Cartesian closed category，"对象 = 数据类型、[[态射]] = 数据类型间可计算变换、函数空间本身也是对象、可以反复变换"的信息世界）。设 '''F: C <math>\to C</math>''' 是一个[[函子]]（"世界内部的一种自我变换"）。如果存在一个'''满射态射'''（surjective morphism，形象地说"覆盖了 F(A) 的全部出口"）
> f: A <math>\to F(A)</math> （每个 F(A) 元素都被 f 的像源元素覆写）
> f: A <math>\to F(A)</math> （每个 F(A) 元素都被 f 的像源元素覆写）
即顺着"A <math>\to F(A) \to A</math>"这条回路绕一圈，既可以按 g 走、也可以按 F(x) 走，'''两条路径等价'''。
即顺着"A <math>\to F(A) \to A</math>"这条回路绕一圈，既可以按 g 走、也可以按 F(x) 走，'''两条路径等价'''。
'''直观解读'''：所谓"自指世界"，就是那种'''函数空间可以作为自身参数来研究'''的地方（Cartesian 闭）。在这种世界里，只要有一个"程序能撞出比自己更复杂的结果"的接口（满射态射），'''任何"全局选择函数"（g）都必有不动物'''——你的 g 想要把世界再次变换回自己，总会撞到某个无法再造新东西的点（x），而那个点正好让变换等于"再变换一次"（F(x) = g）。"自我引用 <math>\to </math>不动点"在这种世界里是不可避免的结构——不论那世界是自然数 + 可计算函数（Turing、Kleene），还是形式系统 + 可证性（Gödel），还是集合论宇宙（Russell、Cantor）。
'''直观解读'''：所谓"自指世界"，就是那种'''函数空间可以作为自身参数来研究'''的地方（Cartesian 闭）。在这种世界里，只要有一个"程序能撞出比自己更复杂的结果"的接口（[[满射]]态射），'''任何"全局选择函数"（g）都必有不动物'''——你的 g 想要把世界再次变换回自己，总会撞到某个无法再造新东西的点（x），而那个点正好让变换等于"再变换一次"（F(x) = g）。"自我引用 <math>\to </math>不动点"在这种世界里是不可避免的结构——不论那世界是自然数 + 可计算函数（Turing、Kleene），还是形式系统 + 可证性（Gödel），还是集合论宇宙（Russell、Cantor）。
'''SRT 是 Lawvere 的特例'''：把上述抽象框架特殊化到可计算函数的世界，就回到 SRT。具体的接口是：
'''SRT 是 Lawvere 的特例'''：把上述抽象框架特殊化到可计算函数的世界，就回到 SRT。具体的接口是：
'''关系定性'''：
'''关系定性'''：
- Lawvere 不动点定理'''不是''' SRT 的"推论"（该定理没有反推 SRT，而是反过来把 SRT 概括出来）；
- [[#Lawvere 不动点定理（1969）|Lawvere 不动点定理]]'''不是''' SRT 的"推论"（该定理没有反推 SRT，而是反过来把 SRT 概括出来）；
- Lawvere 也不仅是 SRT 的"更高层次表述"（它是数学基础层面的定理，把 SRT、Gödel 不动点引理、Turing 停机问题的不可判定性、Russell 悖论、Cantor 对角线'''全部统一为这一个抽象结构的不同时面'''）；
- Lawvere 也不仅是 SRT 的"更高层次表述"（它是数学基础层面的定理，把 SRT、[[#Gödel 不动点引理（对角引理）|Gödel 不动点引理]]、Turing 停机问题的不可判定性、Russell 悖论、Cantor 对角线'''全部统一为这一个抽象结构的不同时面'''）；
- 因此在写作时应避免两种过度描述：①"Lawvere 推翻了 SRT 的独立性"（错，它们不在一个抽象层）；②"SRT 是 Lawvere 的特例，所以 SRT 的定理就是 Lawvere 给出来的"（错，Lawvere 是更高层的解释，不是 SRT 证明的工具；SRT 证明仍然是 §5.3 的对角线论证）。
- 因此在写作时应避免两种过度描述：①"Lawvere 推翻了 SRT 的独立性"（错，它们不在一个抽象层）；②"SRT 是 Lawvere 的特例，所以 SRT 的定理就是 Lawvere 给出来的"（错，Lawvere 是更高层的解释，不是 SRT 证明的工具；SRT 证明仍然是 §5.3 的[[对角线论证]]）。
'''对读者的现实意义'''：如果你做的是程序语义、形式化验证、自指系统、AI 反思架构等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容。<ref name="lawvere1969" />
'''对读者的现实意义'''：如果你做的是程序语义、形式化验证、自指系统、AI 反思架构等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容。<ref name="lawvere1969" />
==== Gödel 第一不完备定理（1931） ====
==== Gödel 第一不完备定理（1931） ====
'''现象'''：任何"足够强"的一致可公理化理论 T（例如 Peano 算术 PA）都不完备：存在一个句子 <math>\sigma</math>，使 T 既证不出 <math>\sigma</math>、也证不出 <math>\neg</math><math>\sigma</math>。<ref name="godel1931" />
'''现象'''：任何"足够强"的一致可公理化理论 T（例如 [[皮亚诺公理|Peano 算术]] PA）都不完备：存在一个句子 <math>\sigma</math>，使 T 既证不出 <math>\sigma</math>、也证不出 <math>\neg</math><math>\sigma</math>。<ref name="godel1931" />
'''术语——PA 与 Q'''：'''PA''' 是 '''Peano 算术（Peano Arithmetic）'''的缩写，是'''一阶算术的标准公理系统'''，用于形式化刻画自然数（0, 1, 2, <math>\ldots</math>）及其加法、乘法。它由意大利数学家 G. Peano（1889）的公理发展而来，包含：①常元 0；②后继运算 S（每个数有唯一后继，0 不是任何数的后继，后继相同则原数相同）；③加法、乘法的递归定义；④'''归纳公理模式'''（induction schema：对任何一阶公式 <math>\phi</math>，若 <math>\phi(0)</math> 成立、且 <math>\phi(n) \Rightarrow \phi(n+1)</math>，则 <math>\phi</math> 对一切自然数成立）。PA 是 Gödel 不完备定理的典型对象——它足够强（能在内部编码所有初等数论），又是可公理化的一致理论。而 '''Q（Robinson 算术）'''是 PA 的一个'''弱化'''：保留①—③、去掉归纳公理模式，只留极有限的几条公理，是"足以推出不完备定理的最弱理论"之一（后文 Myhill 定理即用它）。
'''术语——PA 与 Q'''：'''PA''' 是 '''Peano 算术（Peano Arithmetic）'''的缩写，是'''一阶算术的标准公理系统'''，用于形式化刻画自然数（0, 1, 2, <math>\ldots</math>）及其加法、乘法。它由意大利数学家 G. Peano（1889）的公理发展而来，包含：①常元 0；②后继运算 S（每个数有唯一后继，0 不是任何数的后继，后继相同则原数相同）；③加法、乘法的递归定义；④'''归纳公理模式'''（induction schema：对任何一阶公式 <math>\phi</math>，若 <math>\phi(0)</math> 成立、且 <math>\phi(n) \Rightarrow \phi(n+1)</math>，则 <math>\phi</math> 对一切自然数成立）。PA 是 Gödel 不完备定理的典型对象——它足够强（能在内部编码所有初等数论），又是可公理化的一致理论。而 '''Q（Robinson 算术）'''是 PA 的一个'''弱化'''：保留①—③、去掉归纳公理模式，只留极有限的几条公理，是"足以推出不完备定理的最弱理论"之一（后文 Myhill 定理即用它）。
> '''不动点引理'''：设 T 是任何足够强的可公理化理论，则对任何含一个自由变量的公式 <math>\theta(v)</math>，都存在句子 <math>\sigma</math>，使 T 可证 "<math>\sigma</math> ↔ <math>\theta</math>(⌜<math>\sigma</math>⌝)"（⌜<math>\sigma</math>⌝ 是 <math>\sigma</math> 的哥德尔数）。即：'''任何性质 <math>\theta</math>，都存在一个句子 <math>\sigma</math>，在 T 可证的意义下恰好谈论"自己是否具有 <math>\theta</math>"。'''<ref name="moschovakis2010" />
> '''不动点引理'''：设 T 是任何足够强的可公理化理论，则对任何含一个自由变量的公式 <math>\theta(v)</math>，都存在句子 <math>\sigma</math>，使 T 可证 "<math>\sigma</math> ↔ <math>\theta</math>(⌜<math>\sigma</math>⌝)"（⌜<math>\sigma</math>⌝ 是 <math>\sigma</math> 的哥德尔数）。即：'''任何性质 <math>\theta</math>，都存在一个句子 <math>\sigma</math>，在 T 可证的意义下恰好谈论"自己是否具有 <math>\theta</math>"。'''<ref name="moschovakis2010" />
证明：取 <math>\theta(v)</math> = "v 不可证"，由不动点引理得 <math>\sigma</math> ↔ "<math>\sigma</math> 不可证"。若 <math>\sigma</math> 可证，则它说的是真话（我不可证），矛盾；若 <math>\neg</math><math>\sigma</math> 可证，则"<math>\sigma</math> 可证"，又矛盾。于是 <math>\sigma</math> 与 <math>\neg</math><math>\sigma</math> 都不可证——第一不完备定理成立。把 <math>\theta</math> 换成 Rosser 的精巧变体，还能去掉"<math>\omega</math>-一致性"这个额外假设，得到 '''Rosser 强化'''。<ref name="godel1931" /><ref name="moschovakis2010" />
证明：取 <math>\theta(v)</math> = "v 不可证"，由不动点引理得 <math>\sigma</math> ↔ "<math>\sigma</math> 不可证"。若 <math>\sigma</math> 可证，则它说的是真话（我不可证），矛盾；若 <math>\neg</math><math>\sigma</math> 可证，则"<math>\sigma</math> 可证"，又矛盾。于是 <math>\sigma</math> 与 <math>\neg</math><math>\sigma</math> 都不可证——第一不完备定理成立。把 <math>\theta</math> 换成 [[J. Barkley Rosser|Rosser]] 的精巧变体，还能去掉"<math>\omega</math>-一致性"这个额外假设，得到 '''Rosser 强化'''。<ref name="godel1931" /><ref name="moschovakis2010" />
> '''Myhill 定理（1955）'''：Robinson 算术 Q 的任何一致、可公理化扩张 T，其定理集都是'''创造集'''（见 §6.5.3），从而是 r.e.-完备的。<ref name="moschovakis2010" />
> '''Myhill 定理（1955）'''：[[罗宾逊算术]] Q 的任何一致、可公理化扩张 T，其定理集都是'''创造集'''（见 §6.5.3），从而是 r.e.-完备的。<ref name="moschovakis2010" />
合起来得到一个惊人结论：'''所有'''足够强的一致公理化理论（PA、ZFC<math>\ldots</math><math>\ldots</math>）都自动满足不动点引理的条件，因而都不完备、不可判定；而且任意两个这样的理论，其定理集在递归同构意义下完全相同。<ref name="moschovakis2010" />
合起来得到一个惊人结论：'''所有'''足够强的一致公理化理论（PA、[[ZFC公理系统]]<math>\ldots</math><math>\ldots</math>）都自动满足不动点引理的条件，因而都不完备、不可判定；而且任意两个这样的理论，其定理集在递归同构意义下完全相同。<ref name="moschovakis2010" />
Rogers 还讨论过一个反向的自指：可以构造一个公理系统，其中包含'''断言自身一致性'''的句子（对任何公理集 <math>W_p</math>，存在 n 使 <math>W_n = W_p</math> <math>\cup </math>{⌜<math>W_n</math> 一致⌝}）。但 Gödel '''第二'''不完备定理说明：若 <math>W_p</math> 已含 PA，这个"自信"的系统反而不可能一致。<ref name="rogers1967" />
Rogers 还讨论过一个反向的自指：可以构造一个公理系统，其中包含'''断言自身一致性'''的句子（对任何公理集 <math>W_p</math>，存在 n 使 <math>W_n = W_p</math> <math>\cup </math>{⌜<math>W_n</math> 一致⌝}）。但 Gödel '''第二'''不完备定理说明：若 <math>W_p</math> 已含 PA，这个"自信"的系统反而不可能一致。<ref name="rogers1967" />
'''SRT 如何推出它'''：
'''SRT 如何推出它'''：
> '''定理（自复制图灵机）'''：存在一台图灵机，从空白纸带出发，停机时纸带上恰好写着'''它自己的完整描述（转移表）'''。<ref name="moschovakis2010" />
> '''定理（自复制图灵机）'''：存在一台[[图灵机]]，从空白纸带出发，停机时纸带上恰好写着'''它自己的完整描述（转移表）'''。<ref name="moschovakis2010" />
证明是 SRT 的典型用法：定义 <math>\psi(z)</math> = "把编号 z 的机器的描述打印出来"——一个完全机械、与"谁被打印"无关的变换。SRT 给出不动点 f：程序 f 的行为 = 打印 f 自己的描述。循环凭空闭合。
证明是 SRT 的典型用法：定义 <math>\psi(z)</math> = "把编号 z 的机器的描述打印出来"——一个完全机械、与"谁被打印"无关的变换。SRT 给出不动点 f：程序 f 的行为 = 打印 f 自己的描述。循环凭空闭合。
==== Quine（自打印程序） ====
==== Quine（自打印程序） ====
'''现象'''：一个'''不接受任何输入、只打印出自己源代码副本'''的程序。<ref name="wikipedia_quine_computing" />。它的约束很苛刻——'''不能读自己的源码'''（靠读文件输出自己、如 `cat $0`，被视为"作弊"，不算 quine），只能靠"代码部分 + 代表代码文本的数据部分"来构造性地打印自己；§5.4 例 1 的 Python 程序就是一个标准 quine。"quine" 一词由 Hofstadter 在《哥德尔、艾舍尔、巴赫》中普及（借自哲学家 W. V. O. Quine 的名字，他构造过自指的句子）<ref name="hofstadter1979" />。
'''现象'''：一个'''不接受任何输入、只打印出自己源代码副本'''的程序。<ref name="wikipedia_quine_computing" />。它的约束很苛刻——'''不能读自己的源码'''（靠读文件输出自己、如 `cat $0`，被视为"作弊"，不算 quine），只能靠"代码部分 + 代表代码文本的数据部分"来构造性地打印自己；§5.4 例 1 的 Python 程序就是一个标准 quine。"quine" 一词由 [[侯世达|Hofstadter]] 在《哥德尔、艾舍尔、巴赫》中普及（借自哲学家 W. V. O. Quine 的名字，他构造过自指的句子）<ref name="hofstadter1979" />。
'''SRT 如何推出它'''：把 SRT 里的变换规则 f 直接定义为'''"打印"程序'''——f(c) = "打印出 c 的源码的那个程序"。套用 SRT（<math>\phi_c = \phi_{f(c)}</math>）得到不动点 c：
'''SRT 如何推出它'''：把 SRT 里的变换规则 f 直接定义为'''"打印"程序'''——f(c) = "打印出 c 的源码的那个程序"。套用 SRT（<math>\phi_c = \phi_{f(c)}</math>）得到不动点 c：
=== 沿序数逐层构造之一：通用序数记号系统与 \omega_1^CK ===
=== 沿序数逐层构造之一：通用序数记号系统与 \omega_1^CK ===
这是 SRT '''最初的'''应用（见 3.1）。回顾§3.1 的背景：序数记号系统给可数序数指派自然数代号，使得 0 / 后继 / 极限三分可机械判定、前驱与基本序列可机械取出。在进入定理之前，先把本节反复用到的几个概念交代清楚（"序数"本身的背景见 §3.1 的背景框）：
这是 SRT '''最初的'''应用（见 3.1）。回顾§3.1 的背景：[[序数记号系统]]给可数序数指派自然数代号，使得 0 / 后继 / 极限三分可机械判定、前驱与[[柯西序列|基本序列]]可机械取出。在进入定理之前，先把本节反复用到的几个概念交代清楚（"序数"本身的背景见 §3.1 的背景框）：
- '''代号与所指'''：记号系统里的每个自然数 a 都是一个'''代号'''，它所指的序数记作 |a|。一个序数 <math>\alpha</math> 的'''后继'''（successor）就是 <math>\alpha+1</math>（0 的后继是 1，<math>\omega</math> 的后继是 <math>\omega+1</math>）。'''极限序数'''（limit ordinal，下文统记作 <math>\lambda</math>）则是既非 0 也非任何序数之后继的序数——它不能靠"+1"走到，只能被一列递增的序数"逼近"，最典型的例子是 <math>\omega</math>（0, 1, 2, 3, <math>\ldots</math> 无限数完之后的那一步：任何自然数都不是它的"前一个"）。
- '''代号与所指'''：记号系统里的每个自然数 a 都是一个'''代号'''，它所指的序数记作 |a|。一个序数 <math>\alpha</math> 的'''后继'''（successor）就是 <math>\alpha+1</math>（0 的后继是 1，<math>\omega</math> 的后继是 <math>\omega+1</math>）。'''极限序数'''（limit ordinal，下文统记作 <math>\lambda</math>）则是既非 0 也非任何序数之后继的序数——它不能靠"+1"走到，只能被一列递增的序数"逼近"，最典型的例子是 <math>\omega</math>（0, 1, 2, 3, <math>\ldots</math> 无限数完之后的那一步：任何自然数都不是它的"前一个"）。
顺带分辨两行的差异：第二行 <math>\psi(x) = 2^\psi(P(x))</math> 是'''值依赖值'''的循环，且 P(x) 指向更小的序数，本质上是良基的（"良基"：不存在无穷下降链，所以"沿序数从小到大做归纳"是合法的）；第三行则是'''编号依赖编号'''的循环（e 的代码里嵌着 <math>\psi</math> 的编号），良基性救不了它——必须 SRT。
顺带分辨两行的差异：第二行 <math>\psi(x) = 2^\psi(P(x))</math> 是'''值依赖值'''的循环，且 P(x) 指向更小的序数，本质上是良基的（"良基"：不存在无穷下降链，所以"沿序数从小到大做归纳"是合法的）；第三行则是'''编号依赖编号'''的循环（e 的代码里嵌着 <math>\psi</math> 的编号），良基性救不了它——必须 SRT。
在 <math>S_1</math> 的基础上，Kleene 进一步构造了带树状偏序的'''序数记号系统 O（Kleene's O）'''——"偏序"（partial order）指只在部分代号对之间定义的"小于"关系（O 中记作 <O，反映所指序数的大小）。O 是通用且极大的：每个可被任何合法记号系统命名的序数（称为'''构造序数'''，constructive ordinal）在 O 中都有代号。全体构造序数的上确界（supremum：不小于它们中任何一个的最小序数）
在 <math>S_1</math> 的基础上，Kleene 进一步构造了带树状[[偏序关系]]的'''序数记号系统 O（Kleene's O）'''——"偏序"（partial order）指只在部分代号对之间定义的"小于"关系（O 中记作 <O，反映所指序数的大小）。O 是通用且极大的：每个可被任何合法记号系统命名的序数（称为'''构造序数'''，constructive ordinal）在 O 中都有代号。全体[[递归序数|构造序数]]的[[上确界]]（supremum：不小于它们中任何一个的最小序数）
> '''<math>\omega_1^CK</math> = 最小的非构造序数（Church–Kleene 序数）'''
> '''<math>\omega_1^CK</math> = 最小的非构造序数（Church–Kleene 序数）'''
问题来了：同一序数 <math>\alpha</math> 在系统中有'''无穷多个代号'''，用不同代号构造出的 <math>H_\alpha</math> 会不会不同？
问题来了：同一序数 <math>\alpha</math> 在系统中有'''无穷多个代号'''，用不同代号构造出的 <math>H_\alpha</math> 会不会不同？
'''图5'''：Kleene 记号系统 O 的树状结构示意。每个自然数都是某个序数的代号——规则：|1| = 0（最底层）；|2^x| = |x| + 1（后继，沿着"2 的幂"链向上）；|3<math>\cdot5^e</math>| = li<math>m_n</math> |<math>\phi_e(n)</math>|（'''极限'''——'''记号里携带基本序列程序的编号 e，这正是 SRT 大显身手的地方'''）。所有构造序数都在这棵树上生长；树顶是 <math>\omega_1^CK</math>（无法被任何机械记号触及的边界）。
'''图5'''：[[Kleene's O|Kleene 记号系统 O]] 的树状结构示意。每个自然数都是某个序数的代号——规则：|1| = 0（最底层）；|2^x| = |x| + 1（后继，沿着"2 的幂"链向上）；|3<math>\cdot5^e</math>| = li<math>m_n</math> |<math>\phi_e(n)</math>|（'''极限'''——'''记号里携带基本序列程序的编号 e，这正是 SRT 大显身手的地方'''）。所有构造序数都在这棵树上生长；树顶是 <math>\omega_1^CK</math>（无法被任何机械记号触及的边界）。
Kiselyov 以现代眼光补充了这段历史的思想动机：Kleene 放弃用 <math>\lambda</math> 项（他与 Church 两年前的方案）做序数代号，正是因为 <math>\lambda</math> 项作为'''函数'''无法被机械地比较大小；极限序数的代号必须携带'''程序的编号'''而非函数本身——"只有编号（有穷对象）才能被直接给出，这是有穷主义立场的要求"<ref name="kleene1938" /><ref name="kiselyov" />。
Kiselyov 以现代眼光补充了这段历史的思想动机：Kleene 放弃用 <math>\lambda</math> 项（他与 Church 两年前的方案）做序数代号，正是因为 <math>\lambda</math> 项作为'''函数'''无法被机械地比较大小；极限序数的代号必须携带'''程序的编号'''而非函数本身——"只有编号（有穷对象）才能被直接给出，这是有穷主义立场的要求"<ref name="kleene1938" /><ref name="kiselyov" />。
可数序数有两种自然刻画："'''构造序数'''"（能被某个机械记号系统命名，见 6.1）与"'''递归序数'''"（某个可计算良序的长度——即存在一个可计算的大小关系，把一堆自然数排成该长度的"无限队列"）。
可数序数有两种自然刻画："'''构造序数'''"（能被某个机械记号系统命名，见 6.1）与"'''递归序数'''"（某个可计算良序的长度——即存在一个可计算的大小关系，把一堆自然数排成该长度的"无限队列"）。
> '''Markwald–Spector 定理（1954/1955）'''：两种刻画恰好等价——构造序数 ⟺ 递归序数。<ref name="rogers1967" /><ref name="moschovakis2010" />
> '''Markwald–Spector 定理（1954/1955）'''：两种刻画恰好等价——构造序数 ⟺ [[递归序数]]。<ref name="rogers1967" /><ref name="moschovakis2010" />
这是经典集合论事实"第二数类的两种刻画等价"的可计算版本；两个方向的证明都以 SRT 为归纳枢纽。<ref name="moschovakis2010" />
这是经典集合论事实"第二数类的两种刻画等价"的可计算版本；两个方向的证明都以 SRT 为归纳枢纽。<ref name="moschovakis2010" />
> <math>H_\lambda = \cup</math>ₙ <math>H_{\lambdaₙ}</math> （极限层：把下面各层沿一条可计算上升的序列 <math>\lambda_0 < \lambda_1 < \lambda_2 < \ldots</math> 并起来——'''沿哪条序列取并由 <math>\lambda</math> 的代号给出'''，6.1 里"记号携带程序编号"的约定在此派上用场）
> <math>H_\lambda = \cup</math>ₙ <math>H_{\lambdaₙ}</math> （极限层：把下面各层沿一条可计算上升的序列 <math>\lambda_0 < \lambda_1 < \lambda_2 < \ldots</math> 并起来——'''沿哪条序列取并由 <math>\lambda</math> 的代号给出'''，6.1 里"记号携带程序编号"的约定在此派上用场）
在某一层 <math>H_\alpha</math> 中可计算的集合，称为'''超算术的（hyperarithmetical, HYP）'''。这栋楼的前几层串起熟悉的图景：'''只盖有穷多层，得到的恰好是通常的算术层级'''——穷尽一阶算术（量词只作用于自然数）可定义的全部集合；盖到第 <math>\omega</math> 层（<math>\omega</math> 即 6.1 中最小的无穷序数），得到的集合已足以一举判定 PA （皮亚诺公理体系）的全部真语句——包括所有 PA 证明不了的真命题（对照 5.7.4 的不完备性）；而楼并不停在这里，它沿构造序数一直盖到 <math>\omega_1^CK</math> 为止。HYP 因此是真正高于算术层级的层级——至于它究竟高到哪一步（恰好等价于一个"二阶量词"的定义能力），正是 6.4 的主题。<ref name="moschovakis2010" />
在某一层 <math>H_\alpha</math> 中可计算的集合，称为'''超算术的（hyperarithmetical, HYP）'''。这栋楼的前几层串起熟悉的图景：'''只盖有穷多层，得到的恰好是通常的算术层级'''——穷尽一阶算术（量词只作用于自然数）可定义的全部集合；盖到第 <math>\omega</math> 层（<math>\omega</math> 即 6.1 中最小的无穷序数），得到的集合已足以一举判定 PA （[[皮亚诺公理]]体系）的全部真语句——包括所有 PA 证明不了的真命题（对照 5.7.4 的不完备性）；而楼并不停在这里，它沿构造序数一直盖到 <math>\omega_1^CK</math> 为止。HYP 因此是真正高于算术层级的层级——至于它究竟高到哪一步（恰好等价于一个"二阶量词"的定义能力），正是 6.4 的主题。<ref name="moschovakis2010" />
问题来了：同一序数 <math>\alpha</math> 在系统中有'''无穷多个代号'''，用不同代号构造出的 <math>H_\alpha</math> 会不会不同？
问题来了：同一序数 <math>\alpha</math> 在系统中有'''无穷多个代号'''，用不同代号构造出的 <math>H_\alpha</math> 会不会不同？
> '''Spector 唯一性定理（1955）'''：不会。<math>H_\alpha</math> 的可计算度只依赖序数 <math>\alpha</math> 本身，与代号选择无关；而且不同代号之间的翻译是一致可计算的。<ref name="spector1955" /><ref name="moschovakis2010" />
> '''Spector 唯一性定理（1955）'''：不会。<math>H_\alpha</math> 的可计算度只依赖序数 <math>\alpha</math> 本身，与代号选择无关；而且不同代号之间的翻译是一致可计算的。<ref name="spector1955" /><ref name="moschovakis2010" />
证明需要同时构造'''两个互相缠绕的函数'''（互相引用对方编号），由双递归定理（见 §5.2 的 Smullyan 版本）合法化——这是有效超限递归技术的高峰之一。Kleene 对这个学生的工作推崇备至，他常讲自己如何"行为不端"地接受它作为博士论文、又作为期刊编辑指定自己为审稿人并立即录用——"非常不合规矩，但我认为最终有利于逻辑！"<ref name="moschovakis2010" />
证明需要同时构造'''两个互相缠绕的函数'''（互相引用对方编号），由双递归定理（见 §5.2 的 [[雷蒙德·斯穆里安|Smullyan]] 版本）合法化——这是有效超限递归技术的高峰之一。Kleene 对这个学生的工作推崇备至，他常讲自己如何"行为不端"地接受它作为博士论文、又作为期刊编辑指定自己为审稿人并立即录用——"非常不合规矩，但我认为最终有利于逻辑！"<ref name="moschovakis2010" />
=== 沿序数逐层构造之四：HYP = \Delta^1_1 与有效描述集合论 ===
=== 沿序数逐层构造之四：HYP = \Delta^1_1 与有效描述集合论 ===
> '''Kleene 定理（1955）'''：自然数的集合 A 是 <math>\Delta^1_1</math> 的，当且仅当 A 是超算术的（HYP）。<ref name="kleene1955" /><ref name="moschovakis2010" />
> '''Kleene 定理（1955）'''：自然数的集合 A 是 <math>\Delta^1_1</math> 的，当且仅当 A 是超算术的（HYP）。<ref name="kleene1955" /><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 空间，即自然数无穷序列的空间）推广后，成为'''有效描述集合论'''的引擎，三个代表性结果：
在此基础上，SRT 向实数空间（[[贝尔空间|Baire 空间]]，即自然数无穷序列的空间）推广后，成为'''有效描述集合论'''的引擎，三个代表性结果：
1. '''Suslin–Kleene 定理'''：Borel 集（从开集出发经可数次并、交、补生成的集合）与 <math>\Delta^1_1</math> 集之间可以可计算地互译。它同时蕴含经典 Suslin 定理（<math>\Delta^1_1 = Borel</math>）和上述 Kleene 定理，是两大传统的汇合点<ref name="moschovakis2010" />；
1. '''Suslin–Kleene 定理'''：[[博雷尔集|Borel 集]]（从开集出发经可数次并、交、补生成的集合）与 <math>\Delta^1_1</math> 集之间可以可计算地互译。它同时蕴含经典 [[米哈伊尔·苏斯林|Suslin]] 定理（<math>\Delta^1_1 = Borel</math>）和上述 Kleene 定理，是两大传统的汇合点<ref name="moschovakis2010" />；
2. '''赋范归纳定理'''（Moschovakis 1974）：对带有良好"秩函数"结构的归纳定义，其最小/最大不动点保持在相应的可定义层级内。它的证明使用"关系版 SRT"（不动点代码 <math>\varepsilon</math>* 使自己的每个后继元组都由自己的前段定义）。这可视为对 Kleene 1944 年错误（见 3.3）的"正确打开方式"：SRT 只给某个不动点，要拿到'''最小'''不动点需要额外的秩结构<ref name="moschovakis2010" />；
2. '''赋范归纳定理'''（Moschovakis 1974）：对带有良好"秩函数"结构的归纳定义，其最小/最大不动点保持在相应的可定义层级内。它的证明使用"关系版 SRT"（不动点代码 <math>\varepsilon</math>* 使自己的每个后继元组都由自己的前段定义）。这可视为对 Kleene 1944 年错误（见 3.3）的"正确打开方式"：SRT 只给某个不动点，要拿到'''最小'''不动点需要额外的秩结构<ref name="moschovakis2010" />；
3. '''编码引理'''（Moschovakis 1970）：在 ZF+DC+'''AD'''（确定性公理，一个与大基数理论相关的集合论假设）下，若连续统可满射到基数 <math>\kappa</math>，则可满射到 <math>\kappa</math> 的幂集。证明通过'''带参数的 SRT'''作有效超限递归——SRT 由此进入基数算术这一纯集合论领域；它还是 '''Jackson 定理'''（1989：在 AD 下，三型存在量词的 Kleene 序数恰好等于'''最小的弱不可达基数'''）的基本工具——这是连接高类型递归论与大基数理论的最惊人结果之一<ref name="moschovakis2010" />。
3. '''编码引理'''（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" />。
此外，Kleene 1940 年代为直觉主义数学（拒绝排中律的构造性数学）构造的'''可实现性（realizability）'''解释中，bar 递归定义、bar 归纳与连续性原理的验证也本质地使用 SRT 的各种形式<ref name="moschovakis2010" />。
直觉：任何非平凡的"行为分类"都把停机问题吸收为自己内部的一个子问题——你若想机械地给每个程序的行为贴标签，就不得不先回答"程序 x 停在自己身上吗"，而那正是不可判定的对角线问题。<ref name="rice1953" />
直觉：任何非平凡的"行为分类"都把停机问题吸收为自己内部的一个子问题——你若想机械地给每个程序的行为贴标签，就不得不先回答"程序 x 停在自己身上吗"，而那正是不可判定的对角线问题。<ref name="rice1953" />
> '''注（SRT 捷径，非本质）'''：Rice 定理也可用 SRT 三行证完：设 A 可计算，取变换规则 f(x) = "x <math>\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 m 使 <math>\phi_m = \phi_{f(m)}</math>。若 m <math>\in A</math>，则 f(m) <math>\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；m <math>\notin A</math> 同理。这条证明虽短，却是'''事后捷径'''——它没有揭示 Rice 定理与停机问题的血缘，而后者（上面的归约）才是定理的标准证明与本质机制。<ref name="rogers1967" />
> '''注（SRT 捷径，非本质）'''：[[莱斯定理|Rice 定理]]也可用 SRT 三行证完：设 A 可计算，取变换规则 f(x) = "x <math>\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 m 使 <math>\phi_m = \phi_{f(m)}</math>。若 m <math>\in A</math>，则 f(m) <math>\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；m <math>\notin A</math> 同理。这条证明虽短，却是'''事后捷径'''——它没有揭示 Rice 定理与停机问题的血缘，而后者（上面的归约）才是定理的标准证明与本质机制。<ref name="rogers1967" />
==== Rice-Shapiro 定理（1956） ====
==== Rice-Shapiro 定理（1956） ====
Rice 定理回答"'''能否'''判定"；Rice-Shapiro 定理进一步刻画"'''何时能半判定'''"——把注意力从"A 是否可计算"收窄到"A 自身何时是 r.e. 的"：
Rice 定理回答"'''能否'''判定"；[[莱斯-夏皮罗定理|Rice-Shapiro 定理]]进一步刻画"'''何时能半判定'''"——把注意力从"A 是否可计算"收窄到"A 自身何时是 r.e. 的"：
> 设 A = { e : <math>W_e \in \mathcal{A}</math> } 是索引集。A 是 r.e. 的，'''当且仅当''' <math>\mathcal{A}</math> 是"有限可生成"的：存在一个可计算列举的有限集列 𝒮 = {<math>S_0</math>, <math>S_1</math>, <math>S_2</math>, <math>\ldots</math>}，使得 W <math>\in \mathcal{A}</math> ⟺ 𝒮 中存在某个 <math>S_i \subseteq W</math>。
> 设 A = { e : <math>W_e \in \mathcal{A}</math> } 是索引集。A 是 r.e. 的，'''当且仅当''' <math>\mathcal{A}</math> 是"有限可生成"的：存在一个可计算列举的有限集列 𝒮 = {<math>S_0</math>, <math>S_1</math>, <math>S_2</math>, <math>\ldots</math>}，使得 W <math>\in \mathcal{A}</math> ⟺ 𝒮 中存在某个 <math>S_i \subseteq W</math>。
> '''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 可证性逻辑 ===
'''背景'''：'''可证性逻辑（provability logic）'''研究"可证"这个概念的抽象规律，把 "⌜<math>\phi</math>⌝ 在 PA 中可证" 抽象为模态算子 □<math>\phi</math>。模态逻辑系统 '''GL'''（Gödel–Löb 逻辑）是候选公理系统。
'''背景'''：'''可证性逻辑（provability logic）'''研究"可证"这个概念的抽象规律，把 "⌜<math>\phi</math>⌝ 在 PA 中可证" 抽象为模态算子 □<math>\phi</math>。[[模态逻辑]]系统 '''GL'''（[[Gödel-Löb 逻辑|Gödel-Löb 逻辑]]）是候选公理系统。
> '''Solovay 定理（1976）'''：一个模态公式在 PA 的所有解释下都可证，当且仅当它是 GL 的定理。即 GL '''恰好'''完全刻画了 PA 的可证性逻辑。<ref name="solovay1976" /><ref name="moschovakis2010" />
> '''Solovay 定理（1976）'''：一个模态公式在 PA 的所有解释下都可证，当且仅当它是 [[Gödel-Löb 逻辑|GL]] 的定理。即 GL '''恰好'''完全刻画了 PA 的可证性逻辑。<ref name="solovay1976" /><ref name="moschovakis2010" />
Solovay 的证明漫长精巧，其关键引理需要构造一个'''自指的'''函数 h——h 的定义中引用 h 自己的编号。Solovay 本人用一句话带过："表面上的循环用递归定理以通常方式处理"<ref name="moschovakis2010" />。Moschovakis 评论：无法想象不借助 SRT 如何凭空想出这个构造——在此意义上 SRT 是可证性逻辑这块基石中不可或缺的成分<ref name="moschovakis2010" />。
[[罗伯特·索洛韦|Solovay]] 的证明漫长精巧，其关键引理需要构造一个'''自指的'''函数 h——h 的定义中引用 h 自己的编号。Solovay 本人用一句话带过："表面上的循环用递归定理以通常方式处理"<ref name="moschovakis2010" />。Moschovakis 评论：无法想象不借助 SRT 如何凭空想出这个构造——在此意义上 SRT 是可证性逻辑这块基石中不可或缺的成分<ref name="moschovakis2010" />。
=== 应用地图一览 ===
=== 应用地图一览 ===
:<ref name="rogers1967">'''Rogers, H., Jr. (1967).''' ''Theory of Recursive Functions and Effective Computability''. McGraw-Hill. 第 11 章 The Recursion Theorem, pp. 179–222.【教科书标准表述；第一/第二递归定理的命名来源】</ref>
:<ref name="rogers1967">'''Rogers, H., Jr. (1967).''' ''Theory of Recursive Functions and Effective Computability''. McGraw-Hill. 第 11 章 The Recursion Theorem, pp. 179–222.【教科书标准表述；第一/第二递归定理的命名来源】</ref>
:<ref name="kiselyov">'''Kiselyov, O.''' ''Kleene Second Recursion Theorem: A Functional Pearl''.【<math>\lambda</math> 演算/函数式编程视角；quine、twine、性能分析；Unix `cat` 例子出处】</ref>
:<ref name="kiselyov">'''Kiselyov, O.''' ''Kleene Second Recursion Theorem: A Functional Pearl''.【<math>\lambda</math> 演算/函数式编程视角；quine、twine、性能分析；Unix `cat` 例子出处】</ref>
<references />
<references />