‌ZFC公理集合论系统（Zermelo–Fraenkel set theory with Choice）是现代数学最常用的公理集合论系统，由Zermelo与Fraenkel提出，并在此基础上加入选择公理。它以一阶谓词逻辑为基础，通过一组有限的公理刻画“集合”的基本性质，包括外延性、配对、并集、幂集、无穷公理、替代公理、正则性等。ZFC为绝大多数数学理论提供了统一的基础，其表达能力足以形式化几乎所有常见的数学对象与结构，因此成为数学中事实上的标准基础系统。

‌本节所介绍的是ZFC公理集合论系统的其中一个版本，该版本被用于形式化数学证明项目Metamath，能直接利用计算机进行形式化验证。本图书馆的数学定理均采用Metamath Zero进行形式化验证，保证推理的正确性。可以在math.mimirlib.com中看到形式化证明的内容，当然，也可以点击每个定理中的链接看到对应的证明步骤。

在形式化系统中，类型（type）是一种语法上的约束机制，用来区分不同种类的对象，防止将不相容的对象混用。例如，在自然语言里，我们不会把“数字”直接当作“句子”来使用；类似地，在形式化的集合论中，类型确保对象只能在合法的位置出现。通过为对象分配类型，我们能够建立严谨的推理规则，使系统中的表达式始终保持逻辑一致。ZFC公理集合论系统中的类型只有公式、集合和类，其中只有集合可以被量词约束，这也说明了ZFC公理集合论系统的论域中只有集合。

在ZFC中，命题由公式来表示。公式是由符号有限次组合而成的字符串，其构造遵循逻辑语法规则，因而是良构的表达式。一个公式可以是最基本的谓词，也可以由联结词和量词构成更复杂的命题。

公式的作用是表达一个陈述。通过它，我们才能在系统中表述公理、定理以及各种推理。需要强调的是，在ZFC中，公式本身是语法对象，而不是其语义意义。换句话说，“公式”指的是字符串这一形式层次，而“命题的真值”则是通过模型来解释的。

当某个语法项被赋予公式的类型时，它可以用来表示任意一个逻辑命题。在证明过程中，我们可以操纵公式本身（比如代入、变形），而在语义层次上，这些公式则代表着集合之间的关系或性质。

在ZFC中，集合是最基本的对象。所有的数学构造——不论是自然数、函数、关系还是拓扑空间——都可以在集合论框架下通过集合来刻画。集合的直观理解是“由某些元素组成的整体”，而在公理化的语境下，我们放弃了对集合的直观定义，仅通过一系列公理来约束它们的性质。

在语法层次上，集合对应于集合类型的语法项。这类项可以是变量，也可以是常量符号，还可以是由运算符生成的复合表达式。需要注意的是，在ZFC的论域中，量词所约束的对象都是集合。这一约束正是通过类型系统体现出来的，它保证了系统中一切推理都在“集合”的框架之内进行。

在ZFC中，除了集合之外，还引入了“类”的概念。类可以理解为按照某个性质收集起来的一族集合，例如“所有自然数的集合”“所有序数的集合”乃至“所有集合的整体”。与集合不同的是，类本身不一定是集合。特别是，“所有集合的整体”如果被当作集合会导致悖论（如Russell悖论），因此只能作为类来处理。

在语法层次上，类对应于类类型的语法项。它们可以由性质来刻画，例如“所有满足某条件的集合”，这样形成的就是一个类。由于类不必满足集合公理系统中的约束，它们往往比集合更“庞大”，但也因此不能作为量词的取值对象。换句话说，类可以用来表达和组织集合，但不能像集合那样直接被量化。接下来，我们引入关于类的一个表示。

这个表示的语义是将所有集合中那些满足公式 的集合选择出来，构成一个类。同时，我们定义集合在任何时候都可以看成一个类。

类在ZFC系统中扮演着重要的辅助角色。首先，它们允许我们更方便地描述某些集合的全体，例如“所有有限集合”或“所有群”。其次，类的存在保证了我们可以在语法中操作比集合更大的对象，而不会引发矛盾。最后，每一个集合都可以自然地看作一个类：某个集合所对应的类就是由它的所有成员组成的整体。这样，集合成为类的特殊情况，而类则是集合的推广。

联结词（或逻辑连接词）是用于构建命题的基本符号和操作符。它们定义了如何将较简单的命题组合成更复杂的命题。从类型的角度中，联结词是公式到公式的函数，即可将若干个公式合成为一个新的公式。在ZFC公理系统中，联结词不仅是形式的符号，它们也承载着特定的语义，比如否定、蕴涵、合取、析取、等价等等。

否定联结词 是ZFC公理系统的原子定义，语义上表示命题的否定，即若 为真，则 为假；若 为假，则 为真。

蕴涵联结词 → 是ZFC公理系统的原子定义，语义上表示命题 蕴涵 ，即若 为真，则 为真。

合取联结词 语义上表示命题 和命题 必须都为真。

析取联结词 语义上表示命题 和命题 至少有一个为真。

等价联结词 ↔ 语义上表示命题 和命题 同真同假。

谓词是用于表达某些属性或关系的基本符号和操作符。它们可以对个体或对象的某些性质进行断言，或者表示对象之间的关系。在形式逻辑中，谓词通常与常元或变元一起使用，构成一个更为复杂的命题。从类型的角度来说，谓词是常元或变元到公式函数，接受若干常元和变元，并返回一个公式，表示这些个体是否满足该谓词所描述的条件。例如，谓词“是人”可以用来断定一个个体是否是人，而谓词“在某城市居住”则用来表示个体与城市之间的关系。在ZFC公理系统中，谓词同样承载着特定的语义，它们用于对对象或集合之间的关系进行精确定义与推理。

等于谓词 是ZFC公理系统的原子定义，语义上表示 和 完全相同，即它们在所有相关属性和性质上没有任何区别。

属于谓词 是ZFC公理系统的原子定义，语义上表示 是 的一个元素。

包括谓词 语义上表示 中的元素包括 。

不等于谓词 语义上表示 与 不相等。

不属于谓词 语义上表示 不是 的一个元素。

不包括谓词 语义上表示 中的元素不包括 。

量词是用于表达命题中关于个体的数量或范围的基本符号和操作符。它们可以在命题中对个体的存在性或普遍性进行断言。从类型的角度来说，量词是一个从集合和公式到公式的函数。在ZFC公理系统中，量词只能用于约束集合，而不能约束公式或者类，这保证了不会出现自我指涉或Russell悖论造成的矛盾。量词不仅是形式符号，还承载着特定的语义，用于精确地描述个体与集合之间的关系，从而支持数学中的推理和证明过程。在公式中被量词约束的变元称为约束变元，否则称为自由变元，若变元 在公式 中为自由变元，则称 在 中自由出现，否则称 在 中无自由出现。

任意量词 是ZFC公理系统的原子定义，语义上表示任意 都满足 。

存在量词 语义上表示存在 满足 ，即至少一个 满足 。

不存在量词 语义上表示不存在 满足 。

存在至多一个量词 语义上表示存在至多一个 满足 ，即要么不存在满足 的 ，要么存在唯一一个满足 的 。

存在唯一量词 语义上表示存在唯一一个 满足 。

限域任意量词 语义上表示任意 中的元素 都满足 。

限域存在量词 语义上表示存在 中的元素 满足 。

限域不存在量词 语义上表示不存在 中的元素 满足 。

限域存在至多一个量词 语义上表示存在至多一个 中的元素 满足 。

限域存在至多一个量词 语义上表示存在唯一一个 中的元素 满足 。

用于指代任何一个可证明的命题的符号，类似于布尔代数中的 。

用于指代任何一个可证伪的命题的符号，类似于布尔代数中的 。

用于判断 是否与 无关。若 与 无关，则 可证或 在 中无自由出现，即 的值不会影响 的可证性。

表示集合的替换操作。后续我们会证明 与将 中的所有 的出现替换为 后的公式等价。

公理是在形式化体系中被无条件接受的基本命题，它不依赖推理而直接作为出发点。公理的作用是为整个系统提供最初的依据，规定哪些推理是合法的，哪些对象被认为存在。逻辑公理给出最基本的推理规则，确保演绎过程本身有效；集合论中的类扩展公理或其他专门公理则界定某类对象的存在范围。整体而言，公理是形式系统的“地基”，既不需要证明，也不能在体系内部被推翻，而是用来支撑所有定理的推导。

逻辑公理是形式系统中关于逻辑结构本身的基本假设，它们不依赖任何特定对象，而直接规定命题、量词及逻辑连接的最基本性质。它们的作用不仅是保障推理规则的正确性，还在于界定逻辑语言的运作方式，使得在此之上建立的任何数学理论都能在统一而可靠的逻辑框架中展开。

集合论公理是形式系统中对“集合”这一基本对象及其构造方式的根本规定，它们直接界定了集合的存在条件、生成机制与基本运算规则。这些公理不依赖于具体集合的内容，而是规定集合世界的整体框架，使得所有集合构造与推理都在统一的基础上进行。它们的作用不仅在于提供最小化且一致的集合论出发点，还在于确保整个数学体系可以在此之上展开，从而使数学理论具有普遍性、严整性和可扩展性。

类扩展公理是集合论中专门针对类的基本规定，用于保证类这种广义对象能够在形式系统中得到一致的描述。它们共有三条：类定义公理、类等式公理和类属于公理。这三条公理的引入并没有改变ZFC公理系统的公理基础，可以证明他们都是ZFC公理系统的保守扩充，即与原ZFC公理系统是等价的。