分类公理

维基百科，自由的百科全书

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

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

$\forall A, \exist B, \forall x: x \in B \iff x \in A \and P(x)$

换句话说:

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

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

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

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

[编辑] 无限制概括

无限制的概括公理读做:

$\exist A, \forall x, x \isin A \harr P \left(x\right)$

就是说:

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

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

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

[编辑] 在 NBG 类理论中

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

$\exist A: \forall x, x \isin A \harr \left(P\left(x\right) \and \exist B, x \isin B \right)$

定义了 $Set(x) \leftrightarrow \exist A, x \in A$ 之后，它可以简写为

$\exist A: \forall x, x \isin A \harr \left(P\left(x\right) \and Set(x) \right)$

就是说:

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

$\forall A, \forall x, \left(\exist B, x \isin B\right) \rarr \exist y, \left(\exist B, y \isin B \right) \and \forall z, z \isin y \harr \left(z \isin x \and z \isin A \right)$

就是说:

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

定义了 $\forall x,x \in A \cap B \leftrightarrow x \in A \land x \in B$ 之后，它可以简写为：

$\forall A, \forall x, Set(x) \rarr \exist y, Set(y) \and y= x \cap A$

就是的说:

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

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

[编辑] 在二阶逻辑中

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

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

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

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

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

首先回想替代公理模式:

$\forall A, \exist B, \forall y: y \in B \iff \exist x: x \in A \and y = F(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 是个空集，所以分离公理从替代公理和空集公理共同得出。