查看“︁分类公理”︁的源代码

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

假定 ''P'' 是不含符号 ''B'' 的一个單[[变量]][[谓词]]。在 Zermelo-Fraenkel 公理的[[形式语言]]中，这个公理模式读做：

:<math>\forall A, \exist B, \forall x: x \in B \iff x \in A \land P(x)</math>

换句话说：
: [[全称量化|给定任何]][[集合 (数学)|集合]] ''A''，[[存在量化|有着]]一个集合 ''B''，使得给定任何集合 ''x''，有 ''x'' 是 ''B'' 的成员[[当且仅当]] ''x'' 是 ''A'' 的成员[[逻辑合取|并且]] ''P'' 对于 ''x'' 成立。注意对于所有这种谓词 ''P'' 都有一个公理，所以这是个[[公理模式]]。

要理解这个公理模式，注意集合 ''B'' 必须是 ''A'' 的[[子集]]。所以，这个公理模式实际上说的是，给定集合 ''A'' 和谓词 ''P''，我们可以找到 ''A'' 的子集 ''B''，它的成员正是那些满足 ''P'' 的 ''A'' 的成员。通过[[外延公理]]可知这个集合是唯一的。我们通常使用[[集合建構式符号]]把它指示为 {''x''∈''A'' : ''P''(''x'')}。所以这个公理的本质是：
: 一个通过一个谓词定义的集合的任何[[子类]]自身是一个集合。

分类公理模式是与 [[策梅洛-弗蘭克爾集合論|ZFC 集合论]]有关的公理集合論系統的特征，但在根本上不同的[[可替代的集合论]]系统中通常不出现。例如，[[新基礎集合論]]和[[正集合论]]使用对[[朴素集合论]]的[[概括公理#無限制概括|概括公理]]的不同的限制。Vopenka 的[[可替代的集合论]]有一个特殊要点，它允许集合的真子类的存在，這樣的[[真類]]叫做[[半集合]]。即使在与 ZFC 有关的系统中，这个公理模式有时也限制于带有{{link-en|有界量词|Bounded quantifier}}的公式，比如在{{Link-en|KPU|Kripke–Platek set theory with urelements}}中。

== 与替代公理模式的关系 ==
分离公理模式几乎可以單从[[替代公理|替代公理模式]]推导出来。

首先，替代公理模式读做：

:<math>\forall A, \exist B, \forall y: y \in B \iff \exist x: x \in A \land y = F(x)</math>

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

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

== 无限制概括 ==
无限制的概括公理读做：

:<math>\exist A, \forall x, x \isin A \harr P \left(x\right)</math>

就是说：
: 存在着一个集合 ''A''，它的成员正是满足谓词 ''P'' 的那些对象。同樣地，集合 ''A'' 也是唯一的，并通常指示为 {''x'' : ''P''(''x'')}。

在采纳严格公理化之前，这个公理模式默认的用在早年的[[朴素集合论]]中。不幸的是，若然把''P''(''x'')替換成(''x''∉''x'')，它就直接导致了[[罗素悖论]]。所以，有用的集合论的公理化都不能包括无限制概括，至少不跟[[经典逻辑]]一同被使用。

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

== 在 NBG 类理论中 ==
在[[冯诺伊曼-博内斯-哥德尔集合论|von Neumann-Bernays-Gödel 集合论]]中，對集合和[[类 (数学)|类]]這兩者作出了区分。一个类 ''x'' 是集合，当且仅当它属于某个类 ''B''。在这个理论中，有一个[[定理]]模式读做：

:<math>\exist A: \forall x, x \isin A \harr \left(P\left(x\right) \land \exist B, x \isin B \right)</math>

定义了 <math> Set(x) \leftrightarrow \exist A, x \in A</math> 之后，它可以简写为
:<math>\exist A: \forall x, x \isin A \harr \left(P\left(x\right) \land Set(x) \right)</math>

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

:<math>\forall A, \forall x, \left(\exist B, x \isin B\right) \rarr \exist y, \left(\exist B, y \isin B \right) \land \forall z, z \isin y \harr \left(z \isin x \land z \isin A \right)</math>

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

定义了 <math> \forall x,x \in A \cap B \leftrightarrow  x \in A \land x \in B</math> 之后，它可以简写为：
:<math>\forall A, \forall x, Set(x) \rarr \exist y, Set(y) \land y= x \cap A</math>

就是的说：
: 类 ''A'' 和集合 ''x'' 的[[交集]]是一个集合 ''y''。
在这个公理中，谓词 ''P'' 被替代为可量化在其上的类 ''A''。

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

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

==參考文獻==
{{refbegin}}
*Paul Halmos, ''Naive set theory''. Princeton, NJ: D. Van Nostrand Company, 1960. Reprinted by Springer-Verlag, New York, 1974. ISBN 0-387-90092-6 (Springer-Verlag edition).
*Jech, Thomas, 2003. ''Set Theory: The Third Millennium Edition, Revised and Expanded''.  Springer.  ISBN 3-540-44085-2.
*Kunen, Kenneth, 1980. ''Set Theory: An Introduction to Independence Proofs''. Elsevier.  ISBN 0-444-86839-9.
{{refend}}

[[Category:集合论公理]]

{{集合论}}