集合的形式化 #8 关系 (2) 全序关系、良序关系

    对于 S : 集合 A 和 r : 偏序关系 S，若 r 在 S 的范围内满足完全性，则 r 被称为 S 上的全序关系；对于 S : 集合 A 和 r : 严格偏序关系 S，若 r 在 S 的范围内满足完全性，则 r 被称为 S 上的严格全序关系。对于 r : 偏序关系 S，若 r 满足完全性，则 strict_po r 也满足完全性，所以每个全序关系都可自然对应于一个严格全序关系，这里用 strict_to 表示。对于 r : 全序关系 S，由于 S 中的任意两个元素都是可比较的，所以 x 是极大元当且仅当 x 是最大值，x 是极小元当且仅当 x 是最小值。

    对于 S : 集合 A 和 r : 全序关系 S，若 S 的任意非空子集都有最小值，则 r 被称为 S 上的良序关系；严格良序关系的定义详见代码。每个良序关系同样都可以自然对应于一个严格良序关系，与 strict_po 和 strict_to 一致，这里用 strict_wo 表示。

    已知 S : 集合 A 和 r : 良序关系 S，当需要证明某性质 P : A -> Prop 对 S 中的所有元素都成立时，可以利用良序关系对 S 进行归纳。这可被称为“超限归纳法”，具体的定理内容如下：

    证明思路：已知 A : Type，P : A -> Prop，S : 集合 A，r : 良序关系 S， （这里 y < x 表示 strict_wo r y x）；目标是  。由于  ，所以可将目标转化为  。反证，获得  的条件，目标变为 False。显然有  ，所以根据“wo良序”定理可得 （这里 min 表示 最小值 r），进而得到 a : A 和  ，从而有  ， ，（这里 a <= x 表示 r a x）。将这一命题变形得到  ，这样根据初始的条件就得到了  ，推出了 False。

    现在我们定义了名为“偏序关系”“全序关系”“良序关系”的对象，但这些对象无法直接用于表达“某关系在某集合上偏序/全序/良序”的概念。为了解决这个问题，我们按以下方案定义“偏序”“全序”“良序”等对象，这样“r 在 S 上偏序”就可以表达为“偏序 r S”：

    接下来，我们将证明著名的佐恩引理（Zorn's Lemma）。该定理可被描述为：若偏序集的任意全序子集都有上界，那么这个偏序集有极大元。为了证明它，我们需要先做一些准备工作。（注：虽然作者已经完成了这些定理的形式化证明并通过了 Coq 的验证，但在这里表述时为了思路尽可能清晰不会完全依照形式化证明来表述，故可能会出现错误或表述不准确的地方；而且由于作者在证明时参考了多个来源的证明，也可能会有绕远路的现象，敬请谅解）

    证明思路：根据“良序R'”定理，只需在 T ⊆ S，R ⊆ S，良序 r T，良序 r R，全序 r (T ∪ R)，Q : 集合 A，Q ⊆ T ∪ R，Q <> ∅ 的语境下证明 最小值 r Q <> None 。根据“子集良序”定理可证 良序 r (Q ∩ T) 和 良序 r (Q ∩ R) ，根据交集的分配律可证 Q = (Q ∩ T) ∪ (Q ∩ R) ，故只需证 最小值 r ((Q ∩ T) ∪ (Q ∩ R)) <> None 。当 Q ∩ T 是空集或 Q ∩ R 是空集时易证该结论。当 Q ∩ T 和 Q ∩ R 都不是空集时，可以得到 a, b : A 满足 Q ∩ T 的最小值是 a，Q ∩ R 的最小值是 b 。根据 全序 r (T ∪ R) 的条件可得 r a b \/ r b a 。若 r a b 则可证 最小值 r ((Q ∩ T) ∪ (Q ∩ R)) = Some a；若 r b a 则可证 最小值 r ((Q ∩ T) ∪ (Q ∩ R)) = Some b 。

    证明思路：（x <= y 表示 r x y ；x < y 表示 strict_po r x y）

    【第一部分：初期准备】当 X 为空集时易证结论。当 X 非空时可得 x0 : A，x0 ∈ X 。使用反证法，获得 forall Y, Y ⊆ X -> 良序 r Y -> 上界集 r Y \ Y <> ∅ 的条件（注：上界集 r Y \ Y 表示的是 (上界集 r Y) \ Y，即严格上界集），目标变为 False。通过存在实例化可证 exists s, forall Y, Y ⊆ X -> 良序 r Y -> s Y ∈ 上界集 r Y \ Y ，解构之得到 s : 集合 A -> A 和 forall Y, Y ⊆ X -> 良序 r Y -> s Y ∈ 上界集 r Y \ Y 。定义 P := fun Y => Y ⊆ X /\ 良序 r Y /\ (forall x, x ∈ Y \ 单集 x0 -> x = s { y | y ∈ Y /\ y < x }) /\ 最小值 r Y = Some x0 和 Ω := { x | P x } 。【第一部分结束，此时只有一个目标 False】

    【第二部分：该部分证明 forall Y Y', Y ∈ Ω -> Y' ∈ Ω -> Y \ Y' <> ∅ -> exists x, x ∈ Y /\ Y' = { k | k ∈ Y /\ k < x } 】首先解构整理条件，得到 Y, Y' : 集合 A ，Y ⊆ X ，Y' ⊆ X ，良序 r Y ，良序 r Y' ，x0 ∈ Y ，x0 ∈ Y' ，forall x, x ∈ Y -> x0 <= x ，forall x, x ∈ Y' -> x0 <= x ，forall x, x ∈ Y \ {x0} -> x = s { y | y ∈ Y /\ y < x } ，forall x, x ∈ Y' \ {x0} -> x = s { y | y ∈ Y' /\ y < x } ，Y \ Y' <> ∅ 。此时目标是 exists x, x ∈ Y /\ Y' = { k | k ∈ Y /\ k < x } 。由于 Y \ Y' 非空，所以有最小值，条件新增 x : A ，x ∈ Y \ Y' ，forall y, y ∈ Y \ Y' -> x <= y 。可证 { k | k ∈ Y /\ k < x } ⊆ Y' 。现在欲证明目标只需证明 x ∈ Y /\ Y' = { k | k ∈ Y /\ k < x } ，即只需证明 Y' ⊆ { k | k ∈ Y /\ k < x } 。此时目标是 Y' ⊆ { k | k ∈ Y /\ k < x } 。使用反证法，获得 Y' \ { k | k ∈ Y /\ k < x } <> ∅ 的条件，目标变为 False 。易证 Y' \ { k | k ∈ Y /\ k < x } 有最小值，条件新增 y : A ，y ∈ Y' ，~ (y ∈ Y /\ y < x) ，forall z, z ∈ Y' \ { k | k ∈ Y /\ k < x } -> y <= z 。可证 Y \ { k | k ∈ Y' /\ k < y } 非空，所以它有最小值，条件新增 z : A ，z ∈ Y ，~ (z ∈ Y' /\ z < y) ，forall t, t ∈ Y \ { k | k ∈ Y' /\ k < y } -> z <= t 。【接下来证明 { k | k ∈ Y /\ k < z } = { k | k ∈ Y' /\ k < y } ，根据“互为子集即相等”定理只需证明它们都是对方的子集：(1) 证明 { k | k ∈ Y /\ k < z } ⊆ { k | k ∈ Y' /\ k < y } ：已知 k ∈ Y ，k < z ，假设 ~ k ∈ { k | k ∈ Y' /\ k < y } ，则可得到 z <= k ，矛盾；(2) 证明 { k | k ∈ Y' /\ k < y } ⊆ { k | k ∈ Y /\ k < z } ：已知 k ∈ Y' ，k < y ，由（假设 ~ k ∈ Y ，则 y <= k ，矛盾）得 k ∈ Y ，假设 ~ k < z ，则 z <= k ，从而有 z < y ，由（假设 ~ k < x ，则 y <= k ，矛盾）得 k < x ，从而有 z < x ，根据已证的 { k | k ∈ Y /\ k < x } ⊆ Y' 得到 z ∈ Y' ，与条件 ~ (z ∈ Y' /\ z < y) 矛盾】。根据已有条件可证 z <= x 。依次证明：x0 < x ，x0 < y ，x0 < z ，进而由 z <> x0 和 y <> x0 分别得到 z = s { k | k ∈ Y /\ k < z } 和 y = s { k | k ∈ Y' /\ k < y } 。可证 z = y 。由（假设 z = x ，则 x = y ，易得矛盾）和已证的 z <= x 得 z < x ，进而得到 y < x ；由 z ∈ Y 得到 y ∈ Y 。这就与条件 ~ (y ∈ Y /\ y < x) 矛盾，推出了 False 。【第二部分结束，此时只有一个目标 False，新增条件 forall Y Y', Y ∈ Ω -> Y' ∈ Ω -> Y \ Y' <> ∅ -> exists x, x ∈ Y /\ Y' = { k | k ∈ Y /\ k < x } 】

    【第三部分：该部分从第二部分所得的结论出发得到一些推论】【首先证明 forall Y Y', Y ∈ Ω -> Y' ∈ Ω -> Y ⊆ Y' \/ Y' ⊆ Y ：当 Y \ Y' = ∅ 时，有 Y ⊆ Y' ；当 Y \ Y' <> ∅ 时，使用第二部分所得的结论，解构后得到 x : A ，x ∈ Y ，Y' = { k | k ∈ Y /\ k < x } ，从而有 Y' ⊆ Y 。】【接下来证明 forall Y Y', Y ∈ Ω -> Y' ∈ Ω -> Y' \ Y ⊆ 上界集 r Y \ Y ：当 Y' \ Y = ∅ 时显然。当 Y' \ Y <> ∅ 时，使用第二部分所得的结论，解构后得到 x : A ，x ∈ Y' ，Y = { k | k ∈ Y' /\ k < x } ，此时只需证明 Y' \ { k | k ∈ Y' /\ k < x } ⊆ 上界集 r { k | k ∈ Y' /\ k < x } \ { k | k ∈ Y' /\ k < x } ，即只需在 k : A ，k ∈ Y' ，~ (k ∈ Y' /\ k < x) 的语境下证明 k ∈ 上界集 r { j | j ∈ Y' /\ j < x } 。现在对 Y ∈ Ω 和 Y' ∈ Ω 进行解构和整理，得到 Y ⊆ X ，Y' ⊆ X ，良序 r Y ，良序 r Y' ，x0 ∈ Y ，x0 ∈ Y' ，forall x, x ∈ Y -> x0 <= x ，forall x, x ∈ Y' -> x0 <= x ，forall x, x ∈ Y \ {x0} -> x = s { y | y ∈ Y /\ y < x } ，forall x, x ∈ Y' \ {x0} -> x = s { y | y ∈ Y' /\ y < x } 。欲证明 k ∈ 上界集 r { j | j ∈ Y' /\ j < x } ，只需在 j : A ，j ∈ Y' ，j < x 的语境下证明 j <= k 。由 k ∈ Y' 和 ~ (k ∈ Y' /\ k < x) 可得 ~ k < x ，即 x <= k 。由 j < x 和 x <= k 得到 j <= k 。】【第三部分结束，此时只有一个目标 False，新增条件 forall Y Y', Y ∈ Ω -> Y' ∈ Ω -> Y ⊆ Y' \/ Y' ⊆ Y 和 forall Y Y', Y ∈ Ω -> Y' ∈ Ω -> Y' \ Y ⊆ 上界集 r Y \ Y 】

    【第四部分：该部分定义 Yi 并证明它的一些性质】定义 Yi := big并集 Ω 。展开定义后易证 Yi ⊆ X ，x0 ∈ Yi ，最小值 r Yi = Some x0 。【接下来证明 良序 r Yi ：利用已证的 forall Y Y', Y ∈ Ω -> Y' ∈ Ω -> Y ⊆ Y' \/ Y' ⊆ Y ，不难证明 全序 r Yi ，现在只需证明 forall S, S ⊆ Yi -> S <> ∅ -> 最小值 r S <> None ，即在 S : 集合 A ，S ⊆ Yi ，S <> ∅ 的语境下证明 最小值 r S <> None 。由 S 非空可得 a : A ，a ∈ S ，易得 a ∈ Yi ，由此可得 Y : 集合 A ，Y ∈ Ω ，a ∈ Y 。可证 最小值 r (S ∩ Y) <> None 。设 b : A ，最小值 r (S ∩ Y) = Some b ，解构之可得 b ∈ S ，b ∈ Y ，forall y, y ∈ S ∩ Y -> b <= y 。欲证明目标，只需证明 最小值 r S = Some b ，即只需证明 forall y, y ∈ S -> b <= y ，即在 y : A ，y ∈ S 的语境下证明 b <= y 。当 y ∈ Y 时，由已知条件易证 b <= y ；当 ~ y ∈ Y 时，由 y ∈ Yi 得到 Y' : 集合 A ，Y' ∈ Ω ，y ∈ Y' 。由第三部分证明的结论可得 Y' \ Y ⊆ 上界集 r Y \ Y ，所以 y 是 Y 的上界，b <= y 。】现在由已知条件可得 s Yi ∈ 上界集 r Yi \ Yi ，因此 s Yi ∈ X ，forall y, y ∈ Yi -> y <= s Yi ，~ s Yi ∈ Yi 。欲证明目标 False ，只需证明 s Yi ∈ Yi 。由于（在 Yi ∪ {s Yi} ∈ Ω 的语境下可证 exists T, T ∈ Ω /\ s Yi ∈ T 即 s Yi ∈ Yi），故只需证明 Yi ∪ {s Yi} ∈ Ω 。展开定义，该目标分解为 4 个子目标：Yi ∪ {s Yi} ⊆ X ，良序 r (Yi ∪ {s Yi}) ，forall x, x ∈ Yi ∪ {s Yi} \ {x0} -> x = s { y | y ∈ Yi ∪ {s Yi} /\ y < x } ，最小值 r (Yi ∪ {s Yi}) = Some x0 。【第四部分结束，此时有四个子目标，每个子目标都有新条件 Yi ⊆ X ，x0 ∈ Yi ，最小值 r Yi = Some x0 ，良序 r Yi ，s Yi ∈ X ，forall y, y ∈ Yi -> y <= s Yi 】

    【第五部分：该部分逐个证明四个子目标从而结束整个定理的证明】【证明目标1（Yi ∪ {s Yi} ⊆ X）：由 Yi ⊆ X 和 s Yi ∈ X ，显然。】【证明目标2（良序 r (Yi ∪ {s Yi})）：根据此前的准备工作“良序子集之并集”定理，只需证明 全序 r (Yi ∪ {s Yi}) 。从已知的 良序 r Yi 和 forall y, y ∈ Yi -> y <= s Yi 出发，不难证明。】【证明目标3（forall x, x ∈ Yi ∪ {s Yi} \ {x0} -> x = s { y | y ∈ Yi ∪ {s Yi} /\ y < x }）：分两种情况。【情况1】在 x : A ，x ∈ Yi ，x <> x0 的语境下证明 x = s { y | y ∈ Yi ∪ {s Yi} /\ y < x } ：解构整理条件得 Y : 集合 A ，Y ∈ Ω ，x ∈ Y ，Y ⊆ X ，良序 r Y ，forall x, x ∈ Y \ {x0} -> x = s { y | y ∈ Y /\ y < x } ，最小值 r Y = Some x0 。可证 x = s { y | y ∈ Y /\ y < x } ，故只需证明 { y | y ∈ Y /\ y < x } = { y | y ∈ Yi ∪ {s Yi} /\ y < x } ，根据“互为子集即相等”定理只需证明它们都是对方的子集：(1) 证明 { y | y ∈ Y /\ y < x } ⊆ { y | y ∈ Yi ∪ {s Yi} /\ y < x } ：已知 y : A ，y ∈ Y ，y < x ，易证 y ∈ Yi ；(2) 证明 { y | y ∈ Yi ∪ {s Yi} /\ y < x } ⊆ { y | y ∈ Y /\ y < x } ：分两种情况： (i) 在 y : A ，Y' : 集合 A ，Y' ∈ Ω ，y ∈ Y' ，y < x 的语境下证明 y ∈ Y ：假设 ~ y ∈ Y ，使用第二部分所得的结论可证 y ∈ 上界集 r Y \ Y ，进而 x <= y ，矛盾；(ii) 在 y : A ，y = s Yi ，y < x 的语境下证明 y ∈ Y ：由 x ∈ Yi 得 x <= s Yi ，即 x <= y ，矛盾。【情况2】在 x : A ，x = s Yi ，x <> x0 的语境下证明 x = s { y | y ∈ Yi ∪ {s Yi} /\ y < x } ：只需证明 Yi = { y | y ∈ Yi ∪ {s Yi} /\ y < x } ，即在 y : A 的语境下证明 (y ∈ Yi) = (y ∈ Yi ∪ {x} /\ y < x) 。利用 x = s Yi 可完成左推右，而右推左是显然的。】【证明目标4（最小值 r (Yi ∪ {s Yi}) = Some x0）：只需证明 forall x, x ∈ Yi ∪ {s Yi} -> x0 <= x 。在 x ∈ Yi 的情况中，解构得到 最小值 r Y = Some x0 和 x ∈ Y 后不难证明；在 x = s Yi 的情况中，结合已知的 forall y, y ∈ Yi -> y <= s Yi 即可完成证明。】【第五部分结束，“Zorn引理之引理”定理已完成证明】

    完成以上准备工作后，我们终于可以证明佐恩引理。

    证明思路：在 forall T, T ⊆ S -> 全序 r T -> 上界集 r T <> ∅ ，极大元集 r S = ∅ 的语境下证明 False 即可。极大元集 r S = ∅ 可变形为 forall x, x ∈ S -> exists y, y ∈ S /\ x < y 。【接下来证明 forall Z, 上界集 r Z <> ∅ -> 上界集 r Z \ Z <> ∅ ：在 Z : 集合 A ，z : A ，Z ⊆ S ， z ∈ S ，forall y, y ∈ Z -> y <= z 的语境下证明 exists x : A, (Z ⊆ S /\ x ∈ S /\ (forall y, y ∈ Z -> y <= x)) /\ ~ x ∈ Z 即可，由已知条件可得 x : A ，x ∈ S ，z < x ，易证 (Z ⊆ S /\ x ∈ S /\ (forall y, y ∈ Z -> y <= x)) /\ ~ x ∈ Z 】。根据此前的准备工作“Zorn引理之引理”定理，可得 Y : 集合 A ，Y ⊆ S ，良序 r Y ，上界集 r Y \ Y = ∅ 。由“良序则全序”定理和已知条件，上界集 r Y <> ∅ 。由刚刚证明的结论可进一步得到 上界集 r Y \ Y <> ∅ ，而这与 上界集 r Y \ Y = ∅ 矛盾，推出了 False 。至此，佐恩引理证毕。