2.1. 基础性

元定理 2.1.0.1 (by Bernays). 可有穷公理化.

证明. 我们选取外延公理和九条存在性公理, 然后指出这十条公理构成的集合论与 等效. 这九条存在性公理分别宣称:

1.

: 空集存在.

2.

: 对集 存在.

3.

: 卡氏积 存在.

4.

: 差集 存在.

5.

: 并集 存在.

6.

: 定义域 存在.

7.

: 对所有集合 存在.

8.

: 对所有集合 存在.

9.

: 对所有集合 存在.

这里 又称作 Godel 算子或基础算子. 不难看出它们都是 可证的函数符号, 所以我们的目标是证明它们可以复现 分离公理模式. 我们对公式的结构做元归纳法, 并证明一个稍强的版本的 分离公理模式: 若 公式, 则 . 注意交集 可以算出来, 可以写作 , 可以写作 , 我们不妨设 中只出现 四种符号, 且 两边的变元符号总是不同.

1.

形若 , 我们对 进行归纳.

1.

, 此时共有两种情况.

1.

, 此时 .

2.

, 此时 .

2.

, 此时共有六种情况. 注意 是三阶对称群的两个对换生成元, 我们可以自由调换三元元组的顺序.

1.

, 此时 .

2.

, 此时 .

3.

, 此时 .

4.

, 此时 .

5.

, 此时 .

6.

, 此时 .

3.

, 此时我们要求出示对 的归纳假设, 区分四种情况.

1.

: 取对 的归纳假设的集合, 乘之以 .

2.

: 取对 的归纳假设的集合, 乘之以 , 然后交换三元元组中的后两个元素.

3.

: 以 .

4.

: 以 , 然后交换三元元组中的后两个元素.

2.

形若 , 同样对 归纳.

1.

, 此时 .

2.

, 此时我们要求出示对 的归纳假设, 区分两种情况.

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. 定义 .