更改

'''[[神谕]]（oracle）'''：给程序外接一块只读"数据库"——集合 A。程序运行中可随时查询"数 n 是否属于 A"并立即得到正确答案。这样的 A 称为神谕；"以 A 为神谕可计算"衡量的是：'''若把 A 白送给你，你还能多算出什么'''。

'''[[神谕]]（oracle）'''：给程序外接一块只读"数据库"——集合 A。程序运行中可随时查询"数 n 是否属于 A"并立即得到正确答案。这样的 A 称为神谕；"以 A 为神谕可计算"衡量的是：'''若把 A 白送给你，你还能多算出什么'''。

'''[[Turing跳跃]]（Turing jump）'''：对任何集合 A，把"哪些以 A 为神谕的程序会停机"这一问题本身收集成一个集合，记作 A′（读作"A 撇"）。可以证明：A′ 以 A 为神谕仍不可计算——每跳一次，都得到一个严格更难的"相对版停机问题"。特别地，从空集 <math>\emptyset</math> 出发跳一次得到的 <math>\emptyset'</math>，正是通常意义下的停机问题（[[#图灵停机问题（1936）|5.7.3]]）。

'''[[图灵跳]]（Turing jump）'''：对任何集合 A，把"哪些以 A 为神谕的程序会停机"这一问题本身收集成一个集合，记作 A′（读作"A 撇"）。可以证明：A′ 以 A 为神谕仍不可计算——每跳一次，都得到一个严格更难的"相对版停机问题"。特别地，从空集 <math>\emptyset</math> 出发跳一次得到的 <math>\emptyset'</math>，正是通常意义下的停机问题（[[#图灵停机问题（1936）|5.7.3]]）。

'''沿构造序数"盖楼"'''：现在从 <math>H_0 = \emptyset</math> 出发，沿构造序数（见 [[#通用序数记号系统ω_1^{CK}|5.8.1]]）逐层往上盖：

'''沿构造序数"盖楼"'''：现在从 <math>H_0 = \emptyset</math> 出发，沿构造序数（见[[#通用序数记号系统ω_1^CK|5.8.1]]）逐层往上盖：

: <math>H_{\alpha+1}</math> = (<math>H_\alpha</math>)′　（后继层：再跳一次，复杂度升一级）   

: <math>H_{\alpha+1}</math> = (<math>H_\alpha</math>)′　（后继层：再跳一次，复杂度升一级）   

: <math>H_\lambda = \cup_n H_{\lambda_n}</math>　（极限层：把下面各层沿一条可计算上升的序列 <math>\lambda_0 < \lambda_1 < \lambda_2 < \ldots</math> 并起来——'''沿哪条序列取并由 <math>\lambda</math> 的代号给出'''，[[#通用序数记号系统ω_1^{CK}|5.8.1]] 里"记号携带程序编号"的约定在此派上用场）

: <math>H_\lambda = \cup_n H_{\lambda_n}</math>　（极限层：把下面各层沿一条可计算上升的序列 <math>\lambda_0 < \lambda_1 < \lambda_2 < \ldots</math> 并起来——'''沿哪条序列取并由 <math>\lambda</math> 的代号给出'''，[[#通用序数记号系统ω_1^CK|5.8.1]] 里"记号携带程序编号"的约定在此派上用场）

在某一层 <math>H_\alpha</math> 中可计算的集合，称为'''[[超算术的]]（hyperarithmetical, HYP）'''。这栋楼的前几层串起熟悉的图景：'''只盖有穷多层，得到的恰好是通常的算术层级'''——穷尽一阶算术（量词只作用于自然数）可定义的全部集合；盖到第 <math>\omega</math> 层（<math>\omega</math> 即 [[#通用序数记号系统ω_1^{CK}|5.8.1]] 中最小的无穷序数），得到的集合已足以一举判定[[皮亚诺公理]]体系的全部真语句——包括所有皮亚诺公理体系证明不了的真命题（对照 [[#哥德尔第一不完备定理（1931）|5.7.4]] 的不完备性）；而楼并不停在这里，它沿构造序数一直盖到 <math>\omega_1^CK</math> 为止。HYP 因此是真正高于算术层级的层级——至于它究竟高到哪一步（恰好等价于一个"二阶量词"的定义能力），正是 [[#超算术集与有效描述集合论|5.8.4]] 的主题<ref name="moschovakis2010" />。

在某一层 <math>H_\alpha</math> 中可计算的集合，称为'''[[超算术的]]（hyperarithmetical, HYP）'''。这栋楼的前几层串起熟悉的图景：'''只盖有穷多层，得到的恰好是通常的算术层级'''——穷尽一阶算术（量词只作用于自然数）可定义的全部集合；盖到第 <math>\omega</math> 层（<math>\omega</math> 即 [[#通用序数记号系统ω_1^CK|5.8.1]] 中最小的无穷序数），得到的集合已足以一举判定[[皮亚诺公理]]体系的全部真语句——包括所有皮亚诺公理体系证明不了的真命题（对照 [[#哥德尔第一不完备定理（1931）|5.7.4]] 的不完备性）；而楼并不停在这里，它沿构造序数一直盖到 <math>\omega_1^{CK}</math> 为止。HYP 因此是真正高于算术层级的层级——至于它究竟高到哪一步（恰好等价于一个"二阶量词"的定义能力），正是 [[#超算术集与有效描述集合论|5.8.4]] 的主题<ref name="moschovakis2010" />。

问题来了：同一序数 <math>\alpha</math> 在系统中有'''无穷多个代号'''，用不同代号构造出的 <math>H_\alpha</math> 会不会不同？

问题来了：同一序数 <math>\alpha</math> 在系统中有'''无穷多个代号'''，用不同代号构造出的 <math>H_\alpha</math> 会不会不同？

* '''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" />。

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

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