数学知识
• SF第1卷
• 集合模型论(1-1): 从封闭类构造内模型
• 集合模型论(1-2): 累积层级与集合的秩
• 最好了解后继序数与极限序数, 否则就跳过文章中提及序数的内容, 不影响主线.
极限层
上一篇我们讲了怎么在不引入序数的前提下定义累积层级和集合的秩. 接下来将展示, 即使没有后继序数与极限序数, 我们也可以研究后继层与极限层.
定义1-3-1 (后继层) 我们说x是后继层, 当且仅当存在层y使得 x =Ρ y.
定义1-3-2 (极限层) 我们说x是极限层, 当且仅当x是层且 x ⊆ ⋃ x.
Definition 后继层 x := ∃ y ∈ₚ 层, x = 幂 y. Definition 极限层 x := x ∈ₚ 层 ∧ x ⊆ ⋃ x.
不难看出, 它们跟后继序数和极限序数的定义有类似的形式. 只是按极限序数的定义, 我们应该有 x = ⋃ x. 这可以证明.
备注1-3-3 x是极限层, 当且仅当x是层且 x = ⋃ x.
按极限层的定义右到左是显然的. 左到右用外延公理证x = ⋃ x，按极限层的定义只需证⋃ x ⊆ x, 由层的传递性得证 ∎
Remark 极限层等价定义 x : 极限层 x ↔ x ∈ₚ 层 ∧ x = ⋃ x. Proof. split. - intros [xS sub]. split. auto. apply 外延. auto. apply 并得子集. firstorder using 层传递. - intros [xS eq]. split. auto. rewrite eq at 1. zf. Qed.
另外需要注意按此定义, 空集也是极限层, 所以后文中如有必要会用"非空极限层"以明确所指.
引理1-3-4 如果x是层之集(由层组成的集合), 那么要么⋃ x ∈ x要么x ⊆ ⋃ x.
假设x ⊈ ⋃ x, 则存在y ∈ x且y ∉ ⋃ x. 我们证⋃ x就是y. 只需证y是x的上界, 即对任意z ∈ x有z ⊆ y. 由于y是层, 由层的ϵ线序, 若z ⊈ y, 只能有y ∈ z, 这会导致y ∈ ⋃ x与前提矛盾 ∎
Lemma 层之集二分 x : x ⊆ₚ 层 → ⋃ x ∈ x ∨ x ⊆ ⋃ x. Proof. intros sub. 排中 (x ⊆ ⋃ x); auto. left. apply 非子集 in H as [y[yx yns]]. replace (⋃ x) with y; auto. symmetry. apply 并即上确界. split; auto. intros z zx. destruct (层线序 (sub z zx) (sub y yx)); auto. exfalso. apply yns. apply 并集. now exists z. Qed.
事实1-3-5 层要么是后继层要么是极限层.
设x是层, 对层x归纳, 要证两种情况.
要证当x是层时, 对Ρ x命题成立. 按定义 Ρ x是后继层.
要证当x是层之集时, 对⋃ x命题成立. 另外我们有归纳假设: 对任意y ∈ x命题成立. 对x用引理1-3-4, 分两种情况.
若⋃ x ∈ x, 由归纳假设立即得证.
若x ⊆ ⋃ x, 我们证⋃ x是极限层. 首先由 x是层之集 和 层的定义, ⋃ x是层. 还需证 ⋃ x ⊆ ⋃ ⋃ x, 即证对任意y ∈ ⋃ x (即对任意满足 y ∈ z ∈ x的y和z) 有y ∈ ⋃ ⋃ x. z就见证了y ∈ z ∈ ⋃ x, 其中后半部分由x ⊆ ⋃ x和z ∈ x得证 ∎
Fact 层二分 x : x ∈ₚ 层 → x ∈ₚ 后继层 ∨ x ∈ₚ 极限层. Proof. induction 1 as [x xS _|x xS IH]. - left. exists x. auto. - destruct (层之集二分 xS). + apply IH, H. + right. split. now constructor. intros y [z [yz zx]]%并集. apply 并集. exists z. auto. Qed.
封闭性
我们来考察极限层的封闭性. 由于层是集合而不是类, 我们仿照1-1封闭类的定义, 定义封闭集.
定义1-3-6 (封闭集) 如代码.
Definition 空集封闭 x := ∅ ∈ x. Definition 并集封闭 x := ∀ y ∈ x, ⋃ y ∈ x. Definition 幂集封闭 x := ∀ y ∈ x, 幂 y ∈ x. Definition 替代封闭 x := ∀ R y, 函数性 R → (∀ a b, R a b → a ∈ y → b ∈ x) → y ∈ x → R @ y ∈ x. Definition 替代封闭' x := ∀ R y, 函数性 R → R @ y ⊆ x → y ∈ x → R @ y ∈ x. Definition 配对封闭 x := ∀ a b ∈ x, {a, b} ∈ x. Definition 分离封闭 x := ∀ P, ∀ y ∈ x, y ∩ₚ P ∈ x.
事实1-3-7 定义1-3-6中对替代的两种封闭性定义是等价.
见Github仓库 ∎
Fact 替代封闭_等价表述 x : 替代封闭 x ↔ 替代封闭' x.
对替代的封闭性我们只采用第一种定义.
我们先给出结论: 对极限层来说, 除了对替代的封闭性不成立, 定义1-3-6中的其他5种都成立. 为了使证明更可读, 我们补充3个引理.
引理1-3-8 对集合取并不改变其秩, 即对任意x ∈ 层y, ⋃ x ∈ 层y.
对层y归纳.
要证x ∈ Ρ y 蕴含 ⋃ x ∈ Ρ y, 即证对任意a ∈ b ∈ x ⊆ y有a ∈ y, 由层的传递性得证.
要证对层之集y, x ∈ ⋃ y (即x ∈ a ∈ y) 蕴含 ⋃ x ∈ ⋃ y. 我们证前件的a就见证了⋃ x ∈ a ∈ y, 只需证⋃ x ∈ a. 这由归纳假设: 对任意z, x ∈ z ∈ y蕴含⋃ x ∈ z 得证 ∎
Lemma 并_等秩 x y : x ∈ y → y ∈ₚ 层 → ⋃ x ∈ y. Proof. intros xy. induction 1 as [y yS _|y yS IH]. - apply 幂集 in xy. apply 幂集. intros a [b [ab bx%xy]]%并集. eapply 层传递; eauto. - apply 并集 in xy as [a [xa ax]]. apply 并集. exists a. split; auto. Qed.
引理1-3-9 对集合取幂将提升其秩, 即对任意x ∈ 层y,Ρ x ∈ 层Ρ y.
对层y分类讨论.
• 若x ∈ Ρ y, 要证 x ∈ Ρ y, 即证x ⊆ ΡΡ y 蕴含Ρ x ⊆ Ρ y, 显然成立.
• 若y是层之集且有x ∈ ⋃ y (即x ∈ a ∈ y), 要证Ρ x ∈ Ρ ⋃ y, 即证对任意b ⊆ x有b ∈ ⋃ y. 我们证b ∈ a ∈ y, 只需证b ∈ a, 由层的膨胀性得证 ∎
Lemma 幂_升秩 x y : x ∈ y → y ∈ₚ 层 → 幂 x ∈ 幂 y. Proof. intros xy. destruct 1 as [y _|y yS]. - apply 幂集 in xy. apply 幂集. now apply 幂单调. - apply 并集 in xy as [a [xa ay]]. apply 幂集. intros b bx%幂集. apply 并集. exists a. split; auto. eapply 层膨胀; eauto. Qed.
定义1-3-10 (秩封闭) 我们说x对秩封闭, 当且仅当对x中的任意集合y, 存在一个层z容纳y, 且z也在x中.
Definition 秩封闭 x := ∀ y ∈ x, ∃ z ∈ₚ 层, y ∈ z ∧ z ∈ x.
引理1-3-11 极限层对秩封闭.
设x是极限层, 对层x归纳, 要证两种情况.
• 要证Ρ x ⊆ ⋃ Ρ x = x 蕴含Ρ x对秩封闭, 前提有矛盾.
• 要证 ⋃ x ⊆ ⋃ ⋃ x 蕴含 ⋃ x对秩封闭. 另外我们有归纳假设: x的任意成员y满足 ⋃ y ⊆ ⋃ ⋃ y 蕴含 ⋃ y对秩封闭. 由引理1-3-4, 分两种情况.
◦若⋃ x ∈ x, 使用归纳假设得证.
◦若x ⊆ ⋃ x, 要证对y ∈ ⋃ x存在层z满足y ∈ z ∈ x, 显然成立 ∎
Lemma 极限层对秩封闭 : 极限层 ⊑ 秩封闭. Proof. intros x [xS sub]. induction xS as [x _ _|x xS IH]. - rewrite 并幂 in sub. now apply 幂集在上 in sub. - destruct (层之集二分 xS). now apply IH. intros y [z [yz zx]]%并集. exists z. auto. Qed.
回到封闭性的证明.
引理1-3-12 非空层对空集封闭.
设非空层x. 由于空集也是层, 由层的ϵ线序, 要么 x ⊆ ∅, 这意味着x为空集, 与前提矛盾; 要么 ∅ ∈ x, 命题得证 ∎
Lemma 非空层对空集封闭 x : x ∈ₚ 层 → 非空 x → 空集封闭 x. Proof. intros xS [y yx]. destruct (层线序 xS 空集层); auto. apply H in yx. zf. Qed.
引理1-3-13 极限层对并集封闭.
引理1-3-8已证任意层对并集封闭, 极限这个条件是多余的 ∎
Lemma 极限层对并集封闭 : 极限层 ⊑ 并集封闭. Proof. intros x [xS _] y yx. now apply 并_等秩. Qed.
引理1-3-14 极限层对幂集封闭.
设x是极限层, 要证y ∈ x蕴含 y ∈ x. 由引理1-3-11, 存在层z满足y ∈ z ∈ x. 对层x和层 z, 由层的ϵ线序, 分两种情况.
• 若 z ⊆ x, 由引理1-3-9有Ρ y ∈ Ρ z, 即得Ρ y ∈ x.
• 若x ∈ Ρ z, 即x ⊆ z, 由z ∈ x得到z ∈ z, 违反正则公理 ∎
Lemma 极限层对幂集封闭 : 极限层 ⊑ 幂集封闭. Proof. intros x xL y yx. destruct (极限层对秩封闭 xL yx) as [z [zS [yz zx]]]. destruct xL as [xS _]. destruct (层线序 (幂层 zS) xS). - apply (幂_升秩 yz) in zS as pypz. auto. - exfalso. apply 幂集 in H. specialize (H z zx). now apply 无循环1 in H. Qed.
最后两种封闭性与主线无关, 我们略过它们的证明, 感兴趣的读者可以看Github仓库.
引理1-3-15 对集合做分离不改变其秩.
引理1-3-16 配对的秩高于原集合的秩.
Lemma 分离_等秩 x y P : x ∈ y → y ∈ₚ 层 → x ∩ₚ P ∈ y. Lemma 配对_升秩 a b x : a ∈ x → b ∈ x → {a, b} ∈ 幂 x.
事实1-3-17 极限层对配对封闭.
事实1-3-18 极限层对分离封闭.
Fact 极限层对配对封闭 : 极限层 ⊑ 配对封闭. Fact 极限层对分离封闭 : 极限层 ⊑ 分离封闭.
宇宙
我们考虑封闭类内化为集合的情况.
定义1-3-19 我们说一个集合是宇宙, 当且仅当该集合的成员正好与某个封闭类的成员相吻合.
Notation "A =ₚ P" := (∀ x, x ∈ A ↔ x ∈ₚ P) (at level 70) : zf_scope. Definition 宇宙 u := ∃ P, 封闭类 P ∧ u =ₚ P.
本节将省略一些简单的证明代码, 都可在Github仓库查看.
引理1-3-20 (宇宙的封闭性) 宇宙对空集, 并集, 幂集, 替代封闭.
由宇宙的定义可以立即得证 ∎
Lemma 宇宙对空集封闭 : 宇宙 ⊑ 空集封闭. Lemma 宇宙对并集封闭 : 宇宙 ⊑ 并集封闭. Lemma 宇宙对幂集封闭 : 宇宙 ⊑ 幂集封闭. Lemma 宇宙对替代封闭 : 宇宙 ⊑ 替代封闭.
引理1-3-21 (宇宙的封闭性) 宇宙对成员关系和子集关系封闭.
前者由封闭类的传递性得证. 后者由前者以及宇宙对幂集的封闭性得证 ∎
(* 对成员关系封闭 *) Lemma 宇宙传递 : 宇宙 ⊑ 传递. (* 对子集关系封闭 *) Lemma 宇宙膨胀 : 宇宙 ⊑ 膨胀.
备注1-3-22 若封闭类集化为了宇宙, 那么该宇宙也可以重新类化为封闭类.
依定义 ∎
Remark 宇宙类化 u : 宇宙 u → 封闭类 (λ x, x ∈ u).
引理1-3-23 (宇宙的封闭性) 宇宙对秩封闭, 即如果x在某个宇宙里, 那么x的秩也在该宇宙.
设u是宇宙, x ∈ u, 要证ρ x ∈ u. 由ϵ归纳法, 有归纳假设: ∀ y ∈ x, y ∈ u → ρ y ∈ u. 将ρ换成ρ', 由宇宙对并集的封闭性, 即证 [ρ[x]] ∈ u. 由宇宙对替代的封闭性, 只需证以下两个分支.
• ∀ a b,Ρ a = b → a ∈ ρ[x] → b ∈ u. 由函数式替代的定义改写即证对任意y ∈ x有 Ρ (ρ y) ∈ u. 由宇宙对幂集封闭即证ρ y ∈ u, 由归纳假设和宇宙的传递性得证.
∀ a b, ρ a = b → a ∈ x → b ∈ u. 改写即证ρ a ∈ u, 由归纳假设和宇宙的传递性得证 ∎
Lemma 宇宙对秩封闭 x u : 宇宙 u → x ∈ u → ρ x ∈ u. Proof. intros U xu. induction (正则 x) as [x _ IH]. rewrite ρ等于ρ'. apply 宇宙对并集封闭; auto. repeat apply 宇宙对替代封闭; auto; try congruence. - intros a b <- [y [yx <-]]%函数式替代. apply 宇宙对幂集封闭; auto. apply IH; auto. eapply 宇宙传递; eauto. - intros a b <- ax. apply IH; auto. eapply 宇宙传递; eauto. Qed.
引理1-3-24 宇宙一定是层.
设u是宇宙, 要证u是层. 只要证u = ⋃ (u ∩ₚ 层), 就可以用层的定义证明u是层. 用外延公理证u = ⋃ (u ∩ₚ 层).
• 要证对任意x ∈ ⋃ (u ∩ₚ 层)有x ∈ u, 即证对x ∈ y ∈ u有x ∈ u, 由宇宙的传递性得证.
• 要证对任意x ∈ u有x ∈ ⋃ (u ∩ₚ 层). 我们证x ∈ Ρ (ρ x) ∈ u ∩ₚ 层.
◦对左边, 由幂集公理和ρ规范得证.
◦对右边, 由分离定理, 要证Ρ (ρ x) ∈ u 且Ρ (ρ x) 是层.
▫对左边, 由宇宙对幂集的封闭性和宇宙对秩的封闭性得证.
▫对右边, 由层的定义和ρ规范得证 ∎
Lemma 宇宙是层 : 宇宙 ⊑ 层. Proof. intros u U. enough (⋃ (u ∩ₚ 层) = u) as <-. { constructor. now intros x H%分离. } apply 外延. - intros x [y [xy [yu yS]%分离]]%并集. eapply 宇宙传递; eauto. - intros x xu. apply 并集. exists (幂 (ρ x)). split. + apply 幂集, ρ规范. + apply 分离. split. * now apply 宇宙对幂集封闭, 宇宙对秩封闭. * constructor. apply ρ规范. Qed.
最后, 我们证明本讲的主结论.
定理1-3-25 宇宙等价于对替代封闭的非空极限层.
设宇宙u. 左边到右边: 引理1-3-20已证宇宙对替代和空集封闭; 引理1-3-24已证宇宙是层; 只需证u ⊆ ⋃ u. 对任意x ∈ u, 由宇宙对秩封闭有ρ x ∈ u, 要证x ∈ ⋃ u. 我们证 x ∈ (ρ x) ∈ u.
• 对左边, 由幂集公理和ρ规范得证.
• 对右边, 由宇宙对幂集的封闭性得证.
Theorem 宇宙等价于对替代封闭的非空极限层 u : 宇宙 u ↔ (替代封闭 u ∧ 非空 u ∧ 极限层 u). Proof. split; intros H. - repeat split. + now apply 宇宙对替代封闭. + exists ∅. now apply 宇宙对空集封闭. + now apply 宇宙是层. + intros x xu%宇宙对秩封闭; auto. apply 并集. exists (幂 (ρ x)). split. * apply 幂集, ρ规范. * now apply 宇宙对幂集封闭.
右边到左边: 只需证 (λ x, x ∈ u) 是封闭类, 这由层的传递性, 极限层的封闭性, 以及u对替代封闭的前提得证 ∎
- destruct H as [rc [ne [uS sub]]]. exists (λ x, x ∈ u). split. 2:easy. split. + intros x y xy yu. eapply 层传递; eauto. + now apply 非空层对空集封闭. + now apply 极限层对并集封闭. + now apply 极限层对幂集封闭. + apply rc. Qed.
津ICP备2022002164号-2 © 2016-2023 iHuaBen.com 版权保护声明 不良信息举报:jubao@ihuaben.com
京公网安备11010502036362号