查看“︁冯诺伊曼-博内斯-哥德尔集合论”︁的源代码

{{noteTA
|T=zh-cn:冯·诺伊曼-博内斯-哥德尔集合论; zh-tw:馮·諾伊曼-博內斯-哥德爾集合論; zh-hk:馮·紐曼-博內斯-哥德爾集合論;
|G1=Physics
}}
'''冯·诺伊曼-博内斯-哥德尔集合论'''（{{lang-en|von Neumann–Bernays–Gödel Set Theory}}，'''{{lang|en|NBG}}'''）是種以[[类 (数学)|类]]為直觀動機的[[一阶逻辑|一阶]][[公理化集合论]]，它是配上[[选择公理]]的[[策梅洛-弗兰克尔集合论]]（{{lang-en|Zermelo-Fraenkel Set Theory with the axiom of Choice}}，'''{{lang|en|ZFC}}'''）的[[保守扩展]]（'''{{lang|en|ZFC}}'''裡可以證明的[[一阶逻辑#定理與證明|定理]]也都是'''{{lang|en|NBG}}'''的定理）<ref>{{Cite book|chapter=|url=https://philpapers.org/rec/COHSTA-2|publisher=New York: W. A. Benjamin|date=1966|first=Paul J.|last=Cohen|title=Set Theory and the Continuum Hypothesis|access-date=2023-05-15|archive-date=2023-05-15|archive-url=https://web.archive.org/web/20230515115451/https://philpapers.org/rec/COHSTA-2|dead-url=no}}</ref>，而且'''{{lang|en|NBG}}'''僅需在一階邏輯基本的[[公理模式]]上添加有限数目的公理，但'''{{lang|en|ZFC}}'''需添加與集合有關的公理模式<ref>{{Cite journal |last=Montague |first=Richard |date=1964 |title=Semantical Closure and Non-Finite Axiomatizability I |url=https://philpapers.org/rec/MONSCA-7 |journal=Journal of Symbolic Logic |volume=29 |issue=1 |doi=10.2307/2269797 |access-date=2023-05-15 |archive-date=2023-05-15 |archive-url=https://web.archive.org/web/20230515115450/https://philpapers.org/rec/MONSCA-7 |dead-url=no }}</ref>。

'''{{lang|en|NBG}}'''首先由[[冯·诺伊曼]]在1920年代提出，從1937年开始由{{tsl|en|Paul Bernays|保罗·博内斯}}作修改，在1940年由[[哥德尔]]进一步简化。

== 基本符號 ==

在'''{{lang|en|NBG}}'''下，「属于關係」以一個雙元[[一阶逻辑#斷言符號|斷言符號]] <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」。

以下都把 <math>\vdash_{NBG}</math> 簡寫為普通的 <math>\vdash</math>。

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

=== 類與集合 ===
「類」這個名詞在[[公理化集合论]]出現之前，通常被理解為「以[[集合 (数学)|集合]]為[[元素 (數學)|元素]]的集合。」或是集合（如[[等价类]]）。

但'''{{lang|en|NBG}}'''所談及的一切對象（變數和[[一阶逻辑#項|項]]）'''都是類'''。而'''所謂的集合，是屬於某個類的類'''，也就是說以下的[[合式公式]]（<math>\mathcal{M}</math> 來自[[德语]]的"集合"「{{Lang|de|Menge}}」）式
:<math>\mathcal{M}(x):=\exists y (x \in y)</math>
可直觀理解為「x是集合」，特別注意到，為了避免跟其他合式公式的變數產生混淆， <math>y</math> 必須是展開 <math>\mathcal{M}(x)</math> 時首次出現的變數。反之合式公式
:<math>\mathcal{Pr}(x):=\neg\mathcal{M}(x)</math>
可稱為「 <math>x</math> 是[[真类]]（'''{{lang|en|proper class}}'''）」。

=== 子類 ===
直觀上「x包含於y」意為「所有x的元素a都會屬於y」，以此為動機，'''{{lang|en|NBG}}'''有以下的符號簡寫
:<math>x \subseteq y := \forall a[\,
(a \in x)
\Rightarrow
(a \in y)
\,]</math>
以上可稱為「x包含於y」或「x是y的'''子類'''（'''{{lang|en|subclass}}'''）」；在 <math>\mathcal{M}(x)</math> 和 <math>\mathcal{M}(y)</math> 成立的前提下（也就是「x和y都是集合」），可稱為「x是y的'''子集'''（'''{{lang|en|subset}}'''）」。

=== 與集合相關的量詞簡寫 ===
仿造[[一阶逻辑#量詞的簡寫|量詞的簡寫]]，對於任意變數 <math>x</math> 與合式公式 <math>\mathcal{A}</math> ，可作如下的符號定義

:<math>({\forall}^M x)\mathcal{A} := \forall x[\,\mathcal{M}(x)\Rightarrow \mathcal{A}\,]</math> （對所有 <math>x</math> ， <math>x</math> 是集合則 <math>\mathcal{A}</math> ）

:<math>({\exists}^M x)\mathcal{A} := \exists x[\,\mathcal{M}(x)\wedge \mathcal{A}\,]</math> （存在 <math>x</math> 不但是集合且 <math>\mathcal{A}</math> ）

也有書籍以小寫字母來表示被量化的集合變數<ref>{{Cite book|title=Introduction to Mathematical Logic (6th Edition)|last=Mendelson|first=Elliott|publisher=Chapman & Hall|year=2015|isbn=9781482237726|pages=233-233}}</ref>，但考慮到一般的非邏輯數學書籍都將大小寫的差異挪作他用，為避免混淆本條目採用以上的上標表示法。

== 等號公理 ==

=== 看待等號的不同方式 ===
直觀上，兩個集合相等意為「x的元素就是y的元素」，也就是[[朴素集合论]]的[[外延公理]]，換句話說，可用以下的嚴謹合式公式重寫為
:<math>\forall a[\,
(a \in x)
\Leftrightarrow
(a \in y)
\,]</math>
但一階邏輯的等號可以視為單獨的[[一阶逻辑#斷言符號|斷言符號]]，也可以視為一條複合的合式公式。具體來說，視為一個新的斷言符號 <math>Q(x,\,y)</math> 並簡記為 <math>x = y</math> 的話，需在'''{{lang|en|NBG}}'''內額外添加以下的公理

{{math_theorem
| name = <math>(T^{\prime})</math>
| math_statement = <math>(x=y)
\Leftrightarrow
\forall a[\,
(a \in x)
\Leftrightarrow
(a \in y)
\,]</math>
}}
直觀上可理解為「類x的元素就是類y的元素，等價於類x等於類y」。

但視為一條合式公式，則僅需做以下的符號定義
:<math>(x=y)
:=
\forall a[\,
(a \in x)
\Leftrightarrow
(a \in y)
\,]</math>
不管是何種看待方法，習慣上都會把 <math>\neg(x = y)</math> 簡記成 <math>(x \neq y)</math> （直觀上的「不相等」）。

=== 等號的良置 ===
為了確保 <math>(x = y)</math> 的確符合直觀上對等號的要求，還需添加以下的公理

{{math_theorem
| name = <math>(T)</math>
| math_statement = <math>(x=y)
\Rightarrow
\forall z[\,
(x \in z)
\Leftrightarrow
(y \in z)
\,]</math>
}}

直觀上，這個公理確保「x等於y，則x屬於z等同於y屬於z」。

這樣，以下的[[元定理]]就確保了如此定義的等號是「成功的」。
{{math_theorem
| name = 元定理
| math_statement = '''{{lang|en|NBG}}'''是帶相等符號 <math>(x=y)</math> 的[[一阶逻辑]]理論
}}
{| class="mw-collapsible mw-collapsed wikitable"
!'''證明'''
|-
|以下的證明會逐條檢驗[[一阶逻辑#等式定理|等式定理一節]]所條列的定義

（E1）：

<math>(x=x)</math> 展開來是（或等價於）

: <math>\forall a[\,
(a \in x)
\Leftrightarrow
(a \in x)
\,]</math>

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

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

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

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

所以（E1）得證。

（E2）：

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

: (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>

但依據[[一阶逻辑#量词公理|量词公理]]（A4），(1)可從本節一開始添加的公理（T）所推出；類似地，把 <math>(x=y)</math> 視為斷言符號時，(2)都可以從（T'）配合（A4）推出；若把 <math>(x=y)</math> 視為合式公式的簡寫，(2)也可以用 <math>(x=y)</math> 的定義配上（A4）推出。

（E3）：

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

: <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>

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

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

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

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

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

綜上所述，定理得證。<math>\Box</math>
|}


=== 真子類 ===
在定義「相等」以後，可以把「相等的類」排除出子類的定義中，換句話說，'''{{lang|en|NBG}}'''有以下的符號定義
:<math>x\subset y
:=
(x \subseteq y)
\wedge
(x \neq y)</math>
可直觀理解為「x是y的'''真子類'''（'''{{lang|en|proper subclass}}'''），定義為x包含於y且x不等於y」；在 <math>\mathcal{M}(x)</math> 和 <math>\mathcal{M}(y)</math> 成立的前提下（也就是「x和y都是集合」），可稱為「x是y的'''真子集'''（'''{{lang|en|proper subset}}'''）」。

=== 外延定理 ===
為以下的定理可直觀理解為「x等於y等價於，對所有集合z，z屬於x等價於z屬於y」，也就是說，等於的定義可以「限縮」成元素為集合的狀況。{{math_theorem
|name=外延定理
|math_statement=
<math>\vdash (x = y) \Leftrightarrow (\forall^M z)[\,(z \in x) \Leftrightarrow (z \in y)\,]</math>
}}
{| class="mw-collapsible mw-collapsed wikitable"
!'''證明'''
|-
|
以下取一個不曾出現的變數 <math>t</math> 來展開 <math>\mathcal{M}(z)</math>

(<math>\Rightarrow</math>)<math>\forall z(z\in x\Leftrightarrow z\in y)\vdash\forall z\{\exists t(z \in t)\Rightarrow[(z\in x)\Leftrightarrow(z\in y)]\}</math>

:(1)<math>\forall z(z\in x\Leftrightarrow z\in y)</math> (Hyp)

:(2)<math>z\in x\Leftrightarrow z\in y</math> (MP with 1, A4)

:(3)<math>\exists t(z \in t)\Rightarrow[(z\in x)\Leftrightarrow(z\in y)]</math> (MP with 2, A1)

:(4)<math>\forall z\{\exists t(z \in t)\Rightarrow[(z\in x)\Leftrightarrow(z\in y)]\}</math> (GEN with 3)

(<math>\Leftarrow</math>)<math>\forall z\{\mathcal{M}(z)\Rightarrow[(z\in x)\Leftrightarrow(z\in y)]\}\vdash\forall z(z\in x\Leftrightarrow z\in y)</math>

:<math>\mathcal{A}:=(z\in x)\Leftrightarrow(z\in y)</math>

:(1)<math>\forall z[\exists t(z\in t)\Rightarrow\mathcal{A}]</math> (Hyp)

:(2)<math>\exists t(z\in t)\Rightarrow\mathcal{A}</math> (MP with A4, 1)

:(3)<math>\neg\mathcal{A}\Rightarrow\forall t[\neg(z\in t)]</math> (MP with T, 2)

:(4) <math>\neg\mathcal{A}\Rightarrow[\neg(z\in t)]</math> (D1, with A4, 3)

:(5)<math>(z \in t)\Rightarrow[(z\in x)\Leftrightarrow(z\in y)]</math> (MP with T, 4)

:(6)<math>\forall t\{(z \in t)\Rightarrow[(z\in x)\Leftrightarrow(z\in y)]\}</math> (GEN with 5)

:(7)<math>(z \in x)\Rightarrow[(z\in x)\Leftrightarrow(z\in y)]</math> (MP with A4, 6)

:(8)<math>(z \in y)\Rightarrow[(z\in x)\Leftrightarrow(z\in y)]</math> (MP with A4, 6)

:(9)<math>(z \in x)\Rightarrow[(z\in x)\Rightarrow(z\in y)]</math> (D1 with AND, 7)

:(10)<math>(z \in y)\Rightarrow[(z\in y)\Rightarrow(z\in x)]</math> (D1 with AND, 8)

:(11)<math>(z\in x)\Rightarrow(z\in y)</math> (MP twice with A2, I, 9)

:(12)<math>(z\in y)\Rightarrow(z\in x)</math> (MP twice with A2, I, 10)

:(13)<math>(z\in x)\Leftrightarrow(z\in y)</math> (AND with 11, 12)

:(14)<math>\forall z(z\in x\Leftrightarrow z\in y)</math> (GEN with 13)
|}
引入新的函數符號前，常需要[[一阶逻辑#函數符號與唯一性|唯一存在性]]的證明，而外延定理大大簡化了證明的難度。

=== 特定條件下的存在性 ===
以下關於[[一阶逻辑]]的一般性定理，也大大簡化了 '''{{lang|en|NBG}}''' 引入新公理的過程所需的證明
{{math_theorem
|name=（DC, Definition under certain condition）
|math_statement=
<math>x</math> 於[[合式公式]] <math>\mathcal{A}</math> 完全不自由且 <math>c</math>  是[[一阶逻辑#常數符號|常數符號]]。若

<math>\mathcal{A} \vdash (\exists x)\mathcal{B}</math>　

則有

<math>
\vdash(\exists x)\{\,
[\,\neg\mathcal{A} \wedge (x=c)\,]
\vee
(\mathcal{A} \wedge \mathcal{B})
\,\}</math>
}}
{| class="mw-collapsible mw-collapsed wikitable"
!'''證明'''
|-
|
(1)<math>\mathcal{A}\Rightarrow(\exists x)\mathcal{B}</math> (Hyp)

(2)<math>(\forall x)\{\neg\{[\neg\mathcal{A}\wedge(x=c)]\vee(\mathcal{A}\wedge\mathcal{B})\}\}</math> (Hyp)

(3)<math>\neg\{[\neg\mathcal{A}\wedge(x=c)]\vee(\mathcal{A}\wedge\mathcal{B})\}</math> (MP with A4, 2)

(4)<math>\neg[\neg\mathcal{A}\wedge(x=c)]\wedge\neg(\mathcal{A}\wedge\mathcal{B})</math> (MP with 3, DIS)

(5)<math>\neg[\neg\mathcal{A}\wedge(x=c)]</math> (MP with AND,4)

(6)<math>\neg(\mathcal{A}\wedge\mathcal{B})</math> (MP with AND, 4)

(7)<math>\neg\mathcal{A}\Rightarrow\neg(x=c)</math> (MP with DIS, DN 5)

(8)<math>\mathcal{A}\Rightarrow\neg\mathcal{B}</math> (MP with DIS, DN, 5)

(9)<math>\mathcal{B}\Rightarrow\neg\mathcal{A}</math> (MP with T, 8)

(10)<math>(\exists x)\mathcal{B}\Rightarrow\neg\mathcal{A}</math> (GENe with 9)

(11)<math>\mathcal{A}\Rightarrow\neg(\exists x)\mathcal{B}</math> (MP with T, 11)

(12)<math>\neg\mathcal{A}</math> (A3' with 1, 11)

(13)<math>\neg(x=c)</math> (MP with 7, 12)

(14)<math>(\forall x)[\neg(x=c)]</math> (GEN with 13)

再套用一次（DN）也就是

<math>\mathcal{A}\Rightarrow(\exists x)\mathcal{B}\,\vdash(\forall x)\{\neg\{[\neg\mathcal{A}\wedge(x=c)]\vee(\mathcal{A}\wedge\mathcal{B})\}\}\Rightarrow\neg(\exists x)(x=c)</math>

但由[[一阶逻辑#等式定理|一阶逻辑的等式性質]]有

<math>\vdash c=c</math>

對上式以變數 <math>x</math> 套用一次(GENe)有

<math>\vdash(\exists x)(x=c)</math>

所以由(C2)本定理就會得證。<math>\Box</math>
|}

== 空集合公理 ==
{{math_theorem
| name = <math>(N)</math>
| math_statement = <math>({\exists}^{M} x)({\forall}^{M} y)(y\not\in x)</math>
}}

這個公理的直觀意思是「存在集合x，使的所有集合y都不屬於x」。

事實上這個公理還確保了[[空集]]的唯一性，嚴格來說，它確保了：
{{math_theorem
|name=
|math_statement=
<math>\vdash (\exists!x)[\,
\mathcal{M}(x)
\wedge
({\forall}^{M} y)(y\not\in x)
\,]</math>
}}
{| class="mw-collapsible mw-collapsed wikitable"
!'''證明'''
|-
|
假設

:<math>({\forall}^{M} y)(y\not\in x)</math>
:<math>({\forall}^{M} y)(y\not\in t)</math>

那根據[[一阶逻辑#量词公理|量词公理]]的(A4)有

:<math>\mathcal{M}(y) \Rightarrow (y\not\in x)</math>
:<math>\mathcal{M}(y) \Rightarrow (y\not\in t)</math>

另一方面，根據[[一阶逻辑#常用的推理性質|常用的推理性質]]的(M0)有

:<math>\vdash (y\not\in x) \Rightarrow [\,(y\in x) \Rightarrow (y\in t)\,]</math>
:<math>\vdash (y\not\in t) \Rightarrow [\,(y\in t) \Rightarrow (y\in x)\,]</math>

這樣根據[[一阶逻辑#演繹元定理|演繹定理]]的推論(D1)有

:<math>\mathcal{M}(y) \Rightarrow [\,(y\in x) \Rightarrow (y\in t)\,]</math>
:<math>\mathcal{M}(y) \Rightarrow [\,(y\in t) \Rightarrow (y\in x)\,]</math>

這樣根據[[一阶逻辑#常用的推理性質|常用的推理性質]](T)有

:<math>\neg[\,(y\in x) \Rightarrow (y\in t)\,] \Rightarrow \neg\mathcal{M}(y)</math>
:<math>\neg[\,(y\in t) \Rightarrow (y\in x)\,] \Rightarrow \neg\mathcal{M}(y)</math>

這樣根據[[一阶逻辑#德摩根定律|德摩根定律]]和[[一阶逻辑#邏輯與和邏輯或|邏輯與]]的(DisJ)有

:<math>\neg
\{\,
[\,(y\in x) \Rightarrow (y\in t)\,]
\wedge
[\,(y\in t) \Rightarrow (y\in x)\,]
\,\}
\Rightarrow
\neg\mathcal{M}(y)</math>

這樣再根據(T)有

:<math>\mathcal{M}(y) \Rightarrow [\,(y\in x) \Leftrightarrow (y\in t)\,]</math>

這樣根據[[一阶逻辑#普遍化元定理|普遍化]]有

:<math>(\forall^M y)[\,(y\in x) \Leftrightarrow (y\in t)\,]</math>

那這樣根據上節的[[冯诺伊曼-博内斯-哥德尔集合论#外延定理|外延定理]]有

:<math>x = t</math>

換句話說

:<math>\vdash
[\,({\forall}^{M} y)(y\not\in x) \wedge ({\forall}^{M} y)(y\not\in t)\,]
\Rightarrow
(x = t)</math>

這樣根據[[一阶逻辑#邏輯與和邏輯或|邏輯與的直觀性質]]和(D1)有

:<math>\vdash
\{\,
[\,\mathcal{M}(x) \wedge ({\forall}^{M} y)(y\not\in x)\,]
\wedge
[\,\mathcal{M}(t) \wedge ({\forall}^{M} y)(y\not\in t)\,]
\,\}
\Rightarrow
(x = t)</math>

這樣根據[[一阶逻辑#普遍化元定理|普遍化]]有

: <math>\vdash
(\forall x)(\forall t)\big\{\,
\{\,
[\,\mathcal{M}(x) \wedge ({\forall}^{M} y)(y\not\in x)\,]
\wedge
[\,\mathcal{M}(t) \wedge ({\forall}^{M} y)(y\not\in t)\,]
\,\}
\Rightarrow
(x = t)
\,\big\}</math>
再綜合本節的空集合公理（N），本定理就得証了。<math>\Box</math>
|}

也就是直觀上，「[[空集]]是唯一存在的」，這樣根據[[一阶逻辑#函數符號與唯一性|函數符號與唯一性]]一節，可以在'''{{lang|en|NBG}}'''加入新的常數符號 <math>\varnothing</math> 和以下的新公理（嚴格來說，把完全沒有函數符號和常數符號的'''{{lang|en|NBG}}'''擴展成有 <math>\varnothing</math> 的新'''{{lang|en|NBG}}'''，但兩個理論是等效的）

{{math_theorem
| name = <math>(N^{\prime})</math>
| math_statement = <math>\mathcal{M}(\varnothing)
\wedge
({\forall}^{M} y)(y\not\in \varnothing)</math>
}}

這個新公理直觀上以「<math>\varnothing</math>為集合，且任意集合y都不屬於<math>\varnothing</math>」，把 <math>\varnothing</math> 定義成了[[空集]]的表示符號。

== 配對公理 ==
{{math_theorem
| name = <math>(P)</math>
| math_statement = <math>({\forall}^{M} x)({\forall}^{M} y)({\exists}^{M} p)({\forall}^{M} z)\{(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\}</math>
}}

這個公理的直觀意思是「對所有集合x和集合y，存在一個僅以x跟y為元素的集合p」。

這個公理還確保了以下的唯一性：
{{math_theorem
|name=定理（P-1）
|math_statement=
<math>\mathcal{M}(x) \wedge \mathcal{M}(y)
\vdash (\exists!p)\big\{\,
\mathcal{M}(p)
\wedge
({\forall}^{M} z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}
\,\big\}</math>
}}
{| class="mw-collapsible mw-collapsed wikitable"
!'''證明'''
|-
|
根據[[一阶逻辑#量詞的簡寫|量詞的簡寫]]，配對公理(P)等價於

:<math>(\forall x)(\forall y) \bigg\{\,
\mathcal{M}(x) \wedge \mathcal{M}(y)
\Rightarrow
(\exists p)\big\{\,
\mathcal{M}(p)
\wedge
({\forall}^{M} z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}
\,\big\}
\,\bigg\}</math>

這樣對上式套用兩次[[一阶逻辑#量词公理|量词公理]]的(A4)有

:<math>\mathcal{M}(x) \wedge \mathcal{M}(y)
\Rightarrow
(\exists p)\big\{\,
\mathcal{M}(p)
\wedge
({\forall}^{M} z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}
\,\big\}</math>

這樣在有 <math>\mathcal{M}(x) \wedge \mathcal{M}(y)</math> 的前提就有

:<math>(\exists p)\big\{\,
\mathcal{M}(p)
\wedge
({\forall}^{M} z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}
\,\big\}</math>

所以

:<math>\mathcal{M}(x) \wedge \mathcal{M}(y)
\vdash
(\exists p)\big\{\,
\mathcal{M}(p)
\wedge
({\forall}^{M} z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}
\,\big\}</math>

另一方面，若假設

:<math>\mathcal{M}(p)
\wedge
({\forall}^{M} z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}</math>
:<math>\mathcal{M}(\pi)
\wedge
({\forall}^{M} z)\{\,(z \in \pi)\Leftrightarrow [(z=x)\vee(z=y)]\,\}</math>

這樣根據[[一阶逻辑#邏輯與和邏輯或|邏輯與的直觀性質]]有

:<math>({\forall}^{M} z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}</math>
:<math>({\forall}^{M} z)\{\,(z \in \pi)\Leftrightarrow [(z=x)\vee(z=y)]\,\} </math>

再根據(A4)有

:<math>\mathcal{M}(z)
\Rightarrow
\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}</math>
:<math>\mathcal{M}(z)
\Rightarrow\{\,(z \in \pi)\Leftrightarrow [(z=x)\vee(z=y)]\,\} </math>

如果再假設 <math>\mathcal{M}(z)</math> ，根據[[一阶逻辑#推理规则|MP律]]有

:<math>(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]</math>
:<math>(z \in \pi)\Leftrightarrow [(z=x)\vee(z=y)] </math>

這樣根據[[一阶逻辑#演繹元定理|演繹定理]]的推論(D1)和[[一阶逻辑#邏輯與和邏輯或|邏輯與的直觀性質]]有

:<math>(z\in p) \Leftrightarrow (z\in \pi)</math>

也就是說

:<math>\mathcal{B}(p) \wedge \mathcal{B}(\pi),\,
\mathcal{M}(z)
\,\vdash\,
(z\in p) \Leftrightarrow (z\in \pi)</math>

其中 <math>\mathcal{B}(p)
:=
\mathcal{M}(p)
\wedge
({\forall}^{M} z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}</math> 

因為變數 <math>z</math> 在 <math>\mathcal{B}(p)</math> 和 <math>\mathcal{B}(\pi)</math> 內完全不自由，對上式套用[[一阶逻辑#演繹元定理|演繹定理]](D)將 <math>\mathcal{M}(z)</math> 移到右方後，再對 <math>z</math> 套用[[一阶逻辑#普遍化元定理|普遍化]]會有

:<math>\mathcal{B}(p) \wedge \mathcal{B}(\pi)
\,\vdash\,
(\forall^M z)[\,(z\in p) \Leftrightarrow (z\in \pi)\,]</math>

這樣根據本條目的[[冯诺伊曼-博内斯-哥德尔集合论#外延定理|外延定理]]有

:<math>\mathcal{B}(p) \wedge \mathcal{B}(\pi)
\,\vdash\,
(p = \pi)</math>

那以[[一阶逻辑#演繹元定理|演繹定理]](D)將 <math>\mathcal{B}(p) \wedge \mathcal{B}(\pi)</math> 移到右方，然後接連對 <math>p</math> 和 <math>\pi</math> 使用[[一阶逻辑#普遍化元定理|普遍化]]有

:<math>\vdash
(\forall p)(\forall \pi)
[\,
\mathcal{B}(p) \wedge \mathcal{B}(\pi)
\Rightarrow
(p = \pi)
\,]</math>

故本定理得証。<math>\Box</math>
|}

這樣的話會有
{{math_theorem
|math_statement=
<math>\vdash
(\exists! p)\bigg\{\,
\{\,
\neg[\,\mathcal{M}(x) \wedge \mathcal{M}(y)\,]
\wedge
(p = \varnothing)
\,\}
\vee

\big\{\,
\mathcal{M}(x) \wedge \mathcal{M}(y)
\wedge
\mathcal{M}(p)
\wedge
({\forall}^{M} z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}
\,\big\}
\,\bigg\}</math>
}}
{| class="mw-collapsible mw-collapsed wikitable"
!'''證明'''
|-
|根據（P-1）和本條目的[[#特定條件下的存在性|特定條件下的存在性]](DC)會有
:（P-2）<math>\vdash
(\exists p)\bigg\{\,
\{\,
\neg[\,\mathcal{M}(x) \wedge \mathcal{M}(y)\,]
\wedge
(p = \varnothing)
\,\}
\vee

\big\{\,
\mathcal{M}(x) \wedge \mathcal{M}(y)
\wedge
\mathcal{M}(p)
\wedge
({\forall}^{M} z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}
\,\big\}
\,\bigg\}</math>
設
:<math>\mathcal{A}(p)
:=
\neg[\,\mathcal{M}(x) \wedge \mathcal{M}(y)\,]
\wedge
(p = \varnothing)</math>
:<math>\mathcal{B}(p)
:=
\mathcal{M}(x) \wedge \mathcal{M}(y)
\wedge
\mathcal{M}(p)
\wedge
({\forall}^{M} z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee(z=y)]\,\}</math>
:<math>\mathcal{C}
:=
\mathcal{M}(x) \wedge \mathcal{M}(y)</math>

那連續套用[[一阶逻辑#分配律|邏輯與合邏輯或的分配律]]與[[一阶逻辑#交換性|邏輯與的交換性]]會有
:<math>\vdash
\{\,
[\,\mathcal{A}(p) \vee \mathcal{B}(p)\,]
\wedge
[\,\mathcal{A}(\pi) \vee \mathcal{B}(\pi)\,]
\,\}
\Leftrightarrow
\big\{\,
\{\,
[\,\mathcal{A}(p) \wedge \mathcal{A}(\pi)\,] \vee [\,\mathcal{B}(p) \wedge \mathcal{A}(\pi)\,]
\,\}
\vee
\{\,
[\,\mathcal{A}(p) \wedge \mathcal{B}(\pi)\,] \vee [\,\mathcal{B}(p) \wedge \mathcal{B}(\pi)\,]
\,\}
\,\big\}</math>

但考慮到[[一阶逻辑#邏輯與和邏輯或|邏輯與的直觀性質]]和[[一阶逻辑#公式|逻辑與的定義]]有
:<math>\vdash
[\,\mathcal{B}(p) \wedge \mathcal{A}(\pi)\,]
\Rightarrow
(\neg\mathcal{C}\wedge\mathcal{C})</math>
:<math>\vdash
[\,\mathcal{A}(p) \wedge \mathcal{B}(\pi)\,]
\Rightarrow
(\neg\mathcal{C}\wedge\mathcal{C})</math>
:<math>\vdash
(\neg\mathcal{C}\wedge\mathcal{C})
\Leftrightarrow
\neg(\mathcal{C}\Rightarrow\mathcal{C})</math>

那根據[[一阶逻辑#定理與證明|恆等關係<math>(I)</math>]]和[[一阶逻辑#常用的推理性質|常用的推理性質]](T)有
:<math>\vdash
\neg[\,\mathcal{B}(p) \wedge \mathcal{A}(\pi)\,]</math>
:<math>\vdash
\neg[\,\mathcal{A}(p) \wedge \mathcal{B}(\pi)\,]</math>

所以根據[[一阶逻辑#公式|逻辑或的定義]]來重複使用[[一阶逻辑#演繹元定理|演繹定理]]的推論(D1)會有
:<math>\vdash
\{\,
[\,\mathcal{A}(p) \vee \mathcal{B}(p)\,]
\wedge
[\,\mathcal{A}(\pi) \vee \mathcal{B}(\pi)\,]
\,\}
\Leftrightarrow
\{\,
[\,\mathcal{A}(p) \wedge \mathcal{A}(\pi)\,]
\vee
[\,\mathcal{B}(p) \wedge \mathcal{B}(\pi)\,]
\,\}</math>

然後從'''{{lang|en|NBG}}'''的[[一阶逻辑#等式定理|等式定理]]會有
:<math>\vdash
[\,\mathcal{A}(p) \wedge \mathcal{A}(\pi)\,]
\Rightarrow
(p = \pi)</math>

另一方面，根據（P-1）有
:<math>\vdash
[\,\mathcal{B}(p) \wedge \mathcal{B}(\pi)\,]
\Rightarrow
(p=\pi)</math>

這樣結合[[一阶逻辑#邏輯與和邏輯或|邏輯與]]的(DisJ)有
:<math>\vdash
\{\,
[\,\mathcal{A}(p) \vee \mathcal{B}(p)\,]
\wedge
[\,\mathcal{A}(\pi) \vee \mathcal{B}(\pi)\,]
\,\}
\Rightarrow
(p=\pi)</math>

再對 <math>p</math> 和 <math>\pi</math> 套用[[一阶逻辑#普遍化元定理|普遍化]]有
:<math>\vdash
(\forall p)(\forall \pi)\bigg\{\,
\{\,
[\,\mathcal{A}(p) \vee \mathcal{B}(p)\,]
\wedge
[\,\mathcal{A}(\pi) \vee \mathcal{B}(\pi)\,]
\,\}
\Rightarrow
(p=\pi)
\,\bigg\}</math>

這樣結合剛剛的（P-2）與[[一阶逻辑#邏輯與和邏輯或|邏輯與的直觀性質]]，本定理就得證了。<math>\Box</math>
|}

所以根據[[一阶逻辑#函數符號與唯一性|函數符號與唯一性]]一節，可以在'''{{lang|en|NBG}}'''加入新的雙元[[一阶逻辑#函數符號|函數符號]] <math>f^2_p(x,\,y)</math>（簡記為 <math>\{x,\,y\}</math> ）和以下的新公理

{{math_theorem
| name = <math>(P^{\prime})</math>
| math_statement = <br/>
<math>\bigg\{
    \neg[\,\mathcal{M}(x) \wedge \mathcal{M}(y)\,]
    \wedge
    (\{x,\,y\} = \varnothing)
\bigg\}
\vee
</math>
<br/>
<math>
\bigg\{
    \mathcal{M}(x) \wedge \mathcal{M}(y)
    \wedge
    \mathcal{M}\left(\{x,\,y\}\right)
    \wedge
    ({\forall}^{M} z)\{\,(z\in \{x,\,y\})\Leftrightarrow [(z=x)\vee(z=y)]\,\}
\bigg\}
</math>
}}

這個新公理的直觀意思是「若x和y為集合，則 <math>\{x,\,y\}</math> 就是那個只以x和y為元素的集合；但反之，若x和y不全為集合，則 <math>\{x,\,y\}</math> 為[[空集]]」。

=== 有序對 ===

<math>\{x\}:=\{x,\,x\} </math>

<math>\langle x \rangle
:=
x  </math>

<math>\langle x,\, y \rangle
:=
\{\{x\},\,\{x,\,y\}\}  </math>

<math>\langle x_1,\,\dots,\,\,x_n,\,x_{n+1} \rangle
:=
\langle \langle x_1,\,\dots,\,\,x_n\rangle,\, x_{n+1}\rangle </math>

在不跟括弧產生混淆的情況下，也可以把<math>\langle x_1,\,\dots,\,\,x_n,\,x_{n+1} \rangle </math>記為<math>( x_1,\,\dots,\,\,x_n,\,x_{n+1} ) </math>。

=== 關係 ===
<math>
Rel(f):=(\forall^M a)\big\{\,
(a\in f)
\Rightarrow
(\exists x)(\exists y)\{\,
\mathcal{M}(x) \wedge \mathcal{M}(y)
\wedge
[\,a=(x,\,y)\,]
\,\} 
\,\big\}
</math>

=== 类函數 ===
<math>Fnc(f):=
Rel(f)
\wedge
(\forall^M x)(\forall^M y)(\forall^M \upsilon)\{\,
[\,(x,\,y)\in f\wedge(x,\,\upsilon)\in f \,]
\Rightarrow
(y = \upsilon)
\,\} </math>

類函數跟[[函数|普通函数]]的差別在於普通函數'''是個集合'''。

== 类的存在公理 ==

=== 屬於類公理 ===
{{math_theorem
| name = <math>(K_{\in})</math>
| math_statement = <math>
(\exists e)(\forall^M a)(\forall^M b)\{
    [(a,\,b)\in e]
    \Leftrightarrow
    (a\in b)
\} 
</math>
}}

=== 交類公理 ===
{{math_theorem
| name = <math>(K_{i})</math>
| math_statement = <math>
(\forall x)(\forall y)(\exists i)({\forall}^{M} a)\{
    (a \in i)
    \Leftrightarrow
    [(a\in x) \wedge (a\in y)]
\} 
</math>
}}

=== 補類公理 ===
{{math_theorem
| name = <math>(K_{c})</math>
| math_statement = <math>
(\forall x)(\exists c)({\forall}^{M} a)[
    (a\in c)
    \Leftrightarrow
    (a\not\in x)
]
</math>
}}

=== 定義域公理 ===
{{math_theorem
| name = <math>(K_{D})</math>
| math_statement = <math>
(\forall x)(\exists d)(\forall^M a)\{
    (a\in d)
    \Leftrightarrow
    (\exists^M b)[(a,\,b) \in x]
\}
</math>
}}

=== 積類公理 ===
{{math_theorem
| name = <math>(K_{p})</math>
| math_statement = <math>
(\forall x)(\exists p)(\forall^M a)(\forall^M b)\{
    [\,(a,\,b) \in p\,]
    \Leftrightarrow
    (a \in x)
\}
</math>
}}

=== 置換類公理 ===
{{math_theorem
| name = <math>(K_{\sigma 1})</math>
| math_statement = <math>
(\forall x)(\exists \sigma)(\forall^M a)(\forall^M b)(\forall^M c)\{
    [(a,\,b,\,c) \in x]
    \Leftrightarrow
    [(b,\,c,\,a) \in \sigma]
\}
</math>
}}
{{math_theorem
| name = <math>(K_{\sigma 2})</math>
| math_statement = <math>
(\forall x)(\exists \sigma)(\forall^M a)(\forall^M b)(\forall^M c)\{
    [(a,\,b,\,c) \in x]
    \Leftrightarrow
    [(a,\,c,\,b) \in \sigma]
\} 
</math>
}}

=== 類的存在元定理 ===
這個元定理對應到[[策梅洛-弗兰克尔集合论#分類公理|ZFC尔集合论的分類公理]]。

首先需要[[递归定义|递归地定义]]「可敘述[[合式公式|公式]]」（predicative well-formed formula）：

* 對任意變數 <math>x </math> 和 <math>y </math> ，<math>x \in y </math> 為可敘述公式。
* 若 <math>\mathcal{P} </math> 與 <math>\mathcal{Q} </math> 為可敘述公式， <math>x </math> 為任意變數，則 <math>(\neg\mathcal{P}) </math> 、 <math>(\mathcal{P} \Rightarrow \mathcal{Q}) </math> 與 <math>(\forall^M x)\mathcal{P} </math>  都是可敘述公式。

這樣依據上列諸類存在公理，就有以下元定理：

{{math_theorem
| name = 類的存在元定理
| math_statement = <br/>
<math>\mathcal{P} </math> 為一條只內含變數 <math>x_1,\,\dots,\,x_n,\,y_1,\,\dots,\,y_m  </math> 的可敘述公式，則有
:<math>\vdash
(\exists s)(\forall^M x_1)\ldots(\forall^M x_n)[
    (\langle x_1,\,\dots,\,x_n\rangle \in s)
    \Leftrightarrow
    \mathcal{P}
]</math>
}}
{| class="mw-collapsible mw-collapsed wikitable"
!'''證明'''
|-
|
|}

== 集合的公理 ==

=== 并集公理 ===
{{math_theorem
| name = <math>(U)</math>
| math_statement = <math>
(\forall^M x)(\exists^M u)(\forall^M a)[
    (a \in u)
    \Leftrightarrow
    (\exists^M \xi \in x)(a \in \xi)
] 
</math>
}}

=== 幂集公理 ===
{{math_theorem
| name = <math>(W)</math>
| math_statement = <math>
(\forall^M x)(\exists^M w)(\forall^M \xi)\{
    (\xi \in w)
    \Leftrightarrow
    (\xi \subseteq x)
\} 
</math>
}}

=== 子集公理 ===
{{math_theorem
| name = <math>(S)</math>
| math_statement = <math>
(\forall^M x)(\forall y)(\exists^M z)(\forall^M a)\{
    (a \in z)
    \Leftrightarrow
    [(a \in x) \wedge (a \in y)]
\} 
</math>
}}
== 無窮公理 ==
{{math_theorem
| name = <math>(I)</math>
| math_statement = <math>
(\exists^M I)\{
    (\varnothing \in I)
    \wedge
    (\forall^M a)[
        (a \in I) \Rightarrow (a \cap \{a\} \in I)
    ]
\}
</math>
}}
== 取代公理及其替代 ==
{{math_theorem
| name = <math>(R)</math>
| math_statement = <math>
Fnc(f)
\Rightarrow
(\forall^M x)(\exists^M r)(\forall^M b)\bigg\{
    (b \in r)
    \Rightarrow
    (\exists^M a)\{
        (\langle a,\,b\rangle \in r)
        \wedge
        (a \in x)
    \}
\bigg\}
</math>
}}

直觀意義為「<math>f</math> 為类函数則對任意集合 <math>x</math> ，存在一個集合 <math>r</math> ，正好就是在 <math>f</math> 的規則下映射出的[[函数#像和原像|像]]」。

=== 大小限制公理 ===
* 对于任何类 ''C''，存在一个集合 ''x'' 使得 <math>Rp(C,x)</math> （謂 ''x'' 是 ''C'' 的表示，即 ''C'' 和 ''x'' 所包含的元素一樣），当且仅当没有在 ''C'' 和所有集合的类 ''V'' 之间的双射。

这个公理贡献自冯·诺伊曼，并一下实现了分离公理、替代公理和全局选择公理。他效力相當於原始的替代公理加上这选择公理。完全的大小限制公理蕴涵了[[全局选择公理]]，因为序数的类不是集合，所以有从序数到全集的双射。

== 選擇公理 ==

== 引用 ==
* {{cite book | author=Bernays, Paul | title=Axiomatic Set Theory | publisher=Dover Publications | year=1991 | id=ISBN 978-0-486-66637-2}}
* [[John von Neumann]], 1925, "An Axiomatization of Set Theory." English translation in [[Jean van Heijenoort]], ed., 1967. ''From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931''. Harvard University Press.
* Mendelson, Elliott, 1997 (1964). ''An Introduction to Mathematical Logic'', 4th ed. Chapman & Hall. The classic textbook treatment of NBG set theory, showing how it can found mathematics.
* [[Richard Montague]], 1961, "Semantic Closure and Non-Finite Axiomatizability I," in ''Infinitistic Methods, Proceedings of the Symposium on Foundations of Mathematics'', (Warsaw, 2-[[9 September]] 1959). Pergamon: 45-69.
* {{planetmathref|id=4395|title= von Neumann-Bernays-Gödel set theory|urlname=vonneumannbernaysgodelsettheory}}

{{集合論}}
[[Category:集合论系统]]