查看“︁ZF 公理系统”︁的源代码

[[分类:公理集合论]]
[[分类:以 E. Zermelo 命名]]
[[分类:以 A. Fraenkel 命名]]
{{InfoBox
|name=策梅洛–弗兰克尔公理系统
|eng_name=Zermelo–Fraenkel set theory
|aliases=策梅洛–弗兰克尔公理体系,策梅洛–弗兰克尔公理集合论,ZF,ZF公理体系,ZF公理系统
}}
'''<ins>策梅洛</ins>–<ins>弗兰克尔</ins>公理系统'''('''Zermelo–Fraenkel set theory''')，简称 '''ZF 公理系统'''或 '''ZF''' ，指为避免 Russell 悖论而对[[:分类:朴素集合论|集合论]]进行公理化的[[:分类:公理集合论|公理系统]]之一。如今， ZF 指这一体系下包含 8 条公理的版本，而包含[[选择公理]]或其他等价公理的则称为 [[ZFC 公理系统]]。

== 公理系统 ==

ZF 是一个[[形式化公理系统（逻辑）|形式化公理系统]]，是一种基于[[:分类:谓词逻辑|谓词逻辑]]的系统。
出于简洁性考虑，这里不考虑谓词逻辑层次的框架，也就是说不区分指定操作在谓词逻辑系统中是公理还是定理还是分离规则与它们的结论。

对应地包含以下四方面。

=== 终端元素集合 ===
这一公理系统中，终端元素集包括[[可数无穷多]]的[[个体词（谓词逻辑）|常量及变量]]符号，其中每个可以用于代表一个集合。

=== 算子符号集合 ===
这一公理系统中包括以下算子符号。
* [[逻辑联结词]] <math>\lnot,\land,\lor</math>
* [[量词]] <math>\forall,\exists</math>
* [[等词]] <math>=</math>
* [[成员关系|属于符号]] <math>\in</math>

=== 命题形式 ===
==== 原子公式 ====
ZF 中包括两种形式的原子公式：
* <math>x=y</math>
* <math>x\in y</math>
其中元变量 <math>x,y</math> 可以解释为任意个体变项。

==== 合式公式 ====
ZF 中合式公式（简称公式）包括以下几种：
* 原子公式
* <math>\lnot\varphi</math>
* <math>(\varphi\rightarrow\psi)</math>
* <math>\exists x\varphi</math>
其中元变量 <math>\varphi,\psi</math> 可以解释为任意原子公式，元变量 <math>x</math> 可以解释为任意个体变项。

根据一般习惯，继续定义 <math>\land,\lor,\leftrightarrow,\forall</math> 等算子符号以简化表示，并且按一般习惯定义括号的使用规则。

=== 变换规则 ===
严格地说只有 [[分离规则|mp（分离规则）]]。

这里允许直接使用一阶逻辑中的定理，这些定理相当于一些变化规则（本质上并不是），因此可以认为有：
* mp（分离规则）
* [[全称特化|us/ui（全称特化）]]
* [[存在推广|eg（存在推广）]]
* sub（对公理的[[代入]]）
等变换规则，以及其他操作逻辑联结词的规则，也可以使用标示等操作。

=== 公理 ===
ZF 公理体系有 8 个不同的公理模式。

注：根据习惯和可读性，以下出现在属于符号右侧使用大写字母，左侧使用小写字母，但是原则上它们都是终端符号集中代表集合的符号，是同等地位的个体变项。

==== 外延公理 ====
'''外延公理'''('''axiom of extensionality''', '''axiom of extent''')<ref>外延(extension)，来自逻辑用语，外延(extensional)定义指通过列出全部对象定义，内涵(intensional)定义指通过界定对象特征定义。外延一词在这里表示集合完全由成员确定。</ref>，在 ZF 体系中也称 '''ZF1''' 公理。

<math>\forall A \forall B [\forall x (x \in A \leftrightarrow x\in B) \rightarrow A=B]</math>

这一公理描述了符号集中 <math>=,\in</math> 两个符号的关系，描述了属于符号与被等词代入公理定义的等号的关系。

此时可以定义[[包含关系]]的符号 <math>A\subseteq B</math> 表示 <math>\forall x (x \in A \rightarrow x\in B</math> 。

==== 分离公理模式 ====
'''分离公理模式'''('''axiom schema of specification''', '''axiom schema of separation''')，在 ZF 体系中也称为 '''ZF2''' 公理模式。这是一个公理模式，其中 <math>\varphi(x)</math> 是任意含有个体变项 <math>x</math> 的公式。

<math>\forall A \exists B [\forall x(x\in B \leftrightarrow x\in A \land \varphi(x))]</math>

这一公理是构造性公理，指出对任意集合 <math>A</math> 和任意个体变项 <math>x</math> 的公式（构成一元谓词）都能找出一个集合中满足谓词的新集合。对任意 <math>A</math> 标示出集合个体 <math>B</math> ，可说明这一集合对指定的 <math>A</math> 和 <math>\varphi</math> 唯一，将其记作 <math>\{x\in A\mid\varphi(x)\}</math> 。这里可以演绎出 <math>\forall A[\forall x (\lnot(x\in A) \rightarrow \lnot(x \in \{x\in A\mid\varphi(x)\}))]</math> 。

将公式 <math>\lnot(x=x)</math> 代入 <math>\varphi(x)</math> ，以上述方式标示出其中特殊集合 <math>\varnothing_A=\{x\in A\mid \lnot(x=x)\}</math> ，则可以得到 <math>\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>\forall A[\forall x \lnot(x \in \varnothing_A)]</math> 。根据外延公理可证明 <math>\forall A\forall B(\varnothing_A=\varnothing_B)</math> ，也就是这一特殊集合唯一，称为'''[[空集]]'''，记作 <math>\varnothing</math> 。

==== 配对公理 ====
'''配对公理'''/'''对集公理'''('''axiom of pairing''')，即 '''ZF3''' 。

<math>\forall x\forall y \exists A [\forall z (z\in A \leftrightarrow z=x \lor z=y)]</math>

构造性公理。其中没有要求 <math>\lnot(x=y)</math> ，所以上式用个体常量进行全称特化 <math>x/a,y/a</math> 得到 <math>\exists A\forall z[z\in A\leftrightarrow z=a]</math> ，标示出这一集合称为[[单元素集]]，记作 <math>\{a\}</math> <ref>这里不用同一个字母，是因为 <math>x</math> 是形式语言中的个体变量，而 <math>a</math> 是元语言中的元变量，这里代替任意个体常量。所以虽然 <math>a</math> 仍然是任意的，但解释到形式语言中时就是具体的个体常量了，前后两个“任意”不是同一个量词。</ref>；用不同个体常量全称特化 <math>x/a,y/b</math> 得到 <math>\exists A\forall z[z\in A\leftrightarrow z=a\lor z=b]</math> ，标示出这一集合称为双元素集 <math>\{a,b\}</math> 。

==== 并集公理 ====
'''并集公理'''('''axiom of union''')，即 '''ZF4''' 。

<math>\forall A\exists B [\forall x (x\in B \rightarrow \exists C(x\in C \land C\in A))]</math>

构造性公理。对任意 <math>A</math> 标示出集合 <math>B</math> ，可说明唯一，称为'''[[广义并]]''' <math>\bigcup A</math> 。

对集公理和并集公理给出了'''[[并集]]'''的定义：对个体常量 <math>A,B</math> ，根据对集公理有集合 <math>\{A,B\}</math> ，再根据并集公理有 <math>\bigcup\{A,B\}</math> ，记作 <math>A\cup B</math> 。可以证明 <math>\{a,b\}=\{a\}\cup\{b\}</math> 。这里可以继续定义 <math>\{a,b,c,\cdots,n\} = \{a\}\cup\{b\}\cup\{c\}\cup\cdots\cup\{n\}</math> 。

到这一步可以定义[[自然数]]的 von Neumann 构造，即定义 <math>\mathbf{0}=\varnothing,\mathbf{1}=\{\mathbf{0}\},\mathbf{2}=\{\mathbf{0},\mathbf{1}\},\mathbf{3}=\{\mathbf{0},\mathbf{1},\mathbf{2}\},\cdots</math> ，或者直接使用上述公理，记函项 <math>S(\mathbf{n})=\mathbf{n}\cup\{\mathbf{n}\}</math> 。

这一步骤开始也可以定义集合的自然数[[基数]]。

==== 无穷公理 ====
'''无穷公理'''('''axiom of infinity''')，即 '''ZF6''' 。

<math>\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>\exists X [\varnothing \in I \land \forall x(x\in X\rightarrow S(x)\in I)]</math> 。

如果这里考虑自然数的 von Neumann 构造，就是说存在该构造下的自然数集。可以得知这是给出了一个可数无穷大的集合，出现了第一个超限基数 <math>\beth_0</math> 。

==== 替换公理模式 ====
'''替换公理模式'''('''axiom schema of replacement''')，即 '''ZF8''' 。

<math>\forall A \exists B \forall x (x\in B \leftrightarrow x\in A\land \varphi(x,y))</math>

或者用已经得到的记号， <math>\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>\forall X\exists Y[\forall y (y\in Y \leftrightarrow \forall z(z\in y \rightarrow z \in X))]</math>

或者用已经得到的记号 <math>\forall X\exists Y [\forall y(y \in Y \rightarrow y \subseteq X)]</math> 。

构造性公理，说明了对一个集合可以构造一个新的集合。这里得到的是'''[[幂集]]''' <math>\mathcal{P}(X)</math> 。

结合已经定义的集合基数大小关系，这里可以明确证明幂集是势更大的集合，之前的 <math>\beth_0</math> 的集合被继续扩展到更大的 <math>\beth</math> 数上。

==== 正则公理 ====
'''正则公理'''('''axiom of regularity''')/'''基础公理'''('''axiom of foundation''')，即 '''ZF7''' 。

<math>\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>\forall x (x\neq \varnothing \rightarrow \exist y\in x (y\cap x = \varnothing))</math>