冯诺伊曼-博内斯-哥德尔集合论

Template:NoteTA 冯·诺伊曼-博内斯-哥德尔集合论（Template:Lang-en，Template:Lang）是種以类為直觀動機的一阶公理化集合论，它是配上选择公理的策梅洛-弗兰克尔集合论（Template:Lang-en，Template:Lang）的保守扩展（Template:Lang裡可以證明的定理也都是Template:Lang的定理），而且Template:Lang僅需在一階邏輯基本的公理模式上添加有限数目的公理，但Template:Lang需添加與集合有關的公理模式。

Template:Lang首先由冯·诺伊曼在1920年代提出，從1937年开始由Template:Tsl作修改，在1940年由哥德尔进一步简化。

基本符號

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

以下都把 ${⊢}_{NBG}$ 簡寫為普通的 $⊢$。

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

類與集合

「類」這個名詞在公理化集合论出現之前，通常被理解為「以集合為元素的集合。」或是集合（如等价类）。

但Template:Lang所談及的一切對象（變數和項）都是類。而所謂的集合，是屬於某個類的類，也就是說以下的合式公式（$ℳ$ 來自德语的"集合"「Template:Lang」）式

$ℳ(x):=\mathrm{\exists }y(x\in y)$

可直觀理解為「x是集合」，特別注意到，為了避免跟其他合式公式的變數產生混淆， $y$ 必須是展開 $ℳ(x)$ 時首次出現的變數。反之合式公式

$𝒫𝓇(x):=\mathrm{\neg }ℳ(x)$

可稱為「 $x$ 是真类（Template:Lang）」。

子類

直觀上「x包含於y」意為「所有x的元素a都會屬於y」，以此為動機，Template:Lang有以下的符號簡寫

$x\subseteq y:=\mathrm{\forall }a[(a\in x)\Rightarrow (a\in y)]$

以上可稱為「x包含於y」或「x是y的子類（Template:Lang）」；在 $ℳ(x)$ 和 $ℳ(y)$ 成立的前提下（也就是「x和y都是集合」），可稱為「x是y的子集（Template:Lang）」。

與集合相關的量詞簡寫

仿造量詞的簡寫，對於任意變數 $x$ 與合式公式 $𝒜$ ，可作如下的符號定義

$({\mathrm{\forall }}^{M}x)𝒜:=\mathrm{\forall }x[ℳ(x)\Rightarrow 𝒜]$ （對所有 $x$ ， $x$ 是集合則 $𝒜$ ）

$({\mathrm{\exists }}^{M}x)𝒜:=\mathrm{\exists }x[ℳ(x)\wedge 𝒜]$ （存在 $x$ 不但是集合且 $𝒜$ ）

也有書籍以小寫字母來表示被量化的集合變數，但考慮到一般的非邏輯數學書籍都將大小寫的差異挪作他用，為避免混淆本條目採用以上的上標表示法。

等號公理

看待等號的不同方式

直觀上，兩個集合相等意為「x的元素就是y的元素」，也就是朴素集合论的外延公理，換句話說，可用以下的嚴謹合式公式重寫為

$\mathrm{\forall }a[(a\in x)\iff (a\in y)]$

但一階邏輯的等號可以視為單獨的斷言符號，也可以視為一條複合的合式公式。具體來說，視為一個新的斷言符號 $Q(x,y)$ 並簡記為 $x=y$ 的話，需在Template:Lang內額外添加以下的公理

Template:Math theorem 直觀上可理解為「類x的元素就是類y的元素，等價於類x等於類y」。

但視為一條合式公式，則僅需做以下的符號定義

$(x=y):=\mathrm{\forall }a[(a\in x)\iff (a\in y)]$

不管是何種看待方法，習慣上都會把 $\mathrm{\neg }(x=y)$ 簡記成 $(x\ne y)$ （直觀上的「不相等」）。

等號的良置

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

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

這樣，以下的元定理就確保了如此定義的等號是「成功的」。 Template:Math theorem

證明

以下的證明會逐條檢驗等式定理一節所條列的定義 （E1）： $(x=x)$ 展開來是（或等價於） $\mathrm{\forall }a[(a\in x)\iff (a\in x)]$ 那考慮到恆等關係和(AND)有 $⊢(a\in x)\iff (a\in x)$ 那再套用(GEN)，就會有 $⊢\mathrm{\forall }a[(a\in x)\iff (a\in x)]$ 所以（E1）得證。 （E2）： 因為目前的Template:Lang理論內沒有任何函數符號，所以對變數 $x$ 來說，Template:Lang的原子公式只有 $(x\in z)$ 和 $(z\in x)$ 兩種可能，這樣的話，（E2）等同於要求以下兩式是Template:Lang的定理 (1) $(x=y)\Rightarrow [(x\in z)\Rightarrow (y\in z)]$ (2) $(x=y)\Rightarrow [(z\in x)\Rightarrow (z\in y)]$ 但依據量词公理（A4），(1)可從本節一開始添加的公理（T）所推出；類似地，把 $(x=y)$ 視為斷言符號時，(2)都可以從（T'）配合（A4）推出；若把 $(x=y)$ 視為合式公式的簡寫，(2)也可以用 $(x=y)$ 的定義配上（A4）推出。 （E3）： 本條定義要求以下的合式公式為Template:Lang的定理 $(x=y)\Rightarrow (y=x)$ 從且的交換性有 $⊢(\mathrm{\forall }z)[(z\in x)\iff (z\in y)]\Rightarrow (\mathrm{\forall }z)[(z\in y)\iff (z\in x)]$ 對上式使用(AND)和(D1)就有 $(x=y)⊢(\mathrm{\forall }z)[(z\in y)\iff (z\in x)]$ 再對上面式使用(AND)和(D1)又有 $(x=y)⊢(y=x)$ 所以（E3）的確是Template:Lang的定理。 綜上所述，定理得證。$◻$

真子類

在定義「相等」以後，可以把「相等的類」排除出子類的定義中，換句話說，Template:Lang有以下的符號定義

$x\subset y:=(x\subseteq y)\wedge (x\ne y)$

可直觀理解為「x是y的真子類（Template:Lang），定義為x包含於y且x不等於y」；在 $ℳ(x)$ 和 $ℳ(y)$ 成立的前提下（也就是「x和y都是集合」），可稱為「x是y的真子集（Template:Lang）」。

外延定理

為以下的定理可直觀理解為「x等於y等價於，對所有集合z，z屬於x等價於z屬於y」，也就是說，等於的定義可以「限縮」成元素為集合的狀況。Template:Math theorem

證明

以下取一個不曾出現的變數 $t$ 來展開 $ℳ(z)$ ($\Rightarrow$)$\mathrm{\forall }z(z\in x\iff z\in y)⊢\mathrm{\forall }z\{\mathrm{\exists }t(z\in t)\Rightarrow [(z\in x)\iff (z\in y)]\}$ (1)$\mathrm{\forall }z(z\in x\iff z\in y)$ (Hyp) (2)$z\in x\iff z\in y$ (MP with 1, A4) (3)$\mathrm{\exists }t(z\in t)\Rightarrow [(z\in x)\iff (z\in y)]$ (MP with 2, A1) (4)$\mathrm{\forall }z\{\mathrm{\exists }t(z\in t)\Rightarrow [(z\in x)\iff (z\in y)]\}$ (GEN with 3) ($\Leftarrow$)$\mathrm{\forall }z\{ℳ(z)\Rightarrow [(z\in x)\iff (z\in y)]\}⊢\mathrm{\forall }z(z\in x\iff z\in y)$ $𝒜:=(z\in x)\iff (z\in y)$ (1)$\mathrm{\forall }z[\mathrm{\exists }t(z\in t)\Rightarrow 𝒜]$ (Hyp) (2)$\mathrm{\exists }t(z\in t)\Rightarrow 𝒜$ (MP with A4, 1) (3)$\mathrm{\neg }𝒜\Rightarrow \mathrm{\forall }t[\mathrm{\neg }(z\in t)]$ (MP with T, 2) (4) $\mathrm{\neg }𝒜\Rightarrow [\mathrm{\neg }(z\in t)]$ (D1, with A4, 3) (5)$(z\in t)\Rightarrow [(z\in x)\iff (z\in y)]$ (MP with T, 4) (6)$\mathrm{\forall }t\{(z\in t)\Rightarrow [(z\in x)\iff (z\in y)]\}$ (GEN with 5) (7)$(z\in x)\Rightarrow [(z\in x)\iff (z\in y)]$ (MP with A4, 6) (8)$(z\in y)\Rightarrow [(z\in x)\iff (z\in y)]$ (MP with A4, 6) (9)$(z\in x)\Rightarrow [(z\in x)\Rightarrow (z\in y)]$ (D1 with AND, 7) (10)$(z\in y)\Rightarrow [(z\in y)\Rightarrow (z\in x)]$ (D1 with AND, 8) (11)$(z\in x)\Rightarrow (z\in y)$ (MP twice with A2, I, 9) (12)$(z\in y)\Rightarrow (z\in x)$ (MP twice with A2, I, 10) (13)$(z\in x)\iff (z\in y)$ (AND with 11, 12) (14)$\mathrm{\forall }z(z\in x\iff z\in y)$ (GEN with 13)

引入新的函數符號前，常需要唯一存在性的證明，而外延定理大大簡化了證明的難度。

特定條件下的存在性

以下關於一阶逻辑的一般性定理，也大大簡化了 Template:Lang 引入新公理的過程所需的證明 Template:Math theorem

證明

(1)$𝒜\Rightarrow (\mathrm{\exists }x)ℬ$ (Hyp) (2)$(\mathrm{\forall }x)\{\mathrm{\neg }\{[\mathrm{\neg }𝒜\wedge (x=c)]\vee (𝒜\wedge ℬ)\}\}$ (Hyp) (3)$\mathrm{\neg }\{[\mathrm{\neg }𝒜\wedge (x=c)]\vee (𝒜\wedge ℬ)\}$ (MP with A4, 2) (4)$\mathrm{\neg }[\mathrm{\neg }𝒜\wedge (x=c)]\wedge \mathrm{\neg }(𝒜\wedge ℬ)$ (MP with 3, DIS) (5)$\mathrm{\neg }[\mathrm{\neg }𝒜\wedge (x=c)]$ (MP with AND,4) (6)$\mathrm{\neg }(𝒜\wedge ℬ)$ (MP with AND, 4) (7)$\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }(x=c)$ (MP with DIS, DN 5) (8)$𝒜\Rightarrow \mathrm{\neg }ℬ$ (MP with DIS, DN, 5) (9)$ℬ\Rightarrow \mathrm{\neg }𝒜$ (MP with T, 8) (10)$(\mathrm{\exists }x)ℬ\Rightarrow \mathrm{\neg }𝒜$ (GENe with 9) (11)$𝒜\Rightarrow \mathrm{\neg }(\mathrm{\exists }x)ℬ$ (MP with T, 11) (12)$\mathrm{\neg }𝒜$ (A3' with 1, 11) (13)$\mathrm{\neg }(x=c)$ (MP with 7, 12) (14)$(\mathrm{\forall }x)[\mathrm{\neg }(x=c)]$ (GEN with 13) 再套用一次（DN）也就是 $𝒜\Rightarrow (\mathrm{\exists }x)ℬ⊢(\mathrm{\forall }x)\{\mathrm{\neg }\{[\mathrm{\neg }𝒜\wedge (x=c)]\vee (𝒜\wedge ℬ)\}\}\Rightarrow \mathrm{\neg }(\mathrm{\exists }x)(x=c)$ 但由一阶逻辑的等式性質有 $⊢c=c$ 對上式以變數 $x$ 套用一次(GENe)有 $⊢(\mathrm{\exists }x)(x=c)$ 所以由(C2)本定理就會得證。$◻$

空集合公理

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

事實上這個公理還確保了空集的唯一性，嚴格來說，它確保了： Template:Math theorem

證明

假設 $({\mathrm{\forall }}^{M}y)(y\in ̸x)$ $({\mathrm{\forall }}^{M}y)(y\in ̸t)$ 那根據量词公理的(A4)有 $ℳ(y)\Rightarrow (y\in ̸x)$ $ℳ(y)\Rightarrow (y\in ̸t)$ 另一方面，根據常用的推理性質的(M0)有 $⊢(y\in ̸x)\Rightarrow [(y\in x)\Rightarrow (y\in t)]$ $⊢(y\in ̸t)\Rightarrow [(y\in t)\Rightarrow (y\in x)]$ 這樣根據演繹定理的推論(D1)有 $ℳ(y)\Rightarrow [(y\in x)\Rightarrow (y\in t)]$ $ℳ(y)\Rightarrow [(y\in t)\Rightarrow (y\in x)]$ 這樣根據常用的推理性質(T)有 $\mathrm{\neg }[(y\in x)\Rightarrow (y\in t)]\Rightarrow \mathrm{\neg }ℳ(y)$ $\mathrm{\neg }[(y\in t)\Rightarrow (y\in x)]\Rightarrow \mathrm{\neg }ℳ(y)$ 這樣根據德摩根定律和邏輯與的(DisJ)有 $\mathrm{\neg }\{[(y\in x)\Rightarrow (y\in t)]\wedge [(y\in t)\Rightarrow (y\in x)]\}\Rightarrow \mathrm{\neg }ℳ(y)$ 這樣再根據(T)有 $ℳ(y)\Rightarrow [(y\in x)\iff (y\in t)]$ 這樣根據普遍化有 $({\mathrm{\forall }}^{M}y)[(y\in x)\iff (y\in t)]$ 那這樣根據上節的外延定理有 $x=t$ 換句話說 $⊢[({\mathrm{\forall }}^{M}y)(y\in ̸x)\wedge ({\mathrm{\forall }}^{M}y)(y\in ̸t)]\Rightarrow (x=t)$ 這樣根據邏輯與的直觀性質和(D1)有 $⊢\{[ℳ(x)\wedge ({\mathrm{\forall }}^{M}y)(y\in ̸x)]\wedge [ℳ(t)\wedge ({\mathrm{\forall }}^{M}y)(y\in ̸t)]\}\Rightarrow (x=t)$ 這樣根據普遍化有 $⊢(\mathrm{\forall }x)(\mathrm{\forall }t)\{\{[ℳ(x)\wedge ({\mathrm{\forall }}^{M}y)(y\in ̸x)]\wedge [ℳ(t)\wedge ({\mathrm{\forall }}^{M}y)(y\in ̸t)]\}\Rightarrow (x=t)\}$ 再綜合本節的空集合公理（N），本定理就得証了。$◻$

也就是直觀上，「空集是唯一存在的」，這樣根據函數符號與唯一性一節，可以在Template:Lang加入新的常數符號 $\varnothing$ 和以下的新公理（嚴格來說，把完全沒有函數符號和常數符號的Template:Lang擴展成有 $\varnothing$ 的新Template:Lang，但兩個理論是等效的）

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

配對公理

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

這個公理還確保了以下的唯一性： Template:Math theorem

證明

根據量詞的簡寫，配對公理(P)等價於 $(\mathrm{\forall }x)(\mathrm{\forall }y)\{ℳ(x)\wedge ℳ(y)\Rightarrow (\mathrm{\exists }p)\{ℳ(p)\wedge ({\mathrm{\forall }}^{M}z)\{(z\in p)\iff [(z=x)\vee (z=y)]\}\left\}\right\}$ 這樣對上式套用兩次量词公理的(A4)有 $ℳ(x)\wedge ℳ(y)\Rightarrow (\mathrm{\exists }p)\{ℳ(p)\wedge ({\mathrm{\forall }}^{M}z)\{(z\in p)\iff [(z=x)\vee (z=y)]\}\}$ 這樣在有 $ℳ(x)\wedge ℳ(y)$ 的前提就有 $(\mathrm{\exists }p)\{ℳ(p)\wedge ({\mathrm{\forall }}^{M}z)\{(z\in p)\iff [(z=x)\vee (z=y)]\}\}$ 所以 $ℳ(x)\wedge ℳ(y)⊢(\mathrm{\exists }p)\{ℳ(p)\wedge ({\mathrm{\forall }}^{M}z)\{(z\in p)\iff [(z=x)\vee (z=y)]\}\}$ 另一方面，若假設 $ℳ(p)\wedge ({\mathrm{\forall }}^{M}z)\{(z\in p)\iff [(z=x)\vee (z=y)]\}$ $ℳ(\pi )\wedge ({\mathrm{\forall }}^{M}z)\{(z\in \pi )\iff [(z=x)\vee (z=y)]\}$ 這樣根據邏輯與的直觀性質有 $({\mathrm{\forall }}^{M}z)\{(z\in p)\iff [(z=x)\vee (z=y)]\}$ $({\mathrm{\forall }}^{M}z)\{(z\in \pi )\iff [(z=x)\vee (z=y)]\}$ 再根據(A4)有 $ℳ(z)\Rightarrow \{(z\in p)\iff [(z=x)\vee (z=y)]\}$ $ℳ(z)\Rightarrow \{(z\in \pi )\iff [(z=x)\vee (z=y)]\}$ 如果再假設 $ℳ(z)$ ，根據MP律有 $(z\in p)\iff [(z=x)\vee (z=y)]$ $(z\in \pi )\iff [(z=x)\vee (z=y)]$ 這樣根據演繹定理的推論(D1)和邏輯與的直觀性質有 $(z\in p)\iff (z\in \pi )$ 也就是說 $ℬ(p)\wedge ℬ(\pi ),ℳ(z)⊢(z\in p)\iff (z\in \pi )$ 其中 $ℬ(p):=ℳ(p)\wedge ({\mathrm{\forall }}^{M}z)\{(z\in p)\iff [(z=x)\vee (z=y)]\}$ 因為變數 $z$ 在 $ℬ(p)$ 和 $ℬ(\pi )$ 內完全不自由，對上式套用演繹定理(D)將 $ℳ(z)$ 移到右方後，再對 $z$ 套用普遍化會有 $ℬ(p)\wedge ℬ(\pi )⊢({\mathrm{\forall }}^{M}z)[(z\in p)\iff (z\in \pi )]$ 這樣根據本條目的外延定理有 $ℬ(p)\wedge ℬ(\pi )⊢(p=\pi )$ 那以演繹定理(D)將 $ℬ(p)\wedge ℬ(\pi )$ 移到右方，然後接連對 $p$ 和 $\pi$ 使用普遍化有 $⊢(\mathrm{\forall }p)(\mathrm{\forall }\pi )[ℬ(p)\wedge ℬ(\pi )\Rightarrow (p=\pi )]$ 故本定理得証。$◻$

這樣的話會有 Template:Math theorem

證明

根據（P-1）和本條目的特定條件下的存在性(DC)會有 （P-2）$⊢(\mathrm{\exists }p)\{\{\mathrm{\neg }[ℳ(x)\wedge ℳ(y)]\wedge (p=\varnothing )\}\vee \{ℳ(x)\wedge ℳ(y)\wedge ℳ(p)\wedge ({\mathrm{\forall }}^{M}z)\{(z\in p)\iff [(z=x)\vee (z=y)]\}\left\}\right\}$ 設 $𝒜(p):=\mathrm{\neg }[ℳ(x)\wedge ℳ(y)]\wedge (p=\varnothing )$ $ℬ(p):=ℳ(x)\wedge ℳ(y)\wedge ℳ(p)\wedge ({\mathrm{\forall }}^{M}z)\{(z\in p)\iff [(z=x)\vee (z=y)]\}$ $𝒞:=ℳ(x)\wedge ℳ(y)$ 那連續套用邏輯與合邏輯或的分配律與邏輯與的交換性會有 $⊢\{[𝒜(p)\vee ℬ(p)]\wedge [𝒜(\pi )\vee ℬ(\pi )]\}\iff \{\{[𝒜(p)\wedge 𝒜(\pi )]\vee [ℬ(p)\wedge 𝒜(\pi )]\}\vee \{[𝒜(p)\wedge ℬ(\pi )]\vee [ℬ(p)\wedge ℬ(\pi )]\}\}$ 但考慮到邏輯與的直觀性質和逻辑與的定義有 $⊢[ℬ(p)\wedge 𝒜(\pi )]\Rightarrow (\mathrm{\neg }𝒞\wedge 𝒞)$ $⊢[𝒜(p)\wedge ℬ(\pi )]\Rightarrow (\mathrm{\neg }𝒞\wedge 𝒞)$ $⊢(\mathrm{\neg }𝒞\wedge 𝒞)\iff \mathrm{\neg }(𝒞\Rightarrow 𝒞)$ 那根據恆等關係$(I)$和常用的推理性質(T)有 $⊢\mathrm{\neg }[ℬ(p)\wedge 𝒜(\pi )]$ $⊢\mathrm{\neg }[𝒜(p)\wedge ℬ(\pi )]$ 所以根據逻辑或的定義來重複使用演繹定理的推論(D1)會有 $⊢\{[𝒜(p)\vee ℬ(p)]\wedge [𝒜(\pi )\vee ℬ(\pi )]\}\iff \{[𝒜(p)\wedge 𝒜(\pi )]\vee [ℬ(p)\wedge ℬ(\pi )]\}$ 然後從Template:Lang的等式定理會有 $⊢[𝒜(p)\wedge 𝒜(\pi )]\Rightarrow (p=\pi )$ 另一方面，根據（P-1）有 $⊢[ℬ(p)\wedge ℬ(\pi )]\Rightarrow (p=\pi )$ 這樣結合邏輯與的(DisJ)有 $⊢\{[𝒜(p)\vee ℬ(p)]\wedge [𝒜(\pi )\vee ℬ(\pi )]\}\Rightarrow (p=\pi )$ 再對 $p$ 和 $\pi$ 套用普遍化有 $⊢(\mathrm{\forall }p)(\mathrm{\forall }\pi )\{\{[𝒜(p)\vee ℬ(p)]\wedge [𝒜(\pi )\vee ℬ(\pi )]\}\Rightarrow (p=\pi )\}$ 這樣結合剛剛的（P-2）與邏輯與的直觀性質，本定理就得證了。$◻$

所以根據函數符號與唯一性一節，可以在Template:Lang加入新的雙元函數符號 $f_p^2(x,y)$（簡記為 $\{x,y\}$ ）和以下的新公理

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

有序對

$\{x\}:=\{x,x\}$

$⟨x⟩:=x$

$⟨x,y⟩:=\{\{x\},\{x,y\}\}$

$⟨x_1,\dots ,x_n,x_{n+1}⟩:=⟨⟨x_1,\dots ,x_n⟩,x_{n+1}⟩$

在不跟括弧產生混淆的情況下，也可以把$⟨x_1,\dots ,x_n,x_{n+1}⟩$記為$(x_1,\dots ,x_n,x_{n+1})$。

關係

$Rel(f):=({\mathrm{\forall }}^{M}a)\{(a\in f)\Rightarrow (\mathrm{\exists }x)(\mathrm{\exists }y)\{ℳ(x)\wedge ℳ(y)\wedge [a=(x,y)]\}\}$

类函數

$Fnc(f):=Rel(f)\wedge ({\mathrm{\forall }}^{M}x)({\mathrm{\forall }}^{M}y)({\mathrm{\forall }}^M\upsilon )\{[(x,y)\in f\wedge (x,\upsilon )\in f]\Rightarrow (y=\upsilon )\}$

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

类的存在公理

類的存在元定理

這個元定理對應到ZFC尔集合论的分類公理。

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

• 對任意變數 $x$ 和 $y$ ，$x\in y$ 為可敘述公式。
• 若 $𝒫$ 與 $𝒬$ 為可敘述公式， $x$ 為任意變數，則 $(\mathrm{\neg }𝒫)$ 、 $(𝒫\Rightarrow 𝒬)$ 與 $({\mathrm{\forall }}^{M}x)𝒫$ 都是可敘述公式。

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

證明

取代公理及其替代

直觀意義為「$f$ 為类函数則對任意集合 $x$ ，存在一個集合 $r$ ，正好就是在 $f$ 的規則下映射出的像」。

大小限制公理

• 对于任何类 C，存在一个集合 x 使得 $Rp(C,x)$ （謂 x 是 C 的表示，即 C 和 x 所包含的元素一樣），当且仅当没有在 C 和所有集合的类 V 之间的双射。

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

引用

• Template:Cite book
• 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.
• Template:Planetmathref