策梅洛-弗兰克尔集合论

策梅洛-弗兰克尔集合论（），是数学基础中最常用的一階公理化集合论。含选择公理時常简写为ZFC，不含選擇公理的則簡寫為ZF。它是二十世纪早期为了建构一个不会导致类似罗素悖论的矛盾的集合理论所提出的一个公理系统。

介绍
ZFC旨在构建自一个单一的基本本体论概念集合，和一个单一的本体论假定，就是在论域中所有的个体（就是所有数学对象）都是集合。有一个单一的基本二元关系集合成员关系；集合a是集合b的成员写为a\in b（通常读做"a是b的元素"）。ZFC是一阶理论，所以ZFC包括后台逻辑是一阶逻辑的公理。这些公理支配了集合的行为和交互。ZFC是标准形式的公理化集合论。使用ZFC的大量的正在进行中的普通数学推导请参见[http://us.metamath.org/ Metamath] 在线计划。

在1908年，恩斯特·策梅洛提出了第一个公理化集合论，即策梅洛集合论。然而，这个公理系统无法构建出序数的集合；而序数是许多集合论研究的根本工具。此外，Zermelo的分类公理中使用了被称作“明确性”的性质，而它的实际意义是有歧义的（此时一阶逻辑的概念还未被提出）。在1922年，亞伯拉罕·弗蘭克爾和独立的提议了定义“明确性”为可以在一阶逻辑中公式化并原子公式仅包括集合的公式。他们还同时提出应该用替代公理取代分类公理，并在体系中添加正规公理（首先由 冯诺依曼提出），从而得到了被称作 ZF的公理体系。

再向ZF增加选择公理就诞生了ZFC。选择公理曾饱受争议，因为选择函数的存在性是非构造性的；选择公理确立了选择函数的存在，而不说明如何构造这些函数。所以使用选择公理构造的一些集合，尽管可以证明其存在，但可能无法详细、描述性地构造出。因此，当一个结论依赖于选择公理时，有时会被明确地指出。

ZFC一般由一阶逻辑写出，实际上包含了无穷多个公理，因为替代公理实际上是公理模式。理查德·蒙塔古证明了ZFC和ZF集合论二者都不能用有限个公理来公理化。在另一方面，冯诺伊曼-博内斯-哥德尔集合论（Von Neumann–Bernays–Gödel, NBG）可以被有限公理化。NBG的对象同时包括集合和类；类是有含有元素但不在其他任何类中的实体。NBG和ZFC事实上是等价的，即所有不以任何方式提及类的定理在两个公理体系中同时可以证明或同时不能证明。

依据哥德尔第二不完备定理，ZFC的一致性不能在ZFC之内证明。ZFC的延展包括了通常意义上的大部分数学，所以ZFC的相容性不能在其他数学分支中证明。ZFC的相容性可从弱不可达基数的存在(独立于ZFC)而得出。几乎没有人怀疑ZFC有什么矛盾；通常认为，如果ZFC事实上不自洽，那相应的例子早就应该被发现了。可以肯定的是，ZFC避开了朴素集合论的三大悖论，罗素悖论、布拉利-福尔蒂悖论和康托尔悖论。

文献中讨论过的ZFC的缺陷包括：
*它比几乎所有普通数学所要求的程度还要强（桑德斯·麦克莱恩和所罗门·费弗曼这么认为）；
*相对于其他集合论的公理化，ZFC相对要弱。例如，它不允许全集合（如新基础）或类（如NBG）的存在；
*桑德斯·麦克莱恩（范畴论的缔造者之一）和其他人争论说任何公理化集合论对于实际上的数学工作方式而言都是不正当的。依据他的观点，数学不是关于抽象对象的搜集和它们的性质的学科，而是关于结构和结构保持的映射的学科。

基本符號
ZFC有許多等價的形式。下列的公理是由丘嫩於1980年提出。公理本身以一階邏輯來敘述。

本條目定理的證明會頻繁引用一阶逻辑的定理，定理的代號可以參見常用的推理性質一節。

以下把 \vdash_{ZFC} 和 \vdash_{ZF} 都簡寫為 \vdash，除了強調使用選擇公理的情況。

斷言符號
在**'下，「属于關係」以一個雙元斷言符號 P(x,\,y) 來表示， P(x,\,y) 通常簡記為 x \in y ，並被直觀理解成「x属于y」；類似地， P(x,\,y) 的否定 \neg P(x,\,y) 通稱被簡記為 x \notin y ，並被直觀理解為「x不属于y」。

另外，丘嫩的'系統以一個雙元斷言符號 Q(x,\,y) 來表示「相等關係」（通常簡記為 x = y ），且 x = y 被預先的假設為'理論裡的相等符號，換句話說，對於 x = y 有以下的隱含公理：{{math theorem
| math_statement =

*（E1） 對任意變數 x，(\forall x)(x=x) 為公理。
*（E2） 對於任意變數 x 和 y，若在公式 \mathcal{A} 中自由的 x 都不在 \forall y 的範圍內。若以 \mathcal{A}_y 代表 \mathcal{A} 某些（而非全部）自由的 x 被取代成 y 而成的新公式，則
::(\forall x)(\forall y)[(x=y)\Rightarrow(\mathcal{A}\Rightarrow\mathcal{A}_y)]
:為公理。
| name = 等號公理
}}習慣上會把 \neg(x = y) 簡記成 (x \neq y)。

包含
但'所談及的一切對象為「集合」，直觀上「x包含於y」意為「所有x的元素a都會屬於y」，以此為動機，'有以下的符號簡寫

: x \subseteq y := \forall a[\,
(a \in x)
\Rightarrow
(a \in y)
\,]

以上可稱為「x包含於y」，也可稱為「x是y的子集（'）」。注意到 a 須為展開這個簡寫時首次出現**的變數，才能避免與其他變數混淆。

外延公理
{{math theorem
| math_statement =

(\forall x) (\forall y) \{(\forall z)[(z \in x) \Leftrightarrow (z \in y)] \Rightarrow (x = y)\}

| name = (ext)Axiom of extensionality
}}

目前'內沒有任何函數符號，而且一開始就假設 x = y 為'理論裡的相等符號，所以依據一阶逻辑的等式定理一節應有：
:\vdash
(x = y)\Rightarrow [(z \in x) \Rightarrow (z \in y)]

:\vdash
(y = x)\Rightarrow [(z \in y) \Rightarrow (z \in x)]

:\vdash
(x = y)\Rightarrow (y = x)

這樣結合(AND)和演繹元定理就有：
:\vdash
(x = y)\Rightarrow [(z \in x) \Leftrightarrow (z \in y)]

對上式使用(GEN)有：
:\vdash
(\forall z)\{
(x = y)
\Rightarrow
[(z \in x) \Leftrightarrow (z \in y)]
\}

再結合量词公理(A5)就有：
:\vdash
(x = y)
\Rightarrow
(\forall z)\{
[(z \in x) \Leftrightarrow (z \in y)]
\}

注意對外延公理(ext)使用兩次量词公理(A4)會有：
:\vdash
(\forall z)\{
[(z \in x) \Leftrightarrow (z \in y)]
\}
\Rightarrow
(x = y)

這樣結合(AND)就有：
:\vdash
(x = y)\Leftrightarrow (\forall z)[(z \in x) \Leftrightarrow (z \in y)]

也就是外延公理(ext)搭配等號公理，可以推出「兩個集合相等，若它們有相同的元素。」

視相等符號為公式
除了一開始就假設 x=y 為**'的相等符號，也可以一開始做如下的符號定義，將x = y 定義為以下合式公式的簡寫：
:(x = y)
:=
(\forall z)[(z \in x) \Leftrightarrow (z \in y)]
\land
(\forall z)[(x \in z) \Leftrightarrow (y \in z)]
:（z 須為展開這個簡寫時首次出現的變數）
直觀上，這個符號定義表示「兩個集合相等，若它們有相同的元素；且它們會屬於同個集合」
如此一來，就不需要外延公理，也可以確保 x = y 為**'理論裡的相等符號：

但採用這個符號定義的'與丘嫩的'是兩套不等效的理論，因為在丘嫩的**'裡沒有以下的定理：
: \vdash
[(x \in z) \Leftrightarrow (y \in z)] \Rightarrow (x = y)

真子集
在定義「相等」以後，可以把「相等的集合」排除出子集的定義中，換句話說，**'有以下的符號定義

: x\subset y
:=
(x \subseteq y)
\wedge
(x \neq y)

可直觀理解為「x是y的真子集（**'）」。

正規公理
{{math theorem
| math_statement =

(\forall x)\bigg\{
(\exists a)( a \in x)
\Rightarrow
(\exists y)\Big\{
(y \in x)
\land
\{\lnot (\exists z)[
(z \in y)
\land
(z \in x)
]\}
\Big\}
\bigg\}

| name = (reg)Axiom of regularity / Axiom of foundation
}}

「每個非空集合x都包含一個成員y，使得x和y*不相交。」

替代公理
(Axiom schema of replacement)

令\phi \!是ZFC語言內的任意公式，其自由變數有x,y,A,w_1,\ldots,w_n \!，但B在\phi \!　則不是自由的。則：

:\forall A\forall w_1,\ldots,w_n \bigl[ \forall x ( x\in A \Rightarrow \exists!y\,\phi ) \Rightarrow \exists B \forall x \bigl(x\in A \Rightarrow \exists y (y\in B \land \phi)\bigr)\bigr]。
「若一個可定義的函數f的定義域為一集合，且對定義域的任一x，f(x)也都是集合，則f的值域會是一個集合的子集。」這個限制被需要用來避免一些悖論。

分類公理
{{math theorem
| math_statement =

若變數 s 於公式 \mathcal{P} 完全被約束，則對任意不是 s 的變數 x 與 a ：
:
(\forall x)(\exists s)(\forall a)\{
(a \in S)
\Leftrightarrow
[(a \in x) \land \mathcal{P}]
\}

都是公理。
| name = (compr)Axiom Schema of Comprehension
}}

「對每個集合 x 和任意不含變數 s 的公式 \mathcal{P} ，都有某 x 的子集合 s ，裡面的成員都滿足 \mathcal{P} 」

分類公理事實上是以集合建構式符號為動機。構成的集合通常使用來標記。給定一集合z和具有一自由變數x的公式\phi(x)\!，則由所有在z內，滿足\phi\!的x所組成的集合，標記為
:\{x \in z : \phi(x)\}。

分類公理可以用來證明空集（標記為\varnothing）的存在，只要至少已存在一個集合。通常的方法是找一個所有集合都沒有的性質。例如，設w是一個已存在的集合，而空集可定義為
:\varnothing = \{u \in w \mid (u \in u) \land \lnot (u \in u) \}.
若背景邏輯包含等式，也可定義空集為
:\varnothing = \{u \in w \mid \lnot (u = u) \}.
因此，空集公理可由此處的九個公理中導出。外延公理還可證明空集是唯一的（不依賴w）。通常會以定義性擴展，將符號\varnothing加至ZFC語言中。

分類元定理
分類公理也可以由替代公理和空集公理中導出，而視為一條元定理：

配對公理
(Axiom of pairing)

若x和y是集合，則存在一個集合包含x和y。
:\forall x \forall y \exist z (x \in z \land y \in z)。
這個公理是Z的一部份，但在ZF中就顯得多餘，因為它可以由將替代公理應用至任意有兩個成員的集合上導出。此類集合的存在性可由將無窮公理或冪集公理應用兩次至空集上得到。

聯集公理
(Axiom of union)

對任一個集合\mathcal{F}，總存在一個集合A，包含每個為\mathcal{F}的某個成員的成員的集合。
:\forall \mathcal{F} \,\exists A \, \forall Y\, \forall x [(x \in Y \land Y \in \mathcal{F}) \Rightarrow x \in A]。

無窮公理
(Axiom of infinity)

令S(x)\!為 x \cup \{x\} \!，其中 x \!為某個集合，則存在一個集合X，使得空集\varnothing為X的成員，且當一個集合y為X的成員時，S(y)\!也會是X的成員。
:\exist X \left [\varnothing \in X \land \forall y (y \in X \Rightarrow S(y) \in X)\right ]。
較口語地說，存在一個有無限多成員的集合X。滿足無窮公理的最小集合X為馮諾伊曼序數\omega，這個序數也可想成是自然數的集合\mathbb{N}。

冪集公理
(Axiom of power set)

令z \subseteq x為\forall q (q \in z \Rightarrow q \in x)。對任一個集合x，皆存在一個集合y，為x的冪集的父集。x的冪集為一個其成員為所有x的子集的類。
:\forall x \exists y \forall z [z \subseteq x \Rightarrow z \in y]。

良序定理
(Well-ordering theorem)

對任一集合X，總存在一個可良好排序X的二元關係R。這意指著，R是X上的全序關係，且X內每個非空子集在R下都有一個最小元素。
:\forall X \exists R ( R \;\mbox{well-orders}\; X)。

若給定前八個公理，就可以找到許多個和第九個公理等價的敘述，最著名的則為選擇公理，其敘述如下：令X為一非空集合，則存在一從X映射至X內成員的聯集的函數（稱為「選擇函數」），可使得對所有的Y \in X都會有f(Y) \in Y。因為當X為有限集合時，選擇函數的存在性很容易由前八個公理中證出，所以選擇公理只在無限集合中有意義。選擇公理被認為是非結構的，因為它只聲明一個選擇集合的存在，但完全不講這個選擇集合是如何被「建構」出來的。

参见

• 康托尔定理
• 公理化集合论
• 策梅洛集合论
• 新基础集合论
• ZFC系統無法確定的命題列表

參考資料
文献
亞歷山大·阿比安, 1965. The Theory of Sets and Transfinite Arithmetic*. W B Saunders.
Keith Devlin, 1996 (1984). The Joy of Sets*. Springer.
Abraham Fraenkel, Yehoshua Bar-Hillel, and Levy, Azriel, 1973 (1958). Foundations of Set Theory*. North Holland.
Hatcher, William, 1982 (1968). The Logical Foundations of Mathematics*. Pergamon.
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.
Suppes, Patrick, 1972 (1960). Axiomatic Set Theory*. Dover.
Tourlakis, George, 2003. Lectures in Logic and Set Theory, Vol. 2*. Cambridge Univ. Press.
Jean van Heijenoort, 1967. From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931*. Harvard Univ. Press. Includes annotated English translations of the classic articles by Zermelo, Frankel, and Skolem bearing on ZFC.

外部链接

• [http://us.metamath.org/ Metamath.] An online project building a great deal of mathematics from first-order logic and ZFC. Principia Mathematica done right.
• Stanford Encyclopedia of Philosophy: [http://plato.stanford.edu/entries/set-theory/ Set Theory] —by Thomas Jech.