集合的形式化 #9 基数 (1) 基数的序

    在数学上，基数是一种用来描述集合的元素个数的数。对于集合 S，card S 是一个基数，表示 S 的元素个数。直观上，我们可以这样快速地理解基数：card ∅ = 0，card {3} = 1，card {10, 7} = 2，card N = ℵ0（由于自然数集是无限的，所以自然数集的基数无法用一个自然数表示）。接下来我们将通过形式化的方法严格地定义基数。

    由于我们只需要让“基数”称为一种新的类型，因此可以使用等价类构造的方法（不同于 ZFC）。我们希望 {0, 1}，{true, false}，{Some 1, None} 都能对应到相同的基数，这就需要找到一个等价关系：等势。

    对于（类型可能不同的）集合 S 和 T，S 和 T 是等势的当且仅当存在一个 S 到 T 的双射函数，即 S 和 T 之间能够建立起一一对应的关系。利用已定义的 f_id、反函数、复合函数，易证等势自反、等势对称、等势传递。然而，这些定理并不能直接用于得到一个等价关系，因为等价关系要求建立在一个类型上，而 @等势 : forall A B : Type, 集合 A -> 集合 B -> Prop，类型不符。为了解决这个问题，我们可以定义 uset等势。

    uset等势 具有类型 uset -> uset -> Prop，符合等价关系的要求。现在，有了 等势_等价关系，我们可以通过 等价类构造类型' 定义基数类型。

    对于 S : 集合 A，card S 的类型是基数，表示 S 中元素的个数。对于（类型可能不同的）集合 S 和 T，card S = card T 等价于 S 和 T 等势。对于 A : 基数，基数构造集合 A 的类型是 uset（具有 uset 类型的对象可被解构为一个类型和这个类型上的一个集合），可用于从一个基数中得到一个集合 S 使得 card S 恰好等于这个基数。“forall基数”定理可将一个基数问题转化为一个集合问题，将在基数性质的证明中被广泛使用。（注：同样由于层级问题，card (@空集 基数) 和 card (@全集 基数) 都是语法错误）

    我们现在可以证明以下定理：

    对于基数 A 和 B，A <= B 的定义如下：

    在处理 card S <= card T 时，直接展开定义带来的帮助不大，更实用的是使用下面的两个定理：

    容易证明以下定理：

    下面的“基数leq反对称”定理（这被称为 Cantor–Schröder–Bernstein theorem）的证明有一定的难度：

    证明思路：首先使用“forall基数”定理和“leqcardRR”定理，只需在 A, B : Type ，S : 集合 A ，T : 集合 B ，f : A -> option B ，g : B -> option A ，单射 f ，单射 g ，dom f = S ，ran f ⊆ T ，dom g = T ，ran g ⊆ S 的语境下证明 card S = card T 。接下来定义 C_ := fix C_ (n : nat) := match n with | 0 => S \ (f_map g T) | p.+1 => f_map g (f_map f (C_ p)) end（这是一个递归定义，效果包括 C_ 0 = S \ (f_map g T) 和 C_ n.+1 = f_map g (f_map f (C_ n)) ，其中 n.+1 表示自然数 n 的后继）。定义 C := { x | exists n : nat, x ∈ C_ n } 。可以证明 f_map (g º f) C ⊆ C 和 forall n : nat, C_ n ⊆ C 。定义 h := 分段函数 C f (反函数 g) ，现在只需证明 h 是 S 到 T 的双射。【 (1) 证明 h 是单射：即在 x, y : A ，x ∈ dom h ，y ∈ dom h 的语境下证明 h x = h y -> x = y 。当 x ∈ C ，y ∈ C 时，即证 f x = f y -> x = y ，利用 f 的单射性易证；当 ~ x ∈ C ，y ∈ C 时，即证 反函数 g x = f y -> x = y ，即证 (#g#) (f y) = Some x -> x = y ，而 (#g#) (f y) = Some x 蕴含了 x ∈ f_map (g º f) C ，从而蕴含了 x ∈ C ，矛盾；当 x ∈ C ，~ y ∈ C 时，与上一种情况类似；当 ~ x ∈ C ，~ y ∈ C 时，即证 反函数 g x = 反函数 g y -> x = y ，利用 g 的单射性易证。】【 (2) 证明 h 的定义域为 S：即在 x : A 的语境下证明 (x ∈ C ∩ S ∪ 补集 C ∩ ran g) = (x ∈ S) ，通过分类讨论与反证法，左推右和右推左都不难完成。】【 (3) 证明 h 的值域为 T：在 y : B 的语境下证明 y ∈ ran h -> y ∈ T 和 y ∈ T -> y ∈ ran h 即可。对于前者，只需证明 f_map f C ⊆ T 和 f_map (反函数 g) (补集 C) ⊆ T ，易证；对于后者，分 y ∈ f_map f C 和 ~ y ∈ f_map f C 两种情况。(i) 情况1：可得 x : A ，x ∈ C ，f x = Some y ，y ∈ T ，容易证明 h x = Some y ；(ii) 情况2：可得 ~ y ∈ f_map f C ，y ∈ T ，x : A ，g y = Some x，可证 ~ x ∈ C_ 0 和 forall n : nat, ~ x ∈ C_ n.+1 ，因此 ~ x ∈ C ，从而可证 h x = Some y 。】

    对于 h 的构造，直观上我们可以这样理解：我们的目标是构造一个 S 到 T 的双射函数 h。h 的主体部分可以由 g 的反函数组成；而对于 S 中不属于 g 的值域的元素 x，我们可以规定 h x = f x。这样构造出来的 h 是 S 到 T 的满射，但我们却无法证明 h 是单射的（因为 f_map f (S \ (f_map g T)) 可能会与 T 相交，这样 S 中将会有函数值相同的两个元素）。为了解决这个问题，我们对 h 进行调整，将 g 的反函数中像为 f_map f (S \ (f_map g T)) 的部分删除。对于函数值被删除的元素 x，我们重新规定 h x = f x ，但这样仍然无法证明 h 是单射的（因为 f_map f (f_map g (f_map f (S \ (f_map g T)))) 仍可能会与 T 相交）。于是再次调整 h，删除 g 的反函数的相应部分，将该区域的元素的在 h 下的函数值都设定为在 f 下的函数值。初始的 h 对 C_ 0 中的元素输出其在 f 下的函数值，第一次调整后的 h 对 C_ 0 ∪ C_ 1 中的元素输出其在 f 下的函数值，第二次调整后的 h 对 C_ 0 ∪ C_ 1 ∪ C_2 中的元素输出其在 f 下的函数值，以此类推。无论调整多少次 h，都无法证明 h 是单射的，但如果将 h 设定为【对 C（即所有的 C_ n 的并集）中的所有元素输出其在 f 下的函数值，对于其余元素输出其在 g 的反函数下的函数值】呢？实践表明这个思路是可行的，如上一段所述。

    基数leq 的传递性可通过构造复合函数证明。这样，我们就能得到 基数leq偏序关系。

    下面的“基数leq完全”定理的证明同样比较棘手：

    证明思路：首先使用“forall基数”定理，只需在 A, B : Type ，S : 集合 A ，T : 集合 B 的语境下证明 card S <= card T \/ card T <= card S 。定义 FS := { f | exists S', S' ⊆ S /\ f ∈ 函数空间 S' T /\ 单射 f } ，即满足定义域是 S 的子集且值域是 T 的子集的所有单射函数的集合。定义 r' := fun f g : A -> option B => 函数图像 f ⊆ 函数图像 g ，易证 r' 在 FS 上偏序，从而得到 r : 偏序关系 FS ，r = r' 。【接下来证明 极大元集 r FS <> ∅ ，根据“Zorn引理”定理，只需在 fs : 集合 (A -> option B) ，fs ⊆ FS ，全序 r fs 的语境下证明 上界集 r fs <> ∅ 。【首先证明 exists f : A -> option B, 函数图像 f = big并集 (map 函数图像 fs)：构造 (fun x => 存在实例化_条件定义 (fun y => (x,y) ∈ (big并集 (map 函数图像 fs)))) 即可，证明中会使用到 r 在 fs 上全序的条件。】得到了 f : A -> option B ，函数图像 f = big并集 (map 函数图像 fs) 的条件，现在只需证明 f ∈ 上界集 r fs ，即 f ∈ FS 和 forall g : A -> option B, g ∈ fs -> r g f 。证明前者时需要展开 FS 的定义，分解为多个目标。证明这些目标和后者时，一般利用条件 函数图像 f = big并集 (map 函数图像 fs) 进行代换后就只剩一些琐碎的工作了，但在对 f 的单射性的证明中，还需要用到 r 在 fs 上全序的条件。】现在我们证明了 FS 有极大元，解构整理条件可得 M : A -> option B ，dom M ⊆ S ，ran M ⊆ T ，单射 M ，【forall y : A -> option B, y ∈ FS -> r M y -> M = y】。【接下来证明 dom M = S \/ ran M = T ，使用反证法，只需在 dom M <> S 和 ran M <> T 的语境下证明 False 。易证 S \ (dom M) 和 T \ (ran M) 非空，于是可得 a : A ，a ∈ S ，~ a ∈ dom M ，b : B ，b ∈ T ，~ b ∈ ran M 。定义 f := 分段函数 (dom M) M (常数函数 {a} b) ，易证 dom f = dom M ∪ {a} 和 ran f = ran M ∪ {b} ，所以有 M <> f 。可证 f ∈ FS 和 r M f ，根据已知条件得 M = f ，矛盾。】现在我们分 dom M = S 和 ran M = T 两种情况证明最终的目标 card S <= card T \/ card T <= card S 。在第一种情况下选择证明 card S <= card T，此时使用“leqcardRR”定理，M 就是需要构造的函数；在第二种情况下选择证明 card T <= card S，此时使用“leqcardRR”定理，M 的反函数就是需要构造的函数。

    现在我们得到了 基数leq 是全序的。对于基数 A 和 B，A < B 定义为 A <= B /\ A <> B。于是我们就能得到更多的关于基数的序的性质。（注：基数leq 还应当是良序的，但对它的证明超出了作者的能力范围）

    “基数leq完全”定理可用于证明以下定理，它们可将一个关于多个基数的问题转化为一个关于多个【类型相同的】集合的问题（若只是多次使用“forall基数”定理，则只能将其转化为一个关于多个【类型可能不同的】集合的问题）。