更改

=== 其它形式的第二递归定理 ===

=== 其它形式的第二递归定理 ===

====Uniform 形式====

====Uniform 形式====

'''Uniform不动点定理'''：存在一个全可计算函数<math>r</math>（在标准编号下甚至可以取原始递归的），使得对每一个编号<math>e</math>：

'''Uniform 不动点定理'''：存在一个全可计算函数<math>r</math>（在标准编号下甚至可以取原始递归的），使得对每一个编号<math>e</math>：

:<math>

:<math>

三个要点：

三个要点：

* 输入是在第二递归定理的{{EquationNote|表述A}}中<math>\psi</math>本身的编号。在SRT的所有表述中，<math>\psi</math> 都是“给定的”：表述{{EquationNote|表述A}}对给定的 <math>\psi</math> 断言不动点存在；{{EquationNote|表述C}} 让不动点随参数 <math>u</math> 一致变化。Uniform 版的方向不同——它让不动点随 <math>\psi</math> 的描述（编号) 一致变化：<math>r</math> 是一个“自指编译器”，你喂给它任何一个二元程序的编号，它返回那个让 <math>\phi_e(·,·)</math> 自我指涉的程序编号。

* 该定理的输入<math>e</math>是在第二递归定理的{{EquationNote|表述A}}中<math>\psi</math>本身的编号。在SRT的所有表述中，<math>\psi</math> 都是“给定的”：{{EquationNote|表述A}}对给定的 <math>\psi</math> 断言不动点存在；{{EquationNote|表述C}} 让不动点随参数 <math>y</math> 一致变化。Uniform 版的方向不同——它让不动点随 <math>\psi</math> 的描述（编号) 一致变化：<math>r</math> 是一个“自指编译器”，你喂给它任何一个二元程序的编号，它返回那个让 <math>\phi_e(·,·)</math> 自我指涉的程序编号。

* 无条件的全称命题。注意陈述里没有“若 <math>\phi_e</math> 可计算”之类的前提——对一切 <math>e</math> 都成立。<math>e</math>号程序在 <math>(r(e), x)</math> 上不停机时，两边同时无定义，等式照样成立。这跟“不动点自由的函数必须是不可计算的”（[[#Arslanov 判据|Arslanov 判据]]）是一体两面：<math>r</math> 是全的，所以没有可计算函数能躲开它。

* 无条件的全称命题。注意陈述里没有“若 <math>\phi_e</math> 可计算”之类的前提——对一切 <math>e</math> 都成立。<math>e</math>号程序在 <math>(r(e), x)</math> 上不停机时，两边同时无定义，等式照样成立。这跟“不动点自由的函数必须是不可计算的”（[[#Arslanov 判据|Arslanov 判据]]）是一体两面：<math>r</math> 是全的，所以没有可计算函数能躲开它。

* 构造性到什么程度：把 §[[#证明|5.2]] 展开版证明逐步查一遍——第 0 步用 s-m-n 造 <math>\theta</math> 的编号（原始递归操作），第 2 步 <math>f = S(e,e)</math>（S 原始递归）——每一步都是编号上的原始递归运算。所以复合出来的 <math>e \iff f</math> 就是那个 <math>r</math>，原始递归。这也是为什么说 Kleene 1938/1952 的原始证明“实际上已经是 uniform 的”：证明即算法。

* 该定理的证明如何构造？把 §[[#证明|5.2]] 展开版证明逐步查一遍——第 0 步用 s-m-n 造 <math>\theta</math> 的编号（原始递归操作），第 2 步 <math>f = S(e,e)</math>（S 原始递归）——每一步都是编号上的原始递归运算。所以复合出来的 <math>e \Longrightarrow f</math> 就是那个 <math>r</math>，原始递归。这也是为什么说 Kleene 1938/1952 的原始证明“实际上已经是 uniform 的”：证明即算法。

====Smullyan双递归定理====

====Smullyan双递归定理====