????在數學上，基數是一種用來描述集合的元素個數的數。對于集合 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，符合等價關系的要求?，F在，有了 等勢_等價關系，我們可以通過?等價類構造類型' 定義基數類型。

????對于 S : 集合 A，card S 的類型是基數，表示 S 中元素的個數。對于（類型可能不同的）集合 S 和 T，card S = card T 等價于 S 和 T 等勢。對于 A : 基數，基數構造集合 A 的類型是 uset（具有 uset?類型的對象可被解構為一個類型和這個類型上的一個集合），可用于從一個基數中得到一個集合 S 使得 card S 恰好等于這個基數?！癴orall基數”定理可將一個基數問題轉化為一個集合問題，將在基數性質的證明中被廣泛使用。（注：同樣由于層級問題，card (@空集 基數) 和 card (@全集 基數) 都是語法錯誤）

????我們現在可以證明以下定理：

? ? 對于基數 A 和 B，A <= B 的定義如下：

????在處理 card S <= card T 時，直接展開定義帶來的幫助不大，更實用的是使用下面的兩個定理：

????容易證明以下定理：

????下面的“基數leq反對稱”定理（這被稱為?Cantor–Schr?der–Bernstein theorem）的證明有一定的難度：

? ? 證明思路：首先使用“forall基數”定理和“l(fā)eqcardRR”定理，只需在?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 o 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 o 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，我們可以規(guī)定 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，我們重新規(guī)定 h x = f x ，但這樣仍然無法證明 h 是單射的（因為 f_map f (f_map g (f_map f (S \ (f_map g T)))) 仍可能會與 T 相交）。于是再次調整 h，刪除 g 的反函數的相應部分，將該區(qū)域的元素的在 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】?！窘酉聛碜C明 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 ∪ ，所以有 M <> f ?？勺C f ∈ FS 和 r M f ，根據已知條件得 M = f ，矛盾?！楷F在我們分?dom M = S 和 ran M = T 兩種情況證明最終的目標?card S <= card T \/ card T <= card S 。在第一種情況下選擇證明 card S <= card T，此時使用“l(fā)eqcardRR”定理，M 就是需要構造的函數；在第二種情況下選擇證明 card T <= card S，此時使用“l(fā)eqcardRR”定理，M 的反函數就是需要構造的函數。

????現在我們得到了 基數leq 是全序的。對于基數 A 和 B，A <?B 定義為 A <= B /\ A <> B。于是我們就能得到更多的關于基數的序的性質。（注：基數leq 還應當是良序的，但對它的證明超出了作者的能力范圍）

????“基數leq完全”定理可用于證明以下定理，它們可將一個關于多個基數的問題轉化為一個關于多個【類型相同的】集合的問題（若只是多次使用“forall基數”定理，則只能將其轉化為一個關于多個【類型可能不同的】集合的問題）。