更改

|-

|-

| '''首次出现'''

| '''首次出现'''

| Kleene (1952)《元数学导论》中明确表述<ref name="moschovakis2010" />

| Kleene (1952)《元数学导论》中明确表述<ref name="kleene1952">Kleene, S. C. (1952). ''Introduction to Metamathematics''. D. Van Nostrand.【第一递归定理的明确表述】</ref><ref name="moschovakis2010" />

| Kleene (1938) §2 末尾，当时甚至没有名字，证明只有两行<ref name="kleene1938" />

| Kleene (1938) §2 末尾，当时甚至没有名字，证明只有两行<ref name="kleene1938" />

|}

|}

==== 图灵停机问题（1936） ====

==== 图灵停机问题（1936） ====

'''现象'''：不存在算法 <math>H</math> 能判定"任意程序 <math>e</math> 在任意输入 <math>x</math> 上是否会停机"。这是可计算性理论第一个、也是最著名的"不可判定"结果。<ref name="turing1936" />

'''现象'''：不存在算法 <math>H</math> 能判定"任意程序 <math>e</math> 在任意输入 <math>x</math> 上是否会停机"。这是可计算性理论第一个、也是最著名的"不可判定"结果<ref name="turing1936">'''Turing, A. M. (1936).''' On computable numbers, with an application to the Entscheidungsproblem. ''Proceedings of the London Mathematical Society'', 42, 230–265.【停机问题不可判定】</ref>.

'''双重身份'''：停机不可判定在'''结论性质'''上是否定性的（证明"判定器不存在"），与康托尔、罗素问题同类；但因为它活在"程序"世界，'''又能被 SRT 推出'''。下面展示完整的"套用"过程——这是所有例子里最干净的一个，最能看清 SRT 到底在哪里发力。

'''双重身份'''：停机不可判定在'''结论性质'''上是否定性的（证明"判定器不存在"），与康托尔、罗素问题同类；但因为它活在"程序"世界，'''又能被 SRT 推出'''。下面展示完整的"套用"过程——这是所有例子里最干净的一个，最能看清 SRT 到底在哪里发力。

==== 哥德尔第一不完备定理（1931） ====

==== 哥德尔第一不完备定理（1931） ====

'''现象'''：任何"足够强"的一致可公理化理论 <math>T</math>（例如 [[皮亚诺公理|Peano 算术]]，简写为PA）都不完备：存在一个句子 <math>\sigma</math>，使 <math>T</math> 既证不出 <math>\sigma</math>、也证不出 <math>\neg\sigma</math><ref name="godel1931" />。

'''现象'''：任何"足够强"的一致可公理化理论 <math>T</math>（例如 [[皮亚诺公理|Peano 算术]]，简写为PA）都不完备：存在一个句子 <math>\sigma</math>，使 <math>T</math> 既证不出 <math>\sigma</math>、也证不出 <math>\neg\sigma</math><ref name="godel1931">'''Gödel, K. (1931).''' Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. ''Monatshefte für Mathematik und Physik'', 38, 173–198.【Gödel 不完备定理（Gödel 不动点引理是其核心证明工具，见 §5.6.1）】【§5.7.4】</ref>。

'''术语——皮亚诺算术（PA）与 [[罗宾孙算术]]（Q）'''：'''PA''' 是 '''Peano 算术（Peano Arithmetic）'''的缩写，是'''一阶算术的标准公理系统'''，用于形式化刻画自然数（<math>0, 1, 2, \ldots</math>）及其加法、乘法。它由意大利数学家皮亚诺（G. Peano（1889））的公理发展而来，包含：①常元 0；②后继运算 <math>S</math>（每个数有唯一后继，0 不是任何数的后继，后继相同则原数相同）；③加法、乘法的递归定义；④'''归纳公理模式'''（induction schema：对任何一阶公式 <math>\phi</math>，若 <math>\phi(0)</math> 成立、且 <math>\phi(n) \Rightarrow \phi(n+1)</math>，则 <math>\phi</math> 对一切自然数成立）。PA 是哥德尔不完备定理的典型对象——它足够强（能在内部编码所有初等数论），又是可公理化的一致理论。而 '''Q（[[罗宾孙算术]]）'''是皮亚诺算术的一个'''弱化'''：保留①—③、去掉归纳公理模式，只留极有限的几条公理，是"足以推出不完备定理的最弱理论"之一（后文 [[Myhill定理]]即用它）。

'''术语——皮亚诺算术（PA）与 [[罗宾孙算术]]（Q）'''：'''PA''' 是 '''Peano 算术（Peano Arithmetic）'''的缩写，是'''一阶算术的标准公理系统'''，用于形式化刻画自然数（<math>0, 1, 2, \ldots</math>）及其加法、乘法。它由意大利数学家皮亚诺（G. Peano（1889））的公理发展而来，包含：①常元 0；②后继运算 <math>S</math>（每个数有唯一后继，0 不是任何数的后继，后继相同则原数相同）；③加法、乘法的递归定义；④'''归纳公理模式'''（induction schema：对任何一阶公式 <math>\phi</math>，若 <math>\phi(0)</math> 成立、且 <math>\phi(n) \Rightarrow \phi(n+1)</math>，则 <math>\phi</math> 对一切自然数成立）。PA 是哥德尔不完备定理的典型对象——它足够强（能在内部编码所有初等数论），又是可公理化的一致理论。而 '''Q（[[罗宾孙算术]]）'''是皮亚诺算术的一个'''弱化'''：保留①—③、去掉归纳公理模式，只留极有限的几条公理，是"足以推出不完备定理的最弱理论"之一（后文 [[Myhill定理]]即用它）。

==== [[冯诺伊曼]]的[[自复制自动机]]（1948） ====

==== [[冯诺伊曼]]的[[自复制自动机]]（1948） ====

'''现象'''：存在能在物理上[[自复制自动机]]。[[冯诺伊曼]]在[[洛斯阿拉莫斯实验室]]设计的自动机方案含四部分：'''通用构造器 A'''（读入一段指令，构造出该指令描述的任何机器）、'''通用拷贝器 B'''（复制指令）、'''控制器 C'''（指挥 A 与 B 协同运作、并把指令传给新机器）、以及一段描述 A、B、C 三者如何组合的'''蓝图'''（即指令带）；机器 M<math> = \langle</math> A, B, C, 蓝图<math>\rangle</math> 启动后能造出 M 自己的副本<ref name="vonneumann1966" /><ref name="lee1963" />。

'''现象'''：存在能在物理上[[自复制自动机]]。[[冯诺伊曼]]在[[洛斯阿拉莫斯实验室]]设计的自动机方案含四部分：'''通用构造器 A'''（读入一段指令，构造出该指令描述的任何机器）、'''通用拷贝器 B'''（复制指令）、'''控制器 C'''（指挥 A 与 B 协同运作、并把指令传给新机器）、以及一段描述 A、B、C 三者如何组合的'''蓝图'''（即指令带）；机器 M<math> = \langle</math> A, B, C, 蓝图<math>\rangle</math> 启动后能造出 M 自己的副本<ref name="vonneumann1966">'''von Neumann, J. (1966).''' ''Theory of Self-Reproducing Automata'' (A. W. Burks 编). University of Illinois Press.【自复制自动机的奠基性设计（原稿始于 1948）】【§5.7.5】</ref><ref name="lee1963" />。

'''SRT 如何推出它'''：

'''SRT 如何推出它'''：

'''定理（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" /><ref name="rogers1967" />。

'''定理（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" />。

'''证明的思路'''（这是"有效超限递归"的范式，值得细看）：想要的翻译函数 <math>\psi</math> 应该满足

'''证明的思路'''（这是"有效超限递归"的范式，值得细看）：想要的翻译函数 <math>\psi</math> 应该满足