冯·诺伊曼-博内斯-哥德尔集合论 （英語：von Neumann–Bernays–Gödel Set Theory ，NBG 类 為直觀動機的一阶 公理化集合论 ，它是配上选择公理 的策梅洛-弗兰克尔集合论 （英語：Zermelo-Fraenkel Set Theory with the axiom of Choice ，ZFC 保守扩展 （ZFC 定理 也都是NBG [ 1] NBG 公理模式 上添加有限数目的公理，但ZFC [ 2]
NBG 冯·诺伊曼 在1920年代提出，從1937年开始由保罗·博内斯 哥德尔 进一步简化。
在NBG 斷言符號
P
(
x
,
y
)
{\displaystyle P(x,\,y)}
P
(
x
,
y
)
{\displaystyle P(x,\,y)}
x
∈
y
{\displaystyle x\in y}
P
(
x
,
y
)
{\displaystyle P(x,\,y)}
¬
P
(
x
,
y
)
{\displaystyle \neg P(x,\,y)}
x
∉
y
{\displaystyle x\notin y}
以下都把
⊢
N
B
G
{\displaystyle \vdash _{NBG}}
⊢
{\displaystyle \vdash }
本條目定理的證明會頻繁引用一階邏輯的定理，定理的代號可以參見一阶逻辑#常用的推理性質 一節。
「類」這個名詞在公理化集合论 出現之前，通常被理解為「以集合 為元素 的集合。」或是集合（如等价类 ）。
但NBG 項 ）都是類 。而所謂的集合，是屬於某個類的類 ，也就是說以下的合式公式 （
M
{\displaystyle {\mathcal {M}}}
德语 的"集合"「Menge 」）式
M
(
x
)
:=
∃
y
(
x
∈
y
)
{\displaystyle {\mathcal {M}}(x):=\exists y(x\in y)}
可直觀理解為「x是集合」，特別注意到，為了避免跟其他合式公式的變數產生混淆，
y
{\displaystyle y}
M
(
x
)
{\displaystyle {\mathcal {M}}(x)}
P
r
(
x
)
:=
¬
M
(
x
)
{\displaystyle {\mathcal {Pr}}(x):=\neg {\mathcal {M}}(x)}
可稱為「
x
{\displaystyle x}
真类 （proper class
直觀上「x包含於y」意為「所有x的元素a都會屬於y」，以此為動機，NBG
x
⊆
y
:=
∀
a
[
(
a
∈
x
)
⇒
(
a
∈
y
)
]
{\displaystyle x\subseteq y:=\forall a[\,(a\in x)\Rightarrow (a\in y)\,]}
以上可稱為「x包含於y」或「x是y的子類 （subclass
M
(
x
)
{\displaystyle {\mathcal {M}}(x)}
M
(
y
)
{\displaystyle {\mathcal {M}}(y)}
子集 （subset
仿造量詞的簡寫 ，對於任意變數
x
{\displaystyle x}
A
{\displaystyle {\mathcal {A}}}
(
∀
M
x
)
A
:=
∀
x
[
M
(
x
)
⇒
A
]
{\displaystyle ({\forall }^{M}x){\mathcal {A}}:=\forall x[\,{\mathcal {M}}(x)\Rightarrow {\mathcal {A}}\,]}
x
{\displaystyle x}
x
{\displaystyle x}
A
{\displaystyle {\mathcal {A}}}
(
∃
M
x
)
A
:=
∃
x
[
M
(
x
)
∧
A
]
{\displaystyle ({\exists }^{M}x){\mathcal {A}}:=\exists x[\,{\mathcal {M}}(x)\wedge {\mathcal {A}}\,]}
x
{\displaystyle x}
A
{\displaystyle {\mathcal {A}}}
也有書籍以小寫字母來表示被量化的集合變數[ 3]
直觀上，兩個集合相等意為「x的元素就是y的元素」，也就是朴素集合论 的外延公理 ，換句話說，可用以下的嚴謹合式公式重寫為
∀
a
[
(
a
∈
x
)
⇔
(
a
∈
y
)
]
{\displaystyle \forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}
但一階邏輯的等號可以視為單獨的斷言符號 ，也可以視為一條複合的合式公式。具體來說，視為一個新的斷言符號
Q
(
x
,
y
)
{\displaystyle Q(x,\,y)}
x
=
y
{\displaystyle x=y}
NBG
(
T
′
)
{\displaystyle (T^{\prime })}
—
(
x
=
y
)
⇔
∀
a
[
(
a
∈
x
)
⇔
(
a
∈
y
)
]
{\displaystyle (x=y)\Leftrightarrow \forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}
直觀上可理解為「類x的元素就是類y的元素，等價於類x等於類y」。
但視為一條合式公式，則僅需做以下的符號定義
(
x
=
y
)
:=
∀
a
[
(
a
∈
x
)
⇔
(
a
∈
y
)
]
{\displaystyle (x=y):=\forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}
不管是何種看待方法，習慣上都會把
¬
(
x
=
y
)
{\displaystyle \neg (x=y)}
(
x
≠
y
)
{\displaystyle (x\neq y)}
為了確保
(
x
=
y
)
{\displaystyle (x=y)}
(
T
)
{\displaystyle (T)}
—
(
x
=
y
)
⇒
∀
z
[
(
x
∈
z
)
⇔
(
y
∈
z
)
]
{\displaystyle (x=y)\Rightarrow \forall z[\,(x\in z)\Leftrightarrow (y\in z)\,]}
直觀上，這個公理確保「x等於y，則x屬於z等同於y屬於z」。
這樣，以下的元定理 就確保了如此定義的等號是「成功的」。
元定理 — NBG
(
x
=
y
)
{\displaystyle (x=y)}
一阶逻辑 理論
證明
以下的證明會逐條檢驗等式定理一節 所條列的定義
（E1）：
(
x
=
x
)
{\displaystyle (x=x)}
∀
a
[
(
a
∈
x
)
⇔
(
a
∈
x
)
]
{\displaystyle \forall a[\,(a\in x)\Leftrightarrow (a\in x)\,]}
那考慮到恆等關係 和(AND) 有
⊢
(
a
∈
x
)
⇔
(
a
∈
x
)
{\displaystyle \vdash (a\in x)\Leftrightarrow (a\in x)}
那再套用(GEN) ，就會有
⊢
∀
a
[
(
a
∈
x
)
⇔
(
a
∈
x
)
]
{\displaystyle \vdash \forall a[\,(a\in x)\Leftrightarrow (a\in x)\,]}
所以（E1）得證。
（E2）：
因為目前的NBG 函數符號 ，所以對變數
x
{\displaystyle x}
NBG 原子公式 只有
(
x
∈
z
)
{\displaystyle (x\in z)}
(
z
∈
x
)
{\displaystyle (z\in x)}
NBG
(1)
(
x
=
y
)
⇒
[
(
x
∈
z
)
⇒
(
y
∈
z
)
]
{\displaystyle (x=y)\Rightarrow [\,(x\in z)\Rightarrow (y\in z)\,]}
(2)
(
x
=
y
)
⇒
[
(
z
∈
x
)
⇒
(
z
∈
y
)
]
{\displaystyle (x=y)\Rightarrow [\,(z\in x)\Rightarrow (z\in y)\,]}
但依據量词公理 （A4），(1)可從本節一開始添加的公理（T）所推出；類似地，把
(
x
=
y
)
{\displaystyle (x=y)}
(
x
=
y
)
{\displaystyle (x=y)}
(
x
=
y
)
{\displaystyle (x=y)}
（E3）：
本條定義要求以下的合式公式為NBG
(
x
=
y
)
⇒
(
y
=
x
)
{\displaystyle (x=y)\Rightarrow (y=x)}
從且的交換性 有
⊢
(
∀
z
)
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
⇒
(
∀
z
)
[
(
z
∈
y
)
⇔
(
z
∈
x
)
]
{\displaystyle \vdash (\forall z)[(z\in x)\Leftrightarrow (z\in y)]\Rightarrow (\forall z)[(z\in y)\Leftrightarrow (z\in x)]}
對上式使用(AND) 和(D1) 就有
(
x
=
y
)
⊢
(
∀
z
)
[
(
z
∈
y
)
⇔
(
z
∈
x
)
]
{\displaystyle (x=y)\vdash (\forall z)[(z\in y)\Leftrightarrow (z\in x)]}
再對上面式使用(AND) 和(D1) 又有
(
x
=
y
)
⊢
(
y
=
x
)
{\displaystyle (x=y)\vdash (y=x)}
所以（E3）的確是NBG
綜上所述，定理得證。
◻
{\displaystyle \Box }
在定義「相等」以後，可以把「相等的類」排除出子類的定義中，換句話說，NBG
x
⊂
y
:=
(
x
⊆
y
)
∧
(
x
≠
y
)
{\displaystyle x\subset y:=(x\subseteq y)\wedge (x\neq y)}
可直觀理解為「x是y的真子類 （proper subclass
M
(
x
)
{\displaystyle {\mathcal {M}}(x)}
M
(
y
)
{\displaystyle {\mathcal {M}}(y)}
真子集 （proper subset
為以下的定理可直觀理解為「x等於y等價於，對所有集合z，z屬於x等價於z屬於y」，也就是說，等於的定義可以「限縮」成元素為集合的狀況。
外延定理 —
⊢
(
x
=
y
)
⇔
(
∀
M
z
)
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
{\displaystyle \vdash (x=y)\Leftrightarrow (\forall ^{M}z)[\,(z\in x)\Leftrightarrow (z\in y)\,]}
證明
以下取一個不曾出現的變數
t
{\displaystyle t}
M
(
z
)
{\displaystyle {\mathcal {M}}(z)}
(
⇒
{\displaystyle \Rightarrow }
∀
z
(
z
∈
x
⇔
z
∈
y
)
⊢
∀
z
{
∃
t
(
z
∈
t
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
}
{\displaystyle \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)]\}}
(1)
∀
z
(
z
∈
x
⇔
z
∈
y
)
{\displaystyle \forall z(z\in x\Leftrightarrow z\in y)}
(2)
z
∈
x
⇔
z
∈
y
{\displaystyle z\in x\Leftrightarrow z\in y}
(3)
∃
t
(
z
∈
t
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
{\displaystyle \exists t(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}
(4)
∀
z
{
∃
t
(
z
∈
t
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
}
{\displaystyle \forall z\{\exists t(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}}
(
⇐
{\displaystyle \Leftarrow }
∀
z
{
M
(
z
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
}
⊢
∀
z
(
z
∈
x
⇔
z
∈
y
)
{\displaystyle \forall z\{{\mathcal {M}}(z)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}\vdash \forall z(z\in x\Leftrightarrow z\in y)}
A
:=
(
z
∈
x
)
⇔
(
z
∈
y
)
{\displaystyle {\mathcal {A}}:=(z\in x)\Leftrightarrow (z\in y)}
(1)
∀
z
[
∃
t
(
z
∈
t
)
⇒
A
]
{\displaystyle \forall z[\exists t(z\in t)\Rightarrow {\mathcal {A}}]}
(2)
∃
t
(
z
∈
t
)
⇒
A
{\displaystyle \exists t(z\in t)\Rightarrow {\mathcal {A}}}
(3)
¬
A
⇒
∀
t
[
¬
(
z
∈
t
)
]
{\displaystyle \neg {\mathcal {A}}\Rightarrow \forall t[\neg (z\in t)]}
(4)
¬
A
⇒
[
¬
(
z
∈
t
)
]
{\displaystyle \neg {\mathcal {A}}\Rightarrow [\neg (z\in t)]}
(5)
(
z
∈
t
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
{\displaystyle (z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}
(6)
∀
t
{
(
z
∈
t
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
}
{\displaystyle \forall t\{(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}}
(7)
(
z
∈
x
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
{\displaystyle (z\in x)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}
(8)
(
z
∈
y
)
⇒
[
(
z
∈
x
)
⇔
(
z
∈
y
)
]
{\displaystyle (z\in y)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}
(9)
(
z
∈
x
)
⇒
[
(
z
∈
x
)
⇒
(
z
∈
y
)
]
{\displaystyle (z\in x)\Rightarrow [(z\in x)\Rightarrow (z\in y)]}
(10)
(
z
∈
y
)
⇒
[
(
z
∈
y
)
⇒
(
z
∈
x
)
]
{\displaystyle (z\in y)\Rightarrow [(z\in y)\Rightarrow (z\in x)]}
(11)
(
z
∈
x
)
⇒
(
z
∈
y
)
{\displaystyle (z\in x)\Rightarrow (z\in y)}
(12)
(
z
∈
y
)
⇒
(
z
∈
x
)
{\displaystyle (z\in y)\Rightarrow (z\in x)}
(13)
(
z
∈
x
)
⇔
(
z
∈
y
)
{\displaystyle (z\in x)\Leftrightarrow (z\in y)}
(14)
∀
z
(
z
∈
x
⇔
z
∈
y
)
{\displaystyle \forall z(z\in x\Leftrightarrow z\in y)}
引入新的函數符號前，常需要唯一存在性 的證明，而外延定理大大簡化了證明的難度。
以下關於一阶逻辑 的一般性定理，也大大簡化了 NBG
（DC, Definition under certain condition） —
x
{\displaystyle x}
合式公式
A
{\displaystyle {\mathcal {A}}}
c
{\displaystyle c}
常數符號 。若
A
⊢
(
∃
x
)
B
{\displaystyle {\mathcal {A}}\vdash (\exists x){\mathcal {B}}}
則有
⊢
(
∃
x
)
{
[
¬
A
∧
(
x
=
c
)
]
∨
(
A
∧
B
)
}
{\displaystyle \vdash (\exists x)\{\,[\,\neg {\mathcal {A}}\wedge (x=c)\,]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\,\}}
證明
(1)
A
⇒
(
∃
x
)
B
{\displaystyle {\mathcal {A}}\Rightarrow (\exists x){\mathcal {B}}}
(2)
(
∀
x
)
{
¬
{
[
¬
A
∧
(
x
=
c
)
]
∨
(
A
∧
B
)
}
}
{\displaystyle (\forall x)\{\neg \{[\neg {\mathcal {A}}\wedge (x=c)]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\}\}}
(3)
¬
{
[
¬
A
∧
(
x
=
c
)
]
∨
(
A
∧
B
)
}
{\displaystyle \neg \{[\neg {\mathcal {A}}\wedge (x=c)]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\}}
(4)
¬
[
¬
A
∧
(
x
=
c
)
]
∧
¬
(
A
∧
B
)
{\displaystyle \neg [\neg {\mathcal {A}}\wedge (x=c)]\wedge \neg ({\mathcal {A}}\wedge {\mathcal {B}})}
(5)
¬
[
¬
A
∧
(
x
=
c
)
]
{\displaystyle \neg [\neg {\mathcal {A}}\wedge (x=c)]}
(6)
¬
(
A
∧
B
)
{\displaystyle \neg ({\mathcal {A}}\wedge {\mathcal {B}})}
(7)
¬
A
⇒
¬
(
x
=
c
)
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg (x=c)}
(8)
A
⇒
¬
B
{\displaystyle {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
(9)
B
⇒
¬
A
{\displaystyle {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}
(10)
(
∃
x
)
B
⇒
¬
A
{\displaystyle (\exists x){\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}
(11)
A
⇒
¬
(
∃
x
)
B
{\displaystyle {\mathcal {A}}\Rightarrow \neg (\exists x){\mathcal {B}}}
(12)
¬
A
{\displaystyle \neg {\mathcal {A}}}
(13)
¬
(
x
=
c
)
{\displaystyle \neg (x=c)}
(14)
(
∀
x
)
[
¬
(
x
=
c
)
]
{\displaystyle (\forall x)[\neg (x=c)]}
再套用一次（DN）也就是
A
⇒
(
∃
x
)
B
⊢
(
∀
x
)
{
¬
{
[
¬
A
∧
(
x
=
c
)
]
∨
(
A
∧
B
)
}
}
⇒
¬
(
∃
x
)
(
x
=
c
)
{\displaystyle {\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)}
但由一阶逻辑的等式性質 有
⊢
c
=
c
{\displaystyle \vdash c=c}
對上式以變數
x
{\displaystyle x}
⊢
(
∃
x
)
(
x
=
c
)
{\displaystyle \vdash (\exists x)(x=c)}
所以由(C2)本定理就會得證。
◻
{\displaystyle \Box }
(
N
)
{\displaystyle (N)}
—
(
∃
M
x
)
(
∀
M
y
)
(
y
∉
x
)
{\displaystyle ({\exists }^{M}x)({\forall }^{M}y)(y\not \in x)}
這個公理的直觀意思是「存在集合x，使的所有集合y都不屬於x」。
事實上這個公理還確保了空集 的唯一性，嚴格來說，它確保了：
定理 —
⊢
(
∃
!
x
)
[
M
(
x
)
∧
(
∀
M
y
)
(
y
∉
x
)
]
{\displaystyle \vdash (\exists !x)[\,{\mathcal {M}}(x)\wedge ({\forall }^{M}y)(y\not \in x)\,]}
證明
假設
(
∀
M
y
)
(
y
∉
x
)
{\displaystyle ({\forall }^{M}y)(y\not \in x)}
(
∀
M
y
)
(
y
∉
t
)
{\displaystyle ({\forall }^{M}y)(y\not \in t)}
那根據量词公理 的(A4)有
M
(
y
)
⇒
(
y
∉
x
)
{\displaystyle {\mathcal {M}}(y)\Rightarrow (y\not \in x)}
M
(
y
)
⇒
(
y
∉
t
)
{\displaystyle {\mathcal {M}}(y)\Rightarrow (y\not \in t)}
另一方面，根據常用的推理性質 的(M0)有
⊢
(
y
∉
x
)
⇒
[
(
y
∈
x
)
⇒
(
y
∈
t
)
]
{\displaystyle \vdash (y\not \in x)\Rightarrow [\,(y\in x)\Rightarrow (y\in t)\,]}
⊢
(
y
∉
t
)
⇒
[
(
y
∈
t
)
⇒
(
y
∈
x
)
]
{\displaystyle \vdash (y\not \in t)\Rightarrow [\,(y\in t)\Rightarrow (y\in x)\,]}
這樣根據演繹定理 的推論(D1)有
M
(
y
)
⇒
[
(
y
∈
x
)
⇒
(
y
∈
t
)
]
{\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in x)\Rightarrow (y\in t)\,]}
M
(
y
)
⇒
[
(
y
∈
t
)
⇒
(
y
∈
x
)
]
{\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in t)\Rightarrow (y\in x)\,]}
這樣根據常用的推理性質 (T)有
¬
[
(
y
∈
x
)
⇒
(
y
∈
t
)
]
⇒
¬
M
(
y
)
{\displaystyle \neg [\,(y\in x)\Rightarrow (y\in t)\,]\Rightarrow \neg {\mathcal {M}}(y)}
¬
[
(
y
∈
t
)
⇒
(
y
∈
x
)
]
⇒
¬
M
(
y
)
{\displaystyle \neg [\,(y\in t)\Rightarrow (y\in x)\,]\Rightarrow \neg {\mathcal {M}}(y)}
這樣根據德摩根定律 和邏輯與 的(DisJ)有
¬
{
[
(
y
∈
x
)
⇒
(
y
∈
t
)
]
∧
[
(
y
∈
t
)
⇒
(
y
∈
x
)
]
}
⇒
¬
M
(
y
)
{\displaystyle \neg \{\,[\,(y\in x)\Rightarrow (y\in t)\,]\wedge [\,(y\in t)\Rightarrow (y\in x)\,]\,\}\Rightarrow \neg {\mathcal {M}}(y)}
這樣再根據(T)有
M
(
y
)
⇒
[
(
y
∈
x
)
⇔
(
y
∈
t
)
]
{\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in x)\Leftrightarrow (y\in t)\,]}
這樣根據普遍化 有
(
∀
M
y
)
[
(
y
∈
x
)
⇔
(
y
∈
t
)
]
{\displaystyle (\forall ^{M}y)[\,(y\in x)\Leftrightarrow (y\in t)\,]}
那這樣根據上節的外延定理 有
x
=
t
{\displaystyle x=t}
換句話說
⊢
[
(
∀
M
y
)
(
y
∉
x
)
∧
(
∀
M
y
)
(
y
∉
t
)
]
⇒
(
x
=
t
)
{\displaystyle \vdash [\,({\forall }^{M}y)(y\not \in x)\wedge ({\forall }^{M}y)(y\not \in t)\,]\Rightarrow (x=t)}
這樣根據邏輯與的直觀性質 和(D1)有
⊢
{
[
M
(
x
)
∧
(
∀
M
y
)
(
y
∉
x
)
]
∧
[
M
(
t
)
∧
(
∀
M
y
)
(
y
∉
t
)
]
}
⇒
(
x
=
t
)
{\displaystyle \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)}
這樣根據普遍化 有
⊢
(
∀
x
)
(
∀
t
)
{
{
[
M
(
x
)
∧
(
∀
M
y
)
(
y
∉
x
)
]
∧
[
M
(
t
)
∧
(
∀
M
y
)
(
y
∉
t
)
]
}
⇒
(
x
=
t
)
}
{\displaystyle \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 \}}}
再綜合本節的空集合公理（N），本定理就得証了。
◻
{\displaystyle \Box }
也就是直觀上，「空集 是唯一存在的」，這樣根據函數符號與唯一性 一節，可以在NBG
∅
{\displaystyle \varnothing }
NBG
∅
{\displaystyle \varnothing }
NBG
(
N
′
)
{\displaystyle (N^{\prime })}
—
M
(
∅
)
∧
(
∀
M
y
)
(
y
∉
∅
)
{\displaystyle {\mathcal {M}}(\varnothing )\wedge ({\forall }^{M}y)(y\not \in \varnothing )}
這個新公理直觀上以「
∅
{\displaystyle \varnothing }
∅
{\displaystyle \varnothing }
∅
{\displaystyle \varnothing }
空集 的表示符號。
(
P
)
{\displaystyle (P)}
—
(
∀
M
x
)
(
∀
M
y
)
(
∃
M
p
)
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle ({\forall }^{M}x)({\forall }^{M}y)({\exists }^{M}p)({\forall }^{M}z)\{(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\}}
這個公理的直觀意思是「對所有集合x和集合y，存在一個僅以x跟y為元素的集合p」。
這個公理還確保了以下的唯一性：
定理（P-1） —
M
(
x
)
∧
M
(
y
)
⊢
(
∃
!
p
)
{
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
{\displaystyle {\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 \}}}
證明
根據量詞的簡寫 ，配對公理(P)等價於
(
∀
x
)
(
∀
y
)
{
M
(
x
)
∧
M
(
y
)
⇒
(
∃
p
)
{
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
}
{\displaystyle (\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 \}}}
這樣對上式套用兩次量词公理 的(A4)有
M
(
x
)
∧
M
(
y
)
⇒
(
∃
p
)
{
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
{\displaystyle {\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 \}}}
這樣在有
M
(
x
)
∧
M
(
y
)
{\displaystyle {\mathcal {M}}(x)\wedge {\mathcal {M}}(y)}
(
∃
p
)
{
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
{\displaystyle (\exists p){\big \{}\,{\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}\,{\big \}}}
所以
M
(
x
)
∧
M
(
y
)
⊢
(
∃
p
)
{
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
{\displaystyle {\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 \}}}
另一方面，若假設
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
M
(
π
)
∧
(
∀
M
z
)
{
(
z
∈
π
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\mathcal {M}}(\pi )\wedge ({\forall }^{M}z)\{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
這樣根據邏輯與的直觀性質 有
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
(
∀
M
z
)
{
(
z
∈
π
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle ({\forall }^{M}z)\{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
再根據(A4)有
M
(
z
)
⇒
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\mathcal {M}}(z)\Rightarrow \{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
M
(
z
)
⇒
{
(
z
∈
π
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\mathcal {M}}(z)\Rightarrow \{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
如果再假設
M
(
z
)
{\displaystyle {\mathcal {M}}(z)}
MP律 有
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
{\displaystyle (z\in p)\Leftrightarrow [(z=x)\vee (z=y)]}
(
z
∈
π
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
{\displaystyle (z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]}
這樣根據演繹定理 的推論(D1)和邏輯與的直觀性質 有
(
z
∈
p
)
⇔
(
z
∈
π
)
{\displaystyle (z\in p)\Leftrightarrow (z\in \pi )}
也就是說
B
(
p
)
∧
B
(
π
)
,
M
(
z
)
⊢
(
z
∈
p
)
⇔
(
z
∈
π
)
{\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi ),\,{\mathcal {M}}(z)\,\vdash \,(z\in p)\Leftrightarrow (z\in \pi )}
其中
B
(
p
)
:=
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\mathcal {B}}(p):={\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}
因為變數
z
{\displaystyle z}
B
(
p
)
{\displaystyle {\mathcal {B}}(p)}
B
(
π
)
{\displaystyle {\mathcal {B}}(\pi )}
演繹定理 (D)將
M
(
z
)
{\displaystyle {\mathcal {M}}(z)}
z
{\displaystyle z}
普遍化 會有
B
(
p
)
∧
B
(
π
)
⊢
(
∀
M
z
)
[
(
z
∈
p
)
⇔
(
z
∈
π
)
]
{\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,\vdash \,(\forall ^{M}z)[\,(z\in p)\Leftrightarrow (z\in \pi )\,]}
這樣根據本條目的外延定理 有
B
(
p
)
∧
B
(
π
)
⊢
(
p
=
π
)
{\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,\vdash \,(p=\pi )}
那以演繹定理 (D)將
B
(
p
)
∧
B
(
π
)
{\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )}
p
{\displaystyle p}
π
{\displaystyle \pi }
普遍化 有
⊢
(
∀
p
)
(
∀
π
)
[
B
(
p
)
∧
B
(
π
)
⇒
(
p
=
π
)
]
{\displaystyle \vdash (\forall p)(\forall \pi )[\,{\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\Rightarrow (p=\pi )\,]}
故本定理得証。
◻
{\displaystyle \Box }
這樣的話會有
定理 —
⊢
(
∃
!
p
)
{
{
¬
[
M
(
x
)
∧
M
(
y
)
]
∧
(
p
=
∅
)
}
∨
{
M
(
x
)
∧
M
(
y
)
∧
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
}
{\displaystyle \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 \}}}
證明
根據（P-1）和本條目的特定條件下的存在性 (DC)會有
（P-2）
⊢
(
∃
p
)
{
{
¬
[
M
(
x
)
∧
M
(
y
)
]
∧
(
p
=
∅
)
}
∨
{
M
(
x
)
∧
M
(
y
)
∧
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
}
{\displaystyle \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 \}}}
設
A
(
p
)
:=
¬
[
M
(
x
)
∧
M
(
y
)
]
∧
(
p
=
∅
)
{\displaystyle {\mathcal {A}}(p):=\neg [\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\,]\wedge (p=\varnothing )}
B
(
p
)
:=
M
(
x
)
∧
M
(
y
)
∧
M
(
p
)
∧
(
∀
M
z
)
{
(
z
∈
p
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
{\displaystyle {\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)]\,\}}
C
:=
M
(
x
)
∧
M
(
y
)
{\displaystyle {\mathcal {C}}:={\mathcal {M}}(x)\wedge {\mathcal {M}}(y)}
那連續套用邏輯與合邏輯或的分配律 與邏輯與的交換性 會有
⊢
{
[
A
(
p
)
∨
B
(
p
)
]
∧
[
A
(
π
)
∨
B
(
π
)
]
}
⇔
{
{
[
A
(
p
)
∧
A
(
π
)
]
∨
[
B
(
p
)
∧
A
(
π
)
]
}
∨
{
[
A
(
p
)
∧
B
(
π
)
]
∨
[
B
(
p
)
∧
B
(
π
)
]
}
}
{\displaystyle \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 \}}}
但考慮到邏輯與的直觀性質 和逻辑與的定義 有
⊢
[
B
(
p
)
∧
A
(
π
)
]
⇒
(
¬
C
∧
C
)
{\displaystyle \vdash [\,{\mathcal {B}}(p)\wedge {\mathcal {A}}(\pi )\,]\Rightarrow (\neg {\mathcal {C}}\wedge {\mathcal {C}})}
⊢
[
A
(
p
)
∧
B
(
π
)
]
⇒
(
¬
C
∧
C
)
{\displaystyle \vdash [\,{\mathcal {A}}(p)\wedge {\mathcal {B}}(\pi )\,]\Rightarrow (\neg {\mathcal {C}}\wedge {\mathcal {C}})}
⊢
(
¬
C
∧
C
)
⇔
¬
(
C
⇒
C
)
{\displaystyle \vdash (\neg {\mathcal {C}}\wedge {\mathcal {C}})\Leftrightarrow \neg ({\mathcal {C}}\Rightarrow {\mathcal {C}})}
那根據恆等關係
(
I
)
{\displaystyle (I)}
和常用的推理性質 (T)有
⊢
¬
[
B
(
p
)
∧
A
(
π
)
]
{\displaystyle \vdash \neg [\,{\mathcal {B}}(p)\wedge {\mathcal {A}}(\pi )\,]}
⊢
¬
[
A
(
p
)
∧
B
(
π
)
]
{\displaystyle \vdash \neg [\,{\mathcal {A}}(p)\wedge {\mathcal {B}}(\pi )\,]}
所以根據逻辑或的定義 來重複使用演繹定理 的推論(D1)會有
⊢
{
[
A
(
p
)
∨
B
(
p
)
]
∧
[
A
(
π
)
∨
B
(
π
)
]
}
⇔
{
[
A
(
p
)
∧
A
(
π
)
]
∨
[
B
(
p
)
∧
B
(
π
)
]
}
{\displaystyle \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 )\,]\,\}}
然後從NBG 等式定理 會有
⊢
[
A
(
p
)
∧
A
(
π
)
]
⇒
(
p
=
π
)
{\displaystyle \vdash [\,{\mathcal {A}}(p)\wedge {\mathcal {A}}(\pi )\,]\Rightarrow (p=\pi )}
另一方面，根據（P-1）有
⊢
[
B
(
p
)
∧
B
(
π
)
]
⇒
(
p
=
π
)
{\displaystyle \vdash [\,{\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,]\Rightarrow (p=\pi )}
這樣結合邏輯與 的(DisJ)有
⊢
{
[
A
(
p
)
∨
B
(
p
)
]
∧
[
A
(
π
)
∨
B
(
π
)
]
}
⇒
(
p
=
π
)
{\displaystyle \vdash \{\,[\,{\mathcal {A}}(p)\vee {\mathcal {B}}(p)\,]\wedge [\,{\mathcal {A}}(\pi )\vee {\mathcal {B}}(\pi )\,]\,\}\Rightarrow (p=\pi )}
再對
p
{\displaystyle p}
π
{\displaystyle \pi }
普遍化 有
⊢
(
∀
p
)
(
∀
π
)
{
{
[
A
(
p
)
∨
B
(
p
)
]
∧
[
A
(
π
)
∨
B
(
π
)
]
}
⇒
(
p
=
π
)
}
{\displaystyle \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 \}}}
這樣結合剛剛的（P-2）與邏輯與的直觀性質 ，本定理就得證了。
◻
{\displaystyle \Box }
所以根據函數符號與唯一性 一節，可以在NBG 函數符號
f
p
2
(
x
,
y
)
{\displaystyle f_{p}^{2}(x,\,y)}
{
x
,
y
}
{\displaystyle \{x,\,y\}}
(
P
′
)
{\displaystyle (P^{\prime })}
—
{
¬
[
M
(
x
)
∧
M
(
y
)
]
∧
(
{
x
,
y
}
=
∅
)
}
∨
{\displaystyle {\bigg \{}\neg [\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\,]\wedge (\{x,\,y\}=\varnothing ){\bigg \}}\vee }
{
M
(
x
)
∧
M
(
y
)
∧
M
(
{
x
,
y
}
)
∧
(
∀
M
z
)
{
(
z
∈
{
x
,
y
}
)
⇔
[
(
z
=
x
)
∨
(
z
=
y
)
]
}
}
{\displaystyle {\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 \}}}
這個新公理的直觀意思是「若x和y為集合，則
{
x
,
y
}
{\displaystyle \{x,\,y\}}
{
x
,
y
}
{\displaystyle \{x,\,y\}}
空集 」。
{
x
}
:=
{
x
,
x
}
{\displaystyle \{x\}:=\{x,\,x\}}
⟨
x
⟩
:=
x
{\displaystyle \langle x\rangle :=x}
⟨
x
,
y
⟩
:=
{
{
x
}
,
{
x
,
y
}
}
{\displaystyle \langle x,\,y\rangle :=\{\{x\},\,\{x,\,y\}\}}
⟨
x
1
,
…
,
x
n
,
x
n
+
1
⟩
:=
⟨
⟨
x
1
,
…
,
x
n
⟩
,
x
n
+
1
⟩
{\displaystyle \langle x_{1},\,\dots ,\,\,x_{n},\,x_{n+1}\rangle :=\langle \langle x_{1},\,\dots ,\,\,x_{n}\rangle ,\,x_{n+1}\rangle }
在不跟括弧產生混淆的情況下，也可以把
⟨
x
1
,
…
,
x
n
,
x
n
+
1
⟩
{\displaystyle \langle x_{1},\,\dots ,\,\,x_{n},\,x_{n+1}\rangle }
(
x
1
,
…
,
x
n
,
x
n
+
1
)
{\displaystyle (x_{1},\,\dots ,\,\,x_{n},\,x_{n+1})}
R
e
l
(
f
)
:=
(
∀
M
a
)
{
(
a
∈
f
)
⇒
(
∃
x
)
(
∃
y
)
{
M
(
x
)
∧
M
(
y
)
∧
[
a
=
(
x
,
y
)
]
}
}
{\displaystyle 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 \}}}
F
n
c
(
f
)
:=
R
e
l
(
f
)
∧
(
∀
M
x
)
(
∀
M
y
)
(
∀
M
υ
)
{
[
(
x
,
y
)
∈
f
∧
(
x
,
υ
)
∈
f
]
⇒
(
y
=
υ
)
}
{\displaystyle 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 )\,\}}
類函數跟普通函数 的差別在於普通函數是個集合 。
(
K
∈
)
{\displaystyle (K_{\in })}
—
(
∃
e
)
(
∀
M
a
)
(
∀
M
b
)
{
[
(
a
,
b
)
∈
e
]
⇔
(
a
∈
b
)
}
{\displaystyle (\exists e)(\forall ^{M}a)(\forall ^{M}b)\{[(a,\,b)\in e]\Leftrightarrow (a\in b)\}}
(
K
i
)
{\displaystyle (K_{i})}
—
(
∀
x
)
(
∀
y
)
(
∃
i
)
(
∀
M
a
)
{
(
a
∈
i
)
⇔
[
(
a
∈
x
)
∧
(
a
∈
y
)
]
}
{\displaystyle (\forall x)(\forall y)(\exists i)({\forall }^{M}a)\{(a\in i)\Leftrightarrow [(a\in x)\wedge (a\in y)]\}}
(
K
c
)
{\displaystyle (K_{c})}
—
(
∀
x
)
(
∃
c
)
(
∀
M
a
)
[
(
a
∈
c
)
⇔
(
a
∉
x
)
]
{\displaystyle (\forall x)(\exists c)({\forall }^{M}a)[(a\in c)\Leftrightarrow (a\not \in x)]}
(
K
D
)
{\displaystyle (K_{D})}
—
(
∀
x
)
(
∃
d
)
(
∀
M
a
)
{
(
a
∈
d
)
⇔
(
∃
M
b
)
[
(
a
,
b
)
∈
x
]
}
{\displaystyle (\forall x)(\exists d)(\forall ^{M}a)\{(a\in d)\Leftrightarrow (\exists ^{M}b)[(a,\,b)\in x]\}}
(
K
p
)
{\displaystyle (K_{p})}
—
(
∀
x
)
(
∃
p
)
(
∀
M
a
)
(
∀
M
b
)
{
[
(
a
,
b
)
∈
p
]
⇔
(
a
∈
x
)
}
{\displaystyle (\forall x)(\exists p)(\forall ^{M}a)(\forall ^{M}b)\{[\,(a,\,b)\in p\,]\Leftrightarrow (a\in x)\}}
(
K
σ
1
)
{\displaystyle (K_{\sigma 1})}
—
(
∀
x
)
(
∃
σ
)
(
∀
M
a
)
(
∀
M
b
)
(
∀
M
c
)
{
[
(
a
,
b
,
c
)
∈
x
]
⇔
[
(
b
,
c
,
a
)
∈
σ
]
}
{\displaystyle (\forall x)(\exists \sigma )(\forall ^{M}a)(\forall ^{M}b)(\forall ^{M}c)\{[(a,\,b,\,c)\in x]\Leftrightarrow [(b,\,c,\,a)\in \sigma ]\}}
(
K
σ
2
)
{\displaystyle (K_{\sigma 2})}
—
(
∀
x
)
(
∃
σ
)
(
∀
M
a
)
(
∀
M
b
)
(
∀
M
c
)
{
[
(
a
,
b
,
c
)
∈
x
]
⇔
[
(
a
,
c
,
b
)
∈
σ
]
}
{\displaystyle (\forall x)(\exists \sigma )(\forall ^{M}a)(\forall ^{M}b)(\forall ^{M}c)\{[(a,\,b,\,c)\in x]\Leftrightarrow [(a,\,c,\,b)\in \sigma ]\}}
這個元定理對應到ZFC尔集合论的分類公理 。
首先需要递归地定义 「可敘述公式 」（predicative well-formed formula）：
對任意變數
x
{\displaystyle x}
y
{\displaystyle y}
x
∈
y
{\displaystyle x\in y}
若
P
{\displaystyle {\mathcal {P}}}
Q
{\displaystyle {\mathcal {Q}}}
x
{\displaystyle x}
(
¬
P
)
{\displaystyle (\neg {\mathcal {P}})}
(
P
⇒
Q
)
{\displaystyle ({\mathcal {P}}\Rightarrow {\mathcal {Q}})}
(
∀
M
x
)
P
{\displaystyle (\forall ^{M}x){\mathcal {P}}}
這樣依據上列諸類存在公理，就有以下元定理：
類的存在元定理 —
P
{\displaystyle {\mathcal {P}}}
x
1
,
…
,
x
n
,
y
1
,
…
,
y
m
{\displaystyle x_{1},\,\dots ,\,x_{n},\,y_{1},\,\dots ,\,y_{m}}
⊢
(
∃
s
)
(
∀
M
x
1
)
…
(
∀
M
x
n
)
[
(
⟨
x
1
,
…
,
x
n
⟩
∈
s
)
⇔
P
]
{\displaystyle \vdash (\exists s)(\forall ^{M}x_{1})\ldots (\forall ^{M}x_{n})[(\langle x_{1},\,\dots ,\,x_{n}\rangle \in s)\Leftrightarrow {\mathcal {P}}]}
(
U
)
{\displaystyle (U)}
—
(
∀
M
x
)
(
∃
M
u
)
(
∀
M
a
)
[
(
a
∈
u
)
⇔
(
∃
M
ξ
∈
x
)
(
a
∈
ξ
)
]
{\displaystyle (\forall ^{M}x)(\exists ^{M}u)(\forall ^{M}a)[(a\in u)\Leftrightarrow (\exists ^{M}\xi \in x)(a\in \xi )]}
(
W
)
{\displaystyle (W)}
—
(
∀
M
x
)
(
∃
M
w
)
(
∀
M
ξ
)
{
(
ξ
∈
w
)
⇔
(
ξ
⊆
x
)
}
{\displaystyle (\forall ^{M}x)(\exists ^{M}w)(\forall ^{M}\xi )\{(\xi \in w)\Leftrightarrow (\xi \subseteq x)\}}
(
S
)
{\displaystyle (S)}
—
(
∀
M
x
)
(
∀
y
)
(
∃
M
z
)
(
∀
M
a
)
{
(
a
∈
z
)
⇔
[
(
a
∈
x
)
∧
(
a
∈
y
)
]
}
{\displaystyle (\forall ^{M}x)(\forall y)(\exists ^{M}z)(\forall ^{M}a)\{(a\in z)\Leftrightarrow [(a\in x)\wedge (a\in y)]\}}
(
I
)
{\displaystyle (I)}
—
(
∃
M
I
)
{
(
∅
∈
I
)
∧
(
∀
M
a
)
[
(
a
∈
I
)
⇒
(
a
∩
{
a
}
∈
I
)
]
}
{\displaystyle (\exists ^{M}I)\{(\varnothing \in I)\wedge (\forall ^{M}a)[(a\in I)\Rightarrow (a\cap \{a\}\in I)]\}}
(
R
)
{\displaystyle (R)}
—
F
n
c
(
f
)
⇒
(
∀
M
x
)
(
∃
M
r
)
(
∀
M
b
)
{
(
b
∈
r
)
⇒
(
∃
M
a
)
{
(
⟨
a
,
b
⟩
∈
r
)
∧
(
a
∈
x
)
}
}
{\displaystyle 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 \}}}
直觀意義為「
f
{\displaystyle f}
x
{\displaystyle x}
r
{\displaystyle r}
f
{\displaystyle f}
像 」。
对于任何类 C ，存在一个集合 x 使得
R
p
(
C
,
x
)
{\displaystyle Rp(C,x)}
x 是 C 的表示，即 C 和 x 所包含的元素一樣），当且仅当没有在 C 和所有集合的类 V 之间的双射。 这个公理贡献自冯·诺伊曼，并一下实现了分离公理、替代公理和全局选择公理。他效力相當於原始的替代公理加上这选择公理。完全的大小限制公理蕴涵了全局选择公理 ，因为序数的类不是集合，所以有从序数到全集的双射。
Bernays, Paul. Axiomatic Set Theory. Dover Publications. 1991. 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.von Neumann-Bernays-Gödel set theory . PlanetMath .
^ Cohen, Paul J. Set Theory and the Continuum Hypothesis . New York: W. A. Benjamin. 1966 [2023-05-15 ] . （原始内容存档 于2023-05-15）. ^ Montague, Richard. Semantical Closure and Non-Finite Axiomatizability I . Journal of Symbolic Logic. 1964, 29 (1) [2023-05-15 ] . doi:10.2307/2269797 存档 于2023-05-15）. ^ Mendelson, Elliott. Introduction to Mathematical Logic (6th Edition). Chapman & Hall. 2015: 233–233. ISBN 9781482237726
![{\displaystyle x\subseteq y:=\forall a[\,(a\in x)\Rightarrow (a\in y)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3e54551e2f224d51dd5e4b2f8b9c292c8abac9db)
![{\displaystyle ({\forall }^{M}x){\mathcal {A}}:=\forall x[\,{\mathcal {M}}(x)\Rightarrow {\mathcal {A}}\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/87cc1955428f3dd14742c909ef2b60fc34fa2e32)
![{\displaystyle ({\exists }^{M}x){\mathcal {A}}:=\exists x[\,{\mathcal {M}}(x)\wedge {\mathcal {A}}\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d441686439c8e31bfbc67ed1ddd5fe1841543397)
![{\displaystyle \forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5f414002fb71a39ad26aa5f361a6ffaa8d2c32dc)
![{\displaystyle (x=y)\Leftrightarrow \forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c1c1ab7e92dc01f2fc2d75e8048332e144e06e4d)
![{\displaystyle (x=y):=\forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4483a1038e1057291a3534e521cd83274a21ea67)
![{\displaystyle (x=y)\Rightarrow \forall z[\,(x\in z)\Leftrightarrow (y\in z)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b85d50b484ad637cac5166a889c0de4675c9e642)
![{\displaystyle \forall a[\,(a\in x)\Leftrightarrow (a\in x)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/39799bb561f82ea4b7807813208c037843b23d47)
![{\displaystyle \vdash \forall a[\,(a\in x)\Leftrightarrow (a\in x)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/43c9967717313cfc08cd538155545af8612c6cec)
![{\displaystyle (x=y)\Rightarrow [\,(x\in z)\Rightarrow (y\in z)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6f25e51a4dc54b3e283dfdaadf52563b7284f5fd)
![{\displaystyle (x=y)\Rightarrow [\,(z\in x)\Rightarrow (z\in y)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4b46b631f1d0cdb5190e4d7fda754634cb2d409d)
![{\displaystyle \vdash (\forall z)[(z\in x)\Leftrightarrow (z\in y)]\Rightarrow (\forall z)[(z\in y)\Leftrightarrow (z\in x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/eedf333f77ff04d9ee57d1887fb10a1c40eaf52a)
![{\displaystyle (x=y)\vdash (\forall z)[(z\in y)\Leftrightarrow (z\in x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d9a43568c1169c550d165beb9b2c92ccaf6d70d4)
![{\displaystyle \vdash (x=y)\Leftrightarrow (\forall ^{M}z)[\,(z\in x)\Leftrightarrow (z\in y)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b75f8a251bd3d302502cbe448e7b2e21a2076e01)
![{\displaystyle \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)]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fc19b63abe8425938355bcc4540038e474572c96)
![{\displaystyle \exists t(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f664d470476cbcffcc007a130589fae9e96be3d8)
![{\displaystyle \forall z\{\exists t(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cc4e38b41ddf6dba544e0b046fdf8b37636dfd13)
![{\displaystyle \forall z\{{\mathcal {M}}(z)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}\vdash \forall z(z\in x\Leftrightarrow z\in y)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cf1d4736fbdbed217493ecff972a1079fc027b68)
![{\displaystyle \forall z[\exists t(z\in t)\Rightarrow {\mathcal {A}}]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/41e6bab54de9788eb39ae991c93141d68ecbb38d)
![{\displaystyle \neg {\mathcal {A}}\Rightarrow \forall t[\neg (z\in t)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4dc22050be3d0c65b953a794b7efd3c220b5ed37)
![{\displaystyle \neg {\mathcal {A}}\Rightarrow [\neg (z\in t)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/07608c813f4f96ff170769d323504e6e43bcfc2c)
![{\displaystyle (z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1d39f13a7926955249f83d087b374deb913750cb)
![{\displaystyle \forall t\{(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6ef285b8076d1f3d0658dcbef9dcf648dd601428)
![{\displaystyle (z\in x)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ba324843a03f996966656a36733d7010ee79ae5d)
![{\displaystyle (z\in y)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8a9d4af0834d370271cfd98d26e6a3c8750e267)
![{\displaystyle (z\in x)\Rightarrow [(z\in x)\Rightarrow (z\in y)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fb01886b88fa5d1d2998f8c034521b17a9bb2fd2)
![{\displaystyle (z\in y)\Rightarrow [(z\in y)\Rightarrow (z\in x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/908c383040fb5a744f487ee0973f3a8af543bd03)
![{\displaystyle \vdash (\exists x)\{\,[\,\neg {\mathcal {A}}\wedge (x=c)\,]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\,\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/38cc0f265a071ab8ab6916d31fd64dd5aa99a4ce)
![{\displaystyle (\forall x)\{\neg \{[\neg {\mathcal {A}}\wedge (x=c)]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\}\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b4a2e38ec286b93d1a44c00479e79986b7539dce)
![{\displaystyle \neg \{[\neg {\mathcal {A}}\wedge (x=c)]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0b065f405c6434ae0f94c6d0293fdf49a9d0d754)
![{\displaystyle \neg [\neg {\mathcal {A}}\wedge (x=c)]\wedge \neg ({\mathcal {A}}\wedge {\mathcal {B}})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0565aa103bd0ef806baec9a82d61a60f002628ad)
![{\displaystyle \neg [\neg {\mathcal {A}}\wedge (x=c)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dae4a7a96b36a736f9f9986b0a5dc9d07049f1f8)
![{\displaystyle (\forall x)[\neg (x=c)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4dcb6c7ae950cf6b334d19454cf94bddc7f0b68c)
![{\displaystyle {\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)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/418e062ef2299268391317c8aeff6a9ce7701215)
![{\displaystyle \vdash (\exists !x)[\,{\mathcal {M}}(x)\wedge ({\forall }^{M}y)(y\not \in x)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ba67f1d8620d334084a32845c769abd50db35a49)
![{\displaystyle \vdash (y\not \in x)\Rightarrow [\,(y\in x)\Rightarrow (y\in t)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1dd5b77f3bc3cd80e2612f0dd2c7580790711d21)
![{\displaystyle \vdash (y\not \in t)\Rightarrow [\,(y\in t)\Rightarrow (y\in x)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2826084acf4ac8a141a4156ae56782c004f3bdca)
![{\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in x)\Rightarrow (y\in t)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7ab686156612bc86749d956145e4d0e20e1a62d1)
![{\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in t)\Rightarrow (y\in x)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b0f494e99338e0101548413e5738da320d277af8)
![{\displaystyle \neg [\,(y\in x)\Rightarrow (y\in t)\,]\Rightarrow \neg {\mathcal {M}}(y)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9efeff1247bc20e94db549e7c43e916bb23d4cec)
![{\displaystyle \neg [\,(y\in t)\Rightarrow (y\in x)\,]\Rightarrow \neg {\mathcal {M}}(y)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/19519d5241e52b62ef78314c8dc0b639c745eaae)
![{\displaystyle \neg \{\,[\,(y\in x)\Rightarrow (y\in t)\,]\wedge [\,(y\in t)\Rightarrow (y\in x)\,]\,\}\Rightarrow \neg {\mathcal {M}}(y)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/03d0f71774fbc2509a56fc9ff58e2f69bc1bb52c)
![{\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in x)\Leftrightarrow (y\in t)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1f8e45873ecb23255af032d4797955f5f831ca64)
![{\displaystyle (\forall ^{M}y)[\,(y\in x)\Leftrightarrow (y\in t)\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b7ac999a37929bc6207ec84d91bb44d31493c261)
![{\displaystyle \vdash [\,({\forall }^{M}y)(y\not \in x)\wedge ({\forall }^{M}y)(y\not \in t)\,]\Rightarrow (x=t)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8b38bba154234266e915c148cd40a78343517d58)
![{\displaystyle \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)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/917e30ccd1348237cbefbe8288ad50dc39aadab5)
![{\displaystyle \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 \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/617d50c62533601f6ccb89f7eb185277045158cb)
![{\displaystyle ({\forall }^{M}x)({\forall }^{M}y)({\exists }^{M}p)({\forall }^{M}z)\{(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/970311eabc216a5a6e0bfeb589e2fa7f7c35c9ef)
![{\displaystyle {\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 \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d80440e87eb8ac8d01be9aa3ae32707dff81203a)
![{\displaystyle (\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 \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/01a6b3a7d28bd4df9d8e963ef7ab2db0b2640252)
![{\displaystyle {\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 \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9f7d353ee9ed99487648e3c195e57818e7161d59)
![{\displaystyle (\exists p){\big \{}\,{\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}\,{\big \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/96857dcb065c5d6adde2a4c331db75cf93893379)
![{\displaystyle {\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 \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dddc7c97c04571616bfc61ed404ee480fdf9c494)
![{\displaystyle {\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d45e3de98587233c12ba4f47ee98a8c5c0e07988)
![{\displaystyle {\mathcal {M}}(\pi )\wedge ({\forall }^{M}z)\{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c615af0ea3af9220b8319c766248d8c2611f402b)
![{\displaystyle ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1b74a16e310b92ee66f9d3e338c6097fe4f0b673)
![{\displaystyle ({\forall }^{M}z)\{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b5257a62d97008535ed3ccbce904b84c5f49528e)
![{\displaystyle {\mathcal {M}}(z)\Rightarrow \{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e241401ea0f233965d765ee75a9b04a6ecfd0283)
![{\displaystyle {\mathcal {M}}(z)\Rightarrow \{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/046fba6fdb0b399dec3eb107d1a6ba3f02778b04)
![{\displaystyle (z\in p)\Leftrightarrow [(z=x)\vee (z=y)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2dc70f58521511bd5f263c90a284d6deb6bfdf15)
![{\displaystyle (z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7114adb74956949ddf6bdcb792e9ac9a05e672c4)
![{\displaystyle {\mathcal {B}}(p):={\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/11418e2f259bbb7ae3d3587de712bfe8a7e808b9)
![{\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,\vdash \,(\forall ^{M}z)[\,(z\in p)\Leftrightarrow (z\in \pi )\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b66b8354dda1142dc012ed601213cc167691630f)
![{\displaystyle \vdash (\forall p)(\forall \pi )[\,{\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\Rightarrow (p=\pi )\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c66b01a26ed9c9bb8efd1add92061949102469c8)
![{\displaystyle \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 \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/78ccd2f0905d9df305901bd0aba437ae83e5ed62)
![{\displaystyle \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 \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6e292f98d65067132d969cea200173f5226850e6)
![{\displaystyle {\mathcal {A}}(p):=\neg [\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\,]\wedge (p=\varnothing )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e490a6badb5d9eecf7cd578244025f3dc5043e48)
![{\displaystyle {\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)]\,\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b3226c04e55e44973fad9d577d49d718f094d29b)
![{\displaystyle \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 \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9e7a62d8769175cc8338ea8b3740cfe302eb7de9)
![{\displaystyle \vdash [\,{\mathcal {B}}(p)\wedge {\mathcal {A}}(\pi )\,]\Rightarrow (\neg {\mathcal {C}}\wedge {\mathcal {C}})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c9751856e45d35b87366b153ed56483ac429b6c1)
![{\displaystyle \vdash [\,{\mathcal {A}}(p)\wedge {\mathcal {B}}(\pi )\,]\Rightarrow (\neg {\mathcal {C}}\wedge {\mathcal {C}})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e4deb2633f401668d6f9da005e8d4f108d36b039)
![{\displaystyle \vdash \neg [\,{\mathcal {B}}(p)\wedge {\mathcal {A}}(\pi )\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/547054ebb7bb6b730ad09cbf2b63ac9a9a1a1f8c)
![{\displaystyle \vdash \neg [\,{\mathcal {A}}(p)\wedge {\mathcal {B}}(\pi )\,]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b718d6b7348c7bfdb8c2e44dd865ab317e352af2)
![{\displaystyle \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 )\,]\,\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7605404218c0ddc3ca9b467b20befaa134d3b209)
![{\displaystyle \vdash [\,{\mathcal {A}}(p)\wedge {\mathcal {A}}(\pi )\,]\Rightarrow (p=\pi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/13ff6e35ba8da8c9d83ce3af521261a7a45dc3a1)
![{\displaystyle \vdash [\,{\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,]\Rightarrow (p=\pi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e52da52c3528f7d84b00d77114bcd2935fe5a4bf)
![{\displaystyle \vdash \{\,[\,{\mathcal {A}}(p)\vee {\mathcal {B}}(p)\,]\wedge [\,{\mathcal {A}}(\pi )\vee {\mathcal {B}}(\pi )\,]\,\}\Rightarrow (p=\pi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/304665c4d974c20792224f39dd8686f643a1f629)
![{\displaystyle \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 \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ea6b12db7f2af0ad7b9ef2c73e6c017a0159e187)
![{\displaystyle {\bigg \{}\neg [\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\,]\wedge (\{x,\,y\}=\varnothing ){\bigg \}}\vee }](https://wikimedia.org/api/rest_v1/media/math/render/svg/4e73d2661a683f2363530f274d1be03d8fb7410d)
![{\displaystyle {\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 \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/609f63c179297663f08bfed1fee247b548242ef3)
![{\displaystyle 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 \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d79b22c4acec598cf36a38ba7c815c0800cee122)
![{\displaystyle 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 )\,\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/08b8f3441e5d0937fb1995e21ba21aa40e077bc0)
![{\displaystyle (\exists e)(\forall ^{M}a)(\forall ^{M}b)\{[(a,\,b)\in e]\Leftrightarrow (a\in b)\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4130e8c2ae1b418179c798d61093c6acd7c30253)
![{\displaystyle (\forall x)(\forall y)(\exists i)({\forall }^{M}a)\{(a\in i)\Leftrightarrow [(a\in x)\wedge (a\in y)]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2aa42e8885f330ae37f375ba93aa96c1906baf28)
![{\displaystyle (\forall x)(\exists c)({\forall }^{M}a)[(a\in c)\Leftrightarrow (a\not \in x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b91dbb195ce62792217b608f40eeddacd6032ed8)
![{\displaystyle (\forall x)(\exists d)(\forall ^{M}a)\{(a\in d)\Leftrightarrow (\exists ^{M}b)[(a,\,b)\in x]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b292a8cbf7adb82960c9cbd9f84c5f1ffa8caf42)
![{\displaystyle (\forall x)(\exists p)(\forall ^{M}a)(\forall ^{M}b)\{[\,(a,\,b)\in p\,]\Leftrightarrow (a\in x)\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9f37bd6a9f3eaa47aa2bebb9455914a86b771180)
![{\displaystyle (\forall x)(\exists \sigma )(\forall ^{M}a)(\forall ^{M}b)(\forall ^{M}c)\{[(a,\,b,\,c)\in x]\Leftrightarrow [(b,\,c,\,a)\in \sigma ]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f63ccc16424cf92fbf0a1ea43641e83155f242c3)
![{\displaystyle (\forall x)(\exists \sigma )(\forall ^{M}a)(\forall ^{M}b)(\forall ^{M}c)\{[(a,\,b,\,c)\in x]\Leftrightarrow [(a,\,c,\,b)\in \sigma ]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/11628250d8d9df49962e9e8d23112d86412269a5)
![{\displaystyle \vdash (\exists s)(\forall ^{M}x_{1})\ldots (\forall ^{M}x_{n})[(\langle x_{1},\,\dots ,\,x_{n}\rangle \in s)\Leftrightarrow {\mathcal {P}}]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/98194b27c167bea8c424c77c879f39cbd968db31)
![{\displaystyle (\forall ^{M}x)(\exists ^{M}u)(\forall ^{M}a)[(a\in u)\Leftrightarrow (\exists ^{M}\xi \in x)(a\in \xi )]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dcc6d03b9aa1701827af67a2d1b80424bf0b3636)
![{\displaystyle (\forall ^{M}x)(\forall y)(\exists ^{M}z)(\forall ^{M}a)\{(a\in z)\Leftrightarrow [(a\in x)\wedge (a\in y)]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7f824db36d0ea8a04abcbed557dc9659d3d8b02a)
![{\displaystyle (\exists ^{M}I)\{(\varnothing \in I)\wedge (\forall ^{M}a)[(a\in I)\Rightarrow (a\cap \{a\}\in I)]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0c606dc994b04266ab6a0a380fbcb71f0927b322)
