策梅洛–弗兰克尔集合论，简称 ZF，是一个以集合表示数学对象的集合论公理系统。它规定了支配隶属关系和集合构造的原则，避免了不受限制地构造集合所导致的矛盾。ZF 不包含选择公理；加入这一公理后得到的 ZFC，是数学的一种标准基础。不采用选择公理，并不意味着断言它的否定。(people.math.ethz.ch)
历史发展与形式语言
恩斯特·策梅洛于 1908 年发表了集合论的一套公理化方案。1922 年，亚伯拉罕·弗兰克尔和托拉尔夫·斯科伦各自独立地扩展并澄清了这一框架，尤其是引入替代原则，并明确可定义性质的表述方式。后来的发展又纳入了基础公理；策梅洛于 1930 年提出了一个修订后的系统。现代形式的 ZF 汇集了这些贡献，而非直接源自某一篇最初的文献。(people.math.ethz.ch)
ZF 用带等号的一阶逻辑表述。它唯一的原始非逻辑符号是隶属关系 (x\in y)，读作“(x) 是 (y) 的元素”。变量的取值范围是集合，集合的元素本身也都是集合：通常的表述中没有原始的非集合对象，即原子。子集、并集和函数等表达式通过定义引入，而不是作为额外的原始实体。(people.math.ethz.ch)
公理陈述一条基本原则，而公理模式则为每个符合条件的公式指定一条公理。分离和替代都是公理模式，因此，这些熟悉的名称实际指代无穷多条一阶公理，而不是对任意性质进行量化的单个句子。(plato.stanford.edu)
公理
一种常见的表述包含以下原则：
- **外延公理：**元素完全相同的集合相等。
- **空集公理：**存在一个空集 (\varnothing)。
- **配对公理：**对于任意集合 (a,b)，集合 ({a,b}) 存在。
- **并集公理：**对于任意集合 (A)，存在集合 (\bigcup A)，其元素恰好是 (A) 的各个元素所包含的元素。
- **幂集公理：**每个集合 (A) 都有一个幂集 (\mathcal P(A))，其中包含 (A) 的所有子集。
- **无穷公理：**存在一个集合，它包含 (\varnothing)，并且在运算 (x\mapsto x\cup{x}) 下封闭。
- **分离公理模式：**每个带有允许使用的参数的公式，都定义了一个已给定集合的子集。
- **替代公理模式：**如果一个公式为集合 (A) 的每个元素指定唯一的集合，那么这些对应值构成一个集合。
- 基础公理，又称正则公理：每个非空集合 (A) 都有一个元素 (b)，使得 (A\cap b=\varnothing)。(plato.stanford.edu)
基础公理排除了集合属于自身以及有限的隶属循环。不同表述对冗余公理的处理有所不同：空集的存在性可以由其他原则推导出来，而分离公理模式可由替代公理模式连同其他公理推出。因此，与其统计有名称的公理数量，不如明确这些公理所生成的理论。(cl.cam.ac.uk)
替代公理模式涉及一种可定义的对应关系，这种对应关系不必已经作为集合形式的函数存在。其输出可以包含原定义域之外的对象。相比之下，分离公理模式只从已有集合中选取元素。这一区别使替代公理模式在超限构造中发挥着不可或缺的作用。(plato.stanford.edu)
避免悖论与区分类
不受限制的概括原则允许每个条件都确定一个集合。将这一原则应用于 [ R={x:x\notin x}, ] 就会产生罗素悖论：(R\in R) 当且仅当 (R\notin R)。ZF 只允许受限制的分离表达式 ({x\in A:x\notin x})，其中 (A) 必须已经是一个集合。(plato.stanford.edu)
**真类**是不能构成集合的汇集，例如所有集合的汇集。在通常的 ZF 中，可定义类只是便于表述的描述方式，并不是变量能够取值的额外对象。冯·诺伊曼–伯奈斯–哥德尔集合论等类理论则对类提供了专门的形式化处理。(cl.cam.ac.uk)
构造数学对象
自然数可以用有限的冯·诺伊曼序数表示： [ 0=\varnothing,\qquad 1={0},\qquad 2={0,1},\qquad n+1=n\cup{n}. ] 无穷公理和分离公理模式使得这些数所组成的集合 (\omega) 得以构造。更一般地，序数将这种表示扩展到超限序型。(people.math.ethz.ch)
有序对可以编码为 [ (a,b)={{a},{a,b}}. ] 借助这种编码，可以将笛卡尔积、关系和函数构造为满足适当条件的有序对集合。这类编码展示了如何仅用隶属关系来解释更丰富的数学语言；它们是表示方式，而不是唯一规定的等同方式。(cl.cam.ac.uk)
**累积层级**将集合组织为以序数为索引的各个阶段： [ V_0=\varnothing,\qquad V_{\alpha+1}=\mathcal P(V_\alpha),\qquad V_\lambda=\bigcup_{\beta<\lambda}V_\beta ] 其中 (\lambda) 为极限序数。替代公理模式支持极限阶段的构造，而基础公理蕴含每个集合都属于某个阶段。整个层级是一个真类，而不是一个全集。(plato.stanford.edu)
选择、独立性与相容性
选择公理断言：每个以集合为索引的非空集合族，都存在一个函数，从族中的每个集合里选取一个元素。在 ZF 的基础上，它与适用于任意集合的良序原理等价。假定 ZF 相容，选择公理既不能由 ZF 证明，也不能由 ZF 否证。(plato.stanford.edu)
库尔特·哥德尔利用可构造宇宙建立了相对相容性结果；随后，保罗·科恩发展了**力迫法**，证明了与之互补的独立性结果。两人的工作共同表明：在假定 ZFC 相容的前提下，连续统假设独立于 ZFC。这些结果讨论的是从指定公理能够推出什么，而不是说明这些公理本身存在矛盾。(plato.stanford.edu)
哥德尔不完备定理还揭示了另一项限制：如果 ZF 相容，它就无法证明以标准算术方式表达的自身相容性陈述。因此，相容性证明通常确立的是一种相对结论——一个理论的相容性可由另一个理论的相容性推出——而不是从 ZF 内部给出无条件的保证。(plato.stanford.edu)