1.1. 回顾集论语言
让我们首先回顾集合论语言.
定义 1.1.0.1. 默认的集合论语言 是带有二元谓词 的含等词语言. 正如算术语言将 简记为 , 我们将 记为 , 将 记为 , 并合称这两种形式的量词为受限 (Restricted) 量词. 这同样指出一系列对公式的复杂度分层, 我们称之为 Levy 层级:
• | 我们首先定义这个层级最底端的公式类, 称为 公式:
| ||||||||
• | 我们现在交错地定义 和 语句如下:
|
更多的时候, 我们要考虑理论 下的 Levy 层级.
• | 给定集合论理论 , 如果公式 和 满足 , 且 是 公式 ( 代指 三种符号之一, 下同), 则称 是 公式. |
• | 记仅含经典一阶逻辑公理的集合论理论为 , 我们今后默认一切集合论理论 都是 的扩张. 公式将简称为 公式. |
• | 如果集合论理论 下, 公式 同时是 公式, 也是 公式, 则称 是 公式. 特别地简称 公式为 公式. |
我们来指出一些对于公式复杂度的事实.
元定理 1.1.0.2. 考虑高复杂度的公式被逻辑连接词连接后的复杂度.
• | 对于 : 如果 是 的, 则其否定是 的; 如果 是 的, 则其否定是 的; 如果 是 的, 则其否定同样是 的. |
• | 对于 和 : 如果它们同是 公式, 则连接后仍是 公式; 如果它们一个是 公式, 另一个是 公式, 则连接后是 公式. |
• | 对于 : 将它理解为 . |
• | 对于 : 将它理解为 . |
评注. 受限量化只在加在 公式上时才不增加公式复杂度.
异议. 为何此处我们选取 “元定理” 这一术语呢?
回应. 在这一章中, 我们必须时刻警惕所作的论断究竟是在某个 (弱) 集合论内部形式地给出, 还是在某个特定的集合论外部给出的. 对于后一种定理, 我们将采取将其特别标注为元定理的方式来做出区别. 具体而言, 我们有两种理解外部元定理的方案:
• | 这些元定理涉及了一些并不生活在我们正在处理的具体集合宇宙中的对象, 例如 (元逻辑的) 公式、(绝对标准的元) 自然数, 因此 (暂时) 不能被理解为某一个具体集合宇宙内部的定理. |
• | 这些元定理是对于公式阐明的定理, 因此我们正生活在的世界要临时地被理解为元元语境 (以保证元定理具有正确的形式化版本). |
接下来, 我们来回顾最广为人知的集合论理论: .
定义 1.1.0.3. 我们给 (默认可数变元的一阶) 集合论语言 提名以下公理:
1. | 外延公理 (Ext): |
2. | 空集公理 (Emp): |
3. | 对集公理 (Pair): |
4. | 并集公理 (Union): |
5. | 差集公理 (Diff): |
6. | (集合) 基础公理 (Found): |
7. | 传递包括公理 (TCo): |
8. | 传递闭包公理 (TCl): |
9. | 卡氏积公理 (Cart): |
10. | 幂集公理 (Pow): |
11. | 弱无穷公理 (wInf): |
12. | 无穷公理 (Inf): |
13. | 强无穷公理 (sInf): |
14. | 选择公理 (AC): |
15. | 良序公理 (WO): |
在一阶语言的讨论中, 我们默认一个类就是一个 公式 , 这里小括号中的符号有序列表穷尽其自由变元且不含其约束变元 (换言之, 可以出现公式中并未出现的变元符号). 我们列举以下公理模式.
1. | 分离公理模式 (Sep): 个变元, |
2. | 收集公理模式 (Coll): 个变元, |
3. | 局部收集公理模式 (LColl): 个变元, |
4. | 替代公理模式 (Rep): 个变元, |
5. | 基本 (rudimentary) 替代公理模式 (rRep): 个变元, |
6. | 强替代公理模式 (SRep): 个变元, |
7. | 归纳公理模式 (Ind): 个变元, |
8. | 基础公理模式 (Fnd): 个变元, |
9. | 反射公理模式 (Refl): 个变元, , 这里 是 对 的相对化, 即将 中所有无约束量词变为受限于 的量词所得公式. |
10. | 全反射公理模式 (CRefl): 个变元, . |
这些公理模式都需要我们在元语言中对公式 作量化, 默认是对全部公式量化. 如果他们量化范围是 公式 (), 则称对应的公理模式是 公理模式, 在需要简写时将 作为公理模式的下标.
意指以下公理组: 外延, 对集, 并集, 基础, 幂集, 无穷, 分离模式. 在 的基础上加入了替代公理模式, 在 的基础上加入了选择公理, 在 的基础上加入了替代公理模式和选择公理.
定理 1.1.0.4. 可证以上列举的全体公理和公理模式.