更改

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

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

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

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

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

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

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

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

第三行的 <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> 是这样一个程序的编号：

第三行的 <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> 是这样一个程序的编号：

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

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

- '''值的层面（无害）'''：<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> 的值"这种直接自指。

* '''值的层面（无害）'''：<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> 的值"这种直接自指。

- '''代码的层面（真正的循环）'''：程序 <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> 自己（及其编号）"的所指；这类循环在普通数学里非法。

* '''代码的层面（真正的循环）'''：程序 <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）造一个可计算函数 <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 定理（§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>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" />。