分类公理

在公理化集合论和使用它的逻辑、数学和计算机科学分支中，分类公理模式、或分离公理模式、或受限概括公理模式是 Zermelo-Fraenkel 集合论中的一个公理模式。它也叫做概括公理模式，尽管这个术语也用于下面讨论的无限制概括。

假定 P 是不使用符号 B 的任何一个变量的谓词。在 Zermelo-Fraenkel 公理的形式语言中，这个公理模式读做:

换句话说:

给定任何集合 A，有着一个集合 B，使得给定任何集合 x，有 x 是 B 的成员当且仅当 x 是 A 的成员并且 P 对于 x 成立。注意对于所有这种谓词 P 都有一个公理，所以这是个公理模式。

要理解这个公理模式，注意集合 B 必须是 A 的子集。所以，这个公理模式实际上说的是，给定集合 A 和谓词 P，我们可以找到 A 的子集 B，它的成员完全是满足 P 的 A 的成员。通过外延公理这个集合是唯一的。我们通常使用集合建造符号把它指示为 。所以这个公理的本质是:

一个集合的通过一个谓词定义的所有子类自身是一个集合。

分类公理模式是与平常的 ZFC 集合论有关的系统的特征，而在根本上不同的可替代的集合论系统中通常不出现。例如，新基础和正集合论使用对朴素集合论的概括公理的不同的限制。Vopenka 的可替代的集合论有一个特殊要点，它允许集合的真子类，叫做半集合。即使在与 ZFC 有关的系统中，这个公理模式有时也限制于带有有界量词的公式，比如在 KPU 中。

[编辑] 无限制概括

无限制的概括公理读做:

就是说:

存在着一个集合 A，它的成员完全是满足谓词 P 的那些对象。集合 A 再次是唯一的，并通常指示为 。

在采纳严格公理化之前，这个公理模式默认的用在早年的朴素集合论中。不幸的是，通过采用 P(x) 为(x x)，它直接导致了罗素悖论。所以，有用的集合论的公理化不使用无限制概括，至少不同经典逻辑一起使用。

只接受分类公理模式是公理化集合论的开端。多数其他 Zermelo-Fraenkel 公理(不包括外延公理或正规公理)对充当对概括公理模式的额外替代是必须的；每个这些公理都声称一个特定集合存在，并通过给出它的成员必须满足的谓词来定义这个集合。

[编辑] 在 NBG 类理论中

在von Neumann-Bernays-Gödel 集合论中，在集合和类之间作出区分。一个类 x 是集合，当且仅当它属于某个类 B。在这个理论中，有一个定理模式读做:

定义了 之后，它可以简写为

就是说:

有一个类 A 使得任何类 x 是 A 的成员，当且仅当 x 是满足 P 的一个集合。这个定理模式自身是受限的概括，避免了罗素悖论，因为它要求 x 是一个集合。接着把集合自身的分类写为单一的公理:

就是说:

给定任何类 A 和任何集合 x，有一个集合 y，它的成员完全是 x 和 A 二者共有的成员；

定义了 之后，它可以简写为：

就是的说:

类 A 和集合 x 的交集自身是一个集合 y。

在这个公理中，谓词 P 被替代为可量化在其上的类 A。

[编辑] 在二阶逻辑中

在二阶逻辑中，我们可以量化于谓词，而概括公理模式成为简单的公理。这使用了同前面章节 NBG 公理一样的技巧，把谓词替代为一个类并接着量化于其上。

[编辑] 在蒯因的新基础中

在蒯因所开创的新基础集合论中，给定谓词的概括公理采用无限制形式，但是对可以用于这个模式的谓词自身是有限制的。谓词 (x x) 是禁止的，因为同一个符号 x 出现在成员关系符号的两端(因而有不同"相对类型")；因此避免了罗素悖论。 但是，采用 P(x) 为 (x = x) 是允许的，我们可以形成所有集合的集合。详情请参见层化。

[编辑] 与替代公理模式的关系

分离公理模式几乎可以从替代公理模式推导出来。

首先回想替代公理模式:

对于不使用符号 A, B, x 或 y 的任何一个变量的泛函谓词 F。给定适合分类公理的一个谓词 P，定义映射 F 为：F(x) = x 如果 P(x) 为真，F(x) = z 如果 P(x) 为假，这里的 z 是 A 的使 P(z) 为真的任何成员。那么替代公理所保证的集合 B 完全就是分类公理所要求的集合 B。唯一的问题是这样的 z 有可能不存在。但是在这种情况下，分离公理所要求的集合 B 是个空集，所以分离公理从替代公理和空集公理共同得出。

为此，分离公理模式经常从现代 Zermelo-Fraenkel 公理列表中省略。但是出于历史的考虑，和同下面章节中的集合论的可替代的公理化的比较，它仍是重要的。