替代公理

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

应用例子

序数 ω·2 = ω + ω（使用冯·诺伊曼的现代定义）是第一个不使用替代公理就不能构造的序数。无穷公理断言无限序列ω = {0, 1 ,2 ,...} 的存在，也只断言了这个序列。我们希望定义ω·2 为序列{ω, ω + 1, ω + 2,...}，但是一般的序数的类不一定是集合（例如，所有序数的类不是集合）。替代公理允许你把在ω 中每个有限数n 替代为对应的ω + n，并保证替代所得的类是集合。注意你可以轻易地构造序同构于 ω·2 的良序集合而不需用到替代公理：取 ω 的两个复件的不交并，然后设第二个复件大于第一个便可。但这样所得的集合并不是一个序数，因为它在属于关系下不是一个全序。
显然，若要确保可以指派一个序数给任意的良序集合，也要用到替代公理。类似的，若要确保可以指派一个基数给任意集合（冯·诺伊曼基数指派），我们也需要替代公理，以及选择公理。
所有的可数的极限序数的构造也要求替代公理，就像ω·2 的构造那样。较大的序数则不那么直接地依赖于替代公理。例如 ω₁ 是第一个不可数序数，可以构造如下：由全体可数良序组成的集合，会是℘(N×N) 的一个子集，这点通过分离公理和幂集公理可知（在 A 上的关系是 A×A 的一个子集，因此是幂集 ℘(A×A) 的一个元素。关系的集合因此是℘(A×A) 的子集）。把每个良序集合替代为它的序数。这是可数序数ω₁ 的集合，它自身可以被证明是不可数的。这个构造使用了替代公理两次；第一次确保对每个良序集合的一个序数指派，第二次把良序集合替代为其对应的序数。这是Hartogs 数的结果的特殊情况，而一般情况可以类似的证明。
不带替代公理的选择公理（ZC 集合论）不足以强到证明博雷尔集是确定的；为此你需要替代公理。

历史和哲学

多数可以应用替代公理的应用实际上不需要它。例如，假设 f 是从集合S 到集合T 的函数。接着我们可以构造一个泛函谓词F 使得在x 是 S 的成员的时候有F(x) = f(x)，在其他时候随意设F(x) 为某个对象（这里的指派方式不要紧）。然后，给定S 的一个子集 A，应用替代公理模式于F，构造子集A 在函数f 下的像 f(A) 为 （或表示为F(A)）。但是这里实际上不需要替代公理，因为 f(A) 是 T 的子集，所以我们可以使用分类公理模式来构造这个像为集合。一般的说，当 F 在 A 的成员上的值都属于某个预先构造的集合T 时，使用分类公理就足够了；只在不能获得这样的T 的时候，才需要替代公理，比如定义在真类的子集上的运算。
按某些哲学家的说法，在上述例子中最好应用分类公理于集合T，因为分类公理在逻辑上弱于替代公理。实际上，在普通数学中不需要替代公理，只是需要它作为特定公理化集合论的特征。例如，你需要替代公理来从ω·2 向上构造冯·诺伊曼序数，而冯·诺伊曼序数对特定集合论的结果是必需的。在良序集合的理论就足够应用的情况下，你不需要用替代公理构造这些序数。对于某些钻研数学基础的数学家，特别是那些专注于类型论而非集合论的人，他们或认为这个公理在各种意义上都是不需要的，因此在其工作中不包括这个公理（以及其相对应的类型论版本）。通常在基于拓扑斯 理论建造的基础理论上，都难以表达出替代公理，所以一般不包括它。然而，替代公理的争论不在于有人认为它的推论必然是假的（如选择公理的争论）；只是有部分人认为它是没有必要的。
替代公理模式不是恩斯特·策梅洛 在 1908年所公理化的集合论（Z）的一部分；它由亚伯拉罕·弗兰克尔 在 1922 年引入，从而得到了现代的Zermelo-Fraenkel 集合论(ZF)。陶拉尔夫·斯科伦 在同一年晚些时候独立的发现了这个公理，实际上我们今天使用的公理列表是Skolem的最终版本-- 通常不提及他的贡献是因为每个单独的公理都是Zermelo 或 Fraenkel 早先发现的。从证明论的观点看，增加替代公理形成了很大的差异；把这个公理模式加进Zermelo 公理使系统在逻辑上更强，允许你证明更多的陈述。特别是，在ZF 中你可以通过构造冯·诺伊曼全集 Vω2 为模型，证明 Z 的相容性。（当然，哥德尔第二不完备定理表明这两个理论都不能证明自身的相容性，如果它自身是相容的。）