更改

* '''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.5]] 的 [[雷蒙德·斯穆里安|Smullyan]] 版本）合法化——这是有效超限递归技术的高峰之一。Kleene 对这个学生的工作推崇备至，他常讲自己如何"行为不端"地接受它作为博士论文、又作为期刊编辑指定自己为审稿人并立即录用——"非常不合规矩，但我认为最终有利于逻辑学！"<ref name="moschovakis2010" />。

证明需要同时构造'''两个互相缠绕的函数'''（互相引用对方编号），由双递归定理（见 [[#推论：SRT 衍生出的若干重要结果|§5.5]] 的 [[雷蒙德·斯穆里安|Smullyan]] 版本）合法化——这是有效超限递归技术的高峰之一。Kleene 对这个学生的工作推崇备至，他常讲自己如何"行为不端"地接受它作为博士论文、又作为期刊编辑指定自己为审稿人并立即录用——"这非常不合规矩，但我认为这最终有利于逻辑学！"<ref name="moschovakis2010" />。

==== 超算术集与有效描述集合论 ====

==== 超算术集与有效描述集合论 ====