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

我们给出 BMS 良序性的证明过程。<ref>VARGOVCIK S. Well-orderedness of the bashicu matrix system[A]. 2023.</ref><ref>小清新. 对 BMS 良序性证明的个人理解[EB/OL]. 2023. https://zhuanlan.zhihu.com/p/653719928.</ref>

'''定义''' 在 BMS 中给出如下定义和约定：

(1) 列和行均从 0 开始数起。例如 <math>(000)(111)</math> 的 <math>(000)</math> 是第 0 列。

(2) <math>A</math>：一般指一个 BMS。

(3) <math>A[n]</math>：一般指 <math>A</math> 的基本列第 <math>n</math> 项。

(4) <math>G</math>：一般指“好部”。

(5) <math>B_{x}</math>：一般指“坏部”，其中 <math>B_{0}</math> 一般指最前面的“坏部”。

(6) <math>C</math>：一般指 <math>A</math> 的最后一列。

(7) <math>A_{1} + A_{2}</math>：指把 <math>A_{2}</math> 连接在 <math>A_{1}</math> 的后面，例如 <math>(000)(111) + (222)(333) = (000)(111)(222)(333)</math>。

(8) '''<math>m</math> 父项'''：列 <math>i</math> 是列 <math>j</math> 的 <math>m</math> 父项当且仅当 <math>i < j</math>，列的第 <math>m</math> 个元素小于列 <math>j</math> 的第 <math>m</math> 个元素，当 <math>m > 0</math> 时还需列 <math>i</math> 是列 <math>j</math> 的 <math>m-1</math> 祖先，同时是满足此定义中的最大者。若不存在这样的列 <math>i</math>，则列 <math>j</math> 没有 <math>m</math> 父项。

(9) '''<math>m</math> 祖先'''：列 <math>i</math> 是列 <math>j</math> 的 <math>m</math> 祖先当且仅当列 <math>i</math> 是列 <math>j</math> 的 <math>m</math> 父项或列 <math>i</math> 是列 <math>j</math> 的 <math>m</math> 父项的 <math>m</math> 祖先。（即列 <math>j</math> 的 <math>m</math> 父项，列 <math>j</math> 的 <math>m</math> 父项的 <math>m</math> 父项，列 <math>j</math> 的 <math>m</math> 父项的 <math>m</math> 父项的 <math>m</math> 父项……）例如：在 <math>(000)(111)(220)(331)</math> 中，<math>(220)</math> 是 <math>(331)</math> 的 0 父项、1 父项、2 父项，因此也是 <math>(331)</math> 的 0 祖先、1 祖先、2 祖先。<math>(111)</math> 是 <math>(220)</math> 的 0 父项、1 父项，但不是 <math>(220)</math> 的 2 父项。因此，<math>(111)</math> 是 <math>(331)</math> 的 0 祖先、1 祖先，但不是 2 祖先。

(10) 一个非空的 BMS 可以写成这样的形式：<math>A = G + B_{0} + C</math>，其基本列第 <math>n</math> 项可以写为 <math>A[n] = G + B_{0} + \dots + B_{n}</math>。其中，<math>B_{0}</math> 的第 0 列是 <math>C</math> 的 <math>m_{0}</math> 父项，若 <math>m_{0}</math> 无定义，则 <math>B_{0}</math> 为空。

(11) '''提升'''：设 <math>D</math> 为 <math>B_{0}</math> 中的一列，若 <math>D</math> 为 <math>B_{0}</math> 的第 0 列或 <math>B_{0}</math> 的第 0 列是 <math>D</math> 的 <math>m</math> 祖先，则 <math>D</math> 的第 <math>m</math> 个元素称为提升的（这一定义与原文不同，为行文方便做了修改）。<math>B_{i}</math> 是 <math>B_{0}</math> 的一个复制，但是每个满足行标 <math>m < m_{0}</math> 的提升的元素都要增加 <math>i \times (C</math> 的第 <math>m</math> 个元素 <math>- B_{0}</math> 首列的第 <math>m</math> 个元素<math>)</math>。

'''引理 1''' BMS 在字典序下是全序的。

这定理说的是，任何两个 BMS 都可以比大小。关于这一定理的详细证明从略。

进一步有 BMS 的如下性质：

'''引理 2''' 设 <math>A = G + B_{0} + C</math> 是一个非空的 BMS，<math>n</math> 是一个自然数，<math>l_{0}, l_{1}</math> 分别为 <math>G, B_{0}</math> 的长度。则有以下五点成立：

(1) 任取 <math>i < l_{0}, j < l_{1}, k \in \mathbb{N}</math>，<math>G</math> 的第 <math>i</math> 列是 <math>B_{0}</math> 的第 <math>j</math> 列的 <math>k</math> 祖先当且仅当 <math>G</math> 的第 <math>i</math> 列是 <math>B_{n}</math> 的第 <math>j</math> 列的 <math>k</math> 祖先。

(2) 任取 <math>i, j < l_{1}, k \in \mathbb{N}</math>，<math>B_{0}</math> 的第 <math>i</math> 列是 <math>B_{0}</math> 的第 <math>j</math> 列的 <math>k</math> 祖先当且仅当 <math>B_{n}</math> 的第 <math>i</math> 列是 <math>B_{n}</math> 的第 <math>j</math> 列的 <math>k</math> 祖先。

(3) 设 <math>n > 0, i < l_{1}, k < m_{0}</math>，<math>B_{0}</math> 的第 <math>i</math> 列是 <math>C</math> 的 <math>k</math> 祖先当且仅当 <math>B_{n-1}</math> 的第 <math>i</math> 列是 <math>B_{n}</math> 第 <math>0</math> 列的 <math>k</math> 祖先。

(4) 设 <math>0 < i < l_{1}</math>，<math>B_{n}</math> 的第 <math>i</math> 列的 <math>k</math> 父项只会在 <math>G</math> 或 <math>B_{n}</math> 中。

(5) 任取 <math>i, j < l_{1}, k \in \mathbb{N}, n_{0} < n_{1} < n</math>，<math>B_{n_{0}}</math> 的第 <math>i</math> 列是 <math>B_{n_{1}}</math> 的第 <math>j</math> 列的 <math>k</math> 祖先当且仅当 <math>B_{n_{0}}</math> 的第 <math>i</math> 列是 <math>B_{n_{1} + 1}</math> 的第 <math>j</math> 列的 <math>k</math> 祖先。

（注意，以上的列是从第 0 列开始数的）

证明：用数学归纳法，先证明 <math>k = 0</math> 时定理 2 成立，再假设对所有 <math>k' < k</math>，定理 2 成立（五条全部成立），尝试说明此时定理 2 对 <math>k</math> 成立。

先考虑 <math>k = 0</math> 的情况：

首先证明 (2)：<math>j = 0</math> 时 <math>B_{0}</math> 的第 <math>j</math> 列在 <math>B_{0}</math> 当中不会有祖先（因为它自己就是 <math>B_{0}</math> 最左的一列），因此结论平凡成立。<math>j > 0</math> 时，若 <math>m_{0} = 0</math>，则 <math>B_{0} = B_{n}</math>；若 <math>m_{0} > 0</math>，不难看出 <math>B_{0}</math> 中每一列的第 0 个元素都是提升的，因此 <math>B_{0}</math> 和 <math>B_{n}</math> 当中的 0 祖先关系保持一致，此时 (2) 成立。

(3)：与 (2) 类似，因为假设了 <math>m_{0} > 0</math>，因此 <math>B_{n}</math> 的第 0 个元素不会比 <math>C</math> 的第 0 个元素小。

(4)：<math>B_{0}</math> 的第 0 列一定是 <math>B_{0}</math> 的第 <math>i</math> 列的 0 祖先，因此，用 <math>k = 0</math> 时的 (2)，可得 <math>B_{n}</math> 的第 0 列也是 <math>B_{n}</math> 的第 <math>i</math> 列的 0 祖先。因此，<math>B_{n}</math> 第 <math>i</math> 列的 0 父项自然也会在 <math>B_{n}</math> 中。

(1)：显然，只需注意到若 <math>G</math> 中第 <math>i</math> 列是 <math>B_{0}</math> 中某列的 0 祖先，则任何 <math>B_{x}</math> 中都不会有比其第 0 个元素小的列。

(5)：与 (1) 类似，显然。

接下来，假设定理 2 对 <math>k' < k</math> 成立，考虑 <math>k</math> 的情况：

(2)：<math>j = 0</math> 时显然。<math>j > 0</math> 时设 <math>I</math> 为 <math>B_{0}</math> 第 <math>j</math> 列的 <math>k-1</math> 祖先的列号组成的集合（例如若 <math>B_{0}</math> 是 <math>(00)(11)(22)</math>，<math>k = 1</math>，则此时的 <math>I = \{0, 1\}</math>），则显然有 <math>i \in I</math>，此时有两种情况。

情况一：<math>B_{0}</math> 的首列是 <math>B_{0}</math> 第 <math>j</math> 列的 <math>k</math> 祖先，则此时第 <math>j</math> 列的第 <math>k</math> 个元素就是提升的，同时，第 <math>i</math> 列的第 <math>k</math> 个元素也是提升的，因为要么 <math>i = 0</math>，要么首列也是第 <math>i</math> 列的一个 <math>k</math> 祖先。不难看出，此时所有 <math>I</math> 中的列，第 <math>k</math> 个元素都是提升的。因此在 <math>B_{n}</math> 当中，若第 <math>j</math> 列的第 <math>k</math> 个元素有增加，则 <math>I</math> 中其他列的第 <math>k</math> 个元素也得到了同样的增加，又由于归纳假设，<math>B_{n}</math> 中第 <math>j</math> 列的 <math>k-1</math> 祖先也都是序号在 <math>I</math> 中的那些列，因此 <math>B_{n}</math> 中的祖先关系与 <math>B_{0}</math> 中保持一致。

情况二：<math>B_{0}</math> 的首列不是 <math>B_{0}</math> 第 <math>j</math> 列的 <math>k</math> 祖先，则第 <math>j</math> 列的第 <math>k</math> 个元素是不提升的，且任何 <math>k</math> 祖先所在列的第 <math>k</math> 个元素也是不提升的。又由归纳假设，在 <math>B_{n}</math> 当中祖先关系与 <math>B_{0}</math> 中保持一致。（反过来，<math>B_{n}</math> 推出 <math>B_{0}</math> 也是类似的，第 <math>k</math> 个元素要提升则整个 <math>I</math> 一起提升，若不提升则所有第 <math>j</math> 列的 <math>k</math> 祖先对应的第 <math>k</math> 个元素都不提升。）

(3)：与 (2) 类似，<math>k < m_{0}</math> 保证了 <math>B_{1}</math> 的第 0 个元素不会比 <math>C</math> 的小。

(4)：若存在 <math>k' < k</math>，使得 <math>B_{n}</math> 第 <math>i</math> 列的 <math>k'</math> 父项在 <math>G</math> 中，则 <math>B_{n}</math> 第 <math>i</math> 列的 <math>k</math> 父项也必然在 <math>G</math> 中。配合归纳假设，设对所有 <math>k' < k</math>，<math>B_{n}</math> 第 <math>i</math> 列的 <math>k'</math> 父项都在 <math>B_{n}</math> 中。若存在某个 <math>k'</math> 使得 <math>B_{n}</math> 的首列不是第 <math>i</math> 列的 <math>k'</math> 祖先，则使用归纳假设，可知第 <math>i</math> 列所有的 <math>k'</math> 祖先均在 <math>G</math> 或 <math>B_{n}</math> 中，因此它的 <math>k</math> 父项也必然在其中。若对任意的 <math>k' < k</math>，都有 <math>B_{n}</math> 的首列是第 <math>i</math> 列的 <math>k'</math> 祖先，假设 <math>B_{n}</math> 的第 <math>i</math> 列的 <math>k</math> 父项不在 <math>B_{n}</math> 中，我们证明它一定在 <math>G</math> 中。若 <math>B_{n}</math> 的第 <math>i</math> 列的 <math>k</math> 父项不在 <math>B_{n}</math> 中，则 <math>B_{n}</math> 的首列不是第 <math>i</math> 列的 <math>k</math> 祖先。因此，第 <math>i</math> 列的第 <math>k</math> 个元素一定是不提升的，它与 <math>B_{0}</math> 的第 <math>i</math> 列第 <math>k</math> 个元素相等。由 (ii) 可知，<math>B_{0}</math> 中也不存在某列是第 <math>i</math> 列的 <math>k</math> 父项，因此它的 <math>k</math> 父项一定在 <math>G</math> 中。同时，对于 <math>B_{0}</math> 中所有第 <math>i</math> 列的 <math>k-1</math> 祖先，它们的第 <math>k</math> 个元素一定会大于等于第 <math>i</math> 列的第 <math>k</math> 个元素，因此也大于等于 <math>B_{n}</math> 第 <math>i</math> 列的第 <math>k</math> 个元素。因此，若 <math>B_{n}</math> 第 <math>i</math> 列的 <math>k</math> 父项不在 <math>B_{n}</math> 中，那么它也会是 <math>B_{n}</math> 首列的一个 <math>k</math> 祖先。当 <math>k \geq m_{0}</math> 时，<math>B_{n}</math> 首列的 <math>m_{0}</math> 父项就已经在 <math>G</math> 中了，与我们的假设矛盾。当 <math>k < m_{0}</math> 时，由于 <math>B_{0}</math> 的首列是 <math>C</math> 的 <math>m_{0}</math> 父项，因此也是 <math>C</math> 的 <math>k</math> 祖先，反复使用 (iii) 可得对每个 <math>m > 0</math>，<math>B_{m-1}</math> 的首列都是 <math>B_{m}</math> 首列的 <math>k</math> 祖先。设存在 <math>n' < n</math> 使得 <math>B_{n}</math> 第 <math>i</math> 列的 <math>k</math> 父项在 <math>B_{n'}</math> 中，则由于此列和 <math>B_{n'}</math> 的首列均为 <math>B_{n}</math> 首列的 <math>k</math> 祖先，因此 <math>B_{n'}</math> 的首列也会是此列的 <math>k</math> 祖先，而这是不可能的（<math>B_{n'}</math> 的首列的第 <math>k</math> 个元素严格大于此列的第 <math>k</math> 个元素）。

(1)：若 <math>B_{0}</math> 的首列是第 <math>j</math> 列的 <math>k</math> 祖先，则也是 <math>B_{n}</math> 第 <math>j</math> 列的 <math>k</math> 祖先，此时 (i) 成立。若 <math>B_{0}</math> 的首列不是第 <math>j</math> 列的 <math>k</math> 祖先，由 (iv) 可知 <math>B_{n}</math> 第 <math>j</math> 列的 <math>k</math> 祖先只在 <math>B_{n}</math> 和 <math>G</math> 中，由于此时 <math>B_{0}</math> 第 <math>j</math> 列第 <math>k</math> 个元素不提升，因此 <math>G</math> 中最右边的祖先列也会是 <math>B_{0}</math> 第 <math>j</math> 列的 <math>k</math> 祖先，此时 (i) 成立。

(5)：若 <math>B_{n_{0}}</math> 的第 <math>i</math> 列是 <math>B_{n_{1}}</math> 的第 <math>j</math> 列的 <math>k</math> 祖先，则由 (iv)，<math>B_{n_{1}}</math> 的首列也是 <math>B_{n_{1}}</math> 的第 <math>j</math> 列的 <math>k</math> 祖先，因此 <math>B_{n_{0}}</math> 的第 <math>i</math> 列是 <math>B_{n_{1}}</math> 的首列的 <math>k</math> 祖先。若 <math>k \geq m_{0}</math>，则与 <math>B_{n_{1}}</math> 的首列的 <math>k</math> 父项在 <math>G</math> 中矛盾。若 <math>k < m_{0}</math>，则可以使用 (iii)，得到 <math>B_{n_{0}}</math> 的第 <math>i</math> 列是 <math>B_{n_{1} + 1}</math> 的首列的 <math>k</math> 祖先，再由 (ii) 可得结论，反过来的方向也类似。

利用数学归纳法，在每一层都是 2、3 推出 4，2、3、4 推出 1、5，因此我们就证明了全部的结论。

然后是关于稳定序数的定理。记 <math>\langle L_\alpha,\in\rangle</math> 是第 <math>\alpha</math> 个可构造宇宙层级， <math>M \preceq_{\Sigma_n} N</math> 代表 <math>M</math> 是 <math>N</math> 的 <math>\Sigma_n</math> 初等子结构。记 <math>\alpha \le_n \beta</math> 代表 <math>\langle L_\alpha,\in\rangle \preceq_{\Sigma_{n+1}} \langle L_\beta,\in\rangle</math> ，特别的， <math>\alpha \le_n \mathrm{Ord}</math> 代表 <math>\langle L_\alpha,\in\rangle \preceq_{\Sigma_{n+1}} \langle L,\in\rangle</math> 。记 <math>\sigma</math> 是最小的序数使得存在 <math>\beta</math> ，有任取 <math>n \in \mathbb{N}</math> ，都有 <math>\sigma \le_n \beta</math> 成立。

'''引理 3''' 任取 <math>\alpha,\beta \in \sigma</math>，<math>n \in \mathbb{N}</math> ，若 <math>\omega<\alpha<_n\beta</math> ，任取 <math>X,Y</math> 为有限集，满足 <math>\gamma<\alpha \le \delta<\beta</math> 对任意的 <math>\gamma \in X,\delta \in Y</math> ，存在一个序数集合 <math>Y'</math> 和一个双射 <math>f: Y \rightarrow Y'</math> 对任意 <math>\gamma \in X,\delta_0,\delta_1 \in Y,n \in \mathbb{N},m<n</math> 有以下五条性质:

(1) <math>\gamma<f(\delta_0)<\alpha</math> . 

(2) <math>\gamma <_k \delta_0 \rightarrow \gamma <_k f(\delta_0)</math> . 

(3) <math>\delta_0<\delta_1 \rightarrow f(\delta_0)<f(\delta_1)</math> . 

(4) <math>\delta_0 <_k \delta_1 \rightarrow f(\delta_0) <_k f(\delta_1)</math> . 

(5) <math>\delta_0 <_m \beta \rightarrow f(\delta_0) <_m \alpha</math> 

证明这一引理的思路是构造一个合适的 <math>\Sigma_{n+1}</math> 公式，它能反应我们想要的性质，同时使得它可以在 <math>L_\beta</math> 中验证为真 (代入 <math>Y</math> 中的元素)，因此它在 <math>L_\alpha</math> 中也为真，能使得它为真的那组参数就组成了 <math>Y'</math> 。

证明：记 <math>\gamma_0,\dots,\gamma_{|X|-1} \in X</math> 为固定参数，记 <math>\varphi_0(\eta,\xi)</math> 为 <math>\eta<\xi</math>，<math>\varphi_1(\eta,\xi,k)</math> 为 <math>\eta<_k\xi</math>，<math>\varphi_2(\eta,k)</math> 为 <math>\eta<_k\mathrm{Ord}</math> 。则 <math>\varphi_0</math> 是 <math>\Sigma_0</math> 公式， <math>\varphi_1</math> 是 <math>\Sigma_1</math> 公式，文章[2]的定理 1.8 证明了 <math>\varphi_2</math> 是 <math>\Pi_{k+1}</math> 公式，因此也是 <math>\Sigma_{k+2}</math> 公式。由于 <math>k<n</math> ，这三条公式全都是 <math>\Sigma_{n+1}</math> 公式。由于这里提到的所有序数都在 <math>\sigma</math> 之下，因此任取 <math>\eta,\xi \in X \cup Y</math> ，都只有有限个 <math>k</math> 使得 <math>\varphi_1(\eta,\xi,k)</math> 成立。因此，只有有限个句子 <math>\varphi_0(\gamma_i,\zeta_j),\varphi_1(\gamma_i,\zeta_j,k),\varphi_0(\zeta_i,\zeta_j),\varphi_1(\zeta_i,\zeta_j,k),\varphi_2(\zeta_i,m)</math> 在代入 <math>\delta_i</math> 为 <math>Y</math> 中第 <math>i</math> 小的元素时为真。记 <math>\varphi</math> 为这些句子的合取，则 <math>\varphi</math> 为 <math>\Sigma_{n+1}</math> 公式。同时令 <math>\psi</math> 为断言所有这些 <math>\zeta_i</math> 为序数的句子，则 <math>\varphi \wedge \psi</math> 为 <math>\Sigma_{n+1}</math> 公式。最后，句子 <math>\exists \zeta_0 \exists \zeta_1 \dots \exists \zeta_{|Y|-1}(\varphi \wedge \psi)</math> 也是 <math>\Sigma_{n+1}</math> 公式。在 <math>L_\beta</math> 中，把 <math>Y</math> 中的元素代入，就知道这个句子是真的。又因为 <math>\alpha <_n \beta</math> ，可知在 <math>L_\alpha</math> 中这个句子也是真的。因此， <math>L_\alpha</math> 中使得这个句子为真的那些取值组合成 <math>Y'</math>，<math>Y</math> 和 <math>Y'</math> 之间自然的序同构记为 <math>f</math> ，则引理 3 成立。(例如第一条，在 <math>L_\alpha</math> 中取 <math>\zeta_j</math> 为 <math>f(\delta_j)</math>，<math>\varphi_0(\gamma_i,\zeta_j)</math> 就是说 <math>\gamma_i<f(\delta_j)</math> ，也即第一条性质成立，其他四条也可以用类似的方式得到。)

综合上述两条定理，我们就可以证明 BMS 的良序性

'''定理''' BMS 在字典序下是良序的。

证明的思路是构造一个映射 <math>o:\mathrm{BMS}\to\mathrm{Ord}</math> ，只需证明该映射是保序的即可。定义BMS 的稳定表示函数：设 <math>A</math> 为一个 <math>n</math> 列的 BMS，一个函数 <math>f: n \rightarrow \mathrm{Ord}</math> 是 <math>A</math> 的稳定表示，当且仅当对任意的 <math>i<j<n</math> ，有 <math>f(i)<f(j)</math> 且若 <math>A</math> 的第 <math>i</math> 列为第 <math>j</math> 列的 <math>m</math> 祖先，则 <math>f(i) <_m f(j)</math> 。可以看出，同一个 BMS，对应的稳定表示函数可以有很多。例如任何满足 <math>\alpha <_0 \beta</math> 的序数 <math>\alpha</math> 和 <math>\beta</math> ， <math>f(0)=\alpha,f(1)=\beta</math> 都可以作为 (0)(1) 的稳定表示函数。

定义 <math>o(A)</math> 为最小的序数 <math>\alpha</math> 使得存在一个 <math>A</math> 的稳定表示函数 <math>f</math> ，满足 <math>f(n-1) \le \alpha</math> 。为方便起见，记 <math>\mathrm{BMS}[n]=(0\dots0)(1\dots1)</math> 共 <math>n</math> 个 0 和 <math>n</math> 个 1 ， <math>X_n=\{\mathrm{BMS}[i_0][i_1]\dots[i_n] \}</math> .为方便起见，记 <math>\mathrm{BMS}[n]=(0\dots0)(1\dots1)</math> ，共 <math>n</math> 个 0 和 <math>n</math> 个 1， <math>X_n=\{\mathrm{BMS}[i_0][i_1]\dots[i_n] \}</math> .

证明：(对展开次数做归纳) 首先证明 <math>o</math> 在 <math>X_0</math> 上是保序的，随后证明若 <math>o</math> 在 <math>X_n</math> 是保序的，则 <math>o</math> 在 <math>X_{n+1}</math> 上是保序的。这样就证明了 <math>o</math> 是保序的。

对 <math>X_0</math> ，不难看出若 <math>\alpha_n</math> 是最小的满足存在 <math>\beta_n</math> ，使得 <math>\alpha_n <_{n-1} \beta_n</math> ，则 <math>o((0\dots0)(1\dots1)) = \beta_n</math> （共 <math>n</math> 个 0， <math>n</math> 个 1 ）。因此，显然有 <math>o</math> 在 <math>X_0</math> 上保序。

设 <math>o</math> 在 <math>X_n</math> 上保序，想证明 <math>o</math> 在 <math>X_{n+1}</math> 上保序。任取非空的 BMS <math>A \in X_n</math> ，设 <math>A</math> 的长度为 <math>l</math> 记 <math>f</math> 是 <math>A</math> 的稳定表示，使得 <math>o(A) \ge f(l-1)</math> 。记 <math>l_n</math> 为 <math>A[n]</math> 的长度，则 <math>f</math> 限制在 <math>l_0</math> 上就是 <math>A[0]</math> 的一个稳定表示，记为 <math>f_0</math> 。接下来，我们将递归构造 <math>A[n]</math> 的稳定表示 <math>f_n</math> 。

设 <math>f_k</math> 为 <math>A[k]</math> 的稳定表示，且将 <math>B_k</math> 对应的列号映射到 <math>B_0</math> 对应的列号在 <math>f</math> 下的像。设 <math>\alpha</math> 为 <math>B_0</math> 的首列的列号在 <math>f</math> 下的像， <math>\beta</math> 为 <math>A</math> 的最后一列的列号在 <math>f</math> 下的像。设 <math>Y</math> 为 <math>B_k</math> 对应的列号在 <math>f_k</math> 下的像集， <math>X</math> 为 <math>B_k</math> 之前的列号在 <math>f_k</math> 下的像集 (因此， <math>X</math> 可能为空，但 <math>Y</math> 一定非空) 。由于前述引理，存在那样的 <math>Y'</math> ，我们把 <math>B_k</math> 对应的列号映射到 <math>Y'</math> 的对应元素， <math>B_{k+1}</math> 对应的列号映射到 <math>Y</math> 的对应元素，其他列号的像不变，就得到了 <math>f_{k+1}</math> 。由于引理 2， <math>f_{k+1}</math> 是 <math>A[k+1]</math> 的一个稳定表示，同时它将 <math>B_{k+1}</math> 对应的列号映射到 <math>B_0</math> 对应的列号在 <math>f</math> 下的像。这样，我们就得到了所有的 <math>f_n</math> ，同时，由于任取 <math>m<n</math> <math>f_n</math> 在 <math>l_m</math> 处截断都能得到一个 <math>A[m]</math> 的稳定表示，因此有 <math>m<n \rightarrow o(A[m])<o(A[n])<o(A)</math> 。因此， <math>o</math> 在 <math>X_{n+1}</math> 保序。

这样我们就得到了 <math>o</math> 是保序的（因为任何 BMS 都可以由 BMS 极限取有限次基本列得到），因此 BMS 是良序的，证明完毕。

== 参考资料 ==