3,094
个编辑
更改
跳到导航
跳到搜索
第13行：
第13行： − 两个定理的对照表（其中涉及的符号会在第二节逐一解释，此处可先跳过细节）：+ 第110行：
第110行： − + 第198行：
第198行： − + 第204行：
第204行： − + − + − + − + 第226行：
第226行： − + 第237行：
第237行： − + 第250行：
第250行： − + 第286行：
第286行： − + 第318行：
第318行： − + 第336行：
第336行： − + 第368行：
第368行： − + − + − + 第406行：
第406行： − + 第419行：
第419行： − + − + 第459行：
第459行： − + 第488行：
第488行： − + 第509行：
第509行： − + 第542行：
第542行： − + − 上一节（§5.7）的那些现象都是"自指"本身的例子——程序或句子直接谈论自己。但 SRT 的威力远不止此：它同样是构造不直接涉及自指的复杂数学对象的基本工具。Moschovakis (2010) 以"回顾展"方式列举了 18 个 SRT 发挥关键作用的结果<ref name="moschovakis2010" />，其中最重要的一类是 Kleene 本人最钟爱的'''沿序数逐层构造'''（[[有效超限递归]]）——把递归定义从自然数推广到[[序数]]，从而定义出越来越复杂的对象。本节即以它开篇（前4个例子）；此后转入其余主题——注意第5个板块中的 Rice 家族与 SRT 是“同源，但独立”的关系（并非 SRT 应用），详见该节导言。逻辑学家 Leo Harrington 对 SRT 威力的概括最为传神：+ + − + − + − + 第576行：
第577行： − + 第595行：
第596行： − + 第607行：
第608行： − + − + − + − + 第620行：
第621行： − + + 第633行：
第635行： − + 第640行：
第642行： − + 第646行：
第648行： − + 第654行：
第656行： − + − + 第751行：
第753行： − + − +
无编辑摘要
'''第一递归定理（日常语言版）'''：''任何递归定义——即把一个函数在某处的值，写成它自己在其他输入上的值（比如阶乘 <math>fac(n) = n\cdot fac(n−1)</math>）——都必然有解'' ，而且其中"最小"的那个解一定能被机器算出。换句话说，'''机械式的递归定义永远合法、永远有解'''<ref name="rogers1967" />。
'''第一递归定理（日常语言版）'''：''任何递归定义——即把一个函数在某处的值，写成它自己在其他输入上的值（比如阶乘 <math>fac(n) = n\cdot fac(n−1)</math>）——都必然有解'' ，而且其中"最小"的那个解一定能被机器算出。换句话说，'''机械式的递归定义永远合法、永远有解'''<ref name="rogers1967" />。
两个定理的对照表（其中涉及的符号会在[[#预备知识：读懂本词条所需的全部概念|第二节]]逐一解释，此处可先跳过细节）：
{| class="wikitable"
{| class="wikitable"
=== 一个值得铭记的教训 ===
=== 一个值得铭记的教训 ===
1944 年，Kleene 曾'''错误地'''宣称他构造的记号集 O 具有较低的[[逻辑复杂度]]（属于 <math>\Pi^0_2</math> 类），因为他把第二递归定理给出的'''某一个'''不动点，误当作了归纳定义所要求的'''最小'''不动点。事实上 O 的复杂度要高得多（它是<math>\Pi^1_1</math>-完备），Kleene 直到 1955 年才纠正<ref name="moschovakis2010" />。这个故事最生动地说明了：'''第二递归定理只保证"给你一个不动点"，不保证给你"最小/最特殊的那个"'''——这正是它区别于第一递归定理的关键（见 4.4 与 6.6）。
1944 年，Kleene 曾'''错误地'''宣称他构造的记号集 O 具有较低的[[逻辑复杂度]]（属于 <math>\Pi^0_2</math> 类），因为他把第二递归定理给出的'''某一个'''不动点，误当作了归纳定义所要求的'''最小'''不动点。事实上 O 的复杂度要高得多（它是<math>\Pi^1_1</math>-完备），Kleene 直到 1955 年才纠正<ref name="moschovakis2010" />。这个故事最生动地说明了：'''第二递归定理只保证"给你一个不动点"，不保证给你"最小/最特殊的那个"'''——这正是它区别于第一递归定理的关键（见 [[#与第二递归定理的关系|4.4]] 与 [[#有效运算的连续性：Myhill–Shepherdson 与 KLS–Čeĭnin 定理|6.6]]）。
== 第一递归定理（FRT） ==
== 第一递归定理（FRT） ==
——两个程序可以'''互相引用对方的代码'''。这是 SRT 的"二元推广"，可直接由 SRT 套用：
——两个程序可以'''互相引用对方的代码'''。这是 SRT 的"二元推广"，可直接由 SRT 套用：
# 先用 s-m-n（§2.3）构造两个可计算函数 <math>\psi_1(x) = g(S(x, x), x)</math>、<math>\psi_2(x) = h(S(x, x), x)</math>，二者均依赖自身编号；
# 先用 s-m-n（[[#s-m-n 定理（柯里化 / 参数特化）|§2.3]]）构造两个可计算函数 <math>\psi_1(x) = g(S(x, x), x)</math>、<math>\psi_2(x) = h(S(x, x), x)</math>，二者均依赖自身编号；
# 对 <math>\psi_1</math> 套 SRT 拿到不动点 <math>m</math>；
# 对 <math>\psi_1</math> 套 SRT 拿到不动点 <math>m</math>；
# <math>m</math> 唯一确定后，<math>n</math> 由 <math>\phi_n = \psi_2(m)</math> 的不动点结构给出。
# <math>m</math> 唯一确定后，<math>n</math> 由 <math>\phi_n = \psi_2(m)</math> 的不动点结构给出。
推广到 <math>k</math> 元：对任意 <math>k</math> 个全可计算函数 <math>g_1</math>, <math>\ldots</math>, <math>g_k</math>，存在 <math>k</math> 个程序 <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>。
推广到 <math>k</math> 元：对任意 <math>k</math> 个全可计算函数 <math>g_1</math>, <math>\ldots</math>, <math>g_k</math>，存在 <math>k</math> 个程序 <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">'''Smullyan, R. M. (1961).''' ''Theory of Formal Systems''. Princeton University Press.【双递归定理的提出者；§5.2.1】</ref><ref name="rogers1967" />.
[[#Smullyan 双递归定理（1959, 1961）|双递归定理]]是后续许多重要构造的核心：① [[#超算术层级与 Spector 唯一性定理|§6.3]] 介绍的"两层超算术构造"里，[[克利福德·斯佩克特|Spector]] 定理需要同时构造两个互相缠绕的函数；② [[Myhill-Shepherdson 定理]]（[[#有效运算的连续性：Myhill–Shepherdson 与 KLS–Čeĭnin 定理|§6.6]] 简述）描述"如何用 r.e. 集作为其它 r.e. 集的有效操作"时也需要联立不动点；③ 某些停机问题的"相对化"证明也走双递归路线<ref name="smullyan1961">'''Smullyan, R. M. (1961).''' ''Theory of Formal Systems''. Princeton University Press.【双递归定理的提出者；§5.2.1】</ref><ref name="rogers1967" />.
==== Rogers 同构定理（1958） ====
==== Rogers 同构定理（1958） ====
任意两个'''通用程序枚举'''（即枚举出所有可计算函数的程序编号系统，详见 §2.2；下称 <math>\phi</math> 系统与 <math>\psi</math> 系统）之间，必然存在一个'''可计算同构''' <math>\rho</math>：<math>\mathbb{N} \to \mathbb{N}</math>——一部双向都可计算的"翻译词典"，把 <math>\phi</math> 系统里的每个程序号 <math>e</math> 送到 <math>\psi</math> 系统里的程序号 <math>\rho(e)</math>，并且 '''保 <math>\phi</math> 等价'''、'''保 W 等价'''。这两个"保…等价"是说：这部词典'''不改变任何行为事实'''。逐个拆开看：
任意两个'''通用程序枚举'''（即枚举出所有可计算函数的程序编号系统，详见 [[#通用程序（解释器）|§2.2]]；下称 <math>\phi</math> 系统与 <math>\psi</math> 系统）之间，必然存在一个'''可计算同构''' <math>\rho</math>：<math>\mathbb{N} \to \mathbb{N}</math>——一部双向都可计算的"翻译词典"，把 <math>\phi</math> 系统里的每个程序号 <math>e</math> 送到 <math>\psi</math> 系统里的程序号 <math>\rho(e)</math>，并且 '''保 <math>\phi</math> 等价'''、'''保 W 等价'''。这两个"保…等价"是说：这部词典'''不改变任何行为事实'''。逐个拆开看：
* '''<math>\phi</math> 等价'''：同一编号系统内，若两个程序 <math>e_1</math>、<math>e_2</math> 计算的是同一个（部分）函数（<math>\phi_{e_1} = \phi_{e_2}</math>，§2.1），就说它们 '''<math>\phi</math> 等价'''——编号只是程序的外衣，算出的函数才是实质。
* '''<math>\phi</math> 等价'''：同一编号系统内，若两个程序 <math>e_1</math>、<math>e_2</math> 计算的是同一个（部分）函数（<math>\phi_{e_1} = \phi_{e_2}</math>，[[#"可计算"与"部分函数"|§2.1]]），就说它们 '''<math>\phi</math> 等价'''——编号只是程序的外衣，算出的函数才是实质。
* '''保 <math>\phi</math> 等价'''：要求对每个程序号 <math>e</math> 成立 <math>\phi_e = \psi_{\rho(e)}</math>：<math>e</math> 在 <math>\phi</math> 系统里算什么函数，<math>\rho(e)</math> 在 <math>\psi</math> 系统里就算同一个函数。于是"算同一函数"的程序对，翻译后依然是"算同一函数"的对。
* '''保 <math>\phi</math> 等价'''：要求对每个程序号 <math>e</math> 成立 <math>\phi_e = \psi_{\rho(e)}</math>：<math>e</math> 在 <math>\phi</math> 系统里算什么函数，<math>\rho(e)</math> 在 <math>\psi</math> 系统里就算同一个函数。于是"算同一函数"的程序对，翻译后依然是"算同一函数"的对。
* '''W 等价 / 保 W 等价'''：<math>W_e</math> 是程序 <math>e</math> 的定义域——会让它停机的输入集合（§2.4）。两个程序 '''W 等价'''指 <math>W_{e_1} = W_{e_2}</math>（接受的输入一模一样）；'''保 W 等价'''指翻译也不破坏这层对应。由于词条约定 <math>W_e = dom(\phi_e)</math>，"保 <math>\phi</math>"已自动带出"保 W"；Rogers 原版把两层并列，是因为他的框架允许"函数枚举"与"r.e. 集枚举"彼此独立（§6.5 索引集的 <math>\mathcal{A}</math> 用的正是独立于 <math>\phi</math> 的 W 层）。
* '''W 等价 / 保 W 等价'''：<math>W_e</math> 是程序 <math>e</math> 的定义域——会让它停机的输入集合（[[#递归可枚举集（r.e. set）|§2.4]]）。两个程序 '''W 等价'''指 <math>W_{e_1} = W_{e_2}</math>（接受的输入一模一样）；'''保 W 等价'''指翻译也不破坏这层对应。由于词条约定 <math>W_e = dom(\phi_e)</math>，"保 <math>\phi</math>"已自动带出"保 W"；Rogers 原版把两层并列，是因为他的框架允许"函数枚举"与"r.e. 集枚举"彼此独立（[[#r.e. 索引集理论：Rice、Rice-Shapiro 与 Myhill|§6.5]] 索引集的 <math>\mathcal{A}</math> 用的正是独立于 <math>\phi</math> 的 W 层）。
直觉上：两个不同的程序编号系统乍看像不同的语言（一个把 quine 编号成 42，另一个编号成 100），但实质上说的是同一类对象；Rogers 定理说它们之间必有可计算的"翻译词典"，且词典严格保结构。
直觉上：两个不同的程序编号系统乍看像不同的语言（一个把 quine 编号成 42，另一个编号成 100），但实质上说的是同一类对象；Rogers 定理说它们之间必有可计算的"翻译词典"，且词典严格保结构。
这里一下子出现了三个新名字，先逐个解释：
这里一下子出现了三个新名字，先逐个解释：
* '''r.e. 集合'''：见 §2.4。本词条统一用缩写 r.e.（recursively enumerable，[[递归可枚举集|递归可枚举]]）。
* '''r.e. 集合'''：见 [[#递归可枚举集（r.e. set）|§2.4]]。本词条统一用缩写 r.e.（recursively enumerable，[[递归可枚举集|递归可枚举]]）。
* '''r.e.-完全'''：r.e. 集合这个"复杂度类别"里"最硬核"的一档——任何别的 r.e. 集合 <math>W</math> 都能机械地归约到 <math>C</math>，判定"<math>W</math> 含 <math>x</math>"等价于"问 <math>C</math>"。
* '''r.e.-完全'''：r.e. 集合这个"复杂度类别"里"最硬核"的一档——任何别的 r.e. 集合 <math>W</math> 都能机械地归约到 <math>C</math>，判定"<math>W</math> 含 <math>x</math>"等价于"问 <math>C</math>"。
* '''Turing 归约 / <math>W\leq_T C</math> 通过 <math>f_W</math>'''：<math>A</math> 能 '''Turing 归约'''到 <math>B</math>（记 <math>A\leq_T B</math>），意思是"只要允许把 <math>B</math> 当'''神谕机（oracle，下一条解释）'''——可以向它提任意多个 yes/no 问题并瞬时得到回答——<math>A</math> 就能被判定"。等式 <math>W\leq_T C</math> 通过 <math>f_W</math> 即"编排提问方式的过程由可计算函数 <math>f_W</math> 给出，它把 <math>x</math> 改写成若干个向 <math>C</math> 的查询并综合出答案"。
* '''Turing 归约 / <math>W\leq_T C</math> 通过 <math>f_W</math>'''：<math>A</math> 能 '''Turing 归约'''到 <math>B</math>（记 <math>A\leq_T B</math>），意思是"只要允许把 <math>B</math> 当'''神谕机（oracle，下一条解释）'''——可以向它提任意多个 yes/no 问题并瞬时得到回答——<math>A</math> 就能被判定"。等式 <math>W\leq_T C</math> 通过 <math>f_W</math> 即"编排提问方式的过程由可计算函数 <math>f_W</math> 给出，它把 <math>x</math> 改写成若干个向 <math>C</math> 的查询并综合出答案"。
=== 证明：一行对角线 ===
=== 证明：一行对角线 ===
以表述 A 为例，全部证明如下。函数 <math>\psi(S(y, y), x)</math> 是可计算的（它只是把 §2.3 的[[柯里化操作]] <math>S</math> 和 <math>\psi</math> 复合起来），所以它有编号，设为 <math>e</math>。令 '''<math>f = S(e, e)</math>'''，则对任何输入 <math>x</math>：
以表述 A 为例，全部证明如下。函数 <math>\psi(S(y, y), x)</math> 是可计算的（它只是把 [[#s-m-n 定理（柯里化 / 参数特化）|§2.3]] 的[[柯里化操作]] <math>S</math> 和 <math>\psi</math> 复合起来），所以它有编号，设为 <math>e</math>。令 '''<math>f = S(e, e)</math>'''，则对任何输入 <math>x</math>：
: <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> ∎
* '''1. 把"所有可计算函数的枚举"摆成一张表'''
* '''1. 把"所有可计算函数的枚举"摆成一张表'''
按 §2.2，每个可计算部分函数都有一个编号；所有这种编号的全体记作 <math>\{\phi_k\}</math>。对任意"枚举函数" <math>E</math>（把一列编号映射成一列可计算函数），<math>E</math> 的第 <math>n</math> 项就是 <math>\phi_{E(n)}</math>，即"编号为 <math>E(n)</math> 的程序"。现在考虑所有"可计算函数的枚举"——它们每一个都是某个可计算函数 <math>h</math>。Cutland 把它们自身也排成一张表：用编号为 <math>k</math> 的程序 <math>\phi_k</math> 自己去枚举，得到
按 [[#通用程序（解释器）|§2.2]]，每个可计算部分函数都有一个编号；所有这种编号的全体记作 <math>\{\phi_k\}</math>。对任意"枚举函数" <math>E</math>（把一列编号映射成一列可计算函数），<math>E</math> 的第 <math>n</math> 项就是 <math>\phi_{E(n)}</math>，即"编号为 <math>E(n)</math> 的程序"。现在考虑所有"可计算函数的枚举"——它们每一个都是某个可计算函数 <math>h</math>。Cutland 把它们自身也排成一张表：用编号为 <math>k</math> 的程序 <math>\phi_k</math> 自己去枚举，得到
: <math>E_k</math> = "以 <math>\phi_k</math> 为枚举函数的那种枚举"，即 <math>E_k</math> 的第 <math>n</math> 项 = <math>\phi_{\phi_k(n)}</math>
: <math>E_k</math> = "以 <math>\phi_k</math> 为枚举函数的那种枚举"，即 <math>E_k</math> 的第 <math>n</math> 项 = <math>\phi_{\phi_k(n)}</math>
<math>n</math> 就是 <math>f</math> 的不动点 ∎<ref name="cutland1980">'''Cutland, N. J. (1980).''' ''Computability: An Introduction to Recursive Function Theory''. Cambridge University Press.【§1.9 定理 1.9 给出 totally <math>\psi</math>-introspective 程序的原始定义与存在性证明——"自省程序"概念的最早明确出处（§5.7.7）；§2.3 定理 2.3 给出 SRT 的"列表法"证明（§5.3.1）】</ref>.
<math>n</math> 就是 <math>f</math> 的不动点 ∎<ref name="cutland1980">'''Cutland, N. J. (1980).''' ''Computability: An Introduction to Recursive Function Theory''. Cambridge University Press.【§1.9 定理 1.9 给出 totally <math>\psi</math>-introspective 程序的原始定义与存在性证明——"自省程序"概念的最早明确出处（§5.7.7）；§2.3 定理 2.3 给出 SRT 的"列表法"证明（§5.3.1）】</ref>.
'''与"一行证明"的关系'''：§5.3 的证明把表上 <math>D^* = E_m</math> 的循环直接写成 <math>\psi(S(e,e), x)</math> 的柯里化形式——<math>h(x) = \phi_x(x)</math> 对应"<math>e </math>= 编号(<math>\psi(S(y,y), x)</math>)"，<math>S(e,e)</math> 就是用自应用把表上的对角线点亮；列表法只是把这一行在表格里完整地展开。两者本质相同：列表法暴露了"为什么沿对角线循环必会撞回表里"——每行 <math>E_k</math> 都被对角线穿一格，循环天然闭合。
'''与"一行证明"的关系'''：[[#证明：一行对角线|§5.3]] 的证明把表上 <math>D^* = E_m</math> 的循环直接写成 <math>\psi(S(e,e), x)</math> 的柯里化形式——<math>h(x) = \phi_x(x)</math> 对应"<math>e </math>= 编号(<math>\psi(S(y,y), x)</math>)"，<math>S(e,e)</math> 就是用自应用把表上的对角线点亮；列表法只是把这一行在表格里完整地展开。两者本质相同：列表法暴露了"为什么沿对角线循环必会撞回表里"——每行 <math>E_k</math> 都被对角线穿一格，循环天然闭合。
[[文件:列表法证明.png|无|'''图6'''：Cutland (1980) 列表法证明的视觉化。'''上半'''：四行四列的"枚举之枚举"表 <math>E_0, E_1, E_2, \cdots, E_k</math>，每格填 <math>\phi_{\phi_i(j)}</math>；主对角线（红圈）上的格子构成对角枚举 <math>D</math>。'''黄底 <math>D</math> 行'''：把对角线上的格子抽出，得到 <math>D = (\phi_{\phi_0(0)}, \phi_{\phi_1(1)}, \phi_{\phi_2(2)}, \ldots)</math>。'''<math>D^*</math> 行'''：把 <math>f</math> 套到 <math>D</math> 上得到 <math>D^* = (\phi_{f(\phi_0(0))}, \phi_{f(\phi_1(1))}, \ldots)</math>——可计算 <math>\Rightarrow</math> 必是某行 <math>E_m</math>。'''绿框'''：取 <math>k = m</math> 撞上 <math>E_m</math>，得 <math>\phi_{\phi_m(m)} = \phi_{f(\phi_m(m))}</math>，再设 <math>n = \phi_m(m)</math> 即得 <math>\phi_n = \phi_{f(n)}</math>——<math>f</math> 的不动点。|缩略图|800x800像素]]
[[文件:列表法证明.png|无|'''图6'''：Cutland (1980) 列表法证明的视觉化。'''上半'''：四行四列的"枚举之枚举"表 <math>E_0, E_1, E_2, \cdots, E_k</math>，每格填 <math>\phi_{\phi_i(j)}</math>；主对角线（红圈）上的格子构成对角枚举 <math>D</math>。'''黄底 <math>D</math> 行'''：把对角线上的格子抽出，得到 <math>D = (\phi_{\phi_0(0)}, \phi_{\phi_1(1)}, \phi_{\phi_2(2)}, \ldots)</math>。'''<math>D^*</math> 行'''：把 <math>f</math> 套到 <math>D</math> 上得到 <math>D^* = (\phi_{f(\phi_0(0))}, \phi_{f(\phi_1(1))}, \ldots)</math>——可计算 <math>\Rightarrow</math> 必是某行 <math>E_m</math>。'''绿框'''：取 <math>k = m</math> 撞上 <math>E_m</math>，得 <math>\phi_{\phi_m(m)} = \phi_{f(\phi_m(m))}</math>，再设 <math>n = \phi_m(m)</math> 即得 <math>\phi_n = \phi_{f(n)}</math>——<math>f</math> 的不动点。|缩略图|800x800像素]]
——用公式写就是 <math>\phi_c = \phi_{f(c)}</math>（<math>\phi_c</math> 是程序 <math>c</math> 当作可计算函数看时的整体行为）。把上面那个 <math>f</math> 换成别的——比如"统计字符数"、"对源码求 SHA-256（一种密码学中的哈希函数）"、"把字符串大写"、"把源码上传到某服务器"、"什么都不做只返回自己"——只要 <math>f</math> 是可计算的全函数，'''满足 <math>\phi_c = \phi_{f(c)}</math> 的不动点程序 <math>c</math> 就必然存在'''。这正是 SRT 所承诺的内容：quine 是 SRT 在 <math>f =</math> "Print" 这一个特例上的推论，SRT 则是 quine 在 <math>f =</math> "任意全可计算函数"上的推广。Kiselyov 在分阶段 <math>\lambda</math> 演算里把这一观察形式化为"quine = f = id 的不动点、twine（两程序互相打印对方）= f = 另一程序编号映射的不动点、trade 谜题 = f = 投影函数对的不动点"<ref name="kiselyov" />。
——用公式写就是 <math>\phi_c = \phi_{f(c)}</math>（<math>\phi_c</math> 是程序 <math>c</math> 当作可计算函数看时的整体行为）。把上面那个 <math>f</math> 换成别的——比如"统计字符数"、"对源码求 SHA-256（一种密码学中的哈希函数）"、"把字符串大写"、"把源码上传到某服务器"、"什么都不做只返回自己"——只要 <math>f</math> 是可计算的全函数，'''满足 <math>\phi_c = \phi_{f(c)}</math> 的不动点程序 <math>c</math> 就必然存在'''。这正是 SRT 所承诺的内容：quine 是 SRT 在 <math>f =</math> "Print" 这一个特例上的推论，SRT 则是 quine 在 <math>f =</math> "任意全可计算函数"上的推广。Kiselyov 在分阶段 <math>\lambda</math> 演算里把这一观察形式化为"quine = f = id 的不动点、twine（两程序互相打印对方）= f = 另一程序编号映射的不动点、trade 谜题 = f = 投影函数对的不动点"<ref name="kiselyov" />。
'''SRT 的证明，本身就是一个 Quine 构造——而且方向和 quine 完全相同'''。再回看 §5.3 那一行证明——给定 <math>f</math>，构造 <math>\psi(x) = \phi_{S(x,x)}</math>（其中 <math>S</math> 把 <math>f</math> 与"自应用"组合起来），取 <math>e</math> 满足 <math>\phi_e = \psi</math>，再对 <math>\psi</math> 套 SRT 取不动点——会发现它和 quine 是'''同一种构造'''，差别只在目的（执行层面 vs 输出层面）。两边共用同一种"自指核心动作"——'''让程序合法地把"自己的表示"当作输入'''：
'''SRT 的证明，本身就是一个 Quine 构造——而且方向和 quine 完全相同'''。再回看 [[#证明：一行对角线|§5.3]] 那一行证明——给定 <math>f</math>，构造 <math>\psi(x) = \phi_{S(x,x)}</math>（其中 <math>S</math> 把 <math>f</math> 与"自应用"组合起来），取 <math>e</math> 满足 <math>\phi_e = \psi</math>，再对 <math>\psi</math> 套 SRT 取不动点——会发现它和 quine 是'''同一种构造'''，差别只在目的（执行层面 vs 输出层面）。两边共用同一种"自指核心动作"——'''让程序合法地把"自己的表示"当作输入'''：
{| class="wikitable"
{| class="wikitable"
| '''构造方向'''
| '''构造方向'''
| 先有具体 <math>f</math>（= Print），再造 <math>c</math>（<math>c</math> 的代码里嵌入 <math>f</math> 的引用）
| 先有具体 <math>f</math>（= Print），再造 <math>c</math>（<math>c</math> 的代码里嵌入 <math>f</math> 的引用）
| 先有具体 <math>f</math>（§5.3 假设中任意一个），再造 <math>c</math>（<math>c</math> 由对 <math>f</math> 套 SRT 得到）
| 先有具体 <math>f</math>（[[#证明：一行对角线|§5.3]] 假设中任意一个），再造 <math>c</math>（<math>c</math> 由对 <math>f</math> 套 SRT 得到）
|-
|-
| '''目的'''
| '''目的'''
=== 与其它不动点定理的关系 ===
=== 与其它不动点定理的关系 ===
SRT 衍生出许多重要推论（见 §5.2），但还有些定理与 SRT 的关系'''更微妙'''——它们与 SRT '''同源'''（都基于对角线 / 自指），却走的是独立证明路线，或者处于更高层的[[范畴论]]概括下。这里集中讨论两个最重要的"不动点定理"：Gödel 的[[不动点引理]]与 [[F. William Lawvere|Lawvere]] 的范畴论不动点定理，重点说明 SRT 与它们的精确定位关系。
SRT 衍生出许多重要推论（见 [[#推论：SRT 衍生出的若干重要结果|§5.2]]），但还有些定理与 SRT 的关系'''更微妙'''——它们与 SRT '''同源'''（都基于对角线 / 自指），却走的是独立证明路线，或者处于更高层的[[范畴论]]概括下。这里集中讨论两个最重要的"不动点定理"：Gödel 的[[不动点引理]]与 [[F. William Lawvere|Lawvere]] 的范畴论不动点定理，重点说明 SRT 与它们的精确定位关系。
==== Gödel 不动点引理（对角引理） ====
==== Gödel 不动点引理（对角引理） ====
对任何包含足够算术的递归可公理化理论 <math>T</math>，对 <math>T</math> 中任何公式 <math>\phi(x)</math>，都存在一个"不动点句子"<math>\psi</math>，使得 <math>T</math> 可证 <math>\psi\iff\phi</math>(⌜<math>\psi</math>⌝)。它的证明手法（对角线替换）与 SRT 同源，但 Gödel 早在 1931 年就独立给出了完整论证，'''SRT 推不出 Gödel 自身的不完备定理'''——Gödel 不完备的全部内容（[[一致性]]、[[ω-一致性]]、[[不可判定性]]三层）见 §5.7.4 的详述。
对任何包含足够算术的递归可公理化理论 <math>T</math>，对 <math>T</math> 中任何公式 <math>\phi(x)</math>，都存在一个"不动点句子"<math>\psi</math>，使得 <math>T</math> 可证 <math>\psi\iff\phi</math>(⌜<math>\psi</math>⌝)。它的证明手法（对角线替换）与 SRT 同源，但 Gödel 早在 1931 年就独立给出了完整论证，'''SRT 推不出 Gödel 自身的不完备定理'''——Gödel 不完备的全部内容（[[一致性]]、[[ω-一致性]]、[[不可判定性]]三层）见 [[#哥德尔第一不完备定理（1931）|§5.7.4]] 的详述。
注：'''Gödel 不动点引理本身是 SRT 最干净、最纯粹的推论'''（既可以把 SRT 当证明工具来证它，也可以两边都用"自指 + 对角线"的同源手法独立证明）。它和 SRT 的关系是"同源、互为推论"；但 Gödel 不完备'''定理'''与 SRT 的关系另当别论，见 §5.7.4 的"双重身份"分析。
注：'''Gödel 不动点引理本身是 SRT 最干净、最纯粹的推论'''（既可以把 SRT 当证明工具来证它，也可以两边都用"自指 + 对角线"的同源手法独立证明）。它和 SRT 的关系是"同源、互为推论"；但 Gödel 不完备'''定理'''与 SRT 的关系另当别论，见 [[#哥德尔第一不完备定理（1931）|§5.7.4]] 的"双重身份"分析。
==== [[Lawvere 不动点定理]]（1969） ====
==== [[Lawvere 不动点定理]]（1969） ====
|-
|-
| 满射态射 <math>f: A\to F(A)</math>
| 满射态射 <math>f: A\to F(A)</math>
| 取定 §2.1 中 <math>\phi_e</math> 的"自枚举"——把 <math>\phi_e</math> 编号 <math>e</math> 看作可枚举的元素、保证 <math>F(A)</math> 的每个元素都能表示为"以 <math>f(e)</math> 为参数的程序"，这一步在 SRT 证明中就是 §5.3 一行对角线 <math>e \mapsto \Phi_h(f(e), e)</math>（也称"自评价插值器"）
| 取定 [[#"可计算"与"部分函数"|§2.1]] 中 <math>\phi_e</math> 的"自枚举"——把 <math>\phi_e</math> 编号 <math>e</math> 看作可枚举的元素、保证 <math>F(A)</math> 的每个元素都能表示为"以 <math>f(e)</math> 为参数的程序"，这一步在 SRT 证明中就是 [[#证明：一行对角线|§5.3]] 一行对角线 <math>e \mapsto \Phi_h(f(e), e)</math>（也称"自评价插值器"）
|-
|-
| 任意态射 <math>g: F(A)\to A</math>
| 任意态射 <math>g: F(A)\to A</math>
* [[#Lawvere 不动点定理（1969）|Lawvere 不动点定理]]'''不是''' SRT 的"推论"（该定理没有反推 SRT，而是反过来把 SRT 概括出来）；
* [[#Lawvere 不动点定理（1969）|Lawvere 不动点定理]]'''不是''' SRT 的"推论"（该定理没有反推 SRT，而是反过来把 SRT 概括出来）；
* Lawvere 也不仅是 SRT 的"更高层次表述"（它是数学基础层面的定理，把 SRT、[[#Gödel 不动点引理（对角引理）|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">'''Lawvere, F. W. (1969).''' Diagonal arguments and cartesian closed categories. In ''Category Theory, Homology Theory and their Applications III'', Lecture Notes in Mathematics, vol. 92, Springer.【Lawvere 不动点定理，把 SRT、Gödel 不完备、Turing 停机统一为范畴论特例】【§5.6.2】</ref>。
'''对读者的现实意义'''：如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[AI反思架构]]等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，[[#证明：一行对角线|§5.3]] 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容<ref name="lawvere1969">'''Lawvere, F. W. (1969).''' Diagonal arguments and cartesian closed categories. In ''Category Theory, Homology Theory and their Applications III'', Lecture Notes in Mathematics, vol. 92, Springer.【Lawvere 不动点定理，把 SRT、Gödel 不完备、Turing 停机统一为范畴论特例】【§5.6.2】</ref>。
=== SRT与自指===
=== SRT与自指===
'''现象'''：考虑 <math>R = \{x : x \notin x\}</math>（所有"不属于自己"的集合组成的集合）。问 <math>R\in R</math> 是否成立？若 <math>R\in R</math>，则按定义 <math>R\notin R</math>；若 <math>R\notin R</math>，则按定义 <math>R\in R</math>。两边都矛盾，这个悖论动摇了朴素集合论<ref name="russell1908">'''Russell, B. (1908).''' Mathematical logic as based on the theory of types. ''American Journal of Mathematics'', 30, 222–262.【罗素悖论的现代陈述】</ref>。
'''现象'''：考虑 <math>R = \{x : x \notin x\}</math>（所有"不属于自己"的集合组成的集合）。问 <math>R\in R</math> 是否成立？若 <math>R\in R</math>，则按定义 <math>R\notin R</math>；若 <math>R\notin R</math>，则按定义 <math>R\in R</math>。两边都矛盾，这个悖论动摇了朴素集合论<ref name="russell1908">'''Russell, B. (1908).''' Mathematical logic as based on the theory of types. ''American Journal of Mathematics'', 30, 222–262.【罗素悖论的现代陈述】</ref>。
'''与 SRT 的关系：同源，但独立'''。罗素悖论也是"把谓词'不属于自身'同时用于所有集合"的对角线操作，和 SRT 共享同一个技巧，但 SRT 同样'''推不出'''它——它是朴素集合论内部的问题，不涉及程序。真正值得注意的，是 Rogers 指出的一个'''类比'''：把"集合"换成"可枚举的集合 <math>W_e</math>"、把"<math>\in</math>"换成"<math>e\in W_e</math>"，就得到 <math>K = \{e : e\notin W_e\}</math>——<math>K</math> 可枚举、其补集不可枚举。而"<math>K</math> 的补集不可枚举"恰好'''等价于停机问题不可判定'''（见 5.7.3），后者才是 SRT 真正推得出来的。换言之，"停机问题不可判定"可以看作"递归论版的罗素悖论"，但罗素悖论本身与SRT只是同源关系<ref name="russell1908" /><ref name="rogers1967" />。
'''与 SRT 的关系：同源，但独立'''。罗素悖论也是"把谓词'不属于自身'同时用于所有集合"的对角线操作，和 SRT 共享同一个技巧，但 SRT 同样'''推不出'''它——它是朴素集合论内部的问题，不涉及程序。真正值得注意的，是 Rogers 指出的一个'''类比'''：把"集合"换成"可枚举的集合 <math>W_e</math>"、把"<math>\in</math>"换成"<math>e\in W_e</math>"，就得到 <math>K = \{e : e\notin W_e\}</math>——<math>K</math> 可枚举、其补集不可枚举。而"<math>K</math> 的补集不可枚举"恰好'''等价于停机问题不可判定'''（见 [[#图灵停机问题（1936）|5.7.3]]），后者才是 SRT 真正推得出来的。换言之，"停机问题不可判定"可以看作"递归论版的罗素悖论"，但罗素悖论本身与SRT只是同源关系<ref name="russell1908" /><ref name="rogers1967" />。
==== 图灵停机问题（1936） ====
==== 图灵停机问题（1936） ====
* 证明：取 <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" />。
* 证明：取 <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>，其定理集都是'''[[创造集]]'''（见 §6.5.3），从而是 r.e.-完备的<ref name="moschovakis2010" />.
* '''[[Myhill定理]]（1955）'''：[[罗宾逊算术]] Q 的任何一致、可公理化扩张 <math>T</math>，其定理集都是'''[[创造集]]'''（见 [[#Myhill定理：创造集 = 完备集|§6.5.3]]），从而是 r.e.-完备的<ref name="moschovakis2010" />.
合起来我们可以得到一个惊人结论：'''所有'''足够强的一致公理化理论（皮亚诺算术、[[ZFC公理系统]]<math>\ldots\ldots</math>）都自动满足不动点引理的条件，因而都不完备、不可判定；而且任意两个这样的理论，其定理集在递归同构意义下完全相同<ref name="moschovakis2010" />。
合起来我们可以得到一个惊人结论：'''所有'''足够强的一致公理化理论（皮亚诺算术、[[ZFC公理系统]]<math>\ldots\ldots</math>）都自动满足不动点引理的条件，因而都不完备、不可判定；而且任意两个这样的理论，其定理集在递归同构意义下完全相同<ref name="moschovakis2010" />。
==== Quine（自打印程序） ====
==== Quine（自打印程序） ====
'''现象'''：一个'''不接受任何输入、只打印出自己源代码副本'''的程序<ref name="wikipedia_quine_computing"/>。它的约束很苛刻——'''不能读自己的源码'''（靠读文件输出自己、如 `cat $0`，被视为"作弊"，不算 quine），只能靠"代码部分 + 代表代码文本的数据部分"来构造性地打印自己；§5.4 例 1 的 Python 程序就是一个标准 quine。"quine" 一词由 [[侯世达|Hofstadter]] 在《[[哥德尔、艾舍尔、巴赫]]》中普及（借自哲学家 W. V. O. Quine 的名字，他构造过自指的句子）<ref name="hofstadter1979">'''Hofstadter, D. R. (1979).''' ''Gödel, Escher, Bach: An Eternal Golden Braid''. Basic Books.【"quine" 一词的普及来源】</ref>。
'''现象'''：一个'''不接受任何输入、只打印出自己源代码副本'''的程序<ref name="wikipedia_quine_computing"/>。它的约束很苛刻——'''不能读自己的源码'''（靠读文件输出自己、如 `cat $0`，被视为"作弊"，不算 quine），只能靠"代码部分 + 代表代码文本的数据部分"来构造性地打印自己；[[#直观图景：程序如何"谈论"自己的代码|§5.4]] 例 1 的 Python 程序就是一个标准 quine。"quine" 一词由 [[侯世达|Hofstadter]] 在《[[哥德尔、艾舍尔、巴赫]]》中普及（借自哲学家 W. V. O. Quine 的名字，他构造过自指的句子）<ref name="hofstadter1979">'''Hofstadter, D. R. (1979).''' ''Gödel, Escher, Bach: An Eternal Golden Braid''. Basic Books.【"quine" 一词的普及来源】</ref>。
'''SRT 如何推出它'''：把 SRT 里的变换规则 <math>f</math> 直接定义:'''"打印"程序'''——<math>f(c) =</math> "打印出 <math>c</math> 的源码的那个程序"。套用 SRT（<math>\phi_c = \phi_{f(c)}</math>）得到不动点 <math>c</math>：
'''SRT 如何推出它'''：把 SRT 里的变换规则 <math>f</math> 直接定义:'''"打印"程序'''——<math>f(c) =</math> "打印出 <math>c</math> 的源码的那个程序"。套用 SRT（<math>\phi_c = \phi_{f(c)}</math>）得到不动点 <math>c</math>：
[[文件:自指统一性总结.png|替代=自指/对角线部分总结|自指/对角线部分总结|600px]]
[[文件:自指统一性总结.png|替代=自指/对角线部分总结|自指/对角线部分总结|600px]]
其中图灵停机问题、哥德尔不完备定理拥有'''双重身份'''：结论是否定性的（与康托尔、罗素问题同类），历史原证也走否定性对角线老路、不依赖 SRT；但因活在程序世界，又能被 SRT 事后更简洁地推出（§5.7.3 展示了停机问题的完整套用过程）。它们共同构成 SRT 的"自指"一面；SRT 还有另一面——"沿序数逐层构造"——见第六节。
其中图灵停机问题、哥德尔不完备定理拥有'''双重身份'''：结论是否定性的（与康托尔、罗素问题同类），历史原证也走否定性对角线老路、不依赖 SRT；但因活在程序世界，又能被 SRT 事后更简洁地推出（[[#图灵停机问题（1936）|§5.7.3]] 展示了停机问题的完整套用过程）。它们共同构成 SRT 的"自指"一面；SRT 还有另一面——"沿序数逐层构造"——见[[#SRT的其它应用|第六节]]。
== SRT的其它应用 ==
== SRT的其它应用 ==
上一节（[[#SRT与自指|§5.7]]）的那些现象都是"自指"本身的例子——程序或句子直接谈论自己。但 SRT 的威力远不止此：它同样是构造不直接涉及自指的复杂数学对象的基本工具。Moschovakis (2010) 以"回顾展"方式列举了 18 个 SRT 发挥关键作用的结果<ref name="moschovakis2010" />，其中最重要的一类是 Kleene 本人最钟爱的'''沿序数逐层构造'''（[[有效超限递归]]）——把递归定义从自然数推广到[[序数]]，从而定义出越来越复杂的对象。本节即以它开篇（前4个例子）；此后转入其余主题——注意第5个板块中的 Rice 家族与 SRT 是“同源，但独立”的关系（并非 SRT 应用），详见该节导言。逻辑学家 Leo Harrington 对 SRT 威力的概括最为传神：
'''"You need a number z? You got it!"（你需要一个这样的数 z？给你！）'''<ref name="moschovakis2010" />
'''"You need a number z? You got it!"（你需要一个这样的数 z？给你！）'''<ref name="moschovakis2010" />
=== 通用序数记号系统与<math>\omega_1^{CK}</math> ===
=== 通用序数记号系统与<math>\omega_1^{CK}</math> ===
{{Anchor|6.1}}
这是 SRT '''最初的'''应用（见 3.1）。回顾§3.1 的背景：[[序数记号系统]]给可数序数指派自然数代号，使得 0 / 后继 / 极限三分可机械判定、前驱与[[柯西序列|基本序列]]可机械取出。在进入定理之前，先把本节反复用到的几个概念交代清楚（"序数"本身的背景见 §3.1 的背景框）：
这是 SRT '''最初的'''应用（见 [[#起源：一篇研究"序数记号"的 6 页短文|3.1]]）。回顾[[#起源：一篇研究"序数记号"的 6 页短文|§3.1]] 的背景：[[序数记号系统]]给可数序数指派自然数代号，使得 0 / 后继 / 极限三分可机械判定、前驱与[[柯西序列|基本序列]]可机械取出。在进入定理之前，先把本节反复用到的几个概念交代清楚（"序数"本身的背景见 [[#起源：一篇研究"序数记号"的 6 页短文|§3.1]] 的背景框）：
* '''代号与所指'''：记号系统里的每个自然数 <math>a</math> 都是一个'''代号'''，它所指的序数记作 <math>|a|</math>。一个序数 <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>（<math>0, 1, 2, 3, \ldots</math> 无限数完之后的那一步：任何自然数都不是它的"前一个"）。
* '''代号与所指'''：记号系统里的每个自然数 <math>a</math> 都是一个'''代号'''，它所指的序数记作 <math>|a|</math>。一个序数 <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>（<math>0, 1, 2, 3, \ldots</math> 无限数完之后的那一步：任何自然数都不是它的"前一个"）。
* '''前驱与基本序列'''：后继代号 <math>x</math> 的'''前驱'''（predecessor）记 <math>P(x)</math>——所指序数被"+1"之前那个序数的代号。极限代号 <math>x</math> 的'''基本序列（fundamental sequence）'''是一条可机械取出的递增代号列 <math>x_0</math>, <math>x_1,x_2,\ldots</math>，所指序数 <math>|x_0| < |x_1| < \ldots</math> 逐渐逼近 <math>|x|</math>。
* '''前驱与基本序列'''：后继代号 <math>x</math> 的'''前驱'''（predecessor）记 <math>P(x)</math>——所指序数被"+1"之前那个序数的代号。极限代号 <math>x</math> 的'''基本序列（fundamental sequence）'''是一条可机械取出的递增代号列 <math>x_0</math>, <math>x_1,x_2,\ldots</math>，所指序数 <math>|x_0| < |x_1| < \ldots</math> 逐渐逼近 <math>|x|</math>。
* <math>S_1</math> 的语法（<math>S_1</math> 是下文定理要构造的那个"通用"'''序数记号系统'''，Kleene 1938 为它设计的编码方案；后文的记号系统 O 沿用同一语法）：0 的代号固定为 1；代号 <math>a</math> 的后继的代号写成 '''<math>2^a</math>'''；极限序数的代号写成 '''<math>3\cdot 5^e</math>'''，并约定 <math>|3\cdot5^e| = \lim|\phi_e(n)|</math>（程序 <math>e</math> 逐个吐出逼近该极限的记号列，<math>\phi</math>ₑ 是编号为 <math>e</math> 的程序，见 §2.2）。取这三种质因数形态（1、2 的幂、3<math>\times5</math> 的幂）纯属编码技巧：对代号做质因数分解，就能机械判定它是 0 的代号、后继代号还是极限代号。
* <math>S_1</math> 的语法（<math>S_1</math> 是下文定理要构造的那个"通用"'''序数记号系统'''，Kleene 1938 为它设计的编码方案；后文的记号系统 O 沿用同一语法）：0 的代号固定为 1；代号 <math>a</math> 的后继的代号写成 '''<math>2^a</math>'''；极限序数的代号写成 '''<math>3\cdot 5^e</math>'''，并约定 <math>|3\cdot5^e| = \lim|\phi_e(n)|</math>（程序 <math>e</math> 逐个吐出逼近该极限的记号列，<math>\phi</math>ₑ 是编号为 <math>e</math> 的程序，见 [[#通用程序（解释器）|§2.2]]）。取这三种质因数形态（1、2 的幂、3<math>\times5</math> 的幂）纯属编码技巧：对代号做质因数分解，就能机械判定它是 0 的代号、后继代号还是极限代号。
'''定理（Kleene 1938）'''：存在一个'''通用'''序数记号系统 <math>S_1</math>：对任何其他合法的序数记号系统<math>S</math>（"合法"即满足 §3.1 说的条件——0 / 后继 / 极限三分可机械判定、前驱与基本序列可机械取出），存在可计算函数把 <math>S</math> 的代号'''保序'''地翻译为 <math>S_1</math> 的代号（"保序"：若 <math>|x| < |y|</math>，则翻译后所指的序数仍保持这一大小关系——翻译不打乱任何两个序数的先后）<ref name="kleene1938">'''Kleene, S. C. (1938).''' On notation for ordinal numbers. ''The Journal of Symbolic Logic'', 3(4), 150–155.【第二递归定理的原始出处，定理与证明见 p.153】</ref><ref name="rogers1967" />。
'''定理（Kleene 1938）'''：存在一个'''通用'''序数记号系统 <math>S_1</math>：对任何其他合法的序数记号系统<math>S</math>（"合法"即满足 [[#起源：一篇研究"序数记号"的 6 页短文|§3.1]] 说的条件——0 / 后继 / 极限三分可机械判定、前驱与基本序列可机械取出），存在可计算函数把 <math>S</math> 的代号'''保序'''地翻译为 <math>S_1</math> 的代号（"保序"：若 <math>|x| < |y|</math>，则翻译后所指的序数仍保持这一大小关系——翻译不打乱任何两个序数的先后）<ref name="kleene1938">'''Kleene, S. C. (1938).''' On notation for ordinal numbers. ''The Journal of Symbolic Logic'', 3(4), 150–155.【第二递归定理的原始出处，定理与证明见 p.153】</ref><ref name="rogers1967" />。
'''证明的思路'''（这是"有效超限递归"的范式，值得细看）：想要的翻译函数 <math>\psi</math> 应该满足
'''证明的思路'''（这是"有效超限递归"的范式，值得细看）：想要的翻译函数 <math>\psi</math> 应该满足
* '''代码的层面（真正的循环）'''：程序 <math>e</math> 要对 <math>x_n</math> 运行 <math>\psi</math>，就必须'''在自己的代码里写死 <math>\psi</math> 的程序编号'''——而 <math>\psi</math> 此刻还在定义中。也就是说，想定义 <math>\psi</math>，得先造出一个"代码里引用了 <math>\psi</math> 的编号"的程序。这正是"右边出现了正在定义的 <math>\psi</math> 自己（及其编号）"的所指；这类循环在普通数学里非法。
* '''代码的层面（真正的循环）'''：程序 <math>e</math> 要对 <math>x_n</math> 运行 <math>\psi</math>，就必须'''在自己的代码里写死 <math>\psi</math> 的程序编号'''——而 <math>\psi</math> 此刻还在定义中。也就是说，想定义 <math>\psi</math>，得先造出一个"代码里引用了 <math>\psi</math> 的编号"的程序。这正是"右边出现了正在定义的 <math>\psi</math> 自己（及其编号）"的所指；这类循环在普通数学里非法。
SRT 恰好合法化它：先用 s-m-n 定理（§2.3）造一个可计算函数 <math>q(x, d)</math>——给定 <math>\psi</math> 的编号 <math>d</math>，机械地吐出"读 <math>n</math>、取 <math>x_n</math>、运行程序 <math>d</math>"那个程序的编号。于是想求的 <math>\psi</math> 满足：<math>\psi(x) = 3\cdot5^e</math>，其中 <math>e = q(x, d)</math>，而 <math>d</math> 正是 <math>\psi</math> 自己的编号。把右边整体看作 <math>d</math> 的函数、套 SRT 取不动点 <math>c</math>，令 <math>\psi = \phi_c</math>，循环即闭合；再沿序数归纳验证 <math>\psi</math> 确实是'''全函数'''（"全"：对每个输入代号都有输出，见 §2.1）且保序<ref name="kleene1938" />。
SRT 恰好合法化它：先用 s-m-n 定理（[[#s-m-n 定理（柯里化 / 参数特化）|§2.3]]）造一个可计算函数 <math>q(x, d)</math>——给定 <math>\psi</math> 的编号 <math>d</math>，机械地吐出"读 <math>n</math>、取 <math>x_n</math>、运行程序 <math>d</math>"那个程序的编号。于是想求的 <math>\psi</math> 满足：<math>\psi(x) = 3\cdot5^e</math>，其中 <math>e = q(x, d)</math>，而 <math>d</math> 正是 <math>\psi</math> 自己的编号。把右边整体看作 <math>d</math> 的函数、套 SRT 取不动点 <math>c</math>，令 <math>\psi = \phi_c</math>，循环即闭合；再沿序数归纳验证 <math>\psi</math> 确实是'''全函数'''（"全"：对每个输入代号都有输出，见 [[#"可计算"与"部分函数"|§2.1]]）且保序<ref name="kleene1938" />。
顺带分辨两行的差异：第二行 <math>\psi(x) = 2^\psi(P(x))</math> 是'''值依赖值'''的循环，且 <math>P(x)</math> 指向更小的序数，本质上是良基的（"良基"：不存在无穷下降链，所以"沿序数从小到大做归纳"是合法的）；第三行则是'''编号依赖编号'''的循环（<math>e</math> 的代码里嵌着 <math>\psi</math> 的编号），良基性救不了它——必须 SRT。
顺带分辨两行的差异：第二行 <math>\psi(x) = 2^\psi(P(x))</math> 是'''值依赖值'''的循环，且 <math>P(x)</math> 指向更小的序数，本质上是良基的（"良基"：不存在无穷下降链，所以"沿序数从小到大做归纳"是合法的）；第三行则是'''编号依赖编号'''的循环（<math>e</math> 的代码里嵌着 <math>\psi</math> 的编号），良基性救不了它——必须 SRT。
=== 构造序数 = 递归序数 ===
=== 构造序数 = 递归序数 ===
可数序数有两种自然刻画："'''构造序数'''"（能被某个机械记号系统命名，见 6.1）与"'''递归序数'''"（某个可计算良序的长度——即存在一个可计算的大小关系，把一堆自然数排成该长度的"无限队列"）。
可数序数有两种自然刻画："'''构造序数'''"（能被某个机械记号系统命名，见 [[#6.1|6.1]]）与"'''递归序数'''"（某个可计算良序的长度——即存在一个可计算的大小关系，把一堆自然数排成该长度的"无限队列"）。
* '''Markwald–Spector 定理（1954/1955）'''：两种刻画恰好等价——构造序数 ⟺ [[递归序数]]<ref name="rogers1967" /><ref name="moschovakis2010" />。
* '''Markwald–Spector 定理（1954/1955）'''：两种刻画恰好等价——构造序数 ⟺ [[递归序数]]<ref name="rogers1967" /><ref name="moschovakis2010" />。
'''[[神谕]]（oracle）'''：给程序外接一块只读"数据库"——集合 A。程序运行中可随时查询"数 n 是否属于 A"并立即得到正确答案。这样的 A 称为神谕；"以 A 为神谕可计算"衡量的是：'''若把 A 白送给你，你还能多算出什么'''。
'''[[神谕]]（oracle）'''：给程序外接一块只读"数据库"——集合 A。程序运行中可随时查询"数 n 是否属于 A"并立即得到正确答案。这样的 A 称为神谕；"以 A 为神谕可计算"衡量的是：'''若把 A 白送给你，你还能多算出什么'''。
'''[[Turing跳跃]]（Turing jump）'''：对任何集合 A，把"哪些以 A 为神谕的程序会停机"这一问题本身收集成一个集合，记作 A′（读作"A 撇"）。可以证明：A′ 以 A 为神谕仍不可计算——每跳一次，都得到一个严格更难的"相对版停机问题"。特别地，从空集 <math>\emptyset</math> 出发跳一次得到的 <math>\emptyset'</math>，正是通常意义下的停机问题（5.7.3）。
'''[[Turing跳跃]]（Turing jump）'''：对任何集合 A，把"哪些以 A 为神谕的程序会停机"这一问题本身收集成一个集合，记作 A′（读作"A 撇"）。可以证明：A′ 以 A 为神谕仍不可计算——每跳一次，都得到一个严格更难的"相对版停机问题"。特别地，从空集 <math>\emptyset</math> 出发跳一次得到的 <math>\emptyset'</math>，正是通常意义下的停机问题（[[#图灵停机问题（1936）|5.7.3]]）。
'''沿构造序数"盖楼"'''：现在从 <math>H_0 = \emptyset</math> 出发，沿构造序数（见 6.1）逐层往上盖：
'''沿构造序数"盖楼"'''：现在从 <math>H_0 = \emptyset</math> 出发，沿构造序数（见 [[#6.1|6.1]]）逐层往上盖：
: <math>H_{\alpha+1}</math> = (<math>H_\alpha</math>)′ （后继层：再跳一次，复杂度升一级）
: <math>H_{\alpha+1}</math> = (<math>H_\alpha</math>)′ （后继层：再跳一次，复杂度升一级）
: <math>H_\lambda = \cup_n H_{\lambda_n}</math> （极限层：把下面各层沿一条可计算上升的序列 <math>\lambda_0 < \lambda_1 < \lambda_2 < \ldots</math> 并起来——'''沿哪条序列取并由 <math>\lambda</math> 的代号给出'''，6.1 里"记号携带程序编号"的约定在此派上用场）
: <math>H_\lambda = \cup_n H_{\lambda_n}</math> （极限层：把下面各层沿一条可计算上升的序列 <math>\lambda_0 < \lambda_1 < \lambda_2 < \ldots</math> 并起来——'''沿哪条序列取并由 <math>\lambda</math> 的代号给出'''，[[#6.1|6.1]] 里"记号携带程序编号"的约定在此派上用场）
在某一层 <math>H_\alpha</math> 中可计算的集合，称为'''[[超算术的]]（hyperarithmetical, HYP）'''。这栋楼的前几层串起熟悉的图景：'''只盖有穷多层，得到的恰好是通常的算术层级'''——穷尽一阶算术（量词只作用于自然数）可定义的全部集合；盖到第 <math>\omega</math> 层（<math>\omega</math> 即 6.1 中最小的无穷序数），得到的集合已足以一举判定[[皮亚诺公理]]体系的全部真语句——包括所有皮亚诺公理体系证明不了的真命题（对照 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|6.1]] 中最小的无穷序数），得到的集合已足以一举判定[[皮亚诺公理]]体系的全部真语句——包括所有皮亚诺公理体系证明不了的真命题（对照 [[#哥德尔第一不完备定理（1931）|5.7.4]] 的不完备性）；而楼并不停在这里，它沿构造序数一直盖到 <math>\omega_1^CK</math> 为止。HYP 因此是真正高于算术层级的层级——至于它究竟高到哪一步（恰好等价于一个"二阶量词"的定义能力），正是 [[#6.4|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">Spector, C. (1955). Recursive wellorderings. ''The Journal of Symbolic Logic'', 20, 151–163.</ref><ref name="moschovakis2010" />。
* '''Spector 唯一性定理（1955）'''：不会。<math>H_\alpha</math> 的可计算度只依赖序数 <math>\alpha</math> 本身，与代号选择无关；而且不同代号之间的翻译是一致可计算的<ref name="spector1955">Spector, C. (1955). Recursive wellorderings. ''The Journal of Symbolic Logic'', 20, 151–163.</ref><ref name="moschovakis2010" />。
证明需要同时构造'''两个互相缠绕的函数'''（互相引用对方编号），由双递归定理（见 §5.2 的 [[雷蒙德·斯穆里安|Smullyan]] 版本）合法化——这是有效超限递归技术的高峰之一。Kleene 对这个学生的工作推崇备至，他常讲自己如何"行为不端"地接受它作为博士论文、又作为期刊编辑指定自己为审稿人并立即录用——"非常不合规矩，但我认为最终有利于逻辑！"<ref name="moschovakis2010" />。
证明需要同时构造'''两个互相缠绕的函数'''（互相引用对方编号），由双递归定理（见 [[#推论：SRT 衍生出的若干重要结果|§5.2]] 的 [[雷蒙德·斯穆里安|Smullyan]] 版本）合法化——这是有效超限递归技术的高峰之一。Kleene 对这个学生的工作推崇备至，他常讲自己如何"行为不端"地接受它作为博士论文、又作为期刊编辑指定自己为审稿人并立即录用——"非常不合规矩，但我认为最终有利于逻辑！"<ref name="moschovakis2010" />。
=== <math>HYP = \Delta^1_1</math> 与有效描述集合论 ===
=== <math>HYP = \Delta^1_1</math> 与有效描述集合论 ===
{{Anchor|6.4}}
'''背景'''：在自然数的集合（数学分析的对象）上，可以用"二阶量化"分层：<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> 是"两面都可定义"的集合——可类比为分析学中"既可开逼近又可闭逼近"的集合。
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" />。
=== r.e. 索引集理论：Rice、Rice-Shapiro 与 Myhill ===
=== r.e. 索引集理论：Rice、Rice-Shapiro 与 Myhill ===
本板块把"程序行为性质"当作一个独立的研究对象。核心概念是'''索引集（index set）'''：给定某类程序行为，把"行为落在这类里"的全部程序编号收集起来，就得到 <math>\mathbb{N}</math> 的一个子集。若用程序 e 的定义域 <math>W_e</math>（§2.4）来编码行为、用 <math>\mathcal{A}</math> 表示某类 r.e. 集，则写法是
本板块把"程序行为性质"当作一个独立的研究对象。核心概念是'''索引集（index set）'''：给定某类程序行为，把"行为落在这类里"的全部程序编号收集起来，就得到 <math>\mathbb{N}</math> 的一个子集。若用程序 e 的定义域 <math>W_e</math>（[[#递归可枚举集（r.e. set）|§2.4]]）来编码行为、用 <math>\mathcal{A}</math> 表示某类 r.e. 集，则写法是
: <math>A = \{ e : W_e \in \mathcal{A}\}</math>
: <math>A = \{ e : W_e \in \mathcal{A}\}</math>
（换成函数视角就是 <math>A = { e : \phi_e</math> 具有性质 <math>\mathcal{A}\}</math> 。）可判定、可枚举这类词只能作用于自然数集合，索引集正是那道翻译层——它把"程序行为问题"转写成 <math>\mathbb{N}</math> 的子集，之后才能问"这个性质能判定吗、能枚举吗"。两个要点：其一，此类性质必须'''只看行为、不看代码'''（同一函数的两个不同编号在 A 中必须同真同假），否则退化为平凡的代码分析。
（换成函数视角就是 <math>A = { e : \phi_e</math> 具有性质 <math>\mathcal{A}\}</math> 。）可判定、可枚举这类词只能作用于自然数集合，索引集正是那道翻译层——它把"程序行为问题"转写成 <math>\mathbb{N}</math> 的子集，之后才能问"这个性质能判定吗、能枚举吗"。两个要点：其一，此类性质必须'''只看行为、不看代码'''（同一函数的两个不同编号在 A 中必须同真同假），否则退化为平凡的代码分析。
与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 6.5.3）；'''Rice 与 Rice-Shapiro 不是 SRT 的推论'''——它们的标准证明分别是停机归约（对角线矛盾）与有限集/紧致性论证，全程不需要 SRT，SRT 至多给 Rice 提供一条事后捷径。也就是说，Rice 家族与 SRT"同源，但独立"：共享对角线血统，却不靠 SRT 的代码不动点力量成立。Rice 家族因此不宜与双递归定理等并列在 §5.2 的"推论"名义之下；本文把它们放在本板块，与 Myhill 定理并置，正是为了并排呈现"独立成立"与"依赖 SRT"这两种截然不同的关系。
与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 [[#Myhill定理：创造集 = 完备集|6.5.3]]）；'''Rice 与 Rice-Shapiro 不是 SRT 的推论'''——它们的标准证明分别是停机归约（对角线矛盾）与有限集/紧致性论证，全程不需要 SRT，SRT 至多给 Rice 提供一条事后捷径。也就是说，Rice 家族与 SRT"同源，但独立"：共享对角线血统，却不靠 SRT 的代码不动点力量成立。Rice 家族因此不宜与双递归定理等并列在 [[#推论：SRT 衍生出的若干重要结果|§5.2]] 的"推论"名义之下；本文把它们放在本板块，与 Myhill 定理并置，正是为了并排呈现"独立成立"与"依赖 SRT"这两种截然不同的关系。
==== [[Rice定理]]（1951） ====
==== [[Rice定理]]（1951） ====
* '''证明思路（停机归约——教科书标准路线，不依赖 SRT）'''：
* '''证明思路（停机归约——教科书标准路线，不依赖 SRT）'''：
# 取一个"见证"函数 <math>\phi_a \in \mathcal{A}</math>。若处处无定义的函数恰好也在 <math>\mathcal{A}</math> 中，就对"补性质"（行为不在 <math>\mathcal{A}</math> 中）重做一遍论证——两类情况完全对称，故以下不妨设"恒发散"<math>\notin \mathcal{A}</math>；
# 取一个"见证"函数 <math>\phi_a \in \mathcal{A}</math>。若处处无定义的函数恰好也在 <math>\mathcal{A}</math> 中，就对"补性质"（行为不在 <math>\mathcal{A}</math> 中）重做一遍论证——两类情况完全对称，故以下不妨设"恒发散"<math>\notin \mathcal{A}</math>；
# 对每个 <math>x</math>，用 s-m-n 定理（§2.3）机械地造一个程序 <math>h(x)</math>：它先模拟"程序 <math>x</math> 在输入 <math>x</math> 上"的运行——这一步是对角线（让 <math>x</math> 面对自己的行为）；一旦该模拟停机，<math>h(x)</math> 就转而执行程序 <math>a</math>；若模拟永不停机，<math>h(x)</math> 也永不停机；
# 对每个 <math>x</math>，用 s-m-n 定理（[[#s-m-n 定理（柯里化 / 参数特化）|§2.3]]）机械地造一个程序 <math>h(x)</math>：它先模拟"程序 <math>x</math> 在输入 <math>x</math> 上"的运行——这一步是对角线（让 <math>x</math> 面对自己的行为）；一旦该模拟停机，<math>h(x)</math> 就转而执行程序 <math>a</math>；若模拟永不停机，<math>h(x)</math> 也永不停机；
# 于是 <math>x</math> 停在自己的输入上 ⟺ <math>h(x)</math> 计算的是 <math>\phi_a</math>（<math>\in \mathcal{A}</math>）⟺ <math>h(x) \in A</math>。若 <math>A</math> 可计算，就能机械判定"<math>x</math> 是否停在 <math>x</math> 上"，停机问题被解决——矛盾（§5.7.3）。
# 于是 <math>x</math> 停在自己的输入上 ⟺ <math>h(x)</math> 计算的是 <math>\phi_a</math>（<math>\in \mathcal{A}</math>）⟺ <math>h(x) \in A</math>。若 <math>A</math> 可计算，就能机械判定"<math>x</math> 是否停在 <math>x</math> 上"，停机问题被解决——矛盾（[[#图灵停机问题（1936）|§5.7.3]]）。
* 直觉：任何非平凡的"行为分类"都把停机问题吸收为自己内部的一个子问题——你若想机械地给每个程序的行为贴标签，就不得不先回答"程序 <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 定理原始论文】【§6.5.1】</ref>.
* 直觉：任何非平凡的"行为分类"都把停机问题吸收为自己内部的一个子问题——你若想机械地给每个程序的行为贴标签，就不得不先回答"程序 <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 定理原始论文】【§6.5.1】</ref>.
# '''简单性与普适性的反差'''。SRT 的全部证明只有一行对角线，应用却横跨逻辑学几乎所有分支。Moschovakis 指出：其广泛适用性恰恰'''源于'''这种简单——它极易被翻译到自然数以外的语境（实数空间、任意 Polish 空间、高类型对象、模态逻辑），在每个语境中重新化身<ref name="moschovakis2010" />。
# '''简单性与普适性的反差'''。SRT 的全部证明只有一行对角线，应用却横跨逻辑学几乎所有分支。Moschovakis 指出：其广泛适用性恰恰'''源于'''这种简单——它极易被翻译到自然数以外的语境（实数空间、任意 Polish 空间、高类型对象、模态逻辑），在每个语境中重新化身<ref name="moschovakis2010" />。
# '''两个递归定理的分工'''。第一递归定理保证'''递归定义有最小解'''（函数层面、序理论的不动点）；第二递归定理保证'''自指定义合法'''（代码层面的不动点）。前者回答"这个函数方程有解吗"，后者回答"我能在定义中引用被定义者自己的代码吗"。强定理蕴含弱定理，反之不然（见 4.4）。
# '''两个递归定理的分工'''。第一递归定理保证'''递归定义有最小解'''（函数层面、序理论的不动点）；第二递归定理保证'''自指定义合法'''（代码层面的不动点）。前者回答"这个函数方程有解吗"，后者回答"我能在定义中引用被定义者自己的代码吗"。强定理蕴含弱定理，反之不然（见 [[#与第二递归定理的关系|4.4]]）。
# '''自指的数学化'''。从 Gödel 的替换函数、Turing 的通用机、von Neumann 的自复制自动机，到 quine、计算机病毒、编译器自举，乃至人工智能中"系统改进自身"的设想，"系统谈论自身"的可行性边界都由同一种对角线结构划定。Kleene 递归定理是这一结构最干净、最一般的陈述。
# '''自指的数学化'''。从 Gödel 的替换函数、Turing 的通用机、von Neumann 的自复制自动机，到 quine、计算机病毒、编译器自举，乃至人工智能中"系统改进自身"的设想，"系统谈论自身"的可行性边界都由同一种对角线结构划定。Kleene 递归定理是这一结构最干净、最一般的陈述。
# '''历史反讽'''。Kleene 1938 年发明 SRT 是为了构造序数记号，而 1944 年他恰恰因为"拿到一个不动点却误以为拿到最小不动点"而犯下著名错误，直到 1955 年才纠正（见 3.3）——这个故事最恰当地说明了理解两个递归定理'''区别'''的重要性。
# '''历史反讽'''。Kleene 1938 年发明 SRT 是为了构造序数记号，而 1944 年他恰恰因为"拿到一个不动点却误以为拿到最小不动点"而犯下著名错误，直到 1955 年才纠正（见 [[#一个值得铭记的教训|3.3]]）——这个故事最恰当地说明了理解两个递归定理'''区别'''的重要性。
# '''Rogers 的总评'''：递归定理是"一个基本的研究工具、一个深刻的结果"（a basic research tool <math>\ldots</math> a deep result），它的深刻在于"以优雅和智识上的经济性，处理那些否则需要繁复构造的问题"<ref name="rogers1967" />；虽然它的直接效果常是产生各种"病态"结构（自我枚举的集合、自我打印的程序），但它在 Myhill 定理等结果中起到了"在此前独立定义的概念之间建立正则联系"的作用<ref name="rogers1967" />。
# '''Rogers 的总评'''：递归定理是"一个基本的研究工具、一个深刻的结果"（a basic research tool <math>\ldots</math> a deep result），它的深刻在于"以优雅和智识上的经济性，处理那些否则需要繁复构造的问题"<ref name="rogers1967" />；虽然它的直接效果常是产生各种"病态"结构（自我枚举的集合、自我打印的程序），但它在 Myhill 定理等结果中起到了"在此前独立定义的概念之间建立正则联系"的作用<ref name="rogers1967" />。
<references />
<references />