更改

关键就在第 3 步：<math>\psi</math> 里用的是参数 <math>z</math>（可以正常定义），SRT 把它换成 <math>f</math> 自己——'''没有 SRT，"<math>\phi_f</math> 的行为取决于 <math>H</math> 对 <math>f</math> 的判决"就是非法循环定义，写不出来'''。SRT 的全部威力，就是把这种循环合法化：你只管把"自己"写成参数，存在性交给定理<ref name="moschovakis2010" /><ref name="rogers1967" />。

关键就在第 3 步：<math>\psi</math> 里用的是参数 <math>z</math>（可以正常定义），SRT 把它换成 <math>f</math> 自己——'''没有 SRT，"<math>\phi_f</math> 的行为取决于 <math>H</math> 对 <math>f</math> 的判决"就是非法循环定义，写不出来'''。SRT 的全部威力，就是把这种循环合法化：你只管把"自己"写成参数，存在性交给定理<ref name="moschovakis2010" /><ref name="rogers1967" />。

==== Gödel 第一不完备定理（1931） ====

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

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

'''术语——PA 与 Q'''：'''PA''' 是 '''Peano 算术（Peano Arithmetic）'''&#x7684;缩写，是'''一阶算术的标准公理系统'''，用于形式化刻画自然数（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 算术）'''&#x662F; PA 的一个'''弱化'''：保留①—③、去掉归纳公理模式，只留极有限的几条公理，是"足以推出不完备定理的最弱理论"之一（后文 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定理]]即用它）。

'''双重身份'''：与停机问题一样，Gödel 不完备在结论上是否定性的（证明"完备一致的理论不存在"）；Gödel 1931 的原证走的是 Cantor/Russell 的否定性对角线老路、'''并不依赖 SRT'''。但因为它活在"形式系统可证性"这一可计算世界，事后也能被 SRT 干净地推出。核心是'''不动点引理（Fixed Point Lemma）'''，它是 SRT 最纯粹形式的直接推论：

'''双重身份'''：与停机问题一样，哥德尔不完备在结论上是否定性的（证明"完备一致的理论不存在"）；哥德尔在1931的原证明走的是康托尔/罗素的否定性对角线老路、'''并不依赖 SRT'''。但因为它活在"形式系统可证性"这一可计算的世界，事后也能被 SRT 干净地推出。核心是'''不动点引理（Fixed Point Lemma）'''，它是 SRT 最纯粹形式的直接推论：

> '''不动点引理'''：设 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>T</math> 是任何足够强的可公理化理论，则对任何含一个自由变量的公式 <math>\theta(v)</math>，都存在句子 <math>\sigma</math>，使 <math>T</math> 可证 "<math>\sigma\iff\theta</math>(⌜<math>\sigma</math>⌝)"（⌜<math>\sigma</math>⌝ 是 <math>\sigma</math> 的哥德尔数）。即：'''任何性质 <math>\theta</math>，都存在一个句子 <math>\sigma</math>，在 <math>T</math> 可证的意义下恰好谈论"自己是否具有 <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> 换成 [[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 的任何一致、可公理化扩张 T，其定理集都是'''创造集'''（见 §6.5.3），从而是 r.e.-完备的。<ref name="moschovakis2010" />

* '''[[Myhill定理]]（1955）'''：[[罗宾逊算术]] Q 的任何一致、可公理化扩张 <math>T</math>，其定理集都是'''[[创造集]]'''（见 §6.5.3），从而是 r.e.-完备的<ref name="moschovakis2010" />.

合起来得到一个惊人结论：'''所有'''足够强的一致公理化理论（PA、[[ZFC公理系统]]<math>\ldots</math><math>\ldots</math>）都自动满足不动点引理的条件，因而都不完备、不可判定；而且任意两个这样的理论，其定理集在递归同构意义下完全相同。<ref name="moschovakis2010" />

合起来我们可以得到一个惊人结论：'''所有'''足够强的一致公理化理论（皮亚诺算术、[[ZFC公理系统]]<math>\ldots\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>，存在 <math>n</math> 使 <math>W_n = W_p\cup</math>{⌜<math>W_n</math> 一致⌝}）。但 Gödel '''第二'''不完备定理说明：若 <math>W_p</math> 已含皮亚诺算术，这个"自信"的系统反而不可能一致<ref name="rogers1967" />。

==== von Neumann 自复制自动机（1948） ====

==== von Neumann 自复制自动机（1948） ====