3,094
个编辑
更改
无编辑摘要
推广到 <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）|双递归定理]]是后续许多重要构造的核心：① [[#超算术层级与 Spector 唯一性定理|§5.8.3]] 介绍的"两层超算术构造"里，[[克利福德·斯佩克特|Spector]] 定理需要同时构造两个互相缠绕的函数；② [[Myhill-Shepherdson 定理]]（[[#有效运算的连续性：Myhill–Shepherdson 与 KLS–Čeĭnin 定理|§5.8.6]] 简述）描述"如何用 r.e. 集作为其它 r.e. 集的有效操作"时也需要联立不动点；③ 某些停机问题的"相对化"证明也走双递归路线<ref name="smullyan1961">'''Smullyan, R. M. (1961).''' ''Theory of Formal Systems''. Princeton University Press.【双递归定理的提出者；§[[#Smullyan 双递归定理（1959, 1961）|5.2.1]]】</ref><ref name="rogers1967" />.
[[#Smullyan 双递归定理（1959, 1961）|双递归定理]]是后续许多重要构造的核心：① [[#超算术层级与 Spector 唯一性定理|§5.8.3]] 介绍的"两层超算术构造"里，[[克利福德·斯佩克特|Spector]] 定理需要同时构造两个互相缠绕的函数；② [[Myhill-Shepherdson 定理]]（[[#有效运算的连续性：Myhill–Shepherdson 与 KLS–Čeĭnin 定理|§5.8.6]] 简述）描述"如何用 r.e. 集作为其它 r.e. 集的有效操作"时也需要联立不动点；③ 某些停机问题的"相对化"证明也走双递归路线<ref name="smullyan1961">'''Smullyan, R. M. (1961).''' ''Theory of Formal Systems''. Princeton University Press.【双递归定理的提出者；§[[#Smullyan 双递归定理（1959, 1961）|5.5.1]]】</ref><ref name="rogers1967" />.
另外，值得一提的是，这个双递归定理以及对应的n递归定理的推广形式，实际上可以看成是多个部分互相指涉，互相依赖的形式，因此也就构成了[[自创生理论]]（Autopoesis）的数学基础。
另外，值得一提的是，这个双递归定理以及对应的n递归定理的推广形式，实际上可以看成是多个部分互相指涉，互相依赖的形式，因此也就构成了[[自创生理论]]（Autopoesis）的数学基础。
直觉上：[[R. R. Arslanov|Arslanov]] 判据说"装得下所有 r.e. 集合"等价于"对每个 r.e. 集合都有机械的相对化方式"——这和 SRT 中"对每个全可计算 <math>f</math> 都给出一个不动点"的相对化版本（relativized SRT）说的是同一件事：SRT 的相对化是说"对每个以 <math>C</math> 为'''神谕'''（oracle）可计算的 <math>f</math>，存在不动点 <math>c</math>"；Arslanov 判据说"对每个 <math>W</math>，存在以 <math>C</math> 为[[谕示机|神谕]]可计算的归约"。
直觉上：[[R. R. Arslanov|Arslanov]] 判据说"装得下所有 r.e. 集合"等价于"对每个 r.e. 集合都有机械的相对化方式"——这和 SRT 中"对每个全可计算 <math>f</math> 都给出一个不动点"的相对化版本（relativized SRT）说的是同一件事：SRT 的相对化是说"对每个以 <math>C</math> 为'''神谕'''（oracle）可计算的 <math>f</math>，存在不动点 <math>c</math>"；Arslanov 判据说"对每个 <math>W</math>，存在以 <math>C</math> 为[[谕示机|神谕]]可计算的归约"。
[[Arslanov 判据]]在[[递归论]]里是教科书级工具：①用于证明 Gödel 不完备定理的算术陈述（"[[PA不一致]]"这种陈述）的相对可计算性与停机问题同构；② 用于证明某些 r.e. 集"不可能被简化"<ref name="arslanov1981">'''Arslanov, R. R. (1981).''' On a class of recursively enumerable sets. ''Algebra and Logic'', 20, 324–328.【Arslanov 完全性判据】【§[[#Arslanov 完全性判据（1981）|5.2.3]]】</ref><ref name="soare1987">'''Soare, R. I. (1987).''' ''Recursively Enumerable Sets and Degrees: A Study of Computable Functions and Computably Generated Sets''. Berlin: Springer-Verlag.【r.e. 集与图灵度的标准教科书；Arslanov 完备性判据（§[[#Arslanov 完全性判据（1981）|5.2.3]]）与 Rice–Shapiro 等索引集定理（§[[#r.e. 索引集理论：Rice、Rice-Shapiro 与 Myhill|5.8.5]]）的教科书出处】</ref>
[[Arslanov 判据]]在[[递归论]]里是教科书级工具：①用于证明 Gödel 不完备定理的算术陈述（"[[PA不一致]]"这种陈述）的相对可计算性与停机问题同构；② 用于证明某些 r.e. 集"不可能被简化"<ref name="arslanov1981">'''Arslanov, R. R. (1981).''' On a class of recursively enumerable sets. ''Algebra and Logic'', 20, 324–328.【Arslanov 完全性判据】【§[[#Arslanov 完全性判据（1981）|5.5.3]]】</ref><ref name="soare1987">'''Soare, R. I. (1987).''' ''Recursively Enumerable Sets and Degrees: A Study of Computable Functions and Computably Generated Sets''. Berlin: Springer-Verlag.【r.e. 集与图灵度的标准教科书；Arslanov 完备性判据（§[[#Arslanov 完全性判据（1981）|5.5.3]]）与 Rice–Shapiro 等索引集定理（§[[#r.e. 索引集理论：Rice、Rice-Shapiro 与 Myhill|5.8.5]]）的教科书出处】</ref>
。
。
=== 与其它不动点定理的关系 ===
=== 与其它不动点定理的关系 ===
SRT 衍生出许多重要推论（见 [[#推论：SRT 衍生出的若干重要结果|§5.2]]），但还有些定理与 SRT 的关系'''更微妙'''——它们与 SRT '''同源'''（都基于对角线 / 自指），却走的是独立证明路线，或者处于更高层的[[范畴论]]概括下。这里集中讨论两个最重要的"不动点定理"：Gödel 的[[不动点引理]]与 [[F. William Lawvere|Lawvere]] 的范畴论不动点定理，重点说明 SRT 与它们的精确定位关系。
SRT 衍生出许多重要推论（见 [[#推论：SRT 衍生出的若干重要结果|§5.5]]），但还有些定理与 SRT 的关系'''更微妙'''——它们与 SRT '''同源'''（都基于对角线 / 自指），却走的是独立证明路线，或者处于更高层的[[范畴论]]概括下。这里集中讨论两个最重要的"不动点定理"：Gödel 的[[不动点引理]]与 [[F. William Lawvere|Lawvere]] 的范畴论不动点定理，重点说明 SRT 与它们的精确定位关系。
==== Gödel 不动点引理（对角引理） ====
==== Gödel 不动点引理（对角引理） ====
* '''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" />。
证明需要同时构造'''两个互相缠绕的函数'''（互相引用对方编号），由双递归定理（见 [[#推论：SRT 衍生出的若干重要结果|§5.2]] 的 [[雷蒙德·斯穆里安|Smullyan]] 版本）合法化——这是有效超限递归技术的高峰之一。Kleene 对这个学生的工作推崇备至，他常讲自己如何"行为不端"地接受它作为博士论文、又作为期刊编辑指定自己为审稿人并立即录用——"非常不合规矩，但我认为最终有利于逻辑！"<ref name="moschovakis2010" />。
证明需要同时构造'''两个互相缠绕的函数'''（互相引用对方编号），由双递归定理（见 [[#推论：SRT 衍生出的若干重要结果|§5.5]] 的 [[雷蒙德·斯穆里安|Smullyan]] 版本）合法化——这是有效超限递归技术的高峰之一。Kleene 对这个学生的工作推崇备至，他常讲自己如何"行为不端"地接受它作为博士论文、又作为期刊编辑指定自己为审稿人并立即录用——"非常不合规矩，但我认为最终有利于逻辑！"<ref name="moschovakis2010" />。
==== 超算术集与有效描述集合论 ====
==== 超算术集与有效描述集合论 ====