更改

==== 通用序数记号系统ω_1^{CK}====

==== 通用序数记号系统ω_1^{CK}====

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

这是 SRT '''最初的'''应用（见 [[#起源：一篇研究"序数记号"的 6 页短文|3.1]]）。回顾[[#起源：一篇研究"序数记号"的 6 页短文|§3.1]] 的背景：[[序数记号系统]]给可数序数指派自然数代号，使得 0 / 后继 / 极限这三种构建可以被机械地（可计算的）判定，前驱与[[柯西序列|基本序列]]都可被机械地（计算地）取出。在进入定理之前，我们先把本节反复用到的几个概念交代清楚（"序数"本身的背景见 [[#起源：一篇研究"序数记号"的 6 页短文|§3.1]] 的背景框）：

* '''代号与所指'''：记号系统里的每个自然数 <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> 无限数完之后的那一步：任何自然数都不是它的"前一个"）。

* '''代号与所指'''：记号系统里的每个自然数 <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> 无限数完之后的那一步：任何自然数都不是它的"前一个"）。

* '''前驱与基本序列'''：后继代号 <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|</math>。

* '''前驱与基本序列'''：后继代号 <math>x</math> 的'''前驱'''（predecessor）记 <math>P(x)</math>——指序数x被"+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|</math>。

* <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 的代号、后继代号还是极限代号。

* <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>：对任何其他合法的序数记号系统<math>S</math>（"合法"即满足 [[#起源：一篇研究"序数记号"的 6 页短文|§3.1]] 说的条件——0 / 后继 / 极限三分可机械判定、前驱与基本序列可机械取出），存在可计算函数把 <math>S</math> 的代号'''保序'''地翻译为 <math>S_1</math> 的代号（"保序"：若 <math>|x| < |y|</math>，则翻译后所指的序数仍保持这一大小关系——翻译不打乱任何两个序数的先后）<ref name="kleene1938">'''Kleene, S. C. (1938).''' On notation for ordinal numbers. ''The Journal of Symbolic Logic'', 3(4), 150–155.【第二递归定理的原始出处，定理与证明见 p.153】</ref><ref name="rogers1967" />。

'''定理（Kleene 1938）'''：存在一个'''通用'''序数记号系统 <math>S_1</math>：对任何其他合法的序数记号系统<math>S</math>（"合法"即满足 [[#起源：一篇研究"序数记号"的 6 页短文|§3.1]] 说的条件——0 / 后继 / 极限这三部分都可被机械判定，并且前驱与基本序列可被机械取出），存在可计算函数把 <math>S</math> 的代号'''保序'''地翻译为 <math>S_1</math> 的代号（"保序"：若 <math>|x| < |y|</math>，则翻译后所指的序数仍保持这一大小关系——翻译不打乱任何两个序数的先后顺序）<ref name="kleene1938">'''Kleene, S. C. (1938).''' On notation for ordinal numbers. ''The Journal of Symbolic Logic'', 3(4), 150–155.【第二递归定理的原始出处，定理与证明见 p.153】</ref><ref name="rogers1967" />。

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

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

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

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

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

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

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

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

SRT 恰好合法化它：先用 s-m-n 定理（[[#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" />。

SRT 恰好合法化它：先用 s-m-n 定理（[[#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> 是'''值依赖值'''的循环，且 <math>P(x)</math> 指向更小的序数，本质上是良基的（"良基"：不存在无穷下降链，所以"沿序数从小到大做归纳"是合法的）；第三行则是'''编号依赖编号'''的循环（<math>e</math> 的代码里嵌着 <math>\psi</math> 的编号），良基性救不了它——必须 SRT。

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

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

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

Kiselyov 以现代眼光补充了这段历史的思想动机：Kleene 放弃用 <math>\lambda</math> 项（他与 Church 两年前的方案）做序数代号，正是因为 <math>\lambda</math> 项作为'''函数'''无法被机械地比较大小；极限序数的代号必须携带'''程序的编号'''而非函数本身——"只有编号（有穷对象）才能被直接给出，这是有穷主义立场的要求"<ref name="kleene1938" /><ref name="kiselyov" />。

Kiselyov 以现代眼光补充了这段历史的思想动机：Kleene 放弃用 <math>\lambda</math> 项（他与 Church 两年前的方案）做序数代号，正是因为 <math>\lambda</math> 项作为'''函数'''无法被机械地比较大小；极限序数的代号必须携带'''程序的编号'''而非函数本身——"只有编号（有穷对象）才能被直接给出，这是有穷主义立场的要求"<ref name="kleene1938" /><ref name="kiselyov" />。