策梅洛-弗兰克尔集合论

“ZFC”重定向至此。关于其他用法，请见“ZFC (消歧义)”。

策梅洛-弗兰克尔集合论（英语：Zermelo-Fraenkel Set Theory），是数学基础中最常用的一阶公理化集合论。含选择公理时常简写为ZFC，不含选择公理的则简写为ZF。它是二十世纪早期为了建构一个不会导致类似罗素悖论的矛盾的集合理论所提出的一个公理系统。

介绍

ZFC旨在构建自一个单一的基本本体论概念集合，和一个单一的本体论假定，就是在论域中所有的个体（就是所有数学对象）都是集合。有一个单一的基本二元关系集合成员关系；集合$a$是集合$b$的成员写为$a\in b$（通常读做"$a$是$b$的元素"）。ZFC是一阶理论，所以ZFC包括后台逻辑是一阶逻辑的公理。这些公理支配了集合的行为和交互。ZFC是标准形式的公理化集合论。使用ZFC的大量的正在进行中的普通数学推导请参见Metamath （页面存档备份，存于互联网档案馆）在线计划。

在1908年，恩斯特·策梅洛提出了第一个公理化集合论，即策梅洛集合论。然而，这个公理系统无法构建出序数的集合；而序数是许多集合论研究的根本工具。此外，Zermelo的分类公理中使用了被称作“明确性”的性质，而它的实际意义是有歧义的（此时一阶逻辑的概念还未被提出）。在1922年，亚伯拉罕·弗兰克尔和陶拉尔夫·斯科伦独立的提议了定义“明确性”为可以在一阶逻辑中公式化并原子公式仅包括集合的公式。他们还同时提出应该用替代公理取代分类公理，并在体系中添加正规公理（首先由 冯诺依曼提出），从而得到了被称作 ZF的公理体系。

再向ZF增加选择公理就诞生了ZFC。选择公理曾饱受争议，因为选择函数的存在性是非构造性的；选择公理确立了选择函数的存在，而不说明如何构造这些函数。所以使用选择公理构造的一些集合，尽管可以证明其存在，但可能无法详细、描述性地构造出。因此，当一个结论依赖于选择公理时，有时会被明确地指出。

ZFC一般由一阶逻辑写出，实际上包含了无穷多个公理，因为替代公理实际上是公理模式。理查德·蒙塔古证明了ZFC和ZF集合论二者都不能用有限个公理来公理化。在另一方面，冯诺伊曼-博内斯-哥德尔集合论（Von Neumann–Bernays–Gödel, NBG）可以被有限公理化。NBG的对象同时包括集合和类；类是有含有元素但不在其他任何类中的实体。NBG和ZFC事实上是等价的，即所有不以任何方式提及类的定理在两个公理体系中同时可以证明或同时不能证明。

依据哥德尔第二不完备定理，ZFC的一致性不能在ZFC之内证明。ZFC的延展包括了通常意义上的大部分数学，所以ZFC的相容性不能在其他数学分支中证明。ZFC的相容性可从弱不可达基数的存在(独立于ZFC)而得出。几乎没有人怀疑ZFC有什么矛盾；通常认为，如果ZFC事实上不自洽，那相应的例子早就应该被发现了。可以肯定的是，ZFC避开了朴素集合论的三大悖论，罗素悖论、布拉利-福尔蒂悖论和康托尔悖论。

文献中讨论过的ZFC的缺陷包括：

• 它比几乎所有普通数学所要求的程度还要强（Saunders MacLane和所罗门·费弗曼这么认为）；
• 相对于其他集合论的公理化，ZFC相对要弱。例如，它不允许全集合（如新基础）或类（如NBG）的存在；
• Saunders MacLane（范畴论的缔造者之一）和其他人争论说任何公理化集合论对于实际上的数学工作方式而言都是不正当的。依据他的观点，数学不是关于抽象对象的搜集和它们的性质的学科，而是关于结构和结构保持的映射的学科。

基本符号

ZFC有许多等价的形式。下列的公理是由丘嫩于1980年提出。公理本身以一阶逻辑来叙述。

本条目定理的证明会频繁引用一阶逻辑的定理，定理的代号可以参见常用的推理性质一节。

以下把 $\vdash _{ZFC}$ 和 $\vdash _{ZF}$ 都简写为 $\vdash$，除了强调使用选择公理的情况。

断言符号

在ZF下，“属于关系”以一个双元断言符号 $P(x,\,y)$ 来表示， $P(x,\,y)$ 通常简记为 $x\in y$ ，并被直观理解成“x属于y”；类似地， $P(x,\,y)$ 的否定 $\neg P(x,\,y)$ 通称被简记为 $x\notin y$ ，并被直观理解为“x不属于y”。

另外，丘嫩的ZF系统以一个双元断言符号 $Q(x,\,y)$ 来表示“相等关系”（通常简记为 $x=y$ ），且 $x=y$ 被预先的假设为ZF理论里的相等符号，换句话说，对于 $x=y$ 有以下的隐含公理：

等号公理 — 

• （E1） 对任意变量 $x$ ， $(\forall x)(x=x)$ 为公理。
• （E2） 对于任意变量 $x$ 和 $y$，若在公式 ${\mathcal {A}}$ 中自由的 $x$ 都不在 $\forall y$ 的范围内。若以${\mathcal {A}}_{y}$ 代表 ${\mathcal {A}}$ 某些（而非全部）自由的 $x$ 被取代成 $y$ 而成的新公式，则

$(\forall x)(\forall y)[(x=y)\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {A}}_{y})]$

为公理。

习惯上会把 $\neg (x=y)$ 简记成 $(x\neq y)$。

包含

但ZF所谈及的一切对象为“集合”，直观上“x包含于y”意为“所有x的元素a都会属于y”，以此为动机，ZF有以下的符号简写

$x\subseteq y:=\forall a[\,(a\in x)\Rightarrow (a\in y)\,]$

以上可称为“x包含于y”，也可称为“x是y的子集（subset）”。注意到 $a$ 须为展开这个简写时首次出现的变量，才能避免与其他变量混淆。

外延公理

主条目：外延公理

(ext)Axiom of extensionality — 
$(\forall x)(\forall y)\{(\forall z)[(z\in x)\Leftrightarrow (z\in y)]\Rightarrow (x=y)\}$

目前ZF内没有任何函数符号，而且一开始就假设 $x=y$ 为ZF理论里的相等符号，所以依据一阶逻辑的等式定理一节应有：

$\vdash (x=y)\Rightarrow [(z\in x)\Rightarrow (z\in y)]$

$\vdash (y=x)\Rightarrow [(z\in y)\Rightarrow (z\in x)]$

$\vdash (x=y)\Rightarrow (y=x)$

这样结合(AND)和演绎元定理就有：

$\vdash (x=y)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]$

对上式使用(GEN)有：

$\vdash (\forall z)\{(x=y)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}$

再结合量词公理(A5)就有：

$\vdash (x=y)\Rightarrow (\forall z)\{[(z\in x)\Leftrightarrow (z\in y)]\}$

注意对外延公理(ext)使用两次量词公理(A4)会有：

$\vdash (\forall z)\{[(z\in x)\Leftrightarrow (z\in y)]\}\Rightarrow (x=y)$

这样结合(AND)就有：

$\vdash (x=y)\Leftrightarrow (\forall z)[(z\in x)\Leftrightarrow (z\in y)]$

也就是外延公理(ext)搭配等号公理，可以推出“两个集合相等，若它们有相同的元素。”

视相等符号为公式

除了一开始就假设 $x=y$ 为ZF的相等符号，也可以一开始做如下的符号定义，将$x=y$ 定义为以下合式公式的简写：

$(x=y):=(\forall z)[(z\in x)\Leftrightarrow (z\in y)]\land (\forall z)[(x\in z)\Leftrightarrow (y\in z)]$

（$z$ 须为展开这个简写时首次出现的变量）

直观上，这个符号定义表示“两个集合相等，若它们有相同的元素；且它们会属于同个集合” 如此一来，就不需要外延公理，也可以确保 $x=y$ 为ZF理论里的相等符号：

证明

以下的证明会逐条检验等式定理一节所条列的定义 （E1）： $(x=x)$ 展开来是 $(\forall z)[(z\in x)\Leftrightarrow (z\in x)]\land (\forall z)[(x\in z)\Leftrightarrow (x\in z)]$ 那考虑到恒等关系和(AND)有 $\vdash (z\in x)\Leftrightarrow (z\in x)$ $\vdash (x\in z)\Leftrightarrow (x\in z)$ 那再套用(GEN)有 $\vdash (\forall z)[(z\in x)\Leftrightarrow (z\in x)]$ $\vdash (\forall z)[(x\in z)\Leftrightarrow (x\in z)]$ 对上两式使用(AND)有 $\vdash (\forall z)[(z\in x)\Leftrightarrow (z\in x)]\land (\forall z)[(x\in z)\Leftrightarrow (x\in z)]$ 所以（E1）得证。 （E2）： 目前ZF内没有任何函数符号，所以对变量 $x$ 来说，ZF的原子公式只有 $(x\in z)$ 和 $(z\in x)$ 两种可能，这样的话，（E2）等同于要求以下两式是ZF的定理 (1) $(x=y)\Rightarrow [\,(x\in z)\Rightarrow (y\in z)\,]$ (2) $(x=y)\Rightarrow [\,(z\in x)\Rightarrow (z\in y)\,]$ 对 $(x=y)$ 使用(AND)有 $(x=y)\vdash (\forall z)[(x\in z)\Leftrightarrow (y\in z)]$ $(x=y)\vdash (\forall z)[(z\in x)\Leftrightarrow (z\in y)]$ 那上两式搭配量词公理(A4)与(D1)会有 $(x=y)\vdash (x\in z)\Leftrightarrow (y\in z)$ $(x=y)\vdash (z\in x)\Leftrightarrow (z\in y)$ 对上面两式使用(AND)和(D1)就有 $(x=y)\vdash (x\in z)\Rightarrow (y\in z)$ $(x=y)\vdash (z\in x)\Rightarrow (z\in y)$ 所以根据演绎元定理，（E2）得证。 （E3）： 本条定义要求以下的合式公式为ZF的定理 $(x=y)\Rightarrow (y=x)$ 从且的交换性有 $\vdash (\forall z)[(z\in x)\Leftrightarrow (z\in y)]\Rightarrow (\forall z)[(z\in y)\Leftrightarrow (z\in x)]$ $\vdash (\forall z)[(x\in z)\Leftrightarrow (y\in z)]\Rightarrow (\forall z)[(y\in z)\Leftrightarrow (x\in z)]$ 对上面两式使用(AND)和(D1)就有 $(x=y)\vdash (\forall z)[(z\in y)\Leftrightarrow (z\in x)]$ $(x=y)\vdash (\forall z)[(y\in z)\Leftrightarrow (x\in z)]$ 再对上面两式使用(AND)和(D1)又有 $(x=y)\vdash (y=x)$ 所以（E3）的确是ZF的定理。 综上所述， $x=y$ 的确为ZF理论里的相等符号。$\Box$

但采用这个符号定义的ZF与丘嫩的ZF是两套不等效的理论，因为在丘嫩的ZF里没有以下的定理：

$\vdash [(x\in z)\Leftrightarrow (y\in z)]\Rightarrow (x=y)$

真子集

在定义“相等”以后，可以把“相等的集合”排除出子集的定义中，换句话说，ZF有以下的符号定义

$x\subset y:=(x\subseteq y)\wedge (x\neq y)$

可直观理解为“x是y的真子集（proper subset）”。

正规公理

主条目：正规公理

(reg)Axiom of regularity / Axiom of foundation — 
$(\forall x){\bigg \{}(\exists a)(a\in x)\Rightarrow (\exists y){\Big \{}(y\in x)\land \{\lnot (\exists z)[(z\in y)\land (z\in x)]\}{\Big \}}{\bigg \}}$

“每个非空集合$x$都包含一个成员$y$，使得$x$和$y$不相交。”

替代公理

(Axiom schema of replacement)

主条目：替代公理

令$\phi \!$是ZFC语言内的任意公式，其自由变量有$x,y,A,w_{1},\ldots ,w_{n}\!$，但$B$在$\phi \!$　则不是自由的。则：

$\forall A\forall w_{1},\ldots ,w_{n}{\bigl [}\forall x(x\in A\Rightarrow \exists !y\,\phi )\Rightarrow \exists B\forall x{\bigl (}x\in A\Rightarrow \exists y(y\in B\land \phi ){\bigr )}{\bigr ]}$。

“若一个可定义的函数$f$的定义域为一集合，且对定义域的任一$x$，$f(x)$也都是集合，则$f$的值域会是一个集合的子集。”这个限制被需要用来避免一些悖论。

分类公理

主条目：分类公理

(compr)Axiom Schema of Comprehension — 
若变量 $s$ 于公式 ${\mathcal {P}}$ 完全被约束，则对任意不是 $s$ 的变量 $x$ 与 $a$ ：

$(\forall x)(\exists s)(\forall a)\{(a\in S)\Leftrightarrow [(a\in x)\land {\mathcal {P}}]\}$

都是公理。

“对每个集合 $x$ 和任意不含变量 $s$ 的公式 ${\mathcal {P}}$ ，都有某 $x$ 的子集合 $s$ ，里面的成员都满足 ${\mathcal {P}}$ ”

分类公理事实上是以集合建构式符号为动机。构成的集合通常使用来标记。给定一集合z和具有一自由变量$x$的公式$\phi (x)\!$，则由所有在$z$内，满足$\phi \!$的$x$所组成的集合，标记为

$\{x\in z:\phi (x)\}$。

分类公理可以用来证明空集（标记为$\varnothing$）的存在，只要至少已存在一个集合。通常的方法是找一个所有集合都没有的性质。例如，设$w$是一个已存在的集合，而空集可定义为

$\varnothing =\{u\in w\mid (u\in u)\land \lnot (u\in u)\}$.

若背景逻辑包含等式，也可定义空集为

$\varnothing =\{u\in w\mid \lnot (u=u)\}$.

因此，空集公理可由此处的九个公理中导出。外延公理还可证明空集是唯一的（不依赖$w$）。通常会以定义性扩展，将符号$\varnothing$加至ZFC语言中。

分类元定理

分类公理也可以由替代公理和空集公理中导出，而视为一条元定理：

配对公理

(Axiom of pairing)

主条目：配对公理

若$x$和$y$是集合，则存在一个集合包含$x$和$y$。

$\forall x\forall y\exists z(x\in z\land y\in z)$。

这个公理是Z的一部分，但在ZF中就显得多余，因为它可以由将替代公理应用至任意有两个成员的集合上导出。此类集合的存在性可由将无穷公理或幂集公理应用两次至空集上得到。

并集公理

(Axiom of union)

主条目：并集公理

对任一个集合${\mathcal {F}}$，总存在一个集合$A$，包含每个为${\mathcal {F}}$的某个成员的成员的集合。

$\forall {\mathcal {F}}\,\exists A\,\forall Y\,\forall x[(x\in Y\land Y\in {\mathcal {F}})\Rightarrow x\in A]$。

无穷公理

(Axiom of infinity)

主条目：无穷公理

令$S(x)\!$为$x\cup \{x\}\!$，其中$x\!$为某个集合，则存在一个集合$X$，使得空集$\varnothing$为$X$的成员，且当一个集合$y$为$X$的成员时，$S(y)\!$也会是$X$的成员。

$\exists X\left[\varnothing \in X\land \forall y(y\in X\Rightarrow S(y)\in X)\right]$。

较口语地说，存在一个有无限多成员的集合$X$。满足无穷公理的最小集合$X$为冯诺伊曼序数$\omega$，这个序数也可想成是自然数的集合$\mathbb {N}$。

幂集公理

(Axiom of power set)

主条目：幂集公理

令$z\subseteq x$为$\forall q(q\in z\Rightarrow q\in x)$。对任一个集合$x$，皆存在一个集合$y$，为$x$的幂集的父集。$x$的幂集为一个其成员为所有$x$的子集的类。

$\forall x\exists y\forall z[z\subseteq x\Rightarrow z\in y]$。

选择公理

(Well-ordering theorem)

主条目：良序定理

对任一集合$X$，总存在一个可良好排序X的二元关系$R$。这意指著，$R$是$X$上的全序关系，且$X$内每个非空子集在$R$下都有一个最小元素。

$\forall X\exists R(R\;{\mbox{well-orders}}\;X)$。

若给定前八个公理，就可以找到许多个和第九个公理等价的叙述，最著名的则为选择公理，其叙述如下：令$X$为一非空集合，则存在一从$X$映射至$X$内成员的并集的函数（称为“选择函数”），可使得对所有的$Y\in X$都会有$f(Y)\in Y$。因为当$X$为有限集合时，选择函数的存在性很容易由前八个公理中证出，所以选择公理只在无限集合中有意义。选择公理被认为是非结构的，因为它只声明一个选择集合的存在，但完全不讲这个选择集合是如何被“建构”出来的。

参见

• 康托尔定理
• 公理化集合论
• 策梅洛集合论
• 新基础集合论
• ZFC系统无法确定的命题列表

文献

• 亚历山大·阿比安, 1965. The Theory of Sets and Transfinite Arithmetic. W B Saunders.
• Keith Devlin, 1996 (1984). The Joy of Sets. Springer.
• Abraham Fraenkel, Yehoshua Bar-Hillel, and Levy, Azriel, 1973 (1958). Foundations of Set Theory. North Holland.
• Hatcher, William, 1982 (1968). The Logical Foundations of Mathematics. Pergamon.
• Jech, Thomas, 2003. Set Theory: The Third Millennium Edition, Revised and Expanded. Springer. ISBN 3-540-44085-2.
• Kunen, Kenneth, 1980. Set Theory: An Introduction to Independence Proofs. Elsevier. ISBN 0-444-86839-9.
• Suppes, Patrick, 1972 (1960). Axiomatic Set Theory. Dover.
• Tourlakis, George, 2003. Lectures in Logic and Set Theory, Vol. 2. Cambridge Univ. Press.
• Jean van Heijenoort, 1967. From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931. Harvard Univ. Press. Includes annotated English translations of the classic articles by Zermelo, Frankel, and Skolem bearing on ZFC.

外部链接

• Metamath. （页面存档备份，存于互联网档案馆） An online project building a great deal of mathematics from first-order logic and ZFC. Principia Mathematica done right.
• Stanford Encyclopedia of Philosophy: Set Theory （页面存档备份，存于互联网档案馆） -- by Thomas Jech.