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

冯·诺伊曼-博内斯-哥德尔集合论（von Neumann–Bernays–Gödel Set Theory，NBG）是种以类为直观动机的一阶公理化集合论，它是策梅洛-弗兰克尔集合论（Zermelo-Fraenkel Set Theory，ZF）的保守扩展（ZF里可以证明的定理也都是NBG的定理），而且NBG仅需在一阶逻辑基本的公理模式上添加有限数目的公理，但ZF需添加与集合有关的公理模式。

NBG首先由冯·诺伊曼在1920年代提出，从1937年开始由保罗·博内斯作修改，在1940年由哥德尔进一步简化。

## 基本符号

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

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

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

### 类与集合

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

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

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

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

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

可称为“ $x$ 是真类（proper class）”。

### 子类

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

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

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

### 与集合相关的量词简写

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

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

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

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

## 等号公理

### 看待等号的不同方式

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

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

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

$$(T^{\prime})$$

$$(x=y) \Leftrightarrow \forall a[\, (a \in x) \Leftrightarrow (a \in y) \,]$$ 直观上可理解为“类x的元素就是类y的元素，等价于类x等于类y”。

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

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

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

### 等号的良置

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

$$(T)$$

$$(x=y) \Rightarrow \forall z[\, (x \in z) \Leftrightarrow (y \in z) \,]$$

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

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

NBG是带相等符号 $(x=y)$ 的一阶逻辑理论

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

### 真子类

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

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

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

### 外延定理

为以下的定理可直观理解为“x等于y等价于，对所有集合z，z属于x等价于z属于y”，也就是说，等于的定义可以“限缩”成元素为集合的状况。$\vdash (x = y) \Leftrightarrow (\forall^M z)[\,(z \in x) \Leftrightarrow (z \in y)\,]$

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

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

### 特定条件下的存在性

以下关于一阶逻辑的一般性定理，也大大简化了 NBG 引入新公理的过程所需的证明$x$ 于合式公式 $\mathcal{A}$ 完全不自由且 $c$ 是常数符号。若

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

则有

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

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

## 空集合公理

$$(N)$$

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

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

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

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

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

也就是直观上，“空集是唯一存在的”，这样根据函数符号与唯一性一节，可以在NBG加入新的常数符号 $\varnothing$ 和以下的新公理（严格来说，把完全没有函数符号和常数符号的NBG扩展成有 $\varnothing$ 的新NBG，但两个理论是等效的）

$$(N^{\prime})$$

$$\mathcal{M}(\varnothing) \wedge ({\forall}^{M} y)(y\not\in \varnothing)$$

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

## 配对公理

$$(P)$$

$$({\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”。

这个公理还确保了以下的唯一性：

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

这样的话会有$$\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）$\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\}$ 设 :$\mathcal{A}(p) := \neg[\,\mathcal{M}(x) \wedge \mathcal{M}(y)\,] \wedge (p = \varnothing)$ :$\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)]\,\}$ :$\mathcal{C} := \mathcal{M}(x) \wedge \mathcal{M}(y)$ 那连续套用逻辑与合逻辑或的分配律与逻辑与的交换性会有 :$\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\}$ 但考虑到逻辑与的直观性质和逻辑与的定义有 :$\vdash [\,\mathcal{B}(p) \wedge \mathcal{A}(\pi)\,] \Rightarrow (\neg\mathcal{C}\wedge\mathcal{C})$ :$\vdash [\,\mathcal{A}(p) \wedge \mathcal{B}(\pi)\,] \Rightarrow (\neg\mathcal{C}\wedge\mathcal{C})$ :$\vdash (\neg\mathcal{C}\wedge\mathcal{C}) \Leftrightarrow \neg(\mathcal{C}\Rightarrow\mathcal{C})$ 那根据恒等关系$(I)$和常用的推理性质(T)有 :$\vdash \neg[\,\mathcal{B}(p) \wedge \mathcal{A}(\pi)\,]$ :$\vdash \neg[\,\mathcal{A}(p) \wedge \mathcal{B}(\pi)\,]$ 所以根据逻辑或的定义来重复使用演绎定理的推论(D1)会有 :$\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的等式定理会有 :$\vdash [\,\mathcal{A}(p) \wedge \mathcal{A}(\pi)\,] \Rightarrow (p = \pi)$ 另一方面，根据（P-1）有 :$\vdash [\,\mathcal{B}(p) \wedge \mathcal{B}(\pi)\,] \Rightarrow (p=\pi)$ 这样结合逻辑与的(DisJ)有 :$\vdash \{\, [\,\mathcal{A}(p) \vee \mathcal{B}(p)\,] \wedge [\,\mathcal{A}(\pi) \vee \mathcal{B}(\pi)\,] \,\} \Rightarrow (p=\pi)$ 再对 $p$ 和 $\pi$ 套用普遍化有 :$\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）与逻辑与的直观性质，本定理就得证了。$\Box$

所以根据函数符号与唯一性一节，可以在NBG加入新的双元函数符号 $f^2_p(x,\,y)$（简记为 $\{x,\,y\}$）和以下的新公理

$$(P^{\prime})$$

$$\bigg\{ <pre> \neg[\,\mathcal{M}(x) \wedge \mathcal{M}(y)\,] \wedge (\{x,\,y\} = \varnothing) </pre> \bigg\} \vee$$

$$\bigg\{ <pre> \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)]\,\} </pre> \bigg\}$$

这个新公理的直观意思是“若x和y为集合，则 $\{x,\,y\}$ 就是那个只以x和y为元素的集合；但反之，若x和y不全为集合，则 $\{x,\,y\}$ 为空集”。

### 有序对

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

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

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

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

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

### 关系

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

### 类函数

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

$$(\exists e)(\forall^M a)(\forall^M b)\{ <pre> [(a,\,b)\in e] \Leftrightarrow (a\in b) </pre> \}$$

### 交类公理

$$(K_{i})$$

$$(\forall x)(\forall y)(\exists i)({\forall}^{M} a)\{ <pre> (a \in i) \Leftrightarrow [(a\in x) \wedge (a\in y)] </pre> \}$$

### 补类公理

$$(K_{c})$$

$$(\forall x)(\exists c)({\forall}^{M} a)[ <pre> (a\in c) \Leftrightarrow (a\not\in x) </pre> ]$$

### 定义域公理

$$(K_{D})$$

$$(\forall x)(\exists d)(\forall^M a)\{ <pre> (a\in d) \Leftrightarrow (\exists^M b)[(a,\,b) \in x] </pre> \}$$

### 积类公理

$$(K_{p})$$

$$(\forall x)(\exists p)(\forall^M a)(\forall^M b)\{ <pre> [\,(a,\,b) \in p\,] \Leftrightarrow (a \in x) </pre> \}$$

### 置换类公理

$$(K_{\sigma 1})$$

$$(\forall x)(\exists \sigma)(\forall^M a)(\forall^M b)(\forall^M c)\{ <pre> [(a,\,b,\,c) \in x] \Leftrightarrow [(b,\,c,\,a) \in \sigma] </pre> \}$$ $$(K_{\sigma 2})$$

$$(\forall x)(\exists \sigma)(\forall^M a)(\forall^M b)(\forall^M c)\{ <pre> [(a,\,b,\,c) \in x] \Leftrightarrow [(a,\,c,\,b) \in \sigma] </pre> \}$$

### 类的存在元定理

这个元定理对应到ZFC尔集合论的分类公理。

首先需要递归地定义“可叙述公式”（predicative well-formed formula）：

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

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

$\mathcal{P}$ 为一条只内含变数 $x_1,\,\dots,\,x_n,\,y_1,\,\dots,\,y_m$ 的可叙述公式，则有

$$\vdash (\exists s)(\forall^M x_1)\ldots(\forall^M x_n)[ <pre> (\langle x_1,\,\dots,\,x_n\rangle \in s) \Leftrightarrow \mathcal{P} </pre> ]$$

证明

## 集合的公理

### 并集公理

$$(U)$$

$$(\forall^M x)(\exists^M u)(\forall^M a)[ <pre> (a \in u) \Leftrightarrow (\exists^M \xi \in x)(a \in \xi) </pre> ]$$

### 幂集公理

$$(W)$$

$$(\forall^M x)(\exists^M w)(\forall^M \xi)\{ <pre> (\xi \in w) \Leftrightarrow (\xi \subseteq x) </pre> \}$$

### 子集公理

$$(S)$$

$$(\forall^M x)(\forall y)(\exists^M z)(\forall^M a)\{ <pre> (a \in z) \Leftrightarrow [(a \in x) \wedge (a \in y)] </pre> \}$$

## 无穷公理

$$(I)$$

$$(\exists^M I)\{ <pre> (\varnothing \in I) \wedge (\forall^M a)[ (a \in I) \Rightarrow (a \cap \{a\} \in I) ] </pre> \}$$

## 取代公理及其替代

$$(R)$$

$$Fnc(f) \Rightarrow (\forall^M x)(\exists^M r)(\forall^M b)\bigg\{ <pre> (b \in r) \Rightarrow (\exists^M a)\{ (\langle a,\,b\rangle \in r) \wedge (a \in x) \} </pre> \bigg\}$$

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

### 大小限制公理

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

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

## 引用

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