替换公理模式
断言集合在映射下的象是集合的公理
条目
替换公理模式（英文：axiom schema of replacement），亦称替换公理、置换公理。它指出：对于任何集合X与任何公式A(u,v)确定的映射f，映射的象f(X)是一个确定的集合。由于公式有无穷多个，每个公式都确定一条公理，因此，替换公理实质上是一个公理模式。[1]
19世纪70年代，德国数学家康托尔（Cantor）发表了有关集合元素等概念的一系列论文，奠定了集合论的理论基础，但是也有一些缺陷，这些缺陷推动了公理集合论的诞生。[6][7]1908年，策梅洛（Zermelo）为集合论建立了第一个比较完整的公理系统，但仍存在一些需修正的问题。1917年，日内瓦的米里马诺夫（Mirimanov）研究了无穷递降的 序列，并提出了替换公理的雏形。后来，弗兰克尔（Fraenkel）和斯科伦（Skolem）在该系统的基础上，于1922年前后提出替换公理模式。基于弗兰克尔、斯科伦等人的工作，策梅洛于1930年将替换公理模式及基础公理加入系统，形成了应用较为广泛的ZF公理系统。[2][3][4]
替换公理模式具有多种等价形式，如若
是一个映射，则对任何集合
,
是一个集合等。[1]应用该公理模式，可以推导得出良序集相关的定理，从而帮助定义序型的概念。[5][8]ZF公理系统还包括一些其他公理，它们不是孤立存在的，其中，替换公理模式可以直接推出子集公理与空集公理，与幂集公理相结合可推出对集公理。此外，其他公理系统也存在替换公理模式，如ZB公理系统中，模糊替换公理模式可看成是替换两次的公理。[1][9]
定义
替换公理模式断言：对于给定公式
，并且对任意
，都有唯一的
，使得成立。那么，对任意集合，集合
存在，该公理形式化可表示为：
。[10]