ZF公理系统（外文名：Zermelo-Fraenkel set theory）全称为策梅罗-弗伦克尔公理系统，简称ZF系统，是一个无矛盾的集合论公理系统，它的原始概念是集合和属于的关系。

1895年，格奥尔格·康托尔（Cantor）提出了集合的概念，但他未对集合的概念加以限制，产生了悖论。1902年伯特兰·阿瑟·威廉·罗素（Russell）发现的集合论悖论称为罗素悖论，ZF公理系统就是为了消除罗素悖论产生的。1908年蔡梅罗（Zermelo）发表了集合论的一个公理系统，后来经过弗兰克尔（Fraenkel）和斯科伦（Skolem）的改进，形成了ZF公理系统。

ZF公理系统由空集存在公理、外延公理、并集存在公理、幂集存在公理、无序对公理、置换公理、无限集存在公理、基础公理、子集公理组成。在ZF公理系统中添加选择公理即得到在数学中使用十分广泛的ZFC公理系统。

1895年，德国数学家格奥尔格·康托尔（Cantor）提出了集合的概念，他将具有某种特定性质对象的总体称为集合，他所开创的集合论一般称为朴素集合论或经典集合论。由于康托尔对集合的概念未加以限制，从而导致了理论的不一致，产生了悖论。

1902年，伯特兰·阿瑟·威廉·罗素发现了罗素悖论，揭示了一个基本的事实：一个集合或者是它本身的成员，或者不是它本身的成员。罗素悖论所涉及的概念都是朴素集合论中的基本概念——集合与元素，它的出现立即震动了整个数学界，引起了数学史上的第三次危机。为了消除悖论，人们开始寻找解决悖论的各种途径和方法。

1908年，蔡梅罗（Zermelo）首先发表了集合论的一个公理系统，后来经过弗兰克尔（Fraenkel）和斯科伦（Skolem）的改进，形成了ZF公理系统。同时，蔡梅罗在提出集合论公理系统时还收入了选择公理，称为ZFC公理系统，这是当时在数学界引起长期争论的一个问题，这个系统后来成为数学中使用最广泛的系统。

在逻辑学中，悖论是指命题：由出发，可以找到一个命题，若假定，就可以推出非；若假定非，就可以推出。1902年，伯特兰·阿瑟·威廉·罗素（Russell）构造了一个表示为的集合，是由所有那些不属于自己的集合所组成。假定，因为的任何元素都满足条件，所以，这与假定矛盾。反之，倘若假定，因为是由所有那些满足条件的所组成，所以，这与假定矛盾。这个矛盾称为罗素悖论。

罗素悖论产生后，许多数学家开始寻找解决办法。蔡梅罗提出了划分公理的基本思想。划分公理是指任给一集和一性质，则集合中一切满足性质的元素可以汇集起来构成一集，即为一集合。此处的性质是格奥尔格·康托尔集合论意义下能以用来造集的精确性质，即一元谓词。

根据划分公理，可证定理：任给一集，必有的一个子集，它不是的元素，即总有为真。

证明：设为任给的一个集合，又令为划分公理中所说的性质，则由划分公理可知为一集，为的一个子集。证不是的一个元素，即，否则若设，即为的一个元素。由于集合中的任何元素，要么具有性质，要么具有性质，无一例外。既已设定，则也不例外，它要么具有性质，即为一非本身分子集，即有，要么具有性质，即为一本身分子集，即有。

设有性质，又因假设有，故具有性质，根据的构造可知为的一个元素，从而，即具有性质，这是矛盾的。

再设有性质，即，故为的一个元素，但因的每一元素均有性质，故作为之元素的也不例外，亦应具有性质，故有性质，又是矛盾的。

总之，在原设的前提下，哪种说法都导致矛盾，故原设不能成立，不是的元素。

根据上述定理，即可证明罗素悖论中的“一切非本身分子集的‘集’”不是一个集合。否则，若设为一集合，则由定理可知，必有一子集不是的元素，亦即应有（式1）。

既然为一集合，又是它的子集，于是应承认是一个集合，从而可问是本身分子集，还是非本身分子集。若设为本身分子集，则有，但因，故推知，矛盾于式1。再设为非本身分子集，则因为一切非本身分子集汇集起来构成的集合，从而必为的一个元素，故，又矛盾于式1，总之哪种说法都导致矛盾，这表示原设为集合一事不能成立，从而不是集合。

既然根本不是集合，那也不能问是本身分子集还是非本身分子集，从而也谈不上罗素悖论的出现和存在了。

，该式表明，存在集合，对于任意的集合，都不属于，这就是空集合，用表示。

外延公理是指任一集合都是由其元素决定的。是外延公理的形式化。

，该式表明，给定任意的集合，都存在一个集合以的所有元素为元素。其中表示是集合的元素。

，满足此公理的集合是的幂集。其中是的形式表达。

表示对于任意集合，，都有集合。

，其含义是，对于任何函数，如果它的定义域是一个集合，那么它的值域也是一个集合。其中是的缩写，是的缩写。

，其中“”是缩写符号，。无限公理实际上是后继存在公理，是集合的后继集。

，该式表明，二元关系在每一个非空集合上都是良基的。它要求任一非空集合有一个“”极小元，把以自己为元素的集合排除掉。此公理与正则公理等价。对于任何一个非空集合都 存在它的一个元素，的任意元素都不属于。

，子集公理（也称划分公理）实际上代表着无穷多条公理。对于每一公式，都存在相应的一个子集公理。

GB公理系统式集合论的重要公理系统之一，由约翰·冯·诺依曼（John von Neumann）、贝奈斯（Bernays,Paul Isaak）、库尔特·卡塞雷斯（Kurt Gödel）等人建立。该系统中有集合和类两个基本概念，用小写英文字母作为集合变元，用大写英文字母作为类变元。此外，表示是一类，表示是一集合。

GB公理系统和ZF公理系统都是最重要的公理集合论系统，两个系统都是为了避免罗素悖论、同时又保留格奥尔格·康托尔集合论中的有益成果而构造的，所以大部分公理都相同或相似。

但对于概括原则的修改，GB公理系统和ZF公理系统采取了不同的方案。ZF公理系统确认在一个已有的集合内，可以用一个谓词造一个集，即对任何合式公式，有；GB公理系统不需要有先验的类，直接由（直谓）公式造类，其精神更接近格奥尔格·康托尔概括原则。ZF公理系统的对象仅只“集合”一种，它们都是系统内的个体；而GB公理系统的对象除了“集合”之外，还有“真类”，它们实际上不是GB公理系统的个体，这在一定程度上带来了不便。

在ZF公理系统中添加选择公理而得到的系统称为ZFC公理系统，这个系统是数学中使用最广泛的系统。选择公理是指对任意集族，存在一函数使得对任意非空都有（称为上的选择函数）。选择公理表明给定任意个非空集合，可以同时从每个集合中取出一个元素。

选择公理的相容性是指选择公理不会导致逻辑矛盾的特性。1939年，哥德尔（Godel,K.）用两种在ZF公理系统中构造ZFC模型的方法（内模型法）证明了这种相对相容性。

选择公理对于ZF公理系统的独立性表明，存在着在ZF公理系统之上加入选择公理的弱形式的可能（若不独立，这种加入弱形式的办法是无效的），甚至存在在ZF公理系统之上加入与选择公理相矛盾命题为公理的可能（若不独立，这种加入讲导致矛盾）。

在策梅罗首次提出集合论公理系统后，其中的许多缺点遭到了各方面的批评。特别是斯科兰姆1922年8月在赫尔辛基召开的第五届堪的纳维亚数学家大会上做了公理化集合论的报告,他对策梅罗公理系统提出了八点批评，其中包括策梅罗的公理系统不足以提供通常集合论的基础等。另一方面,许多人对策梅罗公理集合论提出了改进意见。例如,策梅罗公理集合论太狭窄不足以满足对集合论的合法需要,有许多集合不能由它产生出来,也不能够由此造出序数的一般理论和超穷归纳法。为了弥补这一缺陷,弗兰克尔加进一个公理组——代换公理。另外,弗兰克尔还把公理以符号逻辑表示出来,形成了通用的ZF公理系统。