????對于 S : 集合 A 和 r : 偏序關(guān)系 S，若 r 在 S 的范圍內(nèi)滿足完全性，則 r 被稱為 S 上的全序關(guān)系；對于 S : 集合 A 和 r : 嚴格偏序關(guān)系 S，若 r 在 S 的范圍內(nèi)滿足完全性，則 r 被稱為 S 上的嚴格全序關(guān)系。對于 r : 偏序關(guān)系 S，若 r 滿足完全性，則 strict_po r 也滿足完全性，所以每個全序關(guān)系都可自然對應于一個嚴格全序關(guān)系，這里用 strict_to 表示。對于 r : 全序關(guān)系 S，由于 S 中的任意兩個元素都是可比較的，所以 x 是極大元當且僅當 x 是最大值，x 是極小元當且僅當 x 是最小值。

????對于?S?: 集合?A 和 r : 全序關(guān)系 S，若 S 的任意非空子集都有最小值，則 r 被稱為 S 上的良序關(guān)系；嚴格良序關(guān)系的定義詳見代碼。每個良序關(guān)系同樣都可以自然對應于一個嚴格良序關(guān)系，與 strict_po 和 strict_to 一致，這里用 strict_wo 表示。

????已知 S : 集合 A 和 r :?良序關(guān)系 S，當需要證明某性質(zhì) P : A -> Prop 對 S 中的所有元素都成立時，可以利用良序關(guān)系對 S 進行歸納。這可被稱為“超限歸納法”，具體的定理內(nèi)容如下：

????證明思路：已知 A : Type，P : A -> Prop，S : 集合 A，r : 良序關(guān)系 S，?（這里 y < x 表示 strict_wo r y x）；目標是??。由于??，所以可將目標轉(zhuǎn)化為??。反證，獲得??的條件，目標變?yōu)?False。顯然有??，所以根據(jù)“wo良序”定理可得?（這里 min 表示 最小值 r），進而得到 a : A 和??，從而有??，?，（這里 a <= x 表示 r a x）。將這一命題變形得到??，這樣根據(jù)初始的條件就得到了??，推出了 False。

????現(xiàn)在我們定義了名為“偏序關(guān)系”“全序關(guān)系”“良序關(guān)系”的對象，但這些對象無法直接用于表達“某關(guān)系在某集合上偏序/全序/良序”的概念。為了解決這個問題，我們按以下方案定義“偏序”“全序”“良序”等對象，這樣“r 在 S 上偏序”就可以表達為“偏序 r S”：

????接下來，我們將證明著名的佐恩引理（Zorn's Lemma）。該定理可被描述為：若偏序集的任意全序子集都有上界，那么這個偏序集有極大元。為了證明它，我們需要先做一些準備工作。（注：雖然作者已經(jīng)完成了這些定理的形式化證明并通過了 Coq 的驗證，但在這里表述時為了思路盡可能清晰不會完全依照形式化證明來表述，故可能會出現(xiàn)錯誤或表述不準確的地方；而且由于作者在證明時參考了多個來源的證明，也可能會有繞遠路的現(xiàn)象，敬請諒解）

????證明思路：根據(jù)“良序R'”定理，只需在?T ? S，R ? S，良序 r T，良序 r R，全序 r (T ∪ R)，Q : 集合 A，Q?? T?∪ R，Q?<> ? 的語境下證明 最小值 r Q?<> None 。根據(jù)“子集良序”定理可證 良序 r?(Q ∩ T) 和 良序 r?(Q ∩ R) ，根據(jù)交集的分配律可證?Q = (Q ∩ T) ∪?(Q ∩ R)?，故只需證 最小值 r ((Q ∩?T) ∪?(Q ∩ R)) <> None 。當 Q ∩?T 是空集或 Q ∩ R 是空集時易證該結(jié)論。當 Q ∩ T 和 Q ∩ R 都不是空集時，可以得到 a,?b : A 滿足 Q ∩ T?的最小值是 a，Q ∩ R?的最小值是 b 。根據(jù)?全序 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 為空集時易證結(jié)論。當 X 非空時可得 x0 : A，x0 ∈ X 。使用反證法，獲得?forall Y, Y ? X -> 良序 r Y -> 上界集 r Y \ Y <> ? 的條件（注：上界集 r Y?\ Y 表示的是 (上界集 r Y)?\ Y，即嚴格上界集），目標變?yōu)?False。通過存在實例化可證?exists s, forall Y, Y ? X -> 良序 r Y -> s Y ∈ 上界集 r Y \ Y ，解構(gòu)之得到 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 } ?！镜谝徊糠纸Y(jié)束，此時只有一個目標 False】

????【第二部分：該部分證明 forall Y Y', Y ∈ Ω -> Y' ∈ Ω -> Y \ Y' <> ? -> exists x, x ∈ Y /\ Y' = { k | k ∈ Y /\ k < x } 】首先解構(gòu)整理條件，得到 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 ?？勺C?{ k | k ∈ Y /\ k < x } ? Y' ?，F(xiàn)在欲證明目標只需證明?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 } <> ? 的條件，目標變?yōu)?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 ?！窘酉聛碜C明?{ k | k ∈ Y /\ k < z } = { k | k ∈ Y' /\ k < y } ，根據(jù)“互為子集即相等”定理只需證明它們都是對方的子集：(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 ，根據(jù)已證的 { k | k ∈ Y /\ k < x } ? Y' 得到 z ∈ Y' ，與條件 ~ (z ∈ Y' /\?z?<?y) 矛盾】。根據(jù)已有條件可證 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 } ?？勺C z = y 。由（假設 z = x ，則 x = y ，易得矛盾）和已證的 z <= x 得 z < x?，進而得到 y < x ；由 z ∈ Y 得到 y ∈ Y 。這就與條件?~ (y ∈ Y /\ y < x) 矛盾，推出了 False ?！镜诙糠纸Y(jié)束，此時只有一個目標?False，新增條件?forall Y Y',?Y ∈ Ω -> Y' ∈ Ω -> Y \ Y' <> ? ->?exists x, x ∈ Y /\ Y' = { k | k ∈ Y /\?k <?x } 】

????【第三部分：該部分從第二部分所得的結(jié)論出發(fā)得到一些推論】【首先證明?forall Y Y', Y ∈ Ω -> Y' ∈ Ω -> Y ? Y' \/ Y' ? Y ：當 Y \ Y' = ? 時，有 Y ? Y' ；當 Y \ Y' <>?? 時，使用第二部分所得的結(jié)論，解構(gòu)后得到 x : A ，x ∈ Y ，Y' = { k | k ∈ Y /\ k < x } ，從而有 Y' ? Y ?！俊窘酉聛碜C明 forall Y Y', Y ∈ Ω -> Y' ∈ Ω -> Y' \ Y ? 上界集 r Y \ Y ：當 Y' \ Y?= ? 時顯然。當 Y' \ Y?<>?? 時，使用第二部分所得的結(jié)論，解構(gòu)后得到 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 } ?，F(xiàn)在對?Y ∈ Ω 和?Y' ∈ Ω?進行解構(gòu)和整理，得到 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 ?！俊镜谌糠纸Y(jié)束，此時只有一個目標?False，新增條件?forall Y Y',?Y ∈ Ω -> Y' ∈ Ω?-> Y ? Y' \/ Y' ? Y 和 forall?Y Y', Y ∈ Ω -> Y' ∈ Ω -> Y' \ Y ? 上界集 r Y \ Y 】

????【第四部分：該部分定義 Yi 并證明它的一些性質(zhì)】定義 Yi :=?big并集 Ω 。展開定義后易證?Yi ? X ，x0 ∈ Yi ，最小值 r Yi = Some x0 。【接下來證明 良序 r Yi ：利用已證的 forall Y Y',?Y ∈ Ω -> Y' ∈ Ω?-> Y ? Y' \/ Y' ? Y ，不難證明 全序?r Yi ，現(xiàn)在只需證明 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 ，解構(gòu)之可得 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' 。由第三部分證明的結(jié)論可得?Y' \ Y ? 上界集 r Y \ Y ，所以 y 是 Y 的上界，b <= y ?！楷F(xiàn)在由已知條件可得?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 ?！镜谒牟糠纸Y(jié)束，此時有四個子目標，每個子目標都有新條件 Yi ? X ，x0 ∈ Yi ，最小值 r Yi = Some x0 ，良序 r Yi ，s Yi ∈ X ，forall y, y ∈ Yi -> y <= s Yi?】

????【第五部分：該部分逐個證明四個子目標從而結(jié)束整個定理的證明】【證明目標1（Yi ∪ {s Yi} ? X）：由 Yi???X 和 s Yi ∈ X ，顯然?！俊咀C明目標2（良序 r (Yi ∪ {s Yi})）：根據(jù)此前的準備工作“良序子集之并集”定理，只需證明 全序 r (Yi ∪ {s Yi})?。從已知的 良序 r Yi 和 forall y, y ∈ Yi -> y <= s Yi?出發(fā)，不難證明。】【證明目標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 } ：解構(gòu)整理條件得 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 ?？勺C x = s { y | y ∈ Y /\ y < x } ，故只需證明 { y | y ∈ Y /\ y < x } = {?y?| y ∈ Yi ∪ {s Yi} /\ y < x } ，根據(jù)“互為子集即相等”定理只需證明它們都是對方的子集：(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 ，使用第二部分所得的結(jié)論可證 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?可完成左推右，而右推左是顯然的?！俊咀C明目標4（最小值 r (Yi ∪ {s Yi}) = Some x0）：只需證明 forall x, x ∈ Yi ∪ {s Yi} -> x0 <= x 。在 x ∈ Yi 的情況中，解構(gòu)得到 最小值 r Y = Some x0 和 x ∈ Y 后不難證明；在 x = s Yi 的情況中，結(jié)合已知的 forall y, y ∈ Yi -> y <= s Yi 即可完成證明。】【第五部分結(jié)束，“Zorn引理之引理”定理已完成證明】

????完成以上準備工作后，我們終于可以證明佐恩引理。

????證明思路：在?forall T, T ? S -> 全序 r T -> 上界集 r T <> ? ，極大元集 r S =?? 的語境下證明 False 即可。極大元集 r S =?? 可變形為?forall x, x ∈ S -> exists y, y ∈ S /\ x < y ?！窘酉聛碜C明?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 】。根據(jù)此前的準備工作“Zorn引理之引理”定理，可得?Y : 集合 A ，Y ? S ，良序 r Y ，上界集 r Y \ Y = ? 。由“良序則全序”定理和已知條件，上界集 r Y <> ? 。由剛剛證明的結(jié)論可進一步得到?上界集 r Y \ Y <> ? ，而這與?上界集 r Y \ Y = ? 矛盾，推出了 False 。至此，佐恩引理證畢。