无穷公理

在公理化集合论和使用它的逻辑、数学和计算机科学中，无穷公理（）是策梅洛-弗兰克尔集合论的公理之一。

形式陈述
在Zermelo-Fraenkel公理的形式语言中，这个公理读作：
:\exists \mathbf{N}: \varnothing \in \mathbf{N} \land (\forall x: x \in \mathbf{N} \implies x \cup \{x\} \in \mathbf{N})

或用非形式化的語言陳述：存在一个集合\mathbb{N}，使得空集在\mathbb{N}中，并且只要x是\mathbb{N}的成员，则x与它的单元素集合\{x\}此兩者的并集也是\mathbb{N}的成员。这种集合有时也叫做归纳集合。归纳集合是带有如下性质的集合X：对于所有x\in X，x的后继x'也是X的一个元素。

解释
要理解这个公理，首先我们要定义x的后继为x\cup \{x\}。注意配对公理允许我们形成单元素集合\{x\}。
后继是用来定义自然数的常用的集合论编码。在这种编码中，0是空集（0=\varnothing），而1是0的后继：

:1=0\cup\{0\}=\varnothing\cup\{0\}=\{0\}

类似地，2 是1 的后继：
:2=1\cup\{1\}=\{0\}\cup\{1\}=\{0,1\}

如此类推。这个定义的推论是對於任何自然數n，n等同于由它的所有前驱（）組成的集合。

我们希望可以形成包含所有自然数的一個集合，但是只使用其他ZF公理的話並不能做到這一點。因此，有必要加入无穷公理以假定这个集合的存在。它是通过类似于数学归纳法的方法完成的：首先假定有一个集合S包含零，并接着規定对于S的所有元素，这个元素的后继也在S中。

这个集合S可以不只是包含自然数，還包含別的元素。但是我们可以应用分类公理模式来除去不想要的元素，留下所有自然数的集合\mathbb{N}。通过外延公理可知这个集合是唯一的。应用分类（分离）公理的结果是：

\exists \mathbf{N} \forall n (n \in \mathbf{N} \iff ([\forall k \in n(\bot) \lor \exists k \in n( \forall j \in k(j \in n) \land \forall j \in n(j=k \lor j \in k))] \land

\forall m \in n[\forall k \in m(\bot) \lor \exists k \in n(k \in m \land \forall j \in k(j \in m) \land \forall j \in m(j=k \lor j \in k))]))

用非形式化的語言陳述：所有自然数的集合存在；这里的自然数要么是零，要么是一个自然數k的后继，并且k的每个元素要么是0要么是k的另外一个元素的后继。

所以这个公理的本质是：
:有一个集合包含所有的自然数。
无穷公理也是von Neumann-Bernays-Gödel 公理之一。

引用
延伸阅读
Paul Halmos (1960) Naive set theory*. Princeton, NJ: D. Van Nostrand Company. Reprinted 1974 by Springer-Verlag. ISBN 0-387-90092-6.
Thomas Jech (2003) Set Theory: The Third Millennium Edition, Revised and Expanded*. Springer-Verlag. ISBN 3-540-44085-2.
Kenneth Kunen (1980) Set Theory: An Introduction to Independence Proofs*. Elsevier. ISBN 0-444-86839-9.