查看“替代公理”的源代码

在[[公理化集合论]]和使用它的[[逻辑]]、[[数学]]和[[计算机科学]]分支中，'''替代公理模式'''是 [[Zermelo-Fraenkel 集合论]]的一个[[公理模式]]，它本质上断言一个[[集合]]在一个[[泛函谓词|映射]]（泛函谓词）下的[[像]]也是一个集合。它对于构造特定的大集合是必需的。

== 陈述 ==
假定 ''P'' 是一个雙[[变量]][[谓词]]，对于任何集合 ''x'' 有一个唯一的集合 ''y'' 使 ''P''(''x'',''y'') 成立。接着我们可以形成一个單变量的[[泛函谓词]] ''F''，使得 ''F''(''x'') = ''y'' [[当且仅当]] ''P''(''x'',''y'')。

替代公理声称，给定一个集合 ''A''，我们可以找到一个集合 ''B''，它的成员完全是 ''F'' 在 ''A'' 的成员上的值。注意对于每个这樣的谓词 ''P'' 都有一个相對應的公理；所以，这是一个[[公理模式]]。

在 Zermelo-Fraenkel 公理的[[形式语言]]中，这个公理模式读做：
:<math>(\forall x, \exist!\, y: P(x, y)) \rightarrow \forall A, \exist B, \forall y: y \in B \iff \exist x \in A : P(x, y)</math>
换句话说，
: [[实质条件|如果]][[全称量化|给定任何]][[集合]] ''x''，[[唯一量化|有一个唯一的]]集合 ''y'' 使得 ''P'' 对 ''x'' 和 ''y'' 成立，那么给定任何集合 ''A''，[[存在量化|有着]]一个集合 ''B'' 使得，给定任何集合 ''y''，''y'' 是 ''B'' 的一个成员，[[当且仅当]]有是 ''A'' 的成员的一个集合 ''x'' 使得 ''P'' 对于 ''x'' 和 ''y'' 成立。

如果允许在公理模式中使用导出的泛函谓词，则这个公理模式可以写为：
:<math>\forall A, \exist B, \forall y: y \in B \iff \exist x \in A : y = F(x)</math>
对于每个导出的單变量的泛函谓词 ''F''；
换句话说：
: 给定任何集合 ''A''，有一个集合 ''B'' 使得，给定任何集合 ''y''，''y'' 是 ''B'' 的成员，当且仅当有是 ''A'' 的成员的一个集合 ''x'' 使得 ''y'' [[等于]] ''F'' 在 ''x'' 上的值。

通過[[外延公理]]可知这个集合 ''B'' 是唯一的。我们称这个集合 ''B'' 为 ''A'' 在 ''F'' 下的[[像]]，并指示它为 ''F''(''A'') 或（使用[[集合建構式符号]]形式）{''F''(''x''):''x''∈''A''}。

有时引用这个公理不带唯一性要求：
:<math>\forall A (\forall x \in A, \exist y: P(x, y)) \rightarrow \exist B, \forall x \in A, \exist y \in B: P(x, y)</math>
就是说，谓词 ''P'' 不被限制为泛函的：要应用它于一个集合 ''A''，只需存在至少一个元素 ''y'' 对应于 ''A'' 的每个元素 ''x'' 就可以了；''y'' 对每个 ''x'' 是唯一的不是必需的。在这种情况下，被断言存在的像集合 ''B'' 将为 ''A'' 的每个 ''x'' 包含至少一个这样的 ''y''，不保证只包含唯一的一个。

有时陈述这个公理不对谓词加任何限制：
:<math>\forall A, \exist B, \forall x \in A : ((\exist y : P(x, y)) \rightarrow \exist y \in B : P(x, y))</math>
就是说，根本不要求 ''P'' 把集合 ''A'' 的一个元素映射到任何對象。但是如果对于 ''A'' 的一个元素 ''x'' 有至少一个 ''y'' 对应于它，则像集合 ''B'' 将包含至少一个这样的 ''y''。 

這個不對謂詞作限制的公理，也叫做'''有界公理'''或'''搜集公理'''，看似比原先的替代公理更強，但是这两个版本都可以从替代公理推导出来。另一方面，任何泛函谓词都是谓词，所以有界公理也蕴涵替代公理，因此两个公理是等价的（在給定了其他 Zermelo-Fraenkel 公理的情況下）。

== 应用例子 ==

[[序数]] ω·2 = ω + ω（使用[[約翰·馮·紐曼|冯·诺伊曼]]的现代定义）是第一个不使用替代公理就不能构造的序数。[[无穷公理]]断言无限序列 ω = {0, 1 ,2 ,...} 的存在，也只断言了这个序列。我們希望定义 ω·2 为序列 {ω, ω + 1, ω + 2,...}，但是一般的序数的[[类 (数学)|类]]不一定是集合（例如，所有序数的类不是集合）。替代公理允许你把在 ω 中每个有限数 ''n'' 替代为对应的 ω + ''n''，并保证替代所得的类是集合。注意你可以轻易地构造[[序同構]]于 ω·2 的[[良序集合]]而不需用到替代公理：取 ω 的两个复件的[[不交并]]，然后設第二个复件大于第一个便可。但這樣所得的集合並不是一个序数，因为它在[[屬於關係 (集合論)|屬於關係]]下不是一個[[全序關係|全序]]。

顯然，若要確保可以指派一個序數給任意的[[良序關係|良序集合]]，也要用到替代公理。类似的，若要確保可以指派一個[[基數]]給任意集合（[[冯·诺伊曼基数指派]]），我們也需要替代公理，以及[[选择公理]]。

所有的[[可数集合|可数]]的[[极限序数]]的構造也要求替代公理，就像 ω·2 的构造那樣。較大的序数則不那么直接地依赖于替代公理。例如 ω<sub>1</sub> 是第一个[[不可数集合|不可数]]序数，可以构造如下：由全體可数良序組成的集合，會是 ℘('''N'''×'''N''') 的一個[[子集]]，這點通过[[分类公理|分离公理]]和[[幂集公理]]可知（在 ''A'' 上的[[二元关系|关系]]是 ''A''×''A'' 的一个子集，因此是[[幂集]] ℘(''A''×''A'') 的一个元素。关系的集合因此是 ℘(''A''×''A'') 的子集）。把每个良序集合替代为它的序数。这是可数序数 ω<sub>1</sub> 的集合，它自身可以被证明是不可数的。这个构造使用了替代公理两次；第一次确保对每个良序集合的一个序数指派，第二次把良序集合替代为其對應的序数。这是 {{link-en|Hartogs 数|Hartogs number}}的结果的特殊情况，而一般情况可以类似的证明。

不带替代公理的选择公理（ZC 集合论）不足以强到证明 [[博雷爾集]]是{{link-en|确定公理|Axiom of determinacy|确定}}的；为此你需要替代公理。

== 历史和哲学 ==

多数可以应用替代公理的应用实际上不需要它。例如，假设 ''f'' 是从集合 ''S'' 到集合 ''T'' 的[[函数]]。接着我们可以构造一个泛函谓词 ''F'' 使得在 ''x'' 是 ''S'' 的成员的时候有 ''F''(''x'') = ''f''(''x'')，在其他时候隨意设 ''F''(''x'') 為某個對象（這裡的指派方式不要緊）。然後，给定 ''S'' 的一个[[子集]] ''A''，应用替代公理模式于 ''F''，构造子集 ''A'' 在函数 ''f'' 下的[[像]] ''f''(''A'') 为 <math>\{ F(x) : x \in A \}</math>（或表示为 ''<nowiki>F</nowiki>''(''A'')）。但是这里实际上不需要替代公理，因为 ''f''(''A'') 是 ''T'' 的子集，所以我们可以使用[[分类公理|分类公理模式]]来构造这个像为集合 <math>\{ y \in T : \exists x \in A, y = f(x) \}</math>。一般的说，當 ''F'' 在 ''A'' 的成员上的值都属于某个预先构造的集合 ''T'' 时，使用分类公理就足够了；只在不能获得这样的 ''T'' 的时候，才需要替代公理，比如定义在真类的子集上的[[運算]]。

按某些哲学家的說法，在上述例子中最好应用分类公理于集合 ''T''，因为分类公理在逻辑上弱于替代公理。实际上，在普通数学中不需要替代公理，只是需要它作為特定[[公理化集合论]]的特征。例如，你需要替代公理来从 ω·2 向上构造[[冯·诺伊曼序数]]，而冯·诺伊曼序数对特定集合论的结果是必需的。在[[良序集合]]的理论就足够应用的情況下，你不需要用替代公理构造这些[[序数]]。對於某些鑽研[[数学基础]]的数学家，特别是那些專注於[[类型论]]而非集合論的人，他們或認為这个公理在各種意義上都是不需要的，因此在其工作中不包括这个公理（以及其相對應的类型论版本）。通常在基于 [[拓撲斯]] 理论建造的基础理論上，都難以表达出替代公理，所以一般不包括它。然而，替代公理的争论不在于有人認為它的推论必然是假的（如[[选择公理]]的争论）；只是有部分人認為它是没有必要的。

替代公理模式不是 [[恩斯特·策梅洛]] 在 1908年所公理化的集合论（'''Z'''）的一部分；它由 {{link-en|亞伯拉罕·弗蘭克爾|Abraham Fraenkel}} 在 1922 年引入，從而得到了现代的 Zermelo-Fraenkel 集合论 ('''ZF''')。{{link-en|陶拉爾夫·斯科倫|Thoralf Skolem}} 在同一年晚些时候独立的发现了这个公理，实际上我们今天使用的公理列表是Skolem的最终版本 -- 通常不提及他的贡献是因为每个单独的公理都是 Zermelo 或 Fraenkel 早先发现的。从[[证明论]]的观点看，增加替代公理形成了很大的差异；把这个公理模式加進Zermelo 公理使系统在逻辑上更强，允许你证明更多的陈述。特别是，在'''ZF''' 中你可以通过构造[[冯·诺伊曼全集]] V<sub>&omega;2</sub> 为[[模型论|模型]]，证明 '''Z''' 的[[一致性 (邏輯)|相容性]]。（当然，[[哥德尔不完备定理|哥德尔第二不完备定理]]表明这两个理论都不能证明自身的相容性，如果它自身是相容的。）

== 引用 ==
*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.

[[Category:集合论公理]]

{{集合论}}