更改

  '''"You need a number z? You got it!"（你需要一个这样的数 z？给你！）'''<ref name="moschovakis2010" />

  '''"You need a number z? You got it!"（你需要一个这样的数 z？给你！）'''<ref name="moschovakis2010" />

=== 沿序数逐层构造之一：通用序数记号系统与 \omega_1^CK ===

=== 沿序数逐层构造之一：通用序数记号系统与<math>\omega_1^{CK}</math> ===

这是 SRT '''最初的'''应用（见 3.1）。回顾§3.1 的背景：[[序数记号系统]]给可数序数指派自然数代号，使得 0 / 后继 / 极限三分可机械判定、前驱与[[柯西序列|基本序列]]可机械取出。在进入定理之前，先把本节反复用到的几个概念交代清楚（"序数"本身的背景见 §3.1 的背景框）：

这是 SRT '''最初的'''应用（见 3.1）。回顾§3.1 的背景：[[序数记号系统]]给可数序数指派自然数代号，使得 0 / 后继 / 极限三分可机械判定、前驱与[[柯西序列|基本序列]]可机械取出。在进入定理之前，先把本节反复用到的几个概念交代清楚（"序数"本身的背景见 §3.1 的背景框）：

- '''代号与所指'''：记号系统里的每个自然数 a 都是一个'''代号'''，它所指的序数记作 |a|。一个序数 <math>\alpha</math> 的'''后继'''（successor）就是 <math>\alpha+1</math>（0 的后继是 1，<math>\omega</math> 的后继是 <math>\omega+1</math>）。'''极限序数'''（limit ordinal，下文统记作 <math>\lambda</math>）则是既非 0 也非任何序数之后继的序数——它不能靠"+1"走到，只能被一列递增的序数"逼近"，最典型的例子是 <math>\omega</math>（0, 1, 2, 3, <math>\ldots</math> 无限数完之后的那一步：任何自然数都不是它的"前一个"）。

* '''代号与所指'''：记号系统里的每个自然数 <math>a</math> 都是一个'''代号'''，它所指的序数记作 <math>|a|</math>。一个序数 <math>\alpha</math> 的'''后继'''（successor）就是 <math>\alpha+1</math>（0 的后继是 1，<math>\omega</math> 的后继是 <math>\omega+1</math>）。'''极限序数'''（limit ordinal，下文统记作 <math>\lambda</math>）则是既非 0 也非任何序数之后继的序数——它不能靠"+1"走到，只能被一列递增的序数"逼近"，最典型的例子是 <math>\omega</math>（<math>0, 1, 2, 3, \ldots</math> 无限数完之后的那一步：任何自然数都不是它的"前一个"）。

- '''前驱与基本序列'''：后继代号 x 的'''前驱'''（predecessor）记 P(x)——所指序数被"+1"之前那个序数的代号。极限代号 x 的'''基本序列'''（fundamental sequence）是一条可机械取出的递增代号列 <math>x_0</math>, <math>x_1</math>, <math>x_2</math>, <math>\ldots</math>，所指序数 |<math>x_0</math>| < |<math>x_1</math>| < <math>\ldots</math> 逐渐逼近 |x|。

* '''前驱与基本序列'''：后继代号 <math>x</math> 的'''前驱'''（predecessor）记 <math>P(x)</math>——所指序数被"+1"之前那个序数的代号。极限代号 <math>x</math> 的'''基本序列（fundamental sequence）'''是一条可机械取出的递增代号列 <math>x_0</math>, <math>x_1,x_2,\ldots</math>，所指序数 <math>|x_0| < |x_1| < \ldots</math> 逐渐逼近 <math>|x|<m/ath>。

- '''<math>S_1</math> 的语法'''（<math>S_1</math> 是下文定理要构造的那个"通用"'''序数记号系统'''，Kleene 1938 为它设计的编码方案；后文的记号系统 O 沿用同一语法）：0 的代号固定为 '''1'''；代号 a 的后继的代号写成 '''2^a'''；极限序数的代号写成 '''3<math>\cdot5^e</math>'''，并约定 |3<math>\cdot5^e</math>| = lim |<math>\phi</math>ₑ(n)|（程序 e 逐个吐出逼近该极限的记号列，<math>\phi</math>ₑ 是编号为 e 的程序，见 §2.2）。取这三种质因数形态（1、2 的幂、3<math>\times5</math> 的幂）纯属编码技巧：对代号做质因数分解，就能机械判定它是 0 的代号、后继代号还是极限代号。

* <math>S_1</math> 的语法（<math>S_1</math> 是下文定理要构造的那个"通用"'''序数记号系统'''，Kleene 1938 为它设计的编码方案；后文的记号系统 O 沿用同一语法）：0 的代号固定为 1；代号 <math>a</math> 的后继的代号写成 '''<math>2^a</math>'''；极限序数的代号写成 '''<math>3\cdot 5^e</math>'''，并约定 <math>|3\cdot5^e| = \lim|\phi_e(n)|</math>（程序 <math>e</math> 逐个吐出逼近该极限的记号列，<math>\phi</math>ₑ 是编号为 <math>e</math> 的程序，见 §2.2）。取这三种质因数形态（1、2 的幂、3<math>\times5</math> 的幂）纯属编码技巧：对代号做质因数分解，就能机械判定它是 0 的代号、后继代号还是极限代号。

> '''定理（Kleene 1938）'''：存在一个'''通用'''序数记号系统 <math>S_1</math>：对任何其他合法的序数记号系统 S（"合法"即满足 §3.1 说的条件——0 / 后继 / 极限三分可机械判定、前驱与基本序列可机械取出），存在可计算函数把 S 的代号'''保序'''地翻译为 <math>S_1</math> 的代号（"保序"：若 |x| < |y|，则翻译后所指的序数仍保持这一大小关系——翻译不打乱任何两个序数的先后）。<ref name="kleene1938" /><ref name="rogers1967" />

 

'''定理（Kleene 1938）'''：存在一个'''通用'''序数记号系统 <math>S_1</math>：对任何其他合法的序数记号系统<math>S</math>（"合法"即满足 §3.1 说的条件——0 / 后继 / 极限三分可机械判定、前驱与基本序列可机械取出），存在可计算函数把 <math>S</math> 的代号'''保序'''地翻译为 <math>S_1</math> 的代号（"保序"：若 <math>|x| < |y|</math>，则翻译后所指的序数仍保持这一大小关系——翻译不打乱任何两个序数的先后）。<ref name="kleene1938" /><ref name="rogers1967" />

'''证明的思路'''（这是"有效超限递归"的范式，值得细看）：想要的翻译函数 <math>\psi</math> 应该满足

'''证明的思路'''（这是"有效超限递归"的范式，值得细看）：想要的翻译函数 <math>\psi</math> 应该满足

> <math>\psi(x) = 1</math>　　　　　　（x 是 0 的代号时）   

: <math>\psi(x) = 1</math>　　　　　　（x 是 0 的代号时）   

> <math>\psi(x) = 2^\psi(P(x))</math>　　（x 是后继序数的代号时，P(x) 是前驱代号）   

: <math>\psi(x) = 2^\psi(P(x))</math>　　（x 是后继序数的代号时，P(x) 是前驱代号）   

> <math>\psi(x) = 3\cdot5^e</math>　　　　 （x 是极限序数的代号时，e 是"逐点翻译基本序列"那个程序的编号）

: <math>\psi(x) = 3\cdot5^e</math>　　　　 （x 是极限序数的代号时，e 是"逐点翻译基本序列"那个程序的编号）

第三行的 e 值得拆开细看——'''<math>\psi</math> 的定义需要用到 <math>\psi</math>，循环正藏在 e 的代码里'''。设 <math>\lambda</math> 是 S 能命名的某个极限序数（就是上文说的那种"既非 0 也非后继、只能被逼近"的序数，例如 <math>\omega</math>），x 是它在 S 中的代号；S 是合法记号系统，故 x 自带一条可计算的基本序列 <math>x_0</math>, <math>x_1</math>, <math>x_2</math>, <math>\ldots</math>——一列递增的代号，所指序数逐渐逼近 <math>\lambda</math>。按上面交代的语法，极限序数的代号必须写成 3<math>\cdot5^e</math> 的形态，所以 <math>\psi(x)</math> 必须形如 3<math>\cdot5^e</math>，其中 e 是这样一个程序的编号：

第三行的 <math>e</math> 值得拆开细看——'''<math>\psi</math> 的定义需要用到 <math>\psi</math>，循环正藏在 e 的代码里'''。设 <math>\lambda</math> 是 <math>S</math> 能命名的某个极限序数（就是上文说的那种"既非 0 也非后继、只能被逼近"的序数，例如 <math>\omega</math>），<math>x</math> 是它在 <math>S</math> 中的代号；<math>S</math> 是合法记号系统，故 <math>x</math> 自带一条可计算的基本序列 <math>x_0,x_1,x_2,\ldots</math>——一列递增的代号，所指序数逐渐逼近 <math>\lambda</math>。按上面交代的语法，极限序数的代号必须写成 <math>3\cdot 5^e</math> 的形态，所以 <math>\psi(x)</math> 必须形如 <math>3\cdot5^e</math>，其中 <math>e</math> 是这样一个程序的编号：

> 输入 n <math>\to </math>从 x 取出 xₙ <math>\to </math>'''对 xₙ 运行 <math>\psi</math>''' <math>\to </math>输出 <math>\psi(xₙ)</math>

: 输入 <math>n\to </math>从 <math>x</math> 取出 <math>x_n\to </math>'''对 <math>x_n</math> 运行 <math>\psi</math>''' <math>\to </math>输出 <math>\psi(x_n)</math>

（"逐点翻译基本序列"说的就是它。）这里有两个层面的循环，性质完全不同：

（"逐点翻译基本序列"说的就是它。）这里有两个层面的循环，性质完全不同：

- '''值的层面（无害）'''：<math>\psi(x) = 3\cdot5^e</math> 是'''一个完整的数'''，e 只是其中 5 的指数；程序 e 的输出是 <math>\psi(x_0)</math>, <math>\psi(x_1)</math>, <math>\ldots</math>——x '''下面'''各项的翻译——它从不计算 <math>\psi(x)</math> 自己（极限值由记号的形态约定，不是程序算出来的）。所以不存在"<math>\psi(x)</math> 的值里嵌着 <math>\psi(x)</math> 的值"这种直接自指。

- '''值的层面（无害）'''：<math>\psi(x) = 3\cdot5^e</math> 是'''一个完整的数'''，<math>e</math> 只是其中 5 的指数；程序 <math>e</math> 的输出是 <math>\psi(x_0)</math>, <math>\psi(x_1),\ldots</math>——<math>x</math> '''下面'''各项的翻译——它从不计算 <math>\psi(x)</math> 自己（极限值由记号的形态约定，不是程序算出来的）。所以不存在"<math>\psi(x)</math> 的值里嵌着 <math>\psi(x)</math> 的值"这种直接自指。

- '''代码的层面（真正的循环）'''：程序 e 要对 xₙ 运行 <math>\psi</math>，就必须'''在自己的代码里写死 <math>\psi</math> 的程序编号'''——而 <math>\psi</math> 此刻还在定义中。也就是说，想定义 <math>\psi</math>，得先造出一个"代码里引用了 <math>\psi</math> 的编号"的程序。这正是"右边出现了正在定义的 <math>\psi</math> 自己（及其编号）"的所指；这类循环在普通数学里非法。

- '''代码的层面（真正的循环）'''：程序 <math>e</math> 要对 <math>x_n</math> 运行 <math>\psi</math>，就必须'''在自己的代码里写死 <math>\psi</math> 的程序编号'''——而 <math>\psi</math> 此刻还在定义中。也就是说，想定义 <math>\psi</math>，得先造出一个"代码里引用了 <math>\psi</math> 的编号"的程序。这正是"右边出现了正在定义的 <math>\psi</math> 自己（及其编号）"的所指；这类循环在普通数学里非法。

SRT 恰好合法化它：先用 S-m-n 定理（§2.3）造一个可计算函数 q(x, d)——给定 <math>\psi</math> 的编号 d，机械地吐出"读 n、取 xₙ、运行程序 d"那个程序的编号。于是想求的 <math>\psi</math> 满足：<math>\psi(x) = 3\cdot5^e</math>，其中 e = q(x, d)，而 d 正是 <math>\psi</math> 自己的编号。把右边整体看作 d 的函数、套 SRT 取不动点 c，令 <math>\psi = \phi_c</math>，循环即闭合；再沿序数归纳验证 <math>\psi</math> 确实是'''全函数'''（"全"：对每个输入代号都有输出，见 §2.1）且保序。<ref name="kleene1938" />

SRT 恰好合法化它：先用 s-m-n 定理（§2.3）造一个可计算函数 <math>q(x, d)</math>——给定 <math>\psi</math> 的编号 <math>d</math>，机械地吐出"读 <math>n</math>、取 <math>x_n</math>、运行程序 <math>d</math>"那个程序的编号。于是想求的 <math>\psi</math> 满足：<math>\psi(x) = 3\cdot5^e</math>，其中 <math>e = q(x, d)</math>，而 <math>d</math> 正是 <math>\psi</math> 自己的编号。把右边整体看作 <math>d</math> 的函数、套 SRT 取不动点 <math>c</math>，令 <math>\psi = \phi_c</math>，循环即闭合；再沿序数归纳验证 <math>\psi</math> 确实是'''全函数'''（"全"：对每个输入代号都有输出，见 §2.1）且保序<ref name="kleene1938" />。

顺带分辨两行的差异：第二行 <math>\psi(x) = 2^\psi(P(x))</math> 是'''值依赖值'''的循环，且 P(x) 指向更小的序数，本质上是良基的（"良基"：不存在无穷下降链，所以"沿序数从小到大做归纳"是合法的）；第三行则是'''编号依赖编号'''的循环（e 的代码里嵌着 <math>\psi</math> 的编号），良基性救不了它——必须 SRT。

顺带分辨两行的差异：第二行 <math>\psi(x) = 2^\psi(P(x))</math> 是'''值依赖值'''的循环，且 <math>P(x)</math> 指向更小的序数，本质上是良基的（"良基"：不存在无穷下降链，所以"沿序数从小到大做归纳"是合法的）；第三行则是'''编号依赖编号'''的循环（<math>e</math> 的代码里嵌着 <math>\psi</math> 的编号），良基性救不了它——必须 SRT。

在 <math>S_1</math> 的基础上，Kleene 进一步构造了带树状[[偏序关系]]的'''序数记号系统 O（Kleene's O）'''——"偏序"（partial order）指只在部分代号对之间定义的"小于"关系（O 中记作 <O，反映所指序数的大小）。O 是通用且极大的：每个可被任何合法记号系统命名的序数（称为'''构造序数'''，constructive ordinal）在 O 中都有代号。全体[[递归序数|构造序数]]的[[上确界]]（supremum：不小于它们中任何一个的最小序数）

在 <math>S_1</math> 的基础上，Kleene 进一步构造了带树状[[偏序关系]]的'''序数记号系统 O（Kleene's O）'''——"偏序"（partial order）指只在部分代号对之间定义的"小于"关系（O 中记作 <O，反映所指序数的大小）。O 是通用且极大的：每个可被任何合法记号系统命名的序数（称为'''构造序数'''，constructive ordinal）在 O 中都有代号。全体[[递归序数|构造序数]]的[[上确界]]（supremum：不小于它们中任何一个的最小序数）

> '''<math>\omega_1^CK</math> = 最小的非构造序数（Church–Kleene 序数）'''

> '''<math>\omega_1^{CK}</math> = 最小的非构造序数（Church–Kleene 序数）'''

是逻辑学中最基本的"普适常数"之一：它是"机械命名能力"在序数世界中的绝对边界<ref name="kleene1938" /><ref name="rogers1967" />。Rogers 用同样的 SRT 技术证明：O 上的"序数加法"可由一个可计算函数实现<ref name="rogers1967" />。

是逻辑学中最基本的"普适常数"之一：它是"机械命名能力"在序数世界中的绝对边界<ref name="kleene1938" /><ref name="rogers1967" />。Rogers 用同样的 SRT 技术证明：O 上的"序数加法"可由一个可计算函数实现<ref name="rogers1967" />。