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

冯·诺伊曼-博内斯-哥德尔集合论（英语：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年开始由保罗·博内斯（英语：Paul Bernays）作修改，在1940年由哥德尔进一步简化。

基本符号

在NBG下，“属于关系”以一个双元断言符号 ${\displaystyle P(x,\,y)}$ 来表示， ${\displaystyle P(x,\,y)}$ 通常简记为 ${\displaystyle x\in y}$ ，并被直观理解成“x属于y”；类似地， ${\displaystyle P(x,\,y)}$ 的否定 ${\displaystyle \neg P(x,\,y)}$ 通称被简记为 ${\displaystyle x\notin y}$ ，并被直观理解为“x不属于y”。

以下都把 ${\displaystyle \vdash _{NBG}}$ 简写为普通的 ${\displaystyle \vdash }$。

本条目定理的证明会频繁引用一阶逻辑的定理，定理的代号可以参见一阶逻辑#常用的推理性质一节。

类与集合

“类”这个名词在公理化集合论出现之前，通常被理解为“以集合为元素的集合。”或是集合（如等价类）。

但NBG所谈及的一切对象（变数和项）都是类。而所谓的集合，是属于某个类的类，也就是说以下的合式公式（${\displaystyle {\mathcal {M}}}$ 来自德语的"集合"“Menge”）式

${\displaystyle {\mathcal {M}}(x):=\exists y(x\in y)}$

可直观理解为“x是集合”，特别注意到，为了避免跟其他合式公式的变数产生混淆， ${\displaystyle y}$ 必须是展开 ${\displaystyle {\mathcal {M}}(x)}$ 时首次出现的变数。反之合式公式

${\displaystyle {\mathcal {Pr}}(x):=\neg {\mathcal {M}}(x)}$

可称为“ ${\displaystyle x}$ 是真类（proper class）”。

子类

直观上“x包含于y”意为“所有x的元素a都会属于y”，以此为动机，NBG有以下的符号简写

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

以上可称为“x包含于y”或“x是y的子类（subclass）”；在 ${\displaystyle {\mathcal {M}}(x)}$ 和 ${\displaystyle {\mathcal {M}}(y)}$ 成立的前提下（也就是“x和y都是集合”），可称为“x是y的子集（subset）”。

与集合相关的量词简写

仿造量词的简写，对于任意变数 ${\displaystyle x}$ 与合式公式 ${\displaystyle {\mathcal {A}}}$ ，可作如下的符号定义

${\displaystyle ({\forall }^{M}x){\mathcal {A}}:=\forall x[\,{\mathcal {M}}(x)\Rightarrow {\mathcal {A}}\,]}$ （对所有 ${\displaystyle x}$ ， ${\displaystyle x}$ 是集合则 ${\displaystyle {\mathcal {A}}}$ ）

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

也有书籍以小写字母来表示被量化的集合变数^[3]，但考虑到一般的非逻辑数学书籍都将大小写的差异挪作他用，为避免混淆本条目采用以上的上标表示法。

等号公理

看待等号的不同方式

直观上，两个集合相等意为“x的元素就是y的元素”，也就是朴素集合论的外延公理，换句话说，可用以下的严谨合式公式重写为

${\displaystyle \forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}$

但一阶逻辑的等号可以视为单独的断言符号，也可以视为一条复合的合式公式。具体来说，视为一个新的断言符号 ${\displaystyle Q(x,\,y)}$ 并简记为 ${\displaystyle x=y}$ 的话，需在NBG内额外添加以下的公理

${\displaystyle (T^{\prime })}$ — ${\displaystyle (x=y)\Leftrightarrow \forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}$

直观上可理解为“类x的元素就是类y的元素，等价于类x等于类y”。

但视为一条合式公式，则仅需做以下的符号定义

${\displaystyle (x=y):=\forall a[\,(a\in x)\Leftrightarrow (a\in y)\,]}$

不管是何种看待方法，习惯上都会把 ${\displaystyle \neg (x=y)}$ 简记成 ${\displaystyle (x\neq y)}$ （直观上的“不相等”）。

等号的良置

为了确保 ${\displaystyle (x=y)}$ 的确符合直观上对等号的要求，还需添加以下的公理

${\displaystyle (T)}$ — ${\displaystyle (x=y)\Rightarrow \forall z[\,(x\in z)\Leftrightarrow (y\in z)\,]}$

直观上，这个公理确保“x等于y，则x属于z等同于y属于z”。

这样，以下的元定理就确保了如此定义的等号是“成功的”。

元定理 — NBG是带相等符号 ${\displaystyle (x=y)}$ 的一阶逻辑理论

证明

以下的证明会逐条检验等式定理一节所条列的定义 （E1）： ${\displaystyle (x=x)}$ 展开来是（或等价于） ${\displaystyle \forall a[\,(a\in x)\Leftrightarrow (a\in x)\,]}$ 那考虑到恒等关系和(AND)有 ${\displaystyle \vdash (a\in x)\Leftrightarrow (a\in x)}$ 那再套用(GEN)，就会有 ${\displaystyle \vdash \forall a[\,(a\in x)\Leftrightarrow (a\in x)\,]}$ 所以（E1）得证。 （E2）： 因为目前的NBG理论内没有任何函数符号，所以对变数 ${\displaystyle x}$ 来说，NBG的原子公式只有 ${\displaystyle (x\in z)}$ 和 ${\displaystyle (z\in x)}$ 两种可能，这样的话，（E2）等同于要求以下两式是NBG的定理 (1) ${\displaystyle (x=y)\Rightarrow [\,(x\in z)\Rightarrow (y\in z)\,]}$ (2) ${\displaystyle (x=y)\Rightarrow [\,(z\in x)\Rightarrow (z\in y)\,]}$ 但依据量词公理（A4），(1)可从本节一开始添加的公理（T）所推出；类似地，把 ${\displaystyle (x=y)}$ 视为断言符号时，(2)都可以从（T'）配合（A4）推出；若把 ${\displaystyle (x=y)}$ 视为合式公式的简写，(2)也可以用 ${\displaystyle (x=y)}$ 的定义配上（A4）推出。 （E3）： 本条定义要求以下的合式公式为NBG的定理 ${\displaystyle (x=y)\Rightarrow (y=x)}$ 从且的交换性有 ${\displaystyle \vdash (\forall z)[(z\in x)\Leftrightarrow (z\in y)]\Rightarrow (\forall z)[(z\in y)\Leftrightarrow (z\in x)]}$ 对上式使用(AND)和(D1)就有 ${\displaystyle (x=y)\vdash (\forall z)[(z\in y)\Leftrightarrow (z\in x)]}$ 再对上面式使用(AND)和(D1)又有 ${\displaystyle (x=y)\vdash (y=x)}$ 所以（E3）的确是NBG的定理。 综上所述，定理得证。${\displaystyle \Box }$

真子类

在定义“相等”以后，可以把“相等的类”排除出子类的定义中，换句话说，NBG有以下的符号定义

${\displaystyle x\subset y:=(x\subseteq y)\wedge (x\neq y)}$

可直观理解为“x是y的真子类（proper subclass），定义为x包含于y且x不等于y”；在 ${\displaystyle {\mathcal {M}}(x)}$ 和 ${\displaystyle {\mathcal {M}}(y)}$ 成立的前提下（也就是“x和y都是集合”），可称为“x是y的真子集（proper subset）”。

外延定理

为以下的定理可直观理解为“x等于y等价于，对所有集合z，z属于x等价于z属于y”，也就是说，等于的定义可以“限缩”成元素为集合的状况。

外延定理 — ${\displaystyle \vdash (x=y)\Leftrightarrow (\forall ^{M}z)[\,(z\in x)\Leftrightarrow (z\in y)\,]}$

证明

以下取一个不曾出现的变数 ${\displaystyle t}$ 来展开 ${\displaystyle {\mathcal {M}}(z)}$ (${\displaystyle \Rightarrow }$)${\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)${\displaystyle \forall z(z\in x\Leftrightarrow z\in y)}$ (Hyp) (2)${\displaystyle z\in x\Leftrightarrow z\in y}$ (MP with 1, A4) (3)${\displaystyle \exists t(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}$ (MP with 2, A1) (4)${\displaystyle \forall z\{\exists t(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}}$ (GEN with 3) (${\displaystyle \Leftarrow }$)${\displaystyle \forall z\{{\mathcal {M}}(z)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}\vdash \forall z(z\in x\Leftrightarrow z\in y)}$ ${\displaystyle {\mathcal {A}}:=(z\in x)\Leftrightarrow (z\in y)}$ (1)${\displaystyle \forall z[\exists t(z\in t)\Rightarrow {\mathcal {A}}]}$ (Hyp) (2)${\displaystyle \exists t(z\in t)\Rightarrow {\mathcal {A}}}$ (MP with A4, 1) (3)${\displaystyle \neg {\mathcal {A}}\Rightarrow \forall t[\neg (z\in t)]}$ (MP with T, 2) (4) ${\displaystyle \neg {\mathcal {A}}\Rightarrow [\neg (z\in t)]}$ (D1, with A4, 3) (5)${\displaystyle (z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}$ (MP with T, 4) (6)${\displaystyle \forall t\{(z\in t)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]\}}$ (GEN with 5) (7)${\displaystyle (z\in x)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}$ (MP with A4, 6) (8)${\displaystyle (z\in y)\Rightarrow [(z\in x)\Leftrightarrow (z\in y)]}$ (MP with A4, 6) (9)${\displaystyle (z\in x)\Rightarrow [(z\in x)\Rightarrow (z\in y)]}$ (D1 with AND, 7) (10)${\displaystyle (z\in y)\Rightarrow [(z\in y)\Rightarrow (z\in x)]}$ (D1 with AND, 8) (11)${\displaystyle (z\in x)\Rightarrow (z\in y)}$ (MP twice with A2, I, 9) (12)${\displaystyle (z\in y)\Rightarrow (z\in x)}$ (MP twice with A2, I, 10) (13)${\displaystyle (z\in x)\Leftrightarrow (z\in y)}$ (AND with 11, 12) (14)${\displaystyle \forall z(z\in x\Leftrightarrow z\in y)}$ (GEN with 13)

引入新的函数符号前，常需要唯一存在性的证明，而外延定理大大简化了证明的难度。

特定条件下的存在性

以下关于一阶逻辑的一般性定理，也大大简化了 NBG 引入新公理的过程所需的证明

（DC, Definition under certain condition） — ${\displaystyle x}$ 于合式公式 ${\displaystyle {\mathcal {A}}}$ 完全不自由且 ${\displaystyle c}$ 是常数符号。若

${\displaystyle {\mathcal {A}}\vdash (\exists x){\mathcal {B}}}$　

则有

${\displaystyle \vdash (\exists x)\{\,[\,\neg {\mathcal {A}}\wedge (x=c)\,]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\,\}}$

证明

(1)${\displaystyle {\mathcal {A}}\Rightarrow (\exists x){\mathcal {B}}}$ (Hyp) (2)${\displaystyle (\forall x)\{\neg \{[\neg {\mathcal {A}}\wedge (x=c)]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\}\}}$ (Hyp) (3)${\displaystyle \neg \{[\neg {\mathcal {A}}\wedge (x=c)]\vee ({\mathcal {A}}\wedge {\mathcal {B}})\}}$ (MP with A4, 2) (4)${\displaystyle \neg [\neg {\mathcal {A}}\wedge (x=c)]\wedge \neg ({\mathcal {A}}\wedge {\mathcal {B}})}$ (MP with 3, DIS) (5)${\displaystyle \neg [\neg {\mathcal {A}}\wedge (x=c)]}$ (MP with AND,4) (6)${\displaystyle \neg ({\mathcal {A}}\wedge {\mathcal {B}})}$ (MP with AND, 4) (7)${\displaystyle \neg {\mathcal {A}}\Rightarrow \neg (x=c)}$ (MP with DIS, DN 5) (8)${\displaystyle {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}$ (MP with DIS, DN, 5) (9)${\displaystyle {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}$ (MP with T, 8) (10)${\displaystyle (\exists x){\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}$ (GENe with 9) (11)${\displaystyle {\mathcal {A}}\Rightarrow \neg (\exists x){\mathcal {B}}}$ (MP with T, 11) (12)${\displaystyle \neg {\mathcal {A}}}$ (A3' with 1, 11) (13)${\displaystyle \neg (x=c)}$ (MP with 7, 12) (14)${\displaystyle (\forall x)[\neg (x=c)]}$ (GEN with 13) 再套用一次（DN）也就是 ${\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)}$ 但由一阶逻辑的等式性质有 ${\displaystyle \vdash c=c}$ 对上式以变数 ${\displaystyle x}$ 套用一次(GENe)有 ${\displaystyle \vdash (\exists x)(x=c)}$ 所以由(C2)本定理就会得证。${\displaystyle \Box }$

空集合公理

${\displaystyle (N)}$ — ${\displaystyle ({\exists }^{M}x)({\forall }^{M}y)(y\not \in x)}$

这个公理的直观意思是“存在集合x，使的所有集合y都不属于x”。

事实上这个公理还确保了空集的唯一性，严格来说，它确保了：

定理 — ${\displaystyle \vdash (\exists !x)[\,{\mathcal {M}}(x)\wedge ({\forall }^{M}y)(y\not \in x)\,]}$

证明

假设 ${\displaystyle ({\forall }^{M}y)(y\not \in x)}$ ${\displaystyle ({\forall }^{M}y)(y\not \in t)}$ 那根据量词公理的(A4)有 ${\displaystyle {\mathcal {M}}(y)\Rightarrow (y\not \in x)}$ ${\displaystyle {\mathcal {M}}(y)\Rightarrow (y\not \in t)}$ 另一方面，根据常用的推理性质的(M0)有 ${\displaystyle \vdash (y\not \in x)\Rightarrow [\,(y\in x)\Rightarrow (y\in t)\,]}$ ${\displaystyle \vdash (y\not \in t)\Rightarrow [\,(y\in t)\Rightarrow (y\in x)\,]}$ 这样根据演绎定理的推论(D1)有 ${\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in x)\Rightarrow (y\in t)\,]}$ ${\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in t)\Rightarrow (y\in x)\,]}$ 这样根据常用的推理性质(T)有 ${\displaystyle \neg [\,(y\in x)\Rightarrow (y\in t)\,]\Rightarrow \neg {\mathcal {M}}(y)}$ ${\displaystyle \neg [\,(y\in t)\Rightarrow (y\in x)\,]\Rightarrow \neg {\mathcal {M}}(y)}$ 这样根据德摩根定律和逻辑与的(DisJ)有 ${\displaystyle \neg \{\,[\,(y\in x)\Rightarrow (y\in t)\,]\wedge [\,(y\in t)\Rightarrow (y\in x)\,]\,\}\Rightarrow \neg {\mathcal {M}}(y)}$ 这样再根据(T)有 ${\displaystyle {\mathcal {M}}(y)\Rightarrow [\,(y\in x)\Leftrightarrow (y\in t)\,]}$ 这样根据普遍化有 ${\displaystyle (\forall ^{M}y)[\,(y\in x)\Leftrightarrow (y\in t)\,]}$ 那这样根据上节的外延定理有 ${\displaystyle x=t}$ 换句话说 ${\displaystyle \vdash [\,({\forall }^{M}y)(y\not \in x)\wedge ({\forall }^{M}y)(y\not \in t)\,]\Rightarrow (x=t)}$ 这样根据逻辑与的直观性质和(D1)有 ${\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)}$ 这样根据普遍化有 ${\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，但两个理论是等效的）

${\displaystyle (N^{\prime })}$ — ${\displaystyle {\mathcal {M}}(\varnothing )\wedge ({\forall }^{M}y)(y\not \in \varnothing )}$

这个新公理直观上以“${\displaystyle \varnothing }$为集合，且任意集合y都不属于${\displaystyle \varnothing }$”，把 ${\displaystyle \varnothing }$ 定义成了空集的表示符号。

配对公理

${\displaystyle (P)}$ — ${\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） — ${\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)等价于 ${\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)有 ${\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 \}}}$ 这样在有 ${\displaystyle {\mathcal {M}}(x)\wedge {\mathcal {M}}(y)}$ 的前提就有 ${\displaystyle (\exists p){\big \{}\,{\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}\,{\big \}}}$ 所以 ${\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 \}}}$ 另一方面，若假设 ${\displaystyle {\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}$ ${\displaystyle {\mathcal {M}}(\pi )\wedge ({\forall }^{M}z)\{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}$ 这样根据逻辑与的直观性质有 ${\displaystyle ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}$ ${\displaystyle ({\forall }^{M}z)\{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}$ 再根据(A4)有 ${\displaystyle {\mathcal {M}}(z)\Rightarrow \{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}$ ${\displaystyle {\mathcal {M}}(z)\Rightarrow \{\,(z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]\,\}}$ 如果再假设 ${\displaystyle {\mathcal {M}}(z)}$ ，根据MP律有 ${\displaystyle (z\in p)\Leftrightarrow [(z=x)\vee (z=y)]}$ ${\displaystyle (z\in \pi )\Leftrightarrow [(z=x)\vee (z=y)]}$ 这样根据演绎定理的推论(D1)和逻辑与的直观性质有 ${\displaystyle (z\in p)\Leftrightarrow (z\in \pi )}$ 也就是说 ${\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi ),\,{\mathcal {M}}(z)\,\vdash \,(z\in p)\Leftrightarrow (z\in \pi )}$ 其中 ${\displaystyle {\mathcal {B}}(p):={\mathcal {M}}(p)\wedge ({\forall }^{M}z)\{\,(z\in p)\Leftrightarrow [(z=x)\vee (z=y)]\,\}}$ 因为变数 ${\displaystyle z}$ 在 ${\displaystyle {\mathcal {B}}(p)}$ 和 ${\displaystyle {\mathcal {B}}(\pi )}$ 内完全不自由，对上式套用演绎定理(D)将 ${\displaystyle {\mathcal {M}}(z)}$ 移到右方后，再对 ${\displaystyle z}$ 套用普遍化会有 ${\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,\vdash \,(\forall ^{M}z)[\,(z\in p)\Leftrightarrow (z\in \pi )\,]}$ 这样根据本条目的外延定理有 ${\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,\vdash \,(p=\pi )}$ 那以演绎定理(D)将 ${\displaystyle {\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )}$ 移到右方，然后接连对 ${\displaystyle p}$ 和 ${\displaystyle \pi }$ 使用普遍化有 ${\displaystyle \vdash (\forall p)(\forall \pi )[\,{\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\Rightarrow (p=\pi )\,]}$ 故本定理得证。${\displaystyle \Box }$

这样的话会有

定理 — ${\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）${\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 \}}}$ 设 ${\displaystyle {\mathcal {A}}(p):=\neg [\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\,]\wedge (p=\varnothing )}$ ${\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)]\,\}}$ ${\displaystyle {\mathcal {C}}:={\mathcal {M}}(x)\wedge {\mathcal {M}}(y)}$ 那连续套用逻辑与合逻辑或的分配律与逻辑与的交换性会有 ${\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 \}}}$ 但考虑到逻辑与的直观性质和逻辑与的定义有 ${\displaystyle \vdash [\,{\mathcal {B}}(p)\wedge {\mathcal {A}}(\pi )\,]\Rightarrow (\neg {\mathcal {C}}\wedge {\mathcal {C}})}$ ${\displaystyle \vdash [\,{\mathcal {A}}(p)\wedge {\mathcal {B}}(\pi )\,]\Rightarrow (\neg {\mathcal {C}}\wedge {\mathcal {C}})}$ ${\displaystyle \vdash (\neg {\mathcal {C}}\wedge {\mathcal {C}})\Leftrightarrow \neg ({\mathcal {C}}\Rightarrow {\mathcal {C}})}$ 那根据恒等关系${\displaystyle (I)}$和常用的推理性质(T)有 ${\displaystyle \vdash \neg [\,{\mathcal {B}}(p)\wedge {\mathcal {A}}(\pi )\,]}$ ${\displaystyle \vdash \neg [\,{\mathcal {A}}(p)\wedge {\mathcal {B}}(\pi )\,]}$ 所以根据逻辑或的定义来重复使用演绎定理的推论(D1)会有 ${\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的等式定理会有 ${\displaystyle \vdash [\,{\mathcal {A}}(p)\wedge {\mathcal {A}}(\pi )\,]\Rightarrow (p=\pi )}$ 另一方面，根据（P-1）有 ${\displaystyle \vdash [\,{\mathcal {B}}(p)\wedge {\mathcal {B}}(\pi )\,]\Rightarrow (p=\pi )}$ 这样结合逻辑与的(DisJ)有 ${\displaystyle \vdash \{\,[\,{\mathcal {A}}(p)\vee {\mathcal {B}}(p)\,]\wedge [\,{\mathcal {A}}(\pi )\vee {\mathcal {B}}(\pi )\,]\,\}\Rightarrow (p=\pi )}$ 再对 ${\displaystyle p}$ 和 ${\displaystyle \pi }$ 套用普遍化有 ${\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加入新的双元函数符号 ${\displaystyle f_{p}^{2}(x,\,y)}$（简记为 ${\displaystyle \{x,\,y\}}$ ）和以下的新公理

${\displaystyle (P^{\prime })}$ — 
${\displaystyle {\bigg \{}\neg [\,{\mathcal {M}}(x)\wedge {\mathcal {M}}(y)\,]\wedge (\{x,\,y\}=\varnothing ){\bigg \}}\vee }$
${\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为集合，则 ${\displaystyle \{x,\,y\}}$ 就是那个只以x和y为元素的集合；但反之，若x和y不全为集合，则 ${\displaystyle \{x,\,y\}}$ 为空集”。

有序对

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

${\displaystyle \langle x\rangle :=x}$

${\displaystyle \langle x,\,y\rangle :=\{\{x\},\,\{x,\,y\}\}}$

${\displaystyle \langle x_{1},\,\dots ,\,\,x_{n},\,x_{n+1}\rangle :=\langle \langle x_{1},\,\dots ,\,\,x_{n}\rangle ,\,x_{n+1}\rangle }$

在不跟括弧产生混淆的情况下，也可以把${\displaystyle \langle x_{1},\,\dots ,\,\,x_{n},\,x_{n+1}\rangle }$记为${\displaystyle (x_{1},\,\dots ,\,\,x_{n},\,x_{n+1})}$。

关系

${\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 \}}}$

类函数

${\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 )\,\}}$

类函数跟普通函数的差别在于普通函数是个集合。

类的存在公理

属于类公理

${\displaystyle (K_{\in })}$ — ${\displaystyle (\exists e)(\forall ^{M}a)(\forall ^{M}b)\{[(a,\,b)\in e]\Leftrightarrow (a\in b)\}}$

交类公理

${\displaystyle (K_{i})}$ — ${\displaystyle (\forall x)(\forall y)(\exists i)({\forall }^{M}a)\{(a\in i)\Leftrightarrow [(a\in x)\wedge (a\in y)]\}}$

补类公理

${\displaystyle (K_{c})}$ — ${\displaystyle (\forall x)(\exists c)({\forall }^{M}a)[(a\in c)\Leftrightarrow (a\not \in x)]}$

定义域公理

${\displaystyle (K_{D})}$ — ${\displaystyle (\forall x)(\exists d)(\forall ^{M}a)\{(a\in d)\Leftrightarrow (\exists ^{M}b)[(a,\,b)\in x]\}}$

积类公理

${\displaystyle (K_{p})}$ — ${\displaystyle (\forall x)(\exists p)(\forall ^{M}a)(\forall ^{M}b)\{[\,(a,\,b)\in p\,]\Leftrightarrow (a\in x)\}}$

置换类公理

${\displaystyle (K_{\sigma 1})}$ — ${\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 ]\}}$

${\displaystyle (K_{\sigma 2})}$ — ${\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）：

• 对任意变数 ${\displaystyle x}$ 和 ${\displaystyle y}$ ，${\displaystyle x\in y}$ 为可叙述公式。
• 若 ${\displaystyle {\mathcal {P}}}$ 与 ${\displaystyle {\mathcal {Q}}}$ 为可叙述公式， ${\displaystyle x}$ 为任意变数，则 ${\displaystyle (\neg {\mathcal {P}})}$ 、 ${\displaystyle ({\mathcal {P}}\Rightarrow {\mathcal {Q}})}$ 与 ${\displaystyle (\forall ^{M}x){\mathcal {P}}}$ 都是可叙述公式。

这样依据上列诸类存在公理，就有以下元定理：

类的存在元定理 — 
${\displaystyle {\mathcal {P}}}$ 为一条只内含变数 ${\displaystyle x_{1},\,\dots ,\,x_{n},\,y_{1},\,\dots ,\,y_{m}}$ 的可叙述公式，则有

${\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}}]}$

证明

集合的公理

并集公理

${\displaystyle (U)}$ — ${\displaystyle (\forall ^{M}x)(\exists ^{M}u)(\forall ^{M}a)[(a\in u)\Leftrightarrow (\exists ^{M}\xi \in x)(a\in \xi )]}$

幂集公理

${\displaystyle (W)}$ — ${\displaystyle (\forall ^{M}x)(\exists ^{M}w)(\forall ^{M}\xi )\{(\xi \in w)\Leftrightarrow (\xi \subseteq x)\}}$

子集公理

${\displaystyle (S)}$ — ${\displaystyle (\forall ^{M}x)(\forall y)(\exists ^{M}z)(\forall ^{M}a)\{(a\in z)\Leftrightarrow [(a\in x)\wedge (a\in y)]\}}$

无穷公理

${\displaystyle (I)}$ — ${\displaystyle (\exists ^{M}I)\{(\varnothing \in I)\wedge (\forall ^{M}a)[(a\in I)\Rightarrow (a\cap \{a\}\in I)]\}}$

取代公理及其替代

${\displaystyle (R)}$ — ${\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 \}}}$

直观意义为“${\displaystyle f}$ 为类函数则对任意集合 ${\displaystyle x}$ ，存在一个集合 ${\displaystyle r}$ ，正好就是在 ${\displaystyle f}$ 的规则下映射出的像”。

大小限制公理

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

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

选择公理