2.1. 基础性
元定理 2.1.0.1 (by Bernays). 可有穷公理化.
证明. 我们选取外延公理和九条存在性公理, 然后指出这十条公理构成的集合论与 等效. 这九条存在性公理分别宣称:
1. | : 空集存在. |
2. | : 对集 存在. |
3. | : 卡氏积 存在. |
4. | : 差集 存在. |
5. | : 并集 存在. |
6. | : 定义域 存在. |
7. | : 对所有集合 存在. |
8. | : 对所有集合 存在. |
9. | : 对所有集合 存在. |
这里 至 又称作 Godel 算子或基础算子. 不难看出它们都是 可证的函数符号, 所以我们的目标是证明它们可以复现 分离公理模式. 我们对公式的结构做元归纳法, 并证明一个稍强的版本的 分离公理模式: 若 是 公式, 则 . 注意交集 可以算出来, 可以写作 , 可以写作 , 我们不妨设 中只出现 、、、 四种符号, 且 两边的变元符号总是不同.
1. | 形若 , 我们对 进行归纳.
| ||||||||||||||||||||||||||||||
2. | 形若 , 同样对 归纳.
| ||||||||||||||||||||||||||||||
3. | 形若 , 把它当成 即可避免讨论此情况. | ||||||||||||||||||||||||||||||
4. | 形若 , 取差集. | ||||||||||||||||||||||||||||||
5. | 形若 , 取交集. | ||||||||||||||||||||||||||||||
6. | 形若 . 我们的归纳假设能得到集合 , 于是 . | ||||||||||||||||||||||||||||||
7. | 形若 . 完全同上, 只需修改一个符号. |
这提示我们考察以下记号.
定义 2.1.0.2. 我们称函数符号 是基础 (Basic) 的, 若它可在有穷步内由以下操作得到:
1. | 取基础算子 ; |
2. | 取基础函数符号的复合. |
全体基础函数构成的 (元) 集合记为 .
元定理 2.1.0.3. 传递集 是 的模型, 当且仅当它对 中的每个函数符号封闭. 这种集合称作基础闭集.
元定理 2.1.0.4. 如果传递集 是 的模型 (鉴于上个 (元) 定理, 这是说 ), 则令 , 我们有: 任给 模型 , 当且仅当 . 特别的, 显然有 , 因此 是 的模型.
定义 2.1.0.5. 对任何集合 , 令 为其基础闭后继包, 记为 .
元定理 2.1.0.6. 记 , 则递归地定义 和 , 我们有 .
另一方面, 我们考虑对 分离公理模式直接的刻画.
定义 2.1.0.7. 对 公式 , 考虑它给出的 预函数符号 (称作其分离子), 定义为 .
元定理 2.1.0.8. 任何 分离子都是基础函数符号.
定义 2.1.0.9. 定义 .