查看“︁策梅洛-弗兰克尔集合论”︁的源代码

{{NoteTA
|G1 = Math
|1=zh-cn:數學對象;zh-tw:數學物件;
}}
{{redirect|ZFC}}
'''策梅洛-弗兰克尔集合论'''（{{lang-en|Zermelo-Fraenkel Set Theory}}），是[[数学基础]]中最常用的[[一阶逻辑|一階]][[公理化集合论]]。含[[选择公理]]時常简写为'''ZFC'''，不含選擇公理的則簡寫為'''ZF'''。它是二十世纪早期为了建构一个不会导致类似[[罗素悖论]]的矛盾的[[集合论|集合理论]]所提出的一个[[公理系统]]。

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

在1908年，[[恩斯特·策梅洛]]提出了第一个[[公理化集合论]]，即[[策梅洛集合论]]。然而，这个公理系统无法构建出[[序数]]的集合；而序数是许多集合论研究的根本工具。此外，Zermelo的[[分类公理]]中使用了被称作“明确性”的性质，而它的实际意义是有歧义的（此时一阶逻辑的概念还未被提出）。在1922年，[[亞伯拉罕·弗蘭克爾]]和{{link-en|陶拉爾夫·斯科倫|Thoralf Skolem}}独立的提议了定义“明确性”为可以在[[一阶逻辑]]中公式化并[[原子公式]]仅包括集合的公式。他们还同时提出应该用[[替代公理]]取代分类公理，并在体系中添加[[正规公理]]（首先由 [[冯诺依曼]]提出），从而得到了被称作 '''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的缺陷包括：
*它比几乎所有普通数学所要求的程度还要强（[[Saunders MacLane]]和[[所罗门·费弗曼]]这么认为）；
*相对于其他集合论的公理化，ZFC相对要弱。例如，它不允许全集合（如[[新基础]]）或类（如NBG）的存在；
*[[Saunders MacLane]]（[[范畴论]]的缔造者之一）和其他人争论说任何公理化集合论对于实际上的数学工作方式而言都是不正当的。依据他的观点，数学不是关于抽象对象的[[搜集]]和它们的性质的学科，而是关于结构和结构保持的映射的学科。

== 基本符號 ==
ZFC有許多等價的形式<ref name="Fraenkel">對這些等價的公式的一個豐富但有點過時的討論，請見Fraenkel ''et al.'' (1973)</ref>。下列的公理是由[[肯尼思·丘嫩|丘嫩]]於1980年提出<ref>{{Cite book|title=Set Theory An Introduction To Independence Proofs (Studies in Logic and the Foundations of Mathematics, Volume 102)|last=Kunen|first=Kenneth|publisher=North Holland|year=1980|isbn=0444868399}}</ref>。公理本身以[[一階邏輯]]來敘述。

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

以下把 <math>\vdash_{ZFC}</math> 和  <math>\vdash_{ZF}</math> 都簡寫為 <math>\vdash</math>，除了強調使用[[策梅洛-弗兰克尔集合论#選擇公理|選擇公理]]的情況。

=== 斷言符號 ===
在'''{{lang|en|ZF}}'''下，「属于關係」以一個雙元[[一阶逻辑#斷言符號|斷言符號]] <math>P(x,\,y)</math> 來表示， <math>P(x,\,y)</math> 通常簡記為 <math>x \in y</math> ，並被直觀理解成「x属于y」；類似地， <math>P(x,\,y)</math> 的否定 <math>\neg P(x,\,y)</math>  通稱被簡記為 <math>x \notin y</math> ，並被直觀理解為「x不属于y」。

另外，[[肯尼思·丘嫩|丘嫩]]的'''{{lang|en|ZF}}'''系統以一個雙元[[一阶逻辑#斷言符號|斷言符號]] <math>Q(x,\,y)</math> 來表示「[[相等]]關係」（通常簡記為 <math>x = y</math> ），且 <math>x = y</math> 被'''預先的假設'''為'''{{lang|en|ZF}}'''理論裡的[[一阶逻辑#等式定理|相等符號]]，換句話說，對於 <math>x = y</math> 有以下的隱含公理：{{math_theorem
| math_statement = <br/>
*（E1） 對任意變數 <math>x</math>，<math>(\forall x)(x=x)</math> 為公理。
*（E2） 對於任意變數 <math>x</math> 和 <math>y</math>，若在公式 <math>\mathcal{A}</math> 中自由的 <math>x</math> 都不在 <math>\forall y</math> 的範圍內。若以 <math>\mathcal{A}_y</math> 代表 <math>\mathcal{A}</math> 某些（而非全部）自由的 <math>x</math>  被取代成 <math>y</math> 而成的新公式，則
::<math>(\forall x)(\forall y)[(x=y)\Rightarrow(\mathcal{A}\Rightarrow\mathcal{A}_y)]</math> 
:為公理。
| name = 等號公理
}}習慣上會把 <math>\neg(x = y)</math> 簡記成 <math>(x \neq y)</math>。

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

: <math>x \subseteq y := \forall a[\,
(a \in x)
\Rightarrow
(a \in y)
\,]</math>

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

== 外延公理 ==
{{Main|外延公理}}
{{math_theorem
| math_statement = <br/>
<math>
(\forall x) (\forall y) \{(\forall z)[(z \in x) \Leftrightarrow (z \in y)] \Rightarrow (x = y)\}
</math>
| name = (ext)Axiom of extensionality
}}

目前'''{{lang|en|ZF}}'''內沒有任何[[一阶逻辑#函數符號|函數符號]]，而且一開始就假設 <math>x = y</math> 為'''{{lang|en|ZF}}'''理論裡的[[一阶逻辑#等式定理|相等符號]]，所以依據[[一阶逻辑#等式定理|一阶逻辑的等式定理一節]]應有：
:<math>\vdash
(x = y)\Rightarrow [(z \in x) \Rightarrow (z \in y)]
</math>
:<math>\vdash
(y = x)\Rightarrow [(z \in y) \Rightarrow (z \in x)]
</math>
:<math>\vdash
(x = y)\Rightarrow (y = x)
</math>
這樣結合[[一阶逻辑#且與或的直觀意義|(AND)]]和[[一阶逻辑#演繹元定理|演繹元定理]]就有：
:<math>\vdash
(x = y)\Rightarrow [(z \in x) \Leftrightarrow (z \in y)]
</math>
對上式使用[[一阶逻辑#普遍化元定理|(GEN)]]有：
:<math>\vdash
(\forall z)\{
    (x = y)
    \Rightarrow
    [(z \in x) \Leftrightarrow (z \in y)]
\}
</math>
再結合[[一阶逻辑#量词公理|量词公理(A5)]]就有：
:<math>\vdash
(x = y)
\Rightarrow
(\forall z)\{
    [(z \in x) \Leftrightarrow (z \in y)]
\}
</math>
注意對外延公理(ext)使用兩次[[一阶逻辑#量词公理|量词公理(A4)]]會有：
:<math>\vdash
(\forall z)\{
    [(z \in x) \Leftrightarrow (z \in y)]
\}
\Rightarrow
(x = y)

</math>
這樣結合[[一阶逻辑#且與或的直觀意義|(AND)]]就有：
:<math>\vdash
(x = y)\Leftrightarrow (\forall z)[(z \in x) \Leftrightarrow (z \in y)]
</math>
也就是外延公理(ext)搭配等號公理，可以推出「兩個集合相等，若它們有相同的元素。」

=== 視相等符號為公式 ===
除了一開始就假設 <math>x=y</math> 為'''{{lang|en|ZF}}'''的[[一阶逻辑#等式定理|相等符號]]，也可以一開始做如下的符號定義，將<math>x = y</math> 定義為以下[[一阶逻辑#公式|合式公式]]的簡寫：<ref>Hatcher 1982, p. 138, def. 1</ref>
:<math>(x = y)
:=
(\forall z)[(z \in x) \Leftrightarrow (z \in y)]
\land
(\forall z)[(x \in z) \Leftrightarrow (y \in z)]</math>
:（<math>z</math> 須為展開這個簡寫時'''首次出現'''的變數）
直觀上，這個符號定義表示「兩個集合相等，若它們有相同的元素；且它們會屬於同個集合」
如此一來，就不需要外延公理，也可以確保 <math>x = y</math> 為'''{{lang|en|ZF}}'''理論裡的[[一阶逻辑#等式定理|相等符號]]：
{| class="mw-collapsible mw-collapsed wikitable"
!'''證明'''
|-
|以下的證明會逐條檢驗[[一阶逻辑#等式定理|等式定理一節]]所條列的定義
（E1）：

<math>(x = x)</math> 展開來是

: <math>(\forall z)[
    (z \in x)
    \Leftrightarrow
    (z \in x)
]
\land
(\forall z)[
    (x \in z)
    \Leftrightarrow
    (x \in z)
] </math>

那考慮到[[一阶逻辑#定理與證明|恆等關係]]和[[一阶逻辑#且與或的直觀意義|(AND)]]有

: <math>\vdash
(z \in x)
\Leftrightarrow
(z \in x)</math>
: <math>\vdash
(x \in z)
\Leftrightarrow
(x \in z) </math>

那再套用[[一阶逻辑#普遍化元定理|(GEN)]]有

: <math>\vdash
(\forall z)[
    (z \in x)
    \Leftrightarrow
    (z \in x)
]</math>
: <math>\vdash
(\forall z)[
    (x \in z)
    \Leftrightarrow
    (x \in z)
]   </math>

對上兩式使用[[一阶逻辑#且與或的直觀意義|(AND)]]有

: <math>\vdash
(\forall z)[
    (z \in x)
    \Leftrightarrow
    (z \in x)
]
\land
(\forall z)[
    (x \in z)
    \Leftrightarrow
    (x \in z)
] </math>

所以（E1）得證。

（E2）：

目前'''{{lang|en|ZF}}'''內沒有任何[[一阶逻辑#函數符號|函數符號]]，所以對變數 <math>x</math> 來說，'''{{lang|en|ZF}}'''的[[一阶逻辑#原子公式|原子公式]]只有 <math>(x \in z)</math> 和 <math>(z \in x)</math> 兩種可能，這樣的話，（E2）等同於要求以下兩式是'''{{lang|en|ZF}}'''的定理

: (1) <math>(x = y) \Rightarrow [\,
(x \in z)
\Rightarrow
(y \in z)
\,]</math>
: (2) <math>(x = y) \Rightarrow [\,
(z \in x)
\Rightarrow
(z \in y)
\,]</math>

對 <math>(x = y)</math> 使用[[一阶逻辑#量词公理|(AND)]]有

: <math>(x = y)
\vdash
(\forall z)[
    (x \in z)
    \Leftrightarrow
    (y \in z)
]</math>
: <math>(x = y)
\vdash
(\forall z)[
    (z \in x)
    \Leftrightarrow
    (z \in y)
]  </math>

那上兩式搭配[[一阶逻辑#量词公理|量词公理(A4)]]與[[一阶逻辑#演繹元定理|(D1)]]會有

: <math>(x = y)
\vdash
(x \in z)
\Leftrightarrow
(y \in z) </math>
: <math>(x = y)
\vdash
(z \in x)
\Leftrightarrow
(z \in y)  </math>

對上面兩式使用[[一阶逻辑#量词公理|(AND)]]和[[一阶逻辑#且與或的直觀意義|(D1)]]就有

: <math>(x = y)
\vdash
(x \in z)
\Rightarrow
(y \in z) </math>
: <math>(x = y)
\vdash
(z \in x)
\Rightarrow
(z \in y)  </math>

所以根據[[一阶逻辑#演繹元定理|演繹元定理]]，（E2）得證。

（E3）：

本條定義要求以下的合式公式為'''{{lang|en|ZF}}'''的定理

: <math>(x = y)
\Rightarrow
(y = x)</math>

從[[一阶逻辑#且與或的交換性|且的交換性]]有

: <math>\vdash
(\forall z)[(z \in x) \Leftrightarrow (z \in y)]
\Rightarrow
(\forall z)[(z \in y) \Leftrightarrow (z \in x)]</math>
: <math>\vdash
(\forall z)[(x \in z) \Leftrightarrow (y \in z)]
\Rightarrow
(\forall z)[(y \in z) \Leftrightarrow (x \in z)]</math>

對上面兩式使用[[一阶逻辑#量词公理|(AND)]]和[[一阶逻辑#且與或的直觀意義|(D1)]]就有

: <math>(x = y)
\vdash
(\forall z)[(z \in y) \Leftrightarrow (z \in x)]</math>
: <math>(x=y)
\vdash
(\forall z)[(y \in z) \Leftrightarrow (x \in z)]  </math>

再對上面兩式使用[[一阶逻辑#量词公理|(AND)]]和[[一阶逻辑#且與或的直觀意義|(D1)]]又有

: <math>(x = y)
\vdash
(y=x)</math>

所以（E3）的確是'''{{lang|en|ZF}}'''的定理。

綜上所述， <math>x = y</math> 的確為'''{{lang|en|ZF}}'''理論裡的[[一阶逻辑#等式定理|相等符號]]。<math>\Box</math>
|}
但採用這個符號定義的'''{{lang|en|ZF}}'''與[[肯尼思·丘嫩|丘嫩]]的'''{{lang|en|ZF}}'''是兩套不等效的理論，因為在[[肯尼思·丘嫩|丘嫩]]的'''{{lang|en|ZF}}'''裡沒有以下的定理：
: <math>\vdash
[(x \in z) \Leftrightarrow (y \in z)] \Rightarrow (x = y)
</math>

=== 真子集 ===
在定義「相等」以後，可以把「相等的集合」排除出子集的定義中，換句話說，'''{{lang|en|ZF}}'''有以下的符號定義

: <math>x\subset y
:=
(x \subseteq y)
\wedge
(x \neq y)</math>

可直觀理解為「x是y的'''真子集'''（'''{{lang|en|proper subset}}'''）」。

== 正規公理 ==
{{Main|正規公理}}
{{math_theorem
| math_statement = <br/>
<math>
(\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\}
</math>
| name = (reg)Axiom of regularity / Axiom of foundation
}}

「每個'''非空集合'''''<math>x</math>''都包含一個成員''<math>y</math>''，使得''<math>x</math>''和''<math>y</math>''[[交集|不相交]]。」

== 替代公理 ==
'''(Axiom schema of replacement)'''
{{Main|替代公理}}
令<math>\phi \!</math>是ZFC語言內的任意公式，其[[一阶逻辑#自由變數和約束變數|自由變數]]有<math>x,y,A,w_1,\ldots,w_n \!</math>，但<math>B</math>在<math>\phi \!</math>　則不是自由的。則：

:<math>\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]</math>。
「若一個可定義的函數<math>f</math>的[[函数#定義域與值域|定義域]]為一集合，且對定義域的任一<math>x</math>，<math>f(x)</math>也都是集合，則''<math>f</math>''的[[值域]]會是一個集合的子集。」這個限制被需要用來避免一些悖論。

== 分類公理 ==
{{Main|分類公理}}
{{math_theorem
| math_statement = <br/>
若變數 <math>s</math>  於[[一阶逻辑#公式|公式]] <math>\mathcal{P}</math> [[一阶逻辑#自由變數和約束變數|完全被約束]]，則對任意不是 <math>s</math> 的變數 <math>x</math> 與  <math>a</math> ：
:<math>
(\forall x)(\exists s)(\forall a)\{
    (a \in S)
    \Leftrightarrow
    [(a \in x) \land \mathcal{P}]
\}
</math>
都是公理。
| name = (compr)Axiom Schema of Comprehension
}}

「對每個集合 <math>x</math> 和任意不含變數 <math>s</math>  的[[一阶逻辑#公式|公式]] <math>\mathcal{P}</math> ，都有某 <math>x</math> 的子集合 <math>s</math> ，裡面的成員都滿足 <math>\mathcal{P}</math> 」

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

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

=== 分類元定理 ===
[[策梅洛-弗兰克尔集合论#分類公理|分類公理]]也可以由[[替代公理]]和[[空集公理]]中導出，而視為一條[[元定理]]：

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

== 聯集公理 ==
'''(Axiom of union)'''
{{Main|並集公理}}
對任一個集合<math>\mathcal{F}</math>，總存在一個集合<math>A</math>，包含每個為<math>\mathcal{F}</math>的某個成員的成員的集合。
:<math>\forall \mathcal{F} \,\exists A \, \forall Y\, \forall x [(x \in Y \land Y \in \mathcal{F}) \Rightarrow x \in A]</math>。

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

== 冪集公理 ==
'''(Axiom of power set)'''
{{Main|冪集公理}}
令<math>z \subseteq x</math>為<math>\forall q (q \in z \Rightarrow q \in x)</math>。對任一個集合<math>x</math>，皆存在一個集合<math>y</math>，為''<math>x</math>''的[[冪集]]的[[父集]]。<math>x</math>的冪集為一個其成員為所有''<math>x</math>''的子集的類。
:<math>\forall x \exists y  \forall z [z \subseteq x \Rightarrow z \in y]</math>。

== 良序定理 ==
'''(Well-ordering theorem)'''
{{Main|良序定理}}
對任一集合''<math>X</math>''，總存在一個可[[良序關係|良好排序]]''X''的[[二元關係]]<math>R</math>。這意指著，''<math>R</math>''是''<math>X</math>''上的[[全序關係]]，且''<math>X</math>''內每個非空[[子集]]在''<math>R</math>''下都有一個最小元素。
:<math>\forall X \exists R ( R \;\mbox{well-orders}\; X)</math>。

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

== 参见 ==
* [[康托尔定理]]
* [[公理化集合论]]
* [[策梅洛集合论]]
* [[新基础集合论]]
* [[ZFC系統無法確定的命題列表]]

== 參考資料 ==
<references />

==文献==
{{refbegin}}
*[[亞歷山大·阿比安]], 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'''.
{{refend}}

==外部链接==
* [http://us.metamath.org/ Metamath.] {{Wayback|url=http://us.metamath.org/ |date=20201124173846 }} 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] {{Wayback|url=http://plato.stanford.edu/entries/set-theory/ |date=20150314173026 }} -- by Thomas Jech.

[[Category:集合论系统|*]]
[[Category:集合论公理|*]]