策尔梅洛－弗兰克尔公理系统

公理集合论中一种最常使用的形式公理系统。是在1908年策尔梅洛系统的基础上，经A．T．司寇伦、A．A．弗兰克尔的改进与补充而建立的一个公理系统，是康托尔集合论方法的形式化处理。它易于理解，是影响最广的一个系统，人们通常把这系统叫做ZF系统，并简记为ZF。它的原始概念是集合和属于关系，它们不是由定义给出的，而是借助于一阶语言由公理直接予以刻画的。这一系统的公理是下述10条。

①外延公理 对于任意的两个集合x与y，如果x的任一元都是y的元，反之，y的任一元都是x的元，则x=y。换句话说，对于任意两个集合，它们的元素相同时，它们为同一个集合。用公式表示为：

②空集公理 存在一个没有任何元素的集合。也就是说，空集合是存在的。用公式表示为：x y(yx)。空集合通常记作。

③无序对集公理 对于任意的集合x，y，都存在一集合z，它的元素恰好是x与y，即

此公理中的集合z，记作｛x，y｝，称为x与y的无序对集合。当x=y时，它就是｛x｝，此时称｛x｝为x的单元集合。

④并集公理 对于任意的集合x，都存在一集合y，y的元素恰好是x的所有元素的元素，用公式表示为：

此公理中定义的集合y称为x的并集合，记作∪x。由此公理，对于任意的集合S，s，它们的并S∪s就定义为集合∪｛S，S｝。

⑤幂集合公理 对于任意的集合x，都有一个集合y，y的元素恰好是x的全部子集合。用公式表示为：

其中

此公理中定义的集合y称为x的幂集合，记作P(x)。

⑥无穷公理 存在一个无穷集合x。用公式表示为：

此集合记作ω。

⑦分离公理模式 对任意的集合论公式A(z)和任意的集合x，都存在一集合y，y的元素恰好是由满足公式A(z)且属于x的那些元素组成。用公式表示：

⑧替换公理模式 对于任意的公式A(x，y)，如果对任意的集合x，都有唯一的集合y，使得A(x，y)成立，那么对任意的集合S，有一集合S，使得S=｛u｜t∈Si并且A(t，u)｝。也就是说，若A(x，y)具有一对一的性质，这时，对于任一集合S，由S中每一元素经公式A(x，y)对应的值组成一集合，即

式中

公理⑦与公理⑧都是对任意公式而言，一个公式对应一条公理，因为有可数无穷个公式，所以有可数无穷多条公理。但是，这样的公式都有统一的格式，因此，称它们为公理模式。

⑨正则公理(基础公理) 每一非空集合都有一∈最小元。即对于任一非空集合x，都有一集合y，使得y∈x且y与x不交，用公式表示为：

⑩选择公理(参见选择公理)

以上的公理中，②～⑧都是关于集合存在的公理。

在策尔梅洛1908年的论文中，分离公理中的A(z)仅指集合的性质。然而，性质仍然是一个很含混的概念，弗兰克尔把性质形式化为一阶语言中的公式，从而使这一概念清晰和严谨了。在文献中，人们常把公理①～⑦与⑨～⑩一起记为Z(即策尔梅洛系统)，把公理①～⑩一起记为ZF。有时为了突出选择公理，人们也把公理①～⑨记为ZF，而把公理①～⑩记为ZFC。

ZF的独立性问题 ZF不是独立的，例如，由公理①～⑥与⑧～⑨可以推出公理⑦。但由于公理⑦是策尔梅洛首先提出的，具有历史意义，并且运用方便，用它来证明交、笛卡儿乘积等运算的合法性是相当简洁的。因此，一般说来，公理⑦还是给予保留的。

ZF的协调性问题 据哥德尔第二不完全性定理，ZF的协调性只能在比它更强的系统中证明。例如，在ZF十大基数公理(即“存在－大基数”)的公理系统中，可以证明ZF是协调的。在奎因－莫尔斯系统中也可证明ZF的协调性。