分類公理
在公理化集合論和使用它的邏輯、數學和計算機科學分支中,分類公理模式、或分離公理模式、或受限概括公理模式是 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.