查看“︁PrSS的良序性”︁的源代码

=== PrSS 没有无穷降链 ===
首先我们将 [[初等序列系统|PrSS]] 的每个合法表达式 <math>S</math> 对应于一个不超过 <math>\varepsilon_0</math> 的[[序数]] <math>F(S)</math>。然后我们证明 PrSS 表达式展开时，其对应的序数严格递减。于是就可以依据 <math>\varepsilon_0</math> 的[[良序|良序性]]说明 PrSS 没有无穷降链。

'''第一步'''：将 PrSS 的每个合法表达式对应于一个不超过 <math>\varepsilon_0</math> 的序数。

对 PrSS 表达式的长度归纳定义。

任取 PrSS 合法表达式 <math>S=(a_1,a_2,\cdots,a_n)</math>。

若 <math>n=0</math>，则 <math>F(S)=0<\varepsilon_0</math>。

若 <math>n>0</math>，分两种情况讨论：

* 若 <math>\forall i\in\{2,3,\cdots,n\},a_i\neq 0</math>，则取 <math>T=(a_2-1,a_3-1,\cdots,a_n-1)</math>。<br>不难验证，<math>T</math> 是合法的 PrSS 表达式，且 <math>T</math> 的长度比 <math>S</math> 的长度短。令 <math>F(S)=\omega^{F(T)}</math>。<br>因为 <math>F(T)<\varepsilon_0</math>，所以 <math>F(S)<\varepsilon_0</math>。
* 否则，设 <math>S</math> 中有 <math>r</math> 项为零，且 <math>a_{k_1}=a_{k_2}=\cdots=a_{k_r}=0</math>，其中 <math>1=k_1<k_2<k_3<\cdots<k_r<k_{r+1}=n+1</math>。<br>取 <math>S_i=(a_{k_i},a_{k_i+1},\cdots,a_{k_{i+1}-1}),\quad i=1,2,\cdots,r</math>，不难验证 <math>S_1,S_2,\cdots,S_r</math> 都是合法的 PrSS 表达式，且它们的长度都比 <math>S</math> 短。<br>令 <math>F(S)=F(S_1)+F(S_2)+\cdots+F(S_r)</math>。<br>因为 <math>F(S_1),F(S_2),\cdots,F(S_r)<\varepsilon_0</math>，所以 <math>F(S)<\varepsilon_0</math>。

'''第二步'''：证明 PrSS 表达式展开时，其对应的序数严格递减。

对 PrSS 表达式的长度归纳证明。

任取 PrSS 表达式 <math>S=(a_1,a_2,\cdots,a_n)</math>。

若 <math>n=0</math>，则 <math>S</math> 无法展开。下面讨论 <math>n>0</math> 的情况。

若 <math>a_n=0</math>，则 <math>S</math> 的展开式（前驱表达式）是 <math>T=(a_1,a_2,\cdots,a_{n-1})</math>。分为两种情况讨论：

* 若 <math>\forall i\in\{2,3,\cdots,n\},a_i\neq 0</math>，则 <math>S=(0)</math>，<math>F(S)=1</math>，<math>T=()</math>，<math>F(T)=0</math>，<math>F(T)<F(S)</math>。
* 否则，设 <math>S</math> 中有 <math>r</math> 项为零，且 <math>a_{k_1}=a_{k_2}=\cdots=a_{k_r}=0</math>，其中 <math>1=k_1<k_2<k_3<\cdots<k_r=n<k_{r+1}=n+1</math>。<br>取 <math>S_i=(a_{k_i},a_{k_i+1},\cdots,a_{k_{i+1}-1}),\quad i=1,2,\cdots,r</math>，则 <math>F(S)=F(S_1)+F(S_2)+\cdots+F(S_r)</math>。<br>注意到 <math>S_r=(0)</math>，<math>F(S_r)=1</math>，所以 <math>F(T)=F(S_1)+F(S_2)+\cdots+F(S_{r-1})</math>，所以 <math>F(S)=F(T)+1>F(T)</math>。

若 <math>a_n\neq 0</math>，分为三种情况讨论：

* 若 <math>S</math> 中有不止一项是零。<br>设 <math>S</math> 中有 <math>r>1</math> 项为零，且 <math>a_{k_1}=a_{k_2}=\cdots=a_{k_r}=0</math>，其中 <math>1=k_1<k_2<k_3<\cdots<k_r<k_{r+1}=n+1</math>。<br>取 <math>S_i=(a_{k_i},a_{k_i+1},\cdots,a_{k_{i+1}-1}),\quad i=1,2,\cdots,r</math>，则 <math>F(S)=F(S_1)+F(S_2)+\cdots+F(S_r)</math>。<br>设 <math>S</math> 的坏根为 <math>a_x</math>。不难看出，<math>x\ge k_r</math>。<br>设 <math>S_r</math> 的基本列的第 <math>p</math> 项是 <math>V_p</math>。由 PrSS 展开规则，<math>S</math> 的基本列的第 <math>p</math> 项是 <math>U_p=(S_1,S_2,\cdots,S_{r-1},V_p)</math>。<br>因为 <math>S_r</math> 的长度比 <math>S</math> 短，根据归纳假设，有 <math>F(V_p)<F(S_r)</math>。<br>设 <math>V_p=(b_1,b_2,\cdots,b_m)</math> 中有 <math>s</math> 项为零，且 <math>b_{l_1}=b_{l_2}=\cdots=b_{l_s}=0</math>，其中 <math>1=l_1<l_2<l_3<\cdots<l_s<l_{s+1}=m+1</math>。<br>取 <math>T_i=(b_{l_i},b_{l_i+1},\cdots,b_{l_{i+1}-1}),\quad i=1,2,\cdots,s</math>，则 <math>F(V_p)=F(T_1)+F(T_2)+\cdots+F(T_s)</math>。<br>所以 <math display="block">\begin{aligned}F(U_s)\,&=F(S_1)+F(S_2)+\cdots+F(S_{r-1})+F(T_1)+F(T_2)+\cdots+F(T_s)\\&=F(S_1)+F(S_2)+\cdots+F(S_{r-1})+(F(T_1)+F(T_2)+\cdots+F(T_s))\\&=F(S_1)+F(S_2)+\cdots+F(S_{r-1})+F(V_s)\\&<F(S_1)+F(S_2)+\cdots+F(S_{r-1})+F(S_r)\\&=F(S)\end{aligned}</math>
* 若 <math>S</math> 中仅有首项为零，且末项为 <math>a_n=1</math>。<br>令 <math>T_1=(a_1,a_2,\cdots,a_{n-1})</math>。由 PrSS 展开规则，不难看出 <math>S</math> 的基本列的第 <math>p</math> 项是 <math>U_p=(T_1,T_1,\cdots,T_1)</math>，其中有 <math>p</math> 个 <math>T_1</math>。<br>显然 <math>n\ge 2</math>，所以 <math>F(T_1)>0</math>。<br>那么 <math>F(U_p)=F(T_1)+F(T_1)+\cdots+F(T_1)=F(T_1)\times p<F(T_1)\times\omega</math>。<br>令 <math>T_2=(a_2-1,a_3-1,\cdots,a_n-1)</math>，则 <math>F(S)=\omega^{F(T_2)}</math>。<br>令 <math>T_3=(a_2-1,a_3-1,\cdots,a_{n-1}-1)</math>，则 <math>F(T_1)=\omega^{F(T_3)}</math>。<br>因为 <math>a_n-1=0</math>，所以 <math>F(T_2)=F(T_3)+1</math>，所以 <math>F(S)=\omega^{F(T_2)}=\omega^{F(T_3)+1}=\omega^{F(T_3)}\times\omega=F(T_1)\times\omega>F(U_p)</math>。
* 若 <math>S</math> 中仅有首项为零，且末项为 <math>a_n\neq 1</math>。<br>令 <math>T=(a_2-1,a_3-1,\cdots,a_n-1)</math>，因为 <math>a_n-1\neq 0</math>，所以 <math>T</math> 是极限表达式。<br>设 <math>T</math> 的基本列的第 <math>k</math> 项是 <math>T_k=(b_1,b_2,\cdots,b_{m_k})</math>，则由 PrSS 展开规则可以看出 <math>S</math> 的基本列的第 <math>k</math> 项是 <math>S_k=(0,b_1+1,b_2+1,\cdots,b_{m_k}+1)</math>。<br>根据归纳假设有 <math>F(T_k)<F(T)</math>，所以 <math>F(S_k)=\omega^{F(T_k)}<\omega^{F(T)}=F(S)</math>。

证毕。

以上，我们证明了 PrSS 表达式的展开过程不会无限进行，即不存在无穷降链。

至此，PrSS 已经是一个合格的序数记号了。但我们不止于此，我们要给出判断 PrSS 表达式是否标准的方法，并证明 PrSS 标准式的序是字典序。

=== PrSS 标准表达式 ===
PrSS 的极限基本列是 <math>(),(0),(0,1),(0,1,2),\cdots</math>。PrSS 的极限基本列的第 <math>n</math> 项是 <math>L_n=(0,1,2,\cdots,n-1)</math>。

'''定义'''（PrSS 标准表达式）

一个 PrSS 表达式 <math>S</math> 是 '''PrSS 标准表达式'''（简称 '''PrSS 标准式'''），当且仅当存在 <math>n</math> 使得极限基本列的第 <math>n</math> 项 <math>L_n</math> 可以经过若干次展开得到 <math>S</math>。

简单地说，标准式就是能从极限基本列展开得到的表达式。对于大部分的序数记号，存在合法但不标准的表达式。这些不标准的合法表达式往往也能对应于一个序数（例如上一节的映射 <math>F</math> 不要求表达式是标准的），但这将导致不同的合法表达式对应于同一个序数。对应于同一个序数的不同合法表达式，例如 <math>(0,1)</math> 和 <math>(0,0,1)</math> 都是对应于 <math>\omega</math> 的表达式，彼此之间无法展开成对方。这意味着合法表达式集不是全序，更不是良序。不同的标准表达式则不会对应于同一个序数，标准表达式集确实是良序的。

在这一节，我们将给出 PrSS 标准式的必要条件。该条件实际上也是充分的，不过充分性将在下一节证明。在此之前，我们先来定义字典序的概念。

'''定义'''（字典序）

设 <math>A</math> 是一个全序集，其上的全序是 <math>\le</math>。考虑两个数列 <math>S=(a_1,a_2,\cdots,a_n)</math> 和 <math>T=(b_1,b_2,\cdots,b_m)</math>，其中 <math>a_1,a_2,\cdots,a_n,b_1,b_2,\cdots,b_m\in A</math>。在字典序下，<math>S\le T</math> 当且仅当以下两条中的一条成立：
* 存在 <math>0\le k<\min\{n,m\}</math> 使得对任意 <math>i\in\{1,2,\cdots,k\}</math> 有 <math>a_i=b_i</math>，但 <math>a_{k+1}<b_{k+1}</math>；
* 对任意 <math>i\in\{1,2,\cdots,\min\{n,m\}\}</math> 有 <math>a_i=b_i</math>，且 <math>n\le m</math>。

不难看出，对任意两个由 <math>A</math> 中元素组成的有限数列 <math>S,T</math>，总有 <math>S\le T\lor T\le S</math>。也就是说，字典序是全序。

'''引理'''

PrSS 表达式展开时，字典序变小。

'''证明'''

设 <math>S=(a_1,a_2,\cdots,a_n)</math> 是 PrSS 表达式。

如果 <math>a_n=0</math>，则 <math>S</math> 的展开式为 <math>T=(a_1,a_2,\cdots,a_{n-1})</math>。根据定义，对任意 <math>i\in\{1,2,\cdots,n-1\}</math> 有 <math>a_i=a_i</math>，且 <math>n-1<m</math>，所以 <math>T<S</math>。

如果 <math>a_n\neq 0</math>，且展开式 <math>T</math> 是 <math>S</math> 的基本列的第 <math>0</math> 项，则 <math>T</math> 相当于删去 <math>S</math> 的末项，所以 <math>T<S</math>。

如果 <math>a_n\neq 0</math>，且展开式 <math>T</math> 是 <math>S</math> 的基本列的第 <math>k>0</math> 项，则 <math>T</math> 相当于删去 <math>S</math> 的末项，并复制若干次坏部。因为坏部的第一项（坏根）小于末项，所以 <math>T<S</math>。

证毕。

现在可以给出 PrSS 标准式的必要条件了。

'''临时定义'''（PrSS 规范式）

对表达式 <math>S=(a_1,a_2,\cdots,a_n)</math> 的长度 <math>n</math> 归纳定义。

若 <math>n=0</math>，则 <math>S=()</math> 是 PrSS 规范式。

若 <math>n>0</math> 且 <math>S</math> 中仅有首项是零，则 <math>S</math> 是 PrSS 规范式当且仅当 <math>(a_2-1,a_3-1,\cdots,a_n-1)</math> 是 PrSS 规范式。

若 <math>n>0</math> 且 <math>S</math> 中有 <math>r>1</math> 项是零，设 <math>a_{k_1}=a_{k_2}=\cdots=a_{k_r}=0</math>，其中 <math>1=k_1<k_2<\cdots<k_r<k_{r+1}=n+1</math>，令 <math>S_i=(a_{k_i},a_{k_i+1},\cdots,a_{k_{i+1}-1})</math>。则 <math>S</math> 是 PrSS 规范式当且仅当 <math>S_1,S_2,\cdots,S_r</math> 都是 PrSS 规范式且按字典序 <math>S_1\ge S_2\ge\cdots\ge S_r</math>。

PrSS 规范式是本文临时定义的，并不是通用术语。PrSS 规范式实际上等价于 PrSS 标准式。

'''定理'''

PrSS 标准式都是 PrSS 规范式。

'''证明'''

不难看出 PrSS 极限基本列都是 PrSS 规范式，因此只需证明 PrSS 规范式的展开式也是 PrSS 规范式即可。

对规范表达式 <math>S=(a_1,a_2,\cdots,a_n)</math> 的长度 <math>n</math> 归纳证明。

<math>n=0,1</math> 的情况是平凡的，下面讨论 <math>n>1</math> 的情况。

若 <math>S</math> 中有 <math>r>1</math> 项是零，设 <math>a_{k_1}=a_{k_2}=\cdots=a_{k_r}=0</math>，其中 <math>1=k_1<k_2<\cdots<k_r<k_{r+1}=n+1</math>，令 <math>S_i=(a_{k_i},a_{k_i+1},\cdots,a_{k_{i+1}-1})</math>。则 <math>S</math> 的展开相当于 <math>S_r</math> 的展开。根据归纳假设，<math>S_r</math> 的展开式是规范的。因为 <math>S_r</math> 展开后字典序会变小（引理），所以 <math>S</math> 展开后，各部分的字典序依然递减，所以 <math>S</math> 的展开式是规范的。注意这里要讨论 <math>S_r</math> 的展开式有不止一个零的情况，不过这个讨论并不难，感兴趣的读者可以自行讨论。

若 <math>S</math> 中仅有一项是零，且 <math>a_n=1</math>。令 <math>T_1=(a_2-1,a_3-1,\cdots,a_n-1)</math>。因为 <math>S</math> 是规范表达式，根据规范表达式的定义，<math>T_1</math> 也是规范表达式。从规范表达式的定义中不难看出，去掉 <math>T_1</math> 末尾的 <math>a_n-1=0</math> 后依然是规范的，即 <math>T_2=(a_2-1,a_3-1,\cdots,a_{n-1}-1)</math> 规范。所以 <math>T=(a_1,a_2,\cdots,a_{n-1})</math> 规范。注意到 <math>S</math> 的展开式形如 <math>(T,T,\cdots,T)</math>，所以 <math>S</math> 的展开式是规范的。

若 <math>S</math> 中仅有一项是零，且 <math>a_n\neq 1</math>。令 <math>T=(a_2-1,a_3-1,\cdots,a_n-1)</math>。因为 <math>S</math> 规范，所以 <math>T</math> 规范。根据归纳假设，<math>T</math> 的展开式是规范的。设 <math>S</math> 的一个展开式是 <math>(b_1,b_2,\cdots,b_m)</math>，则由 PrSS 展开规则可知 <math>(b_2-1,b_3-1,\cdots,b_m-1)</math> 是 <math>T</math> 的展开式，是规范的，所以 <math>S</math> 的展开式也是规范的。

证毕。

在第一节证明 PrSS 没有无穷降链时，我们使用了序数的良序性。如果想不依赖序数就证明 PrSS 没有无穷降链，参见知乎用户  www620 的证明<ref>https://zhuanlan.zhihu.com/p/13871622947</ref>。这个证明依赖本节的两个结论：PrSS 表达式展开时字典序变小、PrSS 标准式都是规范式。注意到本节的两个结论不依赖第一节，所以没有循环论证的问题。

=== PrSS 标准式集的良序性 ===
上一节我们证明了 PrSS 合法表达式在展开过程中字典序变小，并由此得到了 PrSS 标准式的必要条件。这一节，我们证明字典序变小反过来也意味着可以展开得到，并由此得到 PrSS 标准式的充分条件。

'''定理'''

设 <math>S,T</math> 是 PrSS 规范式，且按字典序 <math>S<T</math>，则 <math>S</math> 经过若干次展开可以得到 <math>T</math>。

注意上一节的引理对任意 PrSS 合法式均成立，而这个定理要求 <math>S,T</math> 都是规范式。

'''证明'''

定义一种特殊的展开函数 <math>E</math>：设 PrSS 表达式 <math>U</math> 的基本列为 <math>U_0,U_1,U_2,\cdots</math>。若存在 <math>i</math> 使得按字典序 <math>U_i\ge S</math>，则取 <math>k=\min\{i\mid U_i\ge S\}</math> 并定义 <math>E(U)=U_k</math>。如果对任意 <math>i</math> 都有按字典序 <math>U_i<S</math>，则取 <math>E(U)=U</math>。如果 <math>U</math> 是后缀表达式，则取 <math>U_0=U_1=\cdots</math> 为 <math>U</math> 的前驱表达式。特殊地，如果 <math>U</math> 是零表达式，则 <math>E(U)=U</math>。

从 <math>E</math> 的定义不难看出，如果按字典序 <math>U\ge S</math>，则按字典序 <math>E(U)\ge S</math>。令 <math>T_0=T</math>，<math>T_{n+1}=E(T_n)</math>。因为按字典序 <math>T>S</math>，所以对任意 <math>i</math> 都有按字典序 <math>T_i\ge S</math>。

而第一节已经证明 PrSS 不存在无穷降链，所以存在 <math>k</math> 使得 <math>T_k=T_{k+1}=\cdots</math>。讨论一下不难得到，这时有两种可能：

* <math>T_k=S</math>。
* 按字典序 <math>T_k>S</math>，但 <math>T_k</math> 的基本列的每一项都按字典序小于 <math>S</math>。进一步讨论还可以看出，这种情况下 <math>T_k</math> 一定是极限表达式。

前一种情况命题已经成立，只需要用反证法证明后一种情况不存在即可。

若存在，设 <math>T_k</math> 的好部是 <math>G</math>，坏部是 <math>B</math>，末项是 <math>L</math>，坏根是 <math>L-1</math>，则 <math>T_k=(G,B,L)</math>，而 <math>T_k</math> 的展开式形如 <math>(G,B,B,\cdots)</math>。

如果 <math>S</math> 按字典序小于 <math>T_k</math> 而大于 <math>(G,B,B,\cdots)</math>，那么 <math>S</math> 一定以 <math>(G,B)</math> 开头。设 <math>S=(G,B,X)</math>，那么 <math>X</math> 的首项等于坏根 <math>L-1</math>，而 <math>X</math> 按字典序大于 <math>(B,B,\cdots)</math>。

这与 <math>S</math> 是规范表达式相矛盾。这个矛盾可以更明确地写出来，但会占据大量篇幅且可能不会提供新的见解，所以在此略。也许以后我会补充。

证毕。

至此，我们已经证明了，规范表达式集上由展开定义的序，等价于字典序。

'''定理'''

PrSS 规范式都是 PrSS 标准式。

'''证明'''

设 <math>S</math> 是 PrSS 规范式。存在 <math>n</math> 使得 <math>T=(0,1,2,\cdots,n-1)</math> 按字典序大于 <math>S</math>。根据上一个定理，<math>T</math> 可以展开成 <math>S</math>，所以 <math>S</math> 是 PrSS 标准式。

证毕。

至此，我们证明了 PrSS 没有无穷降链、PrSS 标准式集的序是字典序，而字典序是全序，所以 PrSS 标准式集上的序是良序。

但我们不止于此。下一节，我们要证明 PrSS 标准式集[[良序|序同构]]于 <math>\varepsilon_0</math>。

=== PrSS 标准式集的序型 ===
为了证明 PrSS 标准式集[[良序|序同构]]于 <math>\varepsilon_0</math>，我们要证明第一节定义的保序映射 <math>F</math> 是 PrSS 标准式集和 <math>\varepsilon_0</math> 之间的双射，结合 PrSS 标准式集的全序性，就能说明 <math>F</math> 是 PrSS 标准式集和 <math>\varepsilon_0</math> 之间的序同构。

'''定理'''

<math>F</math>是 PrSS 标准式集与<math>\varepsilon_0</math>之间的保序双射。

'''证明'''

对于小于<math>\varepsilon_0</math>的序数<math>\alpha</math>，定义<math>Seq(\alpha)=(a_1,a_2,\cdots,a_k)</math>是这样的自然数序列：

* <math>Seq(0)=()</math>为空序列
* <math>\alpha>0</math>时，设它的康托范式为<math>\alpha=\omega^{\alpha_1}+\omega^{\alpha_2}+\omega^{\alpha_3}+\cdots +\omega^{\alpha_n}</math>，则<math>Seq(\alpha)=T(S'(\alpha_1),S'(\alpha_2),\cdots,S'(\alpha_n))</math>，其中<math>T</math>为序列的拼合，而如果<math>Seq(\alpha)=(a_1,a_2,\cdots,a_k)</math>，<math>S'(\alpha)</math>定义为<math>(0,a_1+1,a_2+1,\cdots,a_k+1)</math>

我们给出几个引理：

'''引理 1'''  如果<math>\varepsilon_0>\alpha\geq\beta</math>，则按字典序<math>Seq(\alpha)\geq{Seq(\beta)}</math>

'''引理 2'''  <math>Seq(\alpha)</math>是 PrSS 的规范式。

'''引理 3'''  <math>F(Seq(\alpha))=\alpha</math>

'''引理 4'''  <math>Seq(F(S))=S</math>，其中<math>S</math>为 PrSS 规范式

'''引理 1 的证明'''  取出所有有序对<math>(\alpha,\beta)</math>使<math>\varepsilon_0>\alpha>\beta</math>但按字典序<math>Seq(\alpha)\leq{Seq(\beta)}</math>，取出其中<math>\alpha</math>最小的一组。写出它们的康托范式：

<math>\alpha=\omega^{\alpha_1}+\omega^{\alpha_2}+\omega^{\alpha_3}+\cdots +\omega^{\alpha_p}</math>

<math>\beta=\omega^{\beta_1}+\omega^{\beta_2}+\omega^{\beta_3}+\cdots +\omega^{\beta_q}</math>

则以下两点成立其一：
# 存在某个<math>i\leq{min\{p,q\}}</math>使<math>\alpha_i>\beta_i</math>
# <math>q<p</math>，且对于所有<math>i\leq{q}</math>有<math>\alpha_i=\beta_i</math>

对于前者，由于<math>\alpha_i<\alpha</math>，根据<math>\alpha</math>的最小性，字典序下<math>Seq(\alpha_i)>Seq(\beta_i)</math>，根据定义，字典序下<math>Seq(\alpha)>Seq(\beta)</math>，矛盾。

对于后者，易知<math>Seq(\beta_i)</math>是<math>Seq(\alpha_i)</math>删去后面数项得到的子序列。故字典序下<math>Seq(\alpha)>Seq(\beta)</math>，矛盾。

因此，这样的有序对<math>(\alpha,\beta)</math>不存在，所以如果<math>\varepsilon_0>\alpha\geq\beta</math>，则按字典序<math>Seq(\alpha)\geq{Seq(\beta)}</math>

又如果<math>\varepsilon_0>\alpha=\beta</math>，则按字典序<math>Seq(\alpha)=Seq(\beta)</math>。于是引理1得证。

'''引理 2 的证明'''  设<math>\alpha<\varepsilon_0</math>是最小使得<math>Seq(\alpha)</math>不是 PrSS 的规范式的序数。设它的康托范式为<math>\alpha=\omega^{\alpha_1}+\omega^{\alpha_2}+\omega^{\alpha_3}+\cdots +\omega^{\alpha_n}</math>。

(1) 若<math>n=1</math>，<math>\alpha=\omega^{\alpha_1}</math>，<math>Seq(\alpha)=S'(\alpha_1)</math>。根据定义，<math>Seq(\alpha)</math>是 PrSS 的规范式当且仅当<math>Seq(\alpha_1)</math>是 PrSS 的规范式，而<math>\alpha_1<\alpha</math>，根据最小性，<math>Seq(\alpha_1)</math>是 PrSS 的规范式，故<math>Seq(\alpha)</math>也是 PrSS 的规范式，矛盾。

(2) 若<math>n>1</math>，<math>\alpha=\omega^{\alpha_1}+\omega^{\alpha_2}+\omega^{\alpha_3}+\cdots +\omega^{\alpha_n}</math>，<math>Seq(\alpha)=T(S'(\alpha_1),S'(\alpha_2),\cdots,S'(\alpha_n))</math>。根据定义，<math>Seq(\alpha)</math>是 PrSS 的规范式当且仅当每个<math>Seq(\alpha_k)</math>均是 PrSS 的规范式且<math>Seq(\alpha_k)</math>的字典序不增，<math>k=1,2,\cdots,n</math>。前者是显然的(类似于上文的(1)部分)，而后者由<math>\alpha_1\geq\alpha_2\geq\cdots\alpha_n</math>和引理1保证。于是<math>Seq(\alpha)</math>是 PrSS 的规范式，矛盾。

故这样的<math>\alpha<\varepsilon_0</math>不存在。引理2得证。

'''引理 3 的证明'''  设<math>\alpha<\varepsilon_0</math>是最小的不满足<math>F(Seq(\alpha))=\alpha</math>的序数。它的康托范式为<math>\alpha=\omega^{\alpha_1}+\omega^{\alpha_2}+\omega^{\alpha_3}+\cdots +\omega^{\alpha_n}</math>。

则有<math>Seq(\alpha)=T(S'(\alpha_1),S'(\alpha_2),\cdots,S'(\alpha_n))</math>。根据定义，<math>F(T(S'(\alpha_1),S'(\alpha_2),\cdots,S'(\alpha_n)))=F(S'(\alpha_1))+F(S'(\alpha_2))+\cdots+F(S'(\alpha_n))=\omega^{F(Seq(\alpha_1))}+\omega^{F(Seq(\alpha_2))}+\cdots+\omega^{F(Seq(\alpha_n))}</math>，而<math>\alpha_k<\alpha</math>，<math>k=1,2,\cdots,n</math>，根据最小性，<math>F(Seq(\alpha_k))=\alpha_k</math>，故<math>F(T(S'(\alpha_1),S'(\alpha_2),\cdots,S'(\alpha_n)))=\omega^{\alpha_1}+\omega^{\alpha_2}+\omega^{\alpha_3}+\cdots +\omega^{\alpha_n}=\alpha</math>。矛盾。

故这样的<math>\alpha<\varepsilon_0</math>不存在。引理3得证。

'''引理 4 的证明'''  若对于某个 PrSS 规范式<math>S</math>有<math>Seq(F(S))>S</math>，则由引理1得<math>F(Seq(F(S))>F(S)</math>，由引理3得<math>F(S)>F(S)</math>，矛盾。同理，<math>Seq(F(S))<S</math>则<math>F(S)<F(S)</math>，矛盾。故<math>Seq(F(S))=S</math>。

'''定理的证明'''  由引理1~4，<math>F</math>有逆映射<math>Seq</math>，且<math>Seq</math>保序。于是<math>Seq</math>(和其逆<math>F</math>)是 PrSS 标准式集与<math>\varepsilon_0</math>之间的序同构。

证毕。

----------

在下面，我们介绍另外一种 PrSS 良序性的证法。

=== 证明 ===

我们将使用 <math>E</math> 表示空序列，使用 <math>\frown</math> 表示序列的连接。

对于序列 <math>S</math> ，我们将使用长度 <math>( S )</math> 表示序列 <math>S</math> 的长度，使用 <math>S_{n} ( n < \mathrm {length} ( S ) )</math> 表示 <math>S</math> 的第 <math>n</math> 项，使用 <math>S_{\square}</math> 表示 <math>S</math> 的最后一项，使用 <math>S^{+}</math> 表示对 <math>S</math> 的每个分量加 1 得到的序列。

对于序列 <math>S</math> 和自然数 <math>m ,n</math> ，且 <math>m \leq n \leq</math> 长度 <math>( S )</math> ，设 <math>\operatorname{sub} ( S ,m ,n )</math> 为唯一序列 <math>T</math> ，且<math>T_{x}=S_{m + x}</math> （若 <math>x < n-m</math> ）且长度 <math>( T )=n-m</math> 。

'''定义 1''' 递归地定义 <math>P</math> ，一组有限长度的自然数序列，如下所示。

<math>P_{0} :=\{E \},</math>

<math>P_{n + 1} :=P_{n} \cup \left\{S \smile (0) \smile T^{+} \mid S \in P_{n} \wedge T \in P_{n} \right\},</math>

<math>P :=\bigcup_ {n \in \mathbb {N}} P_{n}.</math>

'''定理 1''' <math>P</math> 具有如下性质：

(1) 对于 <math>P</math> 中的任意元素 <math>S</math> ， <math>S=E</math> 或 <math>S_{0}=0</math> 。

(2) 对于 <math>P</math> 中的任意元素 <math>A ,B ,C ,D</math> ，若 <math>A \frown ( 0 ) \frown B^{+}=C \frown ( 0 ) \frown D^{+}</math> ，则 <math>A=C</math> 且 <math>B=D</math> 。

证明：

1. 运用结构归纳法，构造 <math>P</math> 来证明。

如果 <math>S=E</math> ，则 <math>S=E</math> 或 <math>S_{0}=0</math> 当然成立。假设存在 <math>( s ,t ) \in P^{2}</math> ，使得 <math>S=s \frown (0) \frown t^{+},</math> 且两者均满足条件。如果 <math>s=E</math> ，则 <math>S=s \frown (0) \frown t^{+}=E \frown (0) \frown t^{+}=(0) \frown t^{+},</math> 因此 <math>S_{0}=0</math> 。如果 <math>s_{0}=0</math> ，则 <math>S=s \frown (0) \frown t^{+},</math> 因此 <math>S_{0}=0</math> 。结构归纳表明，对于 <math>P</math> 的任何元素 <math>S</math> ， <math>S=E</math> 或“ <math>S</math> 的第一个项为 0”。

2. 证明逆否命题。换句话说，由于 <math>A \neq C</math> 或 <math>B \neq D</math> ，我们证明 <math>A \frown (0) \frown B^{+} \neq C \frown (0) \frown D^{+}.</math> 如果 <math>A \neq C</math> ，则长度 <math>( A ) \neq \mathrm {length} ( C )</math> ，或者存在 <math>n < \mathrm {length} ( A )</math> ，使得 <math>A_{n} \neq C_{n}</math> 。如果长度 <math>( A ) \neq \mathrm {length} ( C )</math> ，则（不失一般性，令长度 <math>( A ) < \mathrm {length} ( C ) ,</math> ）<math>(C \frown (0) \frown D^{+})_{\text {length} (C)}=((0) \frown D^{+})_{0}=0.</math> 然而，

<math>\begin{array}{l} (A \frown (0) \frown B^{+})_{\text {length} (C)} \\=\left(\left(0\right) \frown B^{+}\right)_{\text {length} (C)-\text {length} (A)} \\=B_{\text {length} (C)-\text {length} (A)-1}^{+} > 0,\\ \end{array}</math>

所以 length(C) 项不匹配，因此 <math>A \frown (0) \frown B^{+} \neq C \frown (0) \frown D^{+}.</math> 如果存在 <math>n < \mathrm {length} ( A )</math> 使得 <math>A_{n} \neq C_{n}</math> ，则对于 <math>n</math> ，<math>(A \frown (0) \frown B^{+})_{n} \neq (C \frown (0) \frown D^{+})_{n},</math> 因此 <math>A \frown (0) \frown B^{+} \neq C \frown (0) \frown D^{+}.</math> 如果 <math>A=C</math> 且 <math>B \neq D</math> ，则 <math>A \frown (0) \frown B^{+}=C \frown (0) \frown B^{+} \neq C \frown (0) \frown D^{+}.</math> 因此，如果 <math>A \neq C</math> 或 <math>B \neq D</math> ，则 <math>A \frown (0) \frown B^{+} \neq C \frown (0) \frown D^{+}.</math>

<math>P</math> 是由 <math>E</math> 和函数 <math>(A,B) \mapsto A \sim (0) \sim B^{+}</math> 生成的函数，上述定理断言它是自由生成的（ <math>P</math> 的一个元素不能用两种不同的方式表示）。由于它是下面证明中的一个重要函数，我们将其缩写为 <math>\operatorname{gen} (A,B) :=A \frown (0) \frown B^{+}.</math>

'''定义 2''' 函数 expand <math>: ( P \backslash \{E \} ) \times \mathbb {N} a r r o w \mathbb {N} < \omega</math> 定义如下。注意，定义域中的元素 <math>S</math> 不为空，因此 <math>S_{\perp}</math> 有定义。

(1) 如果 <math>S_{\perp}=0</math> ，则 <math>\operatorname{expand} (S) :=\operatorname{sub} (S,0,\operatorname{length} (S)-1).</math>

(2) 如果 <math>S_{\perp} > 0</math> ，则（根据引理 1.1.）<math>0 \in \{i \in \mathbb {N} \mid i < \operatorname{length} (S) \wedge S_{i} < S_{\square} \},</math> 因此 <math>\{i \in \mathbb {N} \mid i < \operatorname{length} (S) \wedge S_{i} < S_{\square} \}</math> 非空。

定义 <math>\operatorname{br} (S) :=\max \{i \in \mathbb {N} \mid i < \operatorname{length} (S) \wedge S_{i} < S_{\square} \},</math> <math>\operatorname{gp} (S) :=\operatorname{sub} (S,0,\operatorname{br} (S)),</math> <math>\operatorname{bp} (S) :=\operatorname{sub} (S,\operatorname{br} (S),\operatorname{length} (S)-1),</math> <math>\operatorname{expand} (S) :=\operatorname{gp} (S) \smile \underbrace {\operatorname{bp} (S) \smile \cdots \smile \operatorname{bp} (S)}_{n}.</math>

'''定理 2''' (1) 对于任意 <math>A \in P</math> ，<math>\operatorname{expand} (\operatorname{gen} (A,E),n)=A.</math>

(2) 对于任意 <math>( A ,B ) \in P^{2}</math> ，<math>\operatorname{expand} (\operatorname{gen} (A,\operatorname{gen} (B,E)),n)=A \frown \underbrace {(0) \frown B^{+} \frown \cdots \frown (0) \frown B^{+}}_{n}.</math>

(3) 对于任意的 <math>( A ,B ,C ) \in P^{2} \times ( P \backslash \{E \} )</math> ，<math>\operatorname{expand} (\operatorname{gen} (A,\operatorname{gen} (B,C)),n)=\operatorname{gen} (A,\operatorname{expand} (\operatorname{gen} (B,C),n)).</math>

证明：1. 若 <math>S :=\mathrm {gen} ( A ,E )</math> ，则 <math>S=A \frown (0) \frown E^{+}=A \frown (0).</math> 故 <math>S_{\perp}=0</math> 。因此 <math>\operatorname{expand} (S,n)=\operatorname{sub} (S,0,\operatorname{length} (S)-1)=A.</math>

2. 若 <math>S :=\operatorname{gen} (A,\operatorname{gen} (B,E)),</math> 则 <math>S=A \frown (0) \frown (B \frown (0) \frown E^{+})^{+}=A \frown (0) \frown B^{+} \frown (1).</math> 因此， <math>S_{\perp}=1 > 0</math> 

<math>\begin{array}{l} \operatorname{br} (S)=\max \left\{i \in \mathbb {N} \mid i < \operatorname{length} (S) \wedge S_{i} < S_{\square} \right\} \\=\max \left\{i \in \mathbb {N} \mid i < \operatorname{length} (S) \wedge S_{i} < 1 \right\}\\=\max \{i \in \mathbb {N} \mid i < \operatorname{length} (S) \wedge S_{i}=0 \}. \\ \end{array}</math>

这里，由于 <math>S_{\mathrm {length ~} ( A )}=0</math> ，因此 <math>\operatorname{length} (A) \in \{i \in \mathbb {N} \mid i < \operatorname{length} (S) \wedge S_{i}=0 \}.</math> 另外，对于任意 <math>n ></math> length <math>( S )</math> ，<math>S_{n}=\left(B^{+} \frown (1)\right)_{n-\text {length} (S)-1}=1 + \left(B \frown (0)\right)_{n-\text {length} (S)-1} > 0</math> 所以 <math>n \in \{i \in \mathbb {N} \mid i < \operatorname{length} (S) \wedge S_{i}=0 \}. </math> 因此，<math>\operatorname{br} (S)=\max \left\{i \in \mathbb {N} \mid i < \operatorname{length} (S) \wedge S_{i}=0 \right\}=\operatorname{length} (A).</math> 在这种情况下

<math>\begin{array}{l} \operatorname{gp} (S)=\operatorname{sub} (S,0,\operatorname{br} (S)) \\=\operatorname{sub} (A \frown (0) \frown B^{+} \frown (1),0 (A))\\=A. \\ \end{array}</math>

此外，

<math>\begin{array}{l} \operatorname{bp} (S)=\operatorname{sub} (S,\operatorname{br} (S),\operatorname{length} (S)-1) \\=\operatorname{sub} (A \smile (0) \smile B^{+} \smile (1),\text {length} (A),\text {length}. (S)-1) \\=(0) \frown B^{+}. \\ \end{array}</math>

因此 <math>\operatorname{expand} (S,n)=A \frown \underbrace {(0) \frown B^{+} \frown \cdots \frown (0) \frown B^{+}}_{n}.</math>

3. 若 <math>S :=\operatorname{gen} (A,\operatorname{gen} (B,C)),</math> 则

<math>\begin{array}{l} S=A \frown (0) \frown (B \frown (0) \frown C^{+})^{+} \\=A \frown (0) \frown B^{+} \frown (1) \frown C^{+ +}. \\ \end{array}</math>

由于 <math>C \neq E</math> ，<math>S_{\square}=C_{\square}^{+ +}=C_{\square} + 2 > 1.</math> 又由于 <math>S_{\text {length} (A) + 1 + \text {length} (B)}=1,</math> <math>\operatorname{length} (A) + 1 + \operatorname{length} (B) \in \{i \in \mathbb {N} \mid i < \operatorname{length} (S) \wedge S_{i} < S_{\square} \}.</math> 特别地，

<math>\begin{array}{l} \operatorname{br} (S)=\max \left\{i \in \mathbb {N} \mid i < \operatorname{length} (S) \wedge S_{i} < S_{\square} \right\}\\ \geq \operatorname{length} (A) + 1 + \operatorname{length} (B). \\ \end{array}</math>

令 <math>r :=\ker ( S )</math> ，则

<math>\begin{array}{l} \operatorname{br} (B \frown (0) \frown C^{+}) \\=\max \left\{i \in \mathbb {N} \mid i < \operatorname{length} \left(B \frown (0) \frown C^{+}\right) \right. \\ \land (B \smile (0) \smile C^{+})_{i} < (B \smile (0) \smile C^{+})_{\square} \}. \\ \end{array}</math>

由于 <math>\operatorname{length} (A) + 1 + \operatorname{length} (B \frown (0) \frown C^{+})=\operatorname{length} (S),</math> 我们有 <math>S_{\text {length} (A) + 1 + i}=\left(B \frown (0) \frown C^{+}\right)_{i}-1,</math> 且 <math>S_{\square}=(B \frown (0) \frown C^{+})_{\square}-1,</math>

<math>\begin{array}{l} \{i \in \mathbb {N} \mid i < \operatorname{length} (B \frown (0) \frown C^{+}) \\ \left. \wedge (B \frown (0) \frown C^{+})_{i} < (B \frown (0) \frown C^{+}) \square \right\} \\=\left\{i \in \mathbb {N} \mid \operatorname{length} (A) + 1 + i < \operatorname{length} (S) \wedge S_{\text {length} (A) + 1 + i}. \right. \\ \end{array}</math>

因此

<math>\begin{array}{l} \operatorname{br} (B \smile (0) \smile C^{+}) \\=\max \left\{i \in \mathbb {N} \mid i < \text {length} (B \frown (0) \frown C^{+}) \right. \\ \wedge (B \smile (0) \smile C^{+})_{i} < (B \smile (0) \smile C^{+})_{\square} \} \\=r-\operatorname{length} (A)-1. \\ \end{array}</math>

因此，<math>\operatorname{gp} (B \sim (0) \sim C^{+})=\operatorname{sub} (B \sim (0) \sim C^{+},0,r-\operatorname{length} (A)-1),</math> 所以

<math>\begin{array}{l} \mathrm {gp} (B \smile (0) \smile C^{+})^{+} \\=\operatorname{sub} \left(\left(B \frown (0) \frown C^{+}\right)^{+},0,r-\text {length}. (A)-1\right) \\=\operatorname{sub} (S \operatorname{length} (A) + 1,r). \\ \end{array}</math>

另外，由于

<math>\begin{array}{l} \mathrm {bp} (B \frown (0) \frown C^{+})=\operatorname{sub} (B \frown (0) \frown C^{+}, \\ r-\text {length} (A)-1,\text {length} (B \smile (0) \smile C^{+})),\\ \end{array}</math>

我们有

<math>\begin{array}{l} \mathrm {bp} (B \smile (0) \smile C^{+})^{+} \\=\operatorname{sub} \left(\left(B \frown (0) \frown C^{+}\right)^{+},r-\text {length} (A)-1,\text {length} \left(B \frown (0) \frown C^{+}\right)-1\right) \\=\operatorname{sub} (S,r,\text {length} (S)-1)^{-}. \\ \end{array}</math>

此外 <math>\operatorname{gp} (S)=\operatorname{sub} (S,0,r),\operatorname{bp} (S)=\operatorname{sub} (S,r,\text {length} (S)-1),</math> 因此

<math>\begin{array}{l} \operatorname{expand} (B \smile (0) \smile C^{+},n)^{+} \\=\mathrm {gp} (B \frown (0) \frown C^{+})^{+} \frown \\ \underbrace {\operatorname{bp} \left(B \frown (0) \frown C^{+}\right)^{+} \frown \cdots \frown \operatorname{bp} \left(B \frown (0) \frown C^{+}\right)^{+}}_{n} \\=\operatorname{sub} (S,\operatorname{length} (A) + 1,r) \frown \underbrace {\operatorname{bp} (S) \frown \cdots \frown \operatorname{bp} (S)}_{n}. \\ \end{array}</math>

于是我们得到

<math>\begin{array}{l} \operatorname{expand} (S,n) \\=\operatorname{sub} (S,0,r) \smile \underbrace {\mathrm {bp} (S) \smile \cdots \smile \mathrm {bp} (S)}_{n} \\=A \frown (0) \curvearrowleft \operatorname{sub} (S,\operatorname{length} (A) + 1,r) \curvearrowleft \underbrace {\operatorname{bp} (S) \curvearrowleft \cdots \operatorname{bp}^{(S)}}_{n}\\=A \smile (0) \smile \operatorname{expand} (B \smile (0) \smile C^{+},n)^{+}. \\ \end{array}</math>

证毕。

'''定理 3''' 对于任意 <math>S \in P</math> 和 <math>n \in \mathbb {N}</math> ， <math>S=E</math> 或 <math>\operatorname{expand} ( S ,n ) \in P</math> 。

证明：使用结构归纳法构造 <math>P</math> 。

<math>S=E</math> 的情况是平凡的。假设存在 <math>( T ,U ) \in P^{2}</math> 使得 <math>S=\mathrm {gen} ( T ,U )</math> ，并且两者都满足条件。如果 <math>U=E</math> ，则根据引理 2.1，展开 <math>( S ,n )=T \in P</math> 。从这里开始，假设存在 <math>( V ,W ) \in P^{2}</math> 使得 <math>U=\mathrm {gen} ( V ,W )</math> ，并且两者都满足条件。如果 <math>W=E</math> ，则根据引理 2.2 <math>S=\operatorname{gen} (T,\operatorname{gen} (V,E)).</math> 因此 <math>\operatorname{expand} (S,n)=T \frown \underbrace {(0) \frown V^{+} \frown \cdots \frown (0) \frown V^{+}}_{n}.</math> 现在，利用数学归纳法，我们可以证明 <math>\operatorname{expand} (S,0)=T \in P</math> 且 <math>\operatorname{expand} (S,k + 1)=\operatorname{expand} (S,k) \frown (0) \frown V^{+}=\operatorname{gen} (\operatorname{expand} (S,k),V)</math> 因此对于任何 <math>n \in \mathbb {N}</math> ，我们可以证明 <math>\operatorname{e x pand} ( S ,n ) \in P</math> 。如果 <math>W \neq E</math> ，则 <math>S=\operatorname{gen} (T,\operatorname{gen} (V,W)).</math> 因此 <math>\operatorname{expand} (S,n)=\operatorname{gen} (T,\operatorname{expand} (\operatorname{gen} (V,W),n))=\operatorname{gen} (T,\operatorname{expand} (U,n)) \in P,</math> 因此，对于任何 <math>S \in P</math> ， <math>S=E</math> 或 <math>\operatorname{e x pand} ( S ,n ) \in P</math> 。证毕。

引理 2 是根据 <math>P</math> 的结构对 expand 的行为进行分类的一种方式。引理 3 表明 expand 的输出也是 <math>P</math> 的一个元素。

通过对 <math>P</math> 结构进行递归，定义映射 trans: <math>P \to \varepsilon_{0}</math> ，如下所示。注意， <math>\varepsilon_{0}</math> 是加法和 <math>\omega</math> 运算下封闭的序数映射。

'''定义 3''' (1) 如果 <math>S=E</math> ，则 <math>\mathrm {trans} ( S ) :=0</math> 

(2) 如果存在 <math>( A ,B ) \in P^{2}</math> 使得 <math>S=\mathrm {gen} ( A ,B )</math> ，则 <math>\operatorname{trans} (S) :=\operatorname{trans} (A) + \omega^ {\operatorname{trans} (B)}.</math>

'''定理 4''' 对于任意 <math>S \in P ,n \in \mathbb {N}</math> ，都有 <math>S=E</math> 或 <math>\operatorname{trans} (\operatorname{expand} (S,n)) < \operatorname{trans} (S).</math>

证明：通过构造 <math>P</math> 的结构归纳法来证明。

当 <math>S=E</math> 时，这是平凡的。从现在开始，假设 <math>( T ,U ) \in P^{2}</math> 存在，使得 <math>S=\mathrm {gen} ( T ,U )</math> ，并且两者都满足条件。如果 <math>U=E</math> ，则 <math>S=\mathrm {gen} ( T ,E )</math> ，因此根据引理 2.1， <math>\operatorname{e x pand} ( S ,n )=T</math> 。因此

<math>\begin{array}{l} (\operatorname{expand} (S,n)) \\=\operatorname{trans} (T) < \operatorname{trans} (T) + \omega^ {0} \\=\operatorname{trans} (T) + \omega^ {\text {trans}} (E) \\=\operatorname{trans} (\operatorname{gen} (T,E)) \\=\operatorname{trans} (S). \\ \end{array}</math>

从现在开始，我们假设 <math>( V ,W ) \in P^{2}</math> 存在，使得 <math>U=\mathrm {gen} ( V ,W )</math> 且两者都满足条件。如果 <math>W=E</math> ，则 <math>S=\operatorname{gen} (T,\operatorname{gen} (V,E)),</math> 因此

<math>\begin{array}{l} \operatorname{trans} (S)) \\=\operatorname{trans} (\operatorname{gen} (T,\operatorname{gen} (V,E)))) \\=\operatorname{trans} (T) + \omega^ {\operatorname{trans} (\mathrm {gen} (V,E))}) \\=\operatorname{trans} (T) + \omega^ {\operatorname{trans} (V) + \omega^ {\operatorname{trans} (E)}} \\=\operatorname{trans} (T) + \omega^ {\operatorname{trans} (V) + 1}. \\ \end{array}</math>

另外，根据引理 2.2，<math>\operatorname{expand} (S,n)=T \frown \underbrace {(0) \frown V^{+} \frown \cdots \frown (0) \frown V^{+}}_{n}.</math> 通过数学归纳法，我们可以证明<math>\operatorname{trans} (\operatorname{expand} (S,n))=\operatorname{trans} (T) + \omega^ {\operatorname{trans} (V)} \times n.</math> 因此对于任意 <math>n \in \mathbb {N}</math> ，<math>\operatorname{trans} \left(\exp \left(S,n\right)\right)=\operatorname{trans} (T) + \omega^ {\operatorname{trans} (V)} \times n < \operatorname{trans} (T) + \omega^ {\operatorname{trans} (V) + 1}=\operatorname{trans} (S).</math> 若 <math>W \neq E</math> ，则根据引理 2.3 <math>\operatorname{expand} (S,n)=\operatorname{gen} (T,\operatorname{expand} (U,n).</math> 由于 <math>U</math> 满足 <math>\operatorname{trans} \left(\operatorname{expand} (U,n)\right) < \operatorname{trans} (U)</math> 因此

<math>\begin{array}{l} \operatorname{trans} (\operatorname{expand} (S,n)) \\=\operatorname{trans} \left(\operatorname{gen} (T,\text {expand} (U,n))\right)  \\=\operatorname{trans} (T) + \omega^ {\operatorname{trans} (\exp \left(U,n\right))} \operatorname{trans} (T) + \omega^ {\operatorname{trans} (U)} \\=\operatorname{trans} (S). \\ \end{array}</math>

因此，对于任意的 <math>S \in P ,n \in \mathbb {N}</math> ，都有 <math>S=E</math> 或 <math>\operatorname{trans} ( \exp \mathrm {and} ( S ,n ) ) < \operatorname{trans} ( S )</math> 。证毕。

'''定理 5''' 对于任意 <math>S \in P ,a : \mathbb {N} \mathbb {N}</math> ，都存在 <math>k \in \mathbb N</math> 使得 <math>S \left[a_{0} \right]\left[a_{1} \right]\dots \left[a_{k-1} \right]=E.</math>

证明：假设这样的 <math>k \in \mathbb N</math> 不存在。对于每个 <math>k \in \mathbb {N}</math> ，都有 <math>S \left[a_{0} \right]\left[a_{1} \right]\dots \left[a_{k-1} \right]\neq E,</math> 因此 <math>\operatorname{trans} \left(S[a_{0}][a_{1}]\dots[a_{k-1}]\right) \neq 0.</math> 因此，如果 <math>S \left[a_{0} \right]\left[a_{1} \right]\dots \left[a_{k-1} \right]</math> 有定义，则 <math>S[a_{0}][a_{1}]\dots[a_{k-1}][a_{k}]</math> 也有定义。根据数学归纳法，<math>S[a_{0}][a_{1}]\dots[a_{k-1}]</math> 对于任意 <math>k \in \mathbb N</math> 都有定义。然而，根据引理 4，<math>\operatorname{trans} (S) > \operatorname{trans} \left(S \left[a_{0} \right]\right) > \operatorname{trans} \left(S \left[a_{0} \right]\left[a_{1} \right]\right) > \dots</math> 这是一个无限递减的序数序列。这与序数的良序性相矛盾。矛盾的是，存在 <math>k \in \mathbb N</math> 使得 <math>S \left[a_{0} \right]\left[a_{1} \right]\dots \left[a_{k-1} \right]=E. </math> 这意味着无论选择哪种函数，初等序列都会在有限次数的迭代后都会变成空序列并停止。由此我们证明了 PrSS 的停机性。

<references />
[[分类:集合论相关]]