更改

这是经典集合论事实"第二数类的两种刻画等价"的可计算版本；两个方向的证明都以 SRT 为归纳枢纽<ref name="moschovakis2010" />。

这是经典集合论事实"第二数类的两种刻画等价"的可计算版本；两个方向的证明都以 SRT 为归纳枢纽<ref name="moschovakis2010" />。

=== 沿序数逐层构造之三：超算术层级与 Spector 唯一性定理 ===

=== 超算术层级与 Spector 唯一性定理 ===

'''神谕（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> 出发跳一次得到的 0′，正是通常意义下的停机问题（5.7.3）。

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

'''沿构造序数"盖楼"'''：现在从 <math>H_0 = \emptyset</math> 出发，沿构造序数（见 6.1）逐层往上盖：

'''沿构造序数"盖楼"'''：现在从 <math>H_0 = \emptyset</math> 出发，沿构造序数（见 6.1）逐层往上盖：

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

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

> <math>H_\lambda = \cup</math>ₙ <math>H_{\lambdaₙ}</math>　（极限层：把下面各层沿一条可计算上升的序列 <math>\lambda_0 < \lambda_1 < \lambda_2 < \ldots</math> 并起来——'''沿哪条序列取并由 <math>\lambda</math> 的代号给出'''，6.1 里"记号携带程序编号"的约定在此派上用场）

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

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

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

* '''Spector 唯一性定理（1955）'''：不会。<math>H_\alpha</math> 的可计算度只依赖序数 <math>\alpha</math> 本身，与代号选择无关；而且不同代号之间的翻译是一致可计算的<ref name="spector1955" /><ref name="moschovakis2010" />。

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

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

=== 沿序数逐层构造之四：HYP = \Delta^1_1 与有效描述集合论 ===

=== 沿序数逐层构造之四：HYP = \Delta^1_1 与有效描述集合论 ===