冯·诺伊曼-博内斯-哥德尔集合论 （英语：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 }
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}})}
(
∀
x
M
)
P
{\displaystyle (\forall x^{M}){\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}}]}
集合的公理
编辑
无穷公理
编辑
(
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)]\}}
取代公理及其替代
编辑
选择公理
编辑
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)
![{\displaystyle Fnc(f)\Rightarrow (\forall ^{M}x)(\exists ^{M}r)(\forall ^{M}b){\bigg \{}(b\in r)\Rightarrow (\exists ^{M}a)\{[(a,\,b)\in r]\wedge (a\in x)\}{\bigg \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4a0566dfab1a3b19f3c43af40a91f40c2d4d3cf4)
