分类公理
在公理化集合论和使用它的逻辑、数学和计算机科学分支中,分类公理模式、或分离公理模式、或受限概括公理模式是 Zermelo-Fraenkel 集合论中的一个公理模式。它也叫做概括公理模式,尽管这个术语也用于下面讨论的无限制概括
假定 P 是不含符号 B 的一个单变量谓词。在 Zermelo-Fraenkel 公理的形式语言中,这个公理模式读做:
换句话说:
要理解这个公理模式,注意集合 B 必须是 A 的子集。所以,这个公理模式实际上说的是,给定集合 A 和谓词 P,我们可以找到 A 的子集 B,它的成员正是那些满足 P 的 A 的成员。通过外延公理可知这个集合是唯一的。我们通常使用集合建构式符号把它指示为 {x∈A : P(x)}。所以这个公理的本质是:
- 一个通过一个谓词定义的集合的任何子类自身是一个集合。
分类公理模式是与 ZFC 集合论有关的公理集合论系统的特征,但在根本上不同的可替代的集合论系统中通常不出现。例如,新基础集合论和正集合论使用对朴素集合论的概括公理的不同的限制。Vopenka 的可替代的集合论有一个特殊要点,它允许集合的真子类的存在,这样的真类叫做半集合。即使在与 ZFC 有关的系统中,这个公理模式有时也限制于带有有界量词的公式,比如在KPU中。
与替代公理模式的关系
分离公理模式几乎可以单从替代公理模式推导出来。
首先,替代公理模式读做:
其中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 公理列表中省略。但是出于历史的考虑,和同下面章节中的集合论的可替代的公理化的比较,它仍是重要的。
无限制概括
无限制的概括公理读做:
就是说:
- 存在着一个集合 A,它的成员正是满足谓词 P 的那些对象。同样地,集合 A 也是唯一的,并通常指示为 {x : P(x)}。
在采纳严格公理化之前,这个公理模式默认的用在早年的朴素集合论中。不幸的是,若然把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) 是允许的,我们可以形成所有集合的集合。详情请参见层化。
参考文献
- 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.