ZF 公理系统
| 策梅洛–弗兰克尔公理系统 | |
|---|---|
| 术语名称 | 策梅洛–弗兰克尔公理系统 |
| 英语名称 | Zermelo–Fraenkel set theory |
| 别名 | 策梅洛–弗兰克尔公理体系, 策梅洛–弗兰克尔公理集合论, ZF |
策梅洛–弗兰克尔公理系统(Zermelo–Fraenkel set theory)，简称 ZF 公理系统或 ZF ，指为避免 Russell 悖论而对集合论进行公理化的公理系统之一。如今， ZF 指这一体系下包含 8 条公理的版本，而包含选择公理或其他等价公理的则称为 ZFC 公理系统。
公理系统
ZF 是一个形式化公理系统，是一种基于谓词逻辑的系统。 出于简洁性考虑，这里不考虑谓词逻辑层次的框架，也就是说不区分指定操作在谓词逻辑系统中是公理还是定理还是分离规则与它们的结论。
对应地包含以下四方面。
终端元素集合
这一公理系统中，终端元素集包括可数无穷多的常量及变量符号，其中每个可以用于代表一个集合。
算子符号集合
这一公理系统中包括以下算子符号。
- 逻辑联结词 [math]\displaystyle{ \lnot,\land,\lor }[/math]
- 量词 [math]\displaystyle{ \forall,\exists }[/math]
- 等词 [math]\displaystyle{ = }[/math]
- 属于符号 [math]\displaystyle{ \in }[/math]
命题形式
原子公式
ZF 中包括两种形式的原子公式：
- [math]\displaystyle{ x=y }[/math]
- [math]\displaystyle{ x\in y }[/math]
其中元变量 [math]\displaystyle{ x,y }[/math] 可以解释为任意个体变项。
合式公式
ZF 中合式公式（简称公式）包括以下几种：
- 原子公式
- [math]\displaystyle{ \lnot\varphi }[/math]
- [math]\displaystyle{ (\varphi\rightarrow\psi) }[/math]
- [math]\displaystyle{ \exists x\varphi }[/math]
其中元变量 [math]\displaystyle{ \varphi,\psi }[/math] 可以解释为任意原子公式，元变量 [math]\displaystyle{ x }[/math] 可以解释为任意个体变项。
根据一般习惯，继续定义 [math]\displaystyle{ \land,\lor,\leftrightarrow,\forall }[/math] 等算子符号以简化表示，并且按一般习惯定义括号的使用规则。
变换规则
严格地说只有 mp（分离规则）。
这里允许直接使用一阶逻辑中的定理，这些定理相当于一些变化规则（本质上并不是），因此可以认为有：
- mp（分离规则）
- us/ui（全称特化）
- eg（存在推广）
- sub（对公理的代入）
等变换规则，以及其他操作逻辑联结词的规则，也可以使用标示等操作。
公理
ZF 公理体系有 8 个不同的公理模式。
注：根据习惯和可读性，以下出现在属于符号右侧使用大写字母，左侧使用小写字母，但是原则上它们都是终端符号集中代表集合的符号，是同等地位的个体变项。
外延公理
外延公理(axiom of extensionality, axiom of extent)[1]，在 ZF 体系中也称 ZF1 公理。
[math]\displaystyle{ \forall A \forall B [\forall x (x \in A \leftrightarrow x\in B) \rightarrow A=B] }[/math]
这一公理描述了符号集中 [math]\displaystyle{ =,\in }[/math] 两个符号的关系，描述了属于符号与被等词代入公理定义的等号的关系。
此时可以定义包含关系的符号 [math]\displaystyle{ A\subseteq B }[/math] 表示 [math]\displaystyle{ \forall x (x \in A \rightarrow x\in B }[/math] 。
分离公理模式
分离公理模式(axiom schema of specification, axiom schema of separation)，在 ZF 体系中也称为 ZF2 公理模式。这是一个公理模式，其中 [math]\displaystyle{ \varphi(x) }[/math] 是任意含有个体变项 [math]\displaystyle{ x }[/math] 的公式。
[math]\displaystyle{ \forall A \exists B [\forall x(x\in B \leftrightarrow x\in A \land \varphi(x))] }[/math]
这一公理是构造性公理，指出对任意集合 [math]\displaystyle{ A }[/math] 和任意个体变项 [math]\displaystyle{ x }[/math] 的公式（构成一元谓词）都能找出一个集合中满足谓词的新集合。对任意 [math]\displaystyle{ A }[/math] 标示出集合个体 [math]\displaystyle{ B }[/math] ，可说明这一集合对指定的 [math]\displaystyle{ A }[/math] 和 [math]\displaystyle{ \varphi }[/math] 唯一，将其记作 [math]\displaystyle{ \{x\in A\mid\varphi(x)\} }[/math] 。这里可以演绎出 [math]\displaystyle{ \forall A[\forall x (\lnot(x\in A) \rightarrow \lnot(x \in \{x\in A\mid\varphi(x)\}))] }[/math] 。
将公式 [math]\displaystyle{ \lnot(x=x) }[/math] 代入 [math]\displaystyle{ \varphi(x) }[/math] ，以上述方式标示出其中特殊集合 [math]\displaystyle{ \varnothing_A=\{x\in A\mid \lnot(x=x)\} }[/math] ，则可以得到 [math]\displaystyle{ \forall A[ \forall x (\lnot(x\in A) \rightarrow \lnot(x \in \varnothing_A)) \forall x (x\in A \rightarrow \lnot(x \in \varnothing_A))] }[/math] ，也就是 [math]\displaystyle{ \forall A[\forall x \lnot(x \in \varnothing_A)] }[/math] 。根据外延公理可证明 [math]\displaystyle{ \forall A\forall B(\varnothing_A=\varnothing_B) }[/math] ，也就是这一特殊集合唯一，称为空集，记作 [math]\displaystyle{ \varnothing }[/math] 。
配对公理
配对公理/对集公理(axiom of pairing)，即 ZF3 。
[math]\displaystyle{ \forall x\forall y \exists A [\forall z (z\in A \leftrightarrow z=x \lor z=y)] }[/math]
构造性公理。其中没有要求 [math]\displaystyle{ \lnot(x=y) }[/math] ，所以上式用个体常量进行全称特化 [math]\displaystyle{ x/a,y/a }[/math] 得到 [math]\displaystyle{ \exists A\forall z[z\in A\leftrightarrow z=a] }[/math] ，标示出这一集合称为单元素集，记作 [math]\displaystyle{ \{a\} }[/math] [2]；用不同个体常量全称特化 [math]\displaystyle{ x/a,y/b }[/math] 得到 [math]\displaystyle{ \exists A\forall z[z\in A\leftrightarrow z=a\lor z=b] }[/math] ，标示出这一集合称为双元素集 [math]\displaystyle{ \{a,b\} }[/math] 。
并集公理
并集公理(axiom of union)，即 ZF4 。
[math]\displaystyle{ \forall A\exists B [\forall x (x\in B \rightarrow \exists C(x\in C \land C\in A))] }[/math]
构造性公理。对任意 [math]\displaystyle{ A }[/math] 标示出集合 [math]\displaystyle{ B }[/math] ，可说明唯一，称为广义并 [math]\displaystyle{ \bigcup A }[/math] 。
对集公理和并集公理给出了并集的定义：对个体常量 [math]\displaystyle{ A,B }[/math] ，根据对集公理有集合 [math]\displaystyle{ \{A,B\} }[/math] ，再根据并集公理有 [math]\displaystyle{ \bigcup\{A,B\} }[/math] ，记作 [math]\displaystyle{ A\cup B }[/math] 。可以证明 [math]\displaystyle{ \{a,b\}=\{a\}\cup\{b\} }[/math] 。这里可以继续定义 [math]\displaystyle{ \{a,b,c,\cdots,n\} = \{a\}\cup\{b\}\cup\{c\}\cup\cdots\cup\{n\} }[/math] 。
到这一步可以定义自然数的 von Neumann 构造，即定义 [math]\displaystyle{ \mathbf{0}=\varnothing,\mathbf{1}=\{\mathbf{0}\},\mathbf{2}=\{\mathbf{0},\mathbf{1}\},\mathbf{3}=\{\mathbf{0},\mathbf{1},\mathbf{2}\},\cdots }[/math] ，或者直接使用上述公理，记函项 [math]\displaystyle{ S(\mathbf{n})=\mathbf{n}\cup\{\mathbf{n}\} }[/math] 。
这一步骤开始也可以定义集合的自然数基数。
无穷公理
无穷公理(axiom of infinity)，即 ZF6 。
[math]\displaystyle{ \exists X [\exists E (\forall z \lnot (z \in E) \land e\in X) \land \forall x (x\in X \rightarrow \exists y(y\in X \land \forall a(a\in y \rightarrow a\in x \lor a = x)))] }[/math] 。
使用我们已经得到的记号，简记为 [math]\displaystyle{ \exists X [\varnothing \in I \land \forall x(x\in X\rightarrow S(x)\in I)] }[/math] 。
如果这里考虑自然数的 von Neumann 构造，就是说存在该构造下的自然数集。可以得知这是给出了一个可数无穷大的集合，出现了第一个超限基数 [math]\displaystyle{ \beth_0 }[/math] 。
替换公理模式
替换公理模式(axiom schema of replacement)，即 ZF8 。
[math]\displaystyle{ \forall A \exists B \forall x (x\in B \leftrightarrow x\in A\land \varphi(x,y)) }[/math]
或者用已经得到的记号， [math]\displaystyle{ \forall A \exists B (B = \{y\in A\mid \exists x (x\in A \land \phi(x,y))\}) }[/math] 。
如果这里的谓词标示某种对应关系（实际就是种关系，但是其无法定义在集合前），则说明了某个集合中每个元素在某个关系下关联的元素构成的仍然是集合。
幂集公理
幂集公理(axiom of power set)，即 ZF5 。
[math]\displaystyle{ \forall X\exists Y[\forall y (y\in Y \leftrightarrow \forall z(z\in y \rightarrow z \in X))] }[/math]
或者用已经得到的记号 [math]\displaystyle{ \forall X\exists Y [\forall y(y \in Y \rightarrow y \subseteq X)] }[/math] 。
构造性公理，说明了对一个集合可以构造一个新的集合。这里得到的是幂集 [math]\displaystyle{ \mathcal{P}(X) }[/math] 。
结合已经定义的集合基数大小关系，这里可以明确证明幂集是势更大的集合，之前的 [math]\displaystyle{ \beth_0 }[/math] 的集合被继续扩展到更大的 [math]\displaystyle{ \beth }[/math] 数上。
正则公理
正则公理(axiom of regularity)/基础公理(axiom of foundation)，即 ZF7 。
[math]\displaystyle{ \forall X[\exists x(x\in X) \rightarrow \exists y (y\in X \land \lnot\exists z(z\in y \land z\in x))] }[/math]
或者用已有的记号 [math]\displaystyle{ \forall x (x\neq \varnothing \rightarrow \exist y\in x (y\cap x = \varnothing)) }[/math]