新基础集合论（综述）

贡献者： 待更新

　　 本文根据 CC-BY-SA 协议转载翻译自维基百科相关文章。

　　 在数学逻辑中，新基础（New Foundations，简称 NF）是一种非良基、可有限公理化的集合论，由威拉德·范·奥曼·奎因构思，旨在简化《数学原理》中的类型论。

1. 定义

　　 NF 的良构公式是命题演算的标准公式，具有两个基本谓词：相等（$=$）和成员关系（$\in$）。NF 可以仅通过两个公理模式来表述：

• 外延性：具有相同元素的两个对象是相同的对象。形式化地说，给定任意集合 $A$ 和任意集合 $B$，如果对于任意集合 $X$，$X$ 是 $A$ 的成员当且仅当 $X$ 是 $B$ 的成员，则 $A$ 等于 $B$。
• 受限的理解公理模式：对于每个分层公式 $\varphi$，集合 $\{x\mid \varphi \}$ 存在。

　　 一个公式 $\varphi$ 被称为分层的，如果存在一个从 $\varphi$ 的语法结构的各部分到自然数的函数 $f$，使得：对于 $\varphi$ 中的任意原子子公式 $x\in y$，满足 $f(y)=f(x)+1$；对于 $\varphi$ 中的任意原子子公式 $x=y$，满足 $f(x)=f(y)$。

有限公理化

　　 NF 可以被有限公理化。[1] 这种有限公理化的一个优点是，它消除了分层性的概念。有限公理化中的公理对应于一些自然的基本构造，而分层理解公理虽然强大，但不一定直观。在其入门书籍中，Holmes 选择将有限公理化作为基本框架，并将分层理解公理作为一个定理来证明。[2]

　　 具体的公理集合可能有所不同，但通常包含以下大部分公理，而其余的可以作为定理证明：[3][1]

• 外延性：如果 $A$ 和 $B$ 是集合，并且对于每个对象 $x$，$x$ 是 $A$ 的元素当且仅当 $x$ 是 $B$ 的元素，则 $A=B$。[4] 这一公理也可以视为对相等符号的定义。[5][6]
• 单元素集：对于每个对象 $x$，集合 $\iota (x)=\{x\}=\{y\mid y=x\}$ 存在，并称为 $x$ 的单元素集。[7][8]
• 笛卡尔积：对于任意集合 $A$ 和 $B$，集合 $A\times B=\{(a,b)\mid a\in A\text{ 且 }b\in B\}$ 称为 $A$ 和 $B$ 的笛卡尔积，并且它的存在性被保证。[9] 该公理可以限制为某个特定的交叉积，例如 $A\times V$ 或 $V\times B$ 的存在。[10][11]
• 逆关系：对于每个关系 $R$，集合 $R^{-1}=\{(x,y)\mid (y,x)\in R\}$ 存在；可以观察到，$x{R}^{-1}y$ 当且仅当 $yRx$。[12][13][14]
• 单元素映像：对于任意关系 $R$，集合 $R\iota =\{(\{x\},\{y\})\mid (x,y)\in R\}$ 存在，并称为 $R$ 的单元素映像。[15][16][17]
• 定义域：如果 $R$ 是一个关系，则集合 $\text{dom}(R)=\{x\mid \mathrm{\exists }y.(x,y)\in R\}$ 存在，并称为 $R$ 的定义域。[12] 这一公理可以通过类型降维操作来定义。[18]
• 包含关系：集合 $[\subseteq ]=\{(x,y)\mid x\subseteq y\}$ 存在。[19] 等价地，我们可以考虑集合 $[\in ]=[\subseteq ]\cap (1\times V)=\{(\{x\},y)\mid x\in y\}$ 的存在性。[20][21]
• 补集：对于每个集合 $A$，其补集 $A^c=\{x\mid x\notin A\}$ 存在。[22]
• （布尔）并集：如果 $A$ 和 $B$ 是集合，则它们的并集 $A\cup B=\{x\mid x\in A\text{ 或 }x\in B\text{或两者皆是}\}$ 存在。[23]
• 全集：全集 $V=\{x\mid x=x\}$ 存在。显然，对于任何集合 $$，都有 $x\cup x^c=V$ 其中 $x^c$ 表示 $x$ 的补集。[22]
• 有序对：对于任意对象 $a$ 和 $b$，有序对 $(a,b)$ 存在，并且 $(a,b)=(c,d)⟺a=c\text{ 且 }b=d$ 这种定义也可以推广到更大的元组。如果使用某种有序对的构造方法，则它可以被定义，而不作为一个独立的公理。[24]
• 投影：集合 ${\pi }_1=\{((x,y),x)\mid x,y\in V\}$ 和 ${\pi }_2=\{((x,y),y)\mid x,y\in V\}$ 存在。这些集合对应于有序对的第一和第二分量的投影关系。[25]
• 对角线关系：集合 $[=]=\{(x,x)\mid x\in V\}$ 存在，并被称为相等关系。[25]
• 集合并：如果 $A$ 是一个集合，并且 $A$ 的所有元素都是集合，则集合并 $\bigcup [A]=\{x\mid \mathrm{\exists }B,x\in B\text{ 且 }B\in A\}$ 存在。[26]
• 相对积：如果 $R$ 和 $S$ 是关系，则相对积 $(R|S)=\{(x,y)\mid \mathrm{\exists }z,xRz\text{ 且 }zSy\}$ 存在。[12]
• 反交：集合 $x|y=\{z\mid \mathrm{\neg }(z\in x\wedge z\in y)\}$ 存在。这一运算等价于补集和并集的组合，其中 $x^c=x|x$ 和 $x\cup y=x^c|y^c$[27]
• 基数为 1 的集合：所有单元素集的集合 $1=\{x\mid \mathrm{\exists }y:(\mathrm{\forall }w,w\in x\leftrightarrow w=y)\}$ 存在。[28][29]
• 元组插入：对于一个关系 $R$，集合 $I_2(R)=\{(z,w,t)\mid (z,t)\in R\}$ 和 $I_3(R)=\{(z,w,t)\mid (z,w)\in R\}$ 存在。[30][31]
• 类型降维：对于任何集合 $S$，集合 $TL(S)=\{z\mid \mathrm{\forall }w,(w,\{z\})\in S\}$ 存在。[32][33]

类型化集合论

　　 新基础集合论与拉塞尔型的非分层类型化集合论密切相关。TST 是《数学原理》中类型论的简化版本，采用线性类型层次结构。在这种多排序理论（many-sorted theory）中，每个变量和集合都被赋予一个类型（type）。通常，类型指数使用上标表示：$x^n$ 表示类型为 $n$ 的变量。类型0由未进一步描述的个体组成。对于每个（元）自然数 $n$，类型 $n+1$ 的对象是类型 $n$ 对象的集合。相等关系仅适用于相同类型的对象。类型 $n$ 的集合仅包含类型 $n-1$ 的成员。TST 的公理包括：外延性：适用于相同（正）类型的集合。理解公理：如果 $\varphi (x^n)$ 是一个公式，则集合 $\{x^n\mid \varphi (x^n){\}}^{n+1}$ 存在，即：$\mathrm{\exists }{A}^{n+1}\mathrm{\forall }{x}^n[x^n\in A^{n+1}\leftrightarrow \varphi (x^n)]$ 是一个公理，其中 $A^{n+1}$ 代表集合 $\{x^n\mid \varphi (x^n){\}}^{n+1}$，并且 $A^{n+1}$ 在 $\varphi (x^n)$ 中不是自由变量。这种类型论比《数学原理》中最初提出的类型论要简单得多，后者包括了关系的类型，而这些关系的参数不一定具有相同的类型。

　　 NF 和 TST 之间存在一种类型标注的添加或删除的对应关系：在 NF 的理解模式中，公式是 “分层的” 当且仅当该公式可以按照 TST 的规则赋予类型。这意味着 NF 公式可以映射到 TST 公式的集合，其中每个 TST 公式都带有不同的类型索引。这种映射是一对多的，因为 TST 允许多个相似的公式。例如，在 TST 公式中，将所有类型索引提升 1，仍然会得到一个新的、有效的 TST 公式。

纠缠类型论

　　 纠缠类型论（TTT）是 TST 的扩展，其中每个变量的类型由序数而非自然数标注。其良构的原子公式包括：相等关系：$x^n=y^n$ 成员关系：$x^m\in y^n$（其中 $m<n$）TTT 的公理与 TST 的公理相同，但其中每个类型为 $i$ 的变量都会被映射到一个变量 $s(i)$，其中 $s$ 是一个递增函数。

　　 TTT 被认为是一种 “怪异的” 理论，因为它的每个类型都以相同的方式与所有较低类型相关。例如：类型 2 的集合既可以包含类型 1 的成员，也可以包含类型 0 的成员。外延性公理声明，类型 2 的集合仅由其类型 1 成员或类型 0 成员唯一确定。与 TST 不同：在 TST 中，自然模型满足每个类型 $i+1$ 都是类型 $i$ 的幂集。在 TTT 中，每个类型同时被解释为所有较低类型的幂集。尽管如此：NF 的模型可以很容易地转换为 TTT 的模型，因为在 NF 中，所有类型本质上都是相同的。反过来，经过更复杂的论证，可以证明 TTT 的一致性（Consistency of TTT）能够推出 NF 的一致性。[34]

NFU 及其他变种

　　 带有基数元素的新基础集合论是 NF 的一个重要变种，由 Jensen 提出，[35]并由 Holmes 进一步澄清。[3]基数元素是不是集合的对象：它们不包含任何元素，但可以被包含在集合中。在 NFU 最简单的公理化形式之一中，基数元素被视为多个不同的空集，从而削弱了 NF 的外延性公理，改为：

• 弱外延性（Weak Extensionality）：两个非空对象如果具有相同的元素，则它们是相同的对象。形式化地： $$\mathrm{\forall }xyw.(w\in x)\to (x=y\leftrightarrow (\mathrm{\forall }z.z\in x\leftrightarrow z\in y))$$

　　 这意味着：对于非空集合，外延性仍然成立。对于空集和基数元素，外延性不适用，它们可以是多个不同的对象。在这种公理化下：理解模式保持不变。但是，如果某个集合的定义公式 $\varphi (x)$ 无解（即不可满足），则集合 $\{x\mid \varphi (x)\}$ 可能不是唯一的（即它可以对应多个不同的基数元素）。

　　 然而，为了方便使用，通常更希望有一个唯一的、“标准” 空集。这可以通过引入集合性谓词 $\text{set}(x)$ 来区分集合和基数元素（原子）。 其公理如下：[36]

• 集合公理（Sets）：只有集合才有成员，即：$\mathrm{\forall }xy.x\in y\to \text{set}(y)$ 解释：如果 $x$ 是 $y$ 的成员，则 $y$ 必须是一个集合。这意味着基数元素不能包含任何成员，它们只能被包含在集合中。
• 外延性公理（Extensionality）：两个具有相同元素的集合是相同的集合，即：$\mathrm{\forall }yz.(\text{set}(y)\wedge \text{set}(z)\wedge (\mathrm{\forall }x.x\in y\leftrightarrow x\in z))\to y=z.$ 解释：只有当 $y$ 和 $z$ 都是集合时，才适用外延性。基数元素（原子）不受外延性约束，它们可以是多个不同的对象，即使它们没有元素。
• 理解公理（Comprehension）：对于每个分层公式 $\varphi (x)$，集合 $\{x\mid \varphi (x)\}$ 存在，即：$\mathrm{\exists }A.\text{set}(A)\wedge (\mathrm{\forall }x.x\in A\leftrightarrow \varphi (x))$ 解释：分层公式（Stratified formula）：满足 NF 逻辑规则的公式。集合 $A$ 的存在性：只要 $\varphi (x)$ 符合 NF 的分层性规则，该集合就存在。

　　 $N{F}_3$：NF 的一个子理论，仅允许最多三种类型的分层公式（即 $x,y,z$ 这样的最多三层类型）。$N{F}_4$：与完整的 NF 等价，即没有基数元素，并且允许所有满足分层性条件的理解公理。

　　 数学逻辑（Mathematical Logic, ML）是 NF 的扩展，它不仅包含集合，还包含适当的类。ML 由 Quine 提出，并由 Hao Wang 修订。Wang 证明，NF 与修订后的 ML 具有等一致性，即它们的一致性（无矛盾性）是等价的。

2. 构造

　　 本节讨论 NF 中的一些具有问题的构造。关于 NFU 中数学的进一步发展，以及与 ZFC 体系中相应发展的比较，请参见集合论中数学的实现。

有序对

　　 在 TST（以及 NF 和 NFU）中，关系和函数通常被定义为有序对的集合。从分层性的角度来看，理想的情况是：一个关系或函数的类型应仅比其定义域中的元素的类型高一层。这要求定义有序对的方式，使其类型与其参数相同（即类型级有序对，type-level ordered pair）。然而，常见的有序对定义：$(a,b{)}_K:=\{\{a\},\{a,b\}\}$ 会导致 $(a,b)$ 的类型比参数 $a$ 和 $b$ 的类型高两层。因此，在分层性分析中，一个函数的类型比其定义域中的元素高三层。在 NF 及其相关理论中，通常采用 Quine 的集合论定义的有序对，该定义能够保持有序对的类型与其参数相同，从而避免类型层次的额外提升。然而，Quine 的定义依赖于对每个元素 $a$ 和 $b$ 进行集合运算，因此在 NFU 中无法直接适用。

　　 作为一种替代方法，Holmes[3] 直接将有序对 $(a,b)$ 作为原始概念，并同时引入其左投影和右投影：左投影：${\pi }_1((a,b))=a$ 右投影：${\pi }_2((a,b))=b$ 在 Holmes 对 NFU 的公理化中：理解模式——即对于任意分层公式 $\varphi$，集合 $\{x\mid \varphi (x)\}$ 的存在性——并非直接作为公理，而是后续证明的定理。

　　 因此，类似于 ${\pi }_1=\{((a,b),a)\mid a,b\in V\}$ 这样的表达式不能被视为正式的定义。幸运的是：无论有序对的类型层次（type-level）是通过定义（如 Quine 的方法）还是通过公理假设（即作为原始概念）来保证，通常都不会影响理论的一致性。

自然数与无穷公理

　　 通常形式的无穷公理基于冯·诺伊曼对自然数的构造。然而，该构造不适用于 NF，因为后继运算的定义（以及冯·诺伊曼数的许多其他方面）无法被分层化。在 NF 中，通常使用弗雷格的自然数定义，即：自然数 $n$ 由所有恰好有 $n$ 个元素的集合的集合表示。在这种定义下：零（0）可以简单地定义为：$\{\varnothing \}$ 即仅包含空集的集合。后继运算可以以分层化的方式定义：$S(A)=\{a\cup \{x\}\mid a\in A\wedge x\notin a\}$ 这里：$A$ 是某个自然数 $n$ 对应的集合，$x$ 是一个新元素，不属于 $a$。在此定义下，可以写出类似于通常无穷公理的表述。然而，该表述在 NF 中将是平凡成立的，因为全集 $V$ 本身就是一个归纳集，满足所有自然数构造规则。

　　 由于归纳集总是存在，自然数集合 $\mathbf{N}$ 可以定义为所有归纳集的交集。这一定义使得对分层语句 $P(n)$ 进行数学归纳成为可能，因为：集合 $\{n\in \mathbf{N}\mid P(n)\}$ 可以被构造。当 $P(n)$ 满足数学归纳的条件时，该集合本身就是一个归纳集，从而满足数学归纳法的要求。

　　 有限集合可以定义为属于某个自然数的集合。然而，证明全集 $V$ 不是 “有限集”（即 $|V|$ 不是一个自然数）并不显然。假设：$|V|=n\in \mathbf{N}$ 则：$n=\{V\}$（可以通过归纳证明，有限集合不与其任何真子集等势）。由此推导：$n+1=S(n)=\varnothing$ 并且所有后续的自然数也都会是空集，从而导致算术体系崩溃。为避免这一问题，可以在 NF 中引入无穷公理：$\varnothing \notin \mathbf{N}$ 这确保 $V$ 的基数不会是有限数，从而维持算术的正确性。[37]

　　 从直觉上看，似乎应该可以通过构造某种 “外部” 无限序列（externally infinite sequence）的集合来在 NF(U) 中证明无穷公理，例如：$\varnothing ,\{\varnothing \},\{\{\varnothing \}\},\dots$ 然而，这样的序列只能通过非分层化的方法构造（这一点可以通过 TST 本身存在有限模型来佐证），因此无法在 NF(U) 中进行这样的证明。实际上，无穷公理在 NFU 中是逻辑上独立的：存在 NFU 的模型，其中 $|V|$ 是非标准自然数。在这些模型中，数学归纳法可以应用于 $|V|$，使得它无法与标准的自然数区分开来。

　　 然而，在某些情况下，可以在 NF 及其变种中证明无穷公理，在这些情况下，它可能被称为无穷定理：

• 在 NF（无基数元素的版本）中：Specker[38] 证明了选择公理（Axiom of Choice）在 NF 中是错误的。由于可以通过数学归纳法证明每个有限集合都具有一个选择函数（这是一个分层化的条件），因此全集 $V$ 必然是无限的。
• 在 NFU 中，如果引入公理断言类型级有序对（type-level ordered pair）的存在：全集 $V$ 与其真子集 $V\times \{0\}$ 等势，这蕴含无穷性。[37]反过来，NFU + Infinity + Choice 可以证明类型级有序对的存在（但此结果尚需引用支持）。NFU + Infinity 可以解释（interpret）NFU + “存在类型级有序对”（虽然这两个理论不完全相同，但它们的差异并不重要）。

　　 更强的无穷公理：可以假设自然数集合是一个强康托尔集合。NFUM（即 NFU + Infinity + Large Ordinals + Small Ordinals）等价于 Morse–Kelley 集合论（Morse–Kelley Set Theory, MK），再加上一个对适当类的谓词，该谓词是一个κ-完备的非主超滤，定义在适当类的序数 $\kappa$ 上。[39]

大集合

　　 NF（以及 NFU + Infinity + Choice，它已知是一致的）允许构造两类在 ZFC 及其扩展中被禁止的集合，因为它们 “过大”（在某些集合论中，这些对象被视为适当类）。

• 全集 $V$ 由于 $x=x$ 是一个分层化公式，根据理解公理，全集 $V=\{x\mid x=x\}$ 存在。直接的一个推论是：所有集合都有补集。在 NF 中，整个集合论宇宙具有布尔代数结构。
• 基数与序数在 NF（以及 TST）中，所有具有 $n$ 个元素的集合的集合是存在的（这种 “循环” 只是表面上的）。因此，弗雷格（Frege）的基数定义在 NF 和 NFU 中是有效的：基数定义为等势关系下的集合的等价类。如果存在双射 $f:A\to B$，则集合 $A$ 和 $B$ 等势，记作：$A\sim B$ 序数的定义类似，它是良序集的等价类。

笛卡尔封闭性

　　 在 NF 中，以集合作为对象、以这些集合之间的函数作为箭头构成的范畴不是笛卡尔封闭的。[40]由于 NF 不满足笛卡尔封闭性：并非所有函数都可以柯里化，这与直觉上的期望不同。NF 不是一个拓扑斯。

3. 集合论悖论的解决

　　 NF 乍看之下似乎会遭遇与朴素集合论类似的问题，但事实并非如此。例如：Russell 集合 $\{x\mid x\notin x\}$ 在 NF 中并不是一个公理保证存在的集合，因为公式 $x\notin x$ 不能被分层化。NF 通过完全不同于 ZFC 等良基集合论方法，避免了集合论中的三大悖论。此外，NF 及其变种还基于这些悖论的解决方案发展出许多独特且有用的概念。

罗素悖论

　　 NF 对罗素悖论的解决方案是直接且显然的：$x\notin x$ 不是一个分层化公式，因此，理解公理并不会断言 $\{x\mid x\notin x\}$ 这一集合的存在。Quine 曾表示，他构造 NF 时，首要考虑的就是如何避免罗素悖论。[41]

康托尔悖论与康托尔集合

　　 康托尔悖论的核心问题是：是否存在最大的基数，或者等价地，是否存在一个基数最大的集合。在 NF 中：全集 $V$ 显然是一个基数最大的集合，因为它包含所有集合。然而，在 ZFC 中，康托尔定理表明：对于任何集合 $A$，其幂集 $P(A)$ 的基数严格大于 $A$：$|P(A)|>|A|$ 这意味着，若取 $A=V$，则 $P(V)$ 的基数应该比 $V$ 更大，但 $V$ 已经是最大集合，这似乎导致矛盾。

　　 当然，由于 $V$ 是全集，从 $P(V)$ 到 $V$ 存在一个单射，因此康托尔定理在其原始形式下在 NF 中不成立。实际上，康托尔定理的证明依赖于对角化论证，即构造集合：$B=\{x\in A\mid x\notin f(x)\}$ 在 NF 中：$x$ 和 $f(x)$ 必须被赋予相同的类型，因此 $B$ 的定义无法被分层化，导致该集合无法通过理解公理被构造。更进一步，如果我们选择平凡单射：$f:P(V)\to V,x\mapsto x$ 那么 $B$ 将与罗素悖论中的非法集合完全相同，因此无法存在。由此可见，NF 通过分层性规则自然地避免了康托尔悖论。

　　 这种结论的失败并不令人惊讶，因为在 TST 中，$|A|<|P(A)|$ 没有意义：幂集 $P(A)$ 的类型比 $A$ 高一层，因此它们的基数不具可比性。在 NF 中，由于所有类型被合并，$|A|<|P(A)|$ 成为了一个语法上有效的陈述，但任何涉及理解公理的一般性证明都不太可能成立。

　　 通常修正这种类型问题的方法是：用 $P_1(A)$ 代替 $A$，其中：$P_1(A)$ 表示 $A$ 的所有单元素子集的集合（the set of one-element subsets of $A$）。实际上，康托尔定理的正确类型版本：$|P_1(A)|<|P(A)|$ 在 TST 中是一个定理（依赖于对角化论证），因此它在 NF 中同样成立。特别地，在 NF 中：$|P_1(V)|<|P(V)|$ 即：单元素集合的数量少于一般集合的数量。在 NFU 中，这意味着： 单元素集合的数量少于一般对象的数量。单射 $x\mapsto \{x\}$ 在 NFU 中不是集合从全集 $V$ 到单元素集合 $P_1(V)$ 的 “显然的” 双射：$x\mapsto \{x\}$ 并不是一个集合，因为：该映射的定义不满足分层化，因此它无法通过 NFU 的理解公理构造。NFU + 选择公理的所有模型中：$|P_1(V)|<|P(V)|\ll |V|$ 即：$P_1(V)$ 的基数小于 $P(V)$，且 $P(V)$ 的基数远远小于全集 $V$。选择公理不仅允许证明基数元素的存在，还可以证明 $P(V)$ 和 $V$ 之间存在多个不同的基数。

　　 然而，不同于 TST，$|A|=|P_1(A)|$ 在 NF(U) 中是一个句法上的陈述，并且如上所示，可以讨论其对特定值 $A$ 的真值（例如，当 $A=V$ 时，它是假的）。满足直观上令人信服的条件 $|A|=|P_1(A)|$ 的集合 $A$ 被称为康托尔集合：康托尔集合满足通常形式的康托尔定理。满足进一步条件 $(x\mapsto \{x\})\lceil A$（即单元素映射在 $A$ 上的限制仍是一个集合）的集合 $A$ 不仅是康托尔集合，而且是强康托尔集合。

Burali-Forti 悖论与 T 运算

　　 关于最大序数的Burali-Forti 悖论在 NF（New Foundations）中以相反的方式得到解决：在 NF 中，即使可以访问序数的集合，也无法构造出 “最大序数”。人们可以构造出对应于所有序数的自然良序的序数 $\mathrm{\Omega }$，但这并不意味着 $\mathrm{\Omega }$ 比所有这些序数都大。

　　 要在 NF 中形式化 Burali-Forti 悖论，首先需要对序数的概念进行形式化。在 NF 中，序数的定义方式与朴素集合论相同，即它们被定义为良序集在同构关系下的等价类。这是一个分层的定义，因此可以无问题地定义序数的集合 $\mathrm{Ord}$。在 NF 中，超限归纳适用于分层陈述，这使得可以证明序数的自然序关系是 $\mathrm{Ord}$ 上的一个良序。具体来说：$\alpha \le \beta ⟺\text{ 存在良序关系 }R\in \alpha ,S\in \beta \text{，使得 }S\text{ 是 }R\text{的延续}$ 根据序数的定义，这个良序关系本身也属于某个序数 $\mathrm{\Omega }\in \mathrm{Ord}$。在朴素集合论中，通常可以通过超限归纳证明：每个序数 $\alpha$ 的序型正好是所有小于 $\alpha$ 的序数的自然序关系的序型。但如果在 NF 中应用这一点，就会导致矛盾：因为按照定义，$\mathrm{\Omega }$ 是所有序数的序型，而不是它们的某个真初始片段的序型。这就导致了 Burali-Forti 悖论。

　　 然而，陈述 “$\alpha$ 是所有小于 $\alpha$ 的序数的自然序关系的序型” 并不是分层的，因此超限归纳在 NF 中无法使用。实际上，“小于 $\alpha$ 的序数的自然序关系 $R_{\alpha }$ 的序型 $\beta$” 的类型至少比 $\alpha$ 高出两层：关系 $R_{\alpha }=\{(x,y)\mid x\le y<\alpha \}$ 的类型比 $\alpha$ 高一层（假设有序对 $(x,y)$ 是类型层次上的有序对）。 - 序型（即等价类）$\beta =\{S\mid S\sim R_{\alpha }\}$ 的类型比 $R_{\alpha }$ 再高一层。如果采用的是库拉托夫斯基有序对（即 $(x,y)=\{\{x\},\{x,y\}\}$），那么 $(x,y)$ 的类型会比 $x$ 和 $y$ 高两层，因此 $\beta$ 的类型相对于 $\alpha$ 总共会高出四层。

　　 为了解决这种类型问题，需要使用 T 运算，即 $T(\alpha )$，它的作用类似于 $P_1(A)$“提升” 集合 $A$ 的类型，而 $T(\alpha )$“提升” 序数 $\alpha$ 的类型。T 运算的定义如下：如果 $W\in \alpha$，那么 $T(\alpha )$ 是以下序关系 $W^{\iota }$ 的序型：$W^{\iota }=\{(\{x\},\{y\})\mid xWy\}$ 现在，可以以分层的方式重新表述关于序型的引理。

　　 所有 $<\alpha$ 的序数在自然序关系下的序型是 $T^2(\alpha )$ 或 $T^4(\alpha )$，具体取决于所使用的有序对的定义。这两个版本的陈述都可以通过超限归纳来证明；在下文中，我们假设使用类型层次上的有序对。这意味着：$T^2(\alpha )<\mathrm{\Omega }$ 其中，$\mathrm{\Omega }$ 是所有序数的序型。特别地，有：$T^2(\mathrm{\Omega })<\mathrm{\Omega }$

　　 另一个可以通过超限归纳证明的分层陈述是，$T$ 运算在序数上是严格单调的，即它是保持序关系的运算：$T(\alpha )<T(\beta )⟺\alpha <\beta$ 因此，T 运算不是一个函数：序数的集合 $\{\alpha \mid T(\alpha )<\alpha \}$ 不可能有最小元素，因此它不能构成一个集合。更具体地说，T 运算的单调性意味着存在如下的 “递降序列”：$\mathrm{\Omega }>T^2(\mathrm{\Omega })>T^4(\mathrm{\Omega })>\dots$ 在序数中，这样的序列不能构成一个集合。

　　 有人可能会认为，这一结果表明 NF(U) 的任何模型都不是 “标准”，因为在任何 NFU 的模型中，外部看来序数并非良序。然而，这是一个哲学性问题，而不是形式化理论内部可以证明的问题。需要注意的是，即使在 NFU 内部，也可以证明任何 NFU 的集合模型都包含非良序的 “序数”。但 NFU 并不得出结论，认为整个宇宙 $V$ 是 NFU 的一个模型，尽管 $V$ 是一个集合，因为归属关系并不是一个集合关系。

4. 一致性

　　 一些数学家曾质疑 NF 的一致性，部分原因是它为何能够避免已知的悖论并不明显。其中的一个关键问题是，Specker 证明了 NF 与选择公理结合时是不一致的。该证明涉及 T 运算，相当复杂。然而，自 2010 年以来，Holmes 声称已经证明了 NF 的一致性，相对于标准集合论（ZFC）的一致性。2024 年，Sky Wilshaw 使用 Lean 证明助理验证了 Holmes 的证明。[43]

　　 尽管 NFU 解决悖论的方式与 NF 类似，但它具有更简单的一致性证明。该证明可以在 Peano 算术（PA）内形式化，而 PA 是比 ZF 集合论）更弱的理论，大多数数学家普遍接受它而不质疑。这并不与 Gödel 的第二不完备定理相冲突，因为 NFU 不包含无穷公理，因此 PA 不能在 NFU 中建模，从而避免了矛盾。PA 还证明了：NFU + 无穷公理和 TST + 无穷公理具有相同的一致性。NFU + 无穷公理 + 选择公理和 TST + 无穷公理 + 选择公理也具有相同的一致性。因此，像 ZFC 这样的更强理论能够证明 TST 的一致性，也能证 NFU + 这些扩展公理的一致性。[35]简单来说，NFU 通常被认为比 NF 更弱，因为在 NFU 中，所有集合的集合（即整个宇宙的幂集）可以比宇宙本身更小，尤其是当 NFU 允许存在无元素个体时，这一点在 NFU + 选择公理 下是必要的。

NFU 的模型

　　 Jensen 的证明提供了一种相对简单的方法，可以大规模地构造 NFU 的模型。利用模型理论中的常见技术，可以构造 Zermelo 集合论的非标准模型（这种方法不需要完整的 ZFC，仅需比 Zermelo 集合论稍强的理论）。在这个模型中，存在一个外部自同构 $j$（它不是该模型的一个集合），该自同构会移动累积层级中的某个秩$V_{\alpha }$[^1^]。我们可以不失一般性地假设：$j(\alpha )<\alpha$

　　 NFU 模型的域（domain）将是非标准秩$V_{\alpha }$。其基本思想是，自同构 $j$ 将 “幂集” $V_{\alpha +1}$ 编码到其在 “宇宙” $V_{\alpha }$ 内的外部同构副本 $V_{j(\alpha )+1}$ 中。这样，剩下的那些不对应于宇宙子集的对象会被视为无元素个体。形式化地，NFU 模型的归属关系定义如下：$x{\in }_{NFU}y{\equiv }_{def}j(x)\in y\wedge y\in V_{j(\alpha )+1}$

　　 现在可以证明，该构造确实给出了 NFU 的一个模型。设 $\varphi$ 是 NFU 语言中的一个分层公式。选择一个类型分配，为公式中的所有变量赋予类型，使其满足分层性。然后选择一个自然数 $N$，使其大于该分层中分配给所有变量的类型。

　　 步骤 1：将 NFU 公式翻译到 Zermelo 集合论的非标准模型,使用 NFU 模型中归属关系的定义，将公式 $\varphi$ 展开为 Zermelo 集合论非标准模型（带有自同构 $j$ 中的公式 ${\varphi }_1$。由于 $j$ 是自同构，对等式或归属语句的两边同时应用任何幂次的 $j$，都不会改变其真值。

　　 步骤 2：调整公式，使所有变量的类型一致,对公式 ${\varphi }_1$ 的每个原子公式应用 $j$，使得每个分配类型 $i$ 的变量 $x$ 被应用 $j^{N-i}$。这样，每个变量的类型都会对齐到相同的层次。由于所有 NFU 归属语句转化出的原子归属语句的形式，以及公式本身是分层的，这种变换是可行的。此时，每个全称量化语句 $\mathrm{\forall }x\in V_{\alpha }.\psi (j^{N-i}(x))$ 可以转换为 $\mathrm{\forall }x\in j^{N-i}(V_{\alpha }).\psi (x)$ 存在量化的情况也类似。

　　 步骤 3：消去公式中的 $j$ 应用执行上述变换，使得在公式 ${\varphi }_2$ 中，$j$ 不再应用于任何约束变量。选择 $\varphi$ 中一个被分配类型 $i$ 的自由变量 $y$，对整个公式统一应用 $j^{i-N}$，得到新的公式 ${\varphi }_3$，其中 $y$ 不再带有任何 $j$ 的应用。

　　 步骤 4：构造 NFU 模型中的集合,集合 $\{y\in V_{\alpha }\mid {\varphi }_3\}$ 在外部模型中存在（因为 $j$ 只作用于自由变量和常量），并且属于 $V_{\alpha +1}$。它包含了所有在 NFU 模型中满足原始公式 $\varphi$ 的 $y$。由于 NFU 模型的归属关系不同，$j$ 在 NFU 模型中的应用方式会对其进行修正，即：$j(\{y\in V_{\alpha }\mid {\varphi }_3\})$ 在 NFU 模型中具有正确的外延。

　　 结论：分层理解公理成立.通过上述构造，可以得出 NFU 模型中满足分层理解公理，从而证明该模型确实是 NFU 的一个有效模型。

　　 要验证弱外延性成立是直接的：每个非空元素 $V_{j(\alpha )+1}$ 都从非标准模型继承了一个唯一的外延。空集也继承了它通常的外延。所有其他对象被视为无元素个体。

　　 如果 $\alpha$ 是一个自然数 $n$，那么所得的 NFU 模型 声称整个宇宙是有限的（当然，从外部来看它仍然是无限的）。如果 $\alpha$ 是无限的，且非标准 ZFC 模型中满足选择公理，那么构造出的 NFU 模型将满足：$\text{NFU}+\text{Infinity}+\text{Choice}$.

NFU 中数学基础的自给自足性

　　 出于哲学原因，需要注意的是，要完成这一证明，并不需要在 ZFC 或任何相关系统中进行。反对将 NFU 作为数学基础的常见论点之一是，依赖它的理由通常与直觉上认为 ZFC 是正确的有关。然而，接受 TST（实际上是 TSTU）就已经足够了。概述如下：取类型论 TSTU（允许每个正类型中包含无元素集）作为元理论，并在 TSTU 中考虑 TSTU 的集合模型理论（这些模型将是集合序列 $T_i$（在元理论中它们全部属于相同类型），其中包含从 $P(T_i)$ 到 $P_1(T_{i+1})$ 的嵌入，这些嵌入编码了幂集 $P(T_i)$ 到 $T_{i+1}$ 的类型保持映射）。在给定 $T_0$ 到 $T_1$ 的嵌入（将基本 “类型” 的元素识别为该基本类型的子集）的情况下，可以以自然的方式从每个 “类型” 构造到其后继的嵌入。这可以谨慎地推广到超限序列 $T_{\alpha }$。

　　 请注意，这类集合序列的构造受限于它们所在类型的大小；这一限制使得 TSTU 无法证明自身的一致性（TSTU + 无限公理可以证明 TSTU 的一致性；但要证明 TSTU+无限公理的一致性，则需要一个包含基数 ${\beth }_{\omega }$ 的集合的类型，而在不作更强假设的情况下，TSTU+无限公理无法证明这样的类型的存在）。现在，我们可以使用相同的模型理论结果来构造 NFU 的一个模型，并以类似的方式验证它是 NFU 的一个模型，其中 $T_{\alpha }$ 取代了通常构造中的 $V_{\alpha }$。最终的关键步骤是，既然 NFU 是一致的，我们就可以在元理论中放弃使用绝对类型，从而通过自举的方式，将元理论从 TSTU 迁移到 NFU。

关于自同构 $j$ 的事实

　　 这种模型的自同构 $j$ 与 NFU 中的某些自然运算密切相关。例如，如果 $W$ 是非标准模型中的一个良序（我们假设使用库拉托夫斯基对，使得两个理论中的函数编码在某种程度上保持一致），并且 $W$ 在 NFU 中也是一个良序（NFU 中的所有良序在 Zermelo 集合论的非标准模型中也是良序，但反之不成立，因为在模型的构造过程中会形成无元素集），且 $W$ 在 NFU 中的类型为 $\alpha$，那么 $j(W)$ 在 NFU 中将是一个类型为 $T(\alpha )$ 的良序。

　　 实际上，$j$ 由 NFU 模型中的一个函数编码。在非标准模型中，将 $V_{j(\alpha )}$ 的任何元素的单元素集映射到其唯一元素的函数，在 NFU 中变为一个函数，该函数将每个单元素集 $\{x\}$（其中 $x$ 是宇宙中的任意对象）映射到 $j(x)$。称此函数为 Endo，它具有以下性质：Endo 是从单元素集的集合到集合的集合的一个单射，并且满足 $\text{Endo}(\{x\})=\{\text{Endo}(\{y\})\mid y\in x\}$ 对任意集合 $x$ 都成立。该函数可以在宇宙上定义一个类型级别的 “成员” 关系，从而重现原始非标准模型中的成员关系。

5. 历史

　　 1914 年，诺伯特·维纳展示了如何将有序对编码为集合的集合，使得可以用 TST（类型化集合理论）中的线性集合层次结构来替代《数学原理》中的关系类型。现在通常使用的有序对定义最早由库拉托夫斯基在 1921 年提出。威拉德·范·奥曼·奎因在 1937 年的一篇文章《数学逻辑的新基础》（New 中首次提出 NF（新基础）作为避免 TST 中 “令人不悦的后果” 的一种方法，因此 NF 得名于此。奎因在其 1940 年出版的著作《数学逻辑》中扩展了这一理论。在书中，奎因引入了 “数学逻辑”，简称ML）系统，这是 NF 的扩展，包含了适当类和集合。该书第一版中的集合论将 NF 与 NBG（冯·诺伊曼-伯恩赛因-哥德尔）集合论的适当类相结合，并包含了适用于适当类的不受限制的理解公理模式。然而，J. 巴克利·罗斯瑟证明该系统会导致布拉利-福尔蒂悖论。随后，王浩展示了如何修正奎因在 ML 系统中的公理，使其避免该问题。奎因在 1951 年出版的第二版（最终版）中纳入了这一修正后的公理化体系。

　　 1944 年，西奥多·海尔佩林证明了理解公理等价于其有限个实例的合取命题。[1]1953 年，恩斯特·施佩克证明了选择公理在 NF（无无元素集的情况下）中是不成立的。[38]1969 年，詹森（Jensen）证明，向 NF 中添加无元素集会得到一个可证明一致的理论，即 NFU。[35]同年，格里申证明了 NF₃ 的一致性。[46]施佩克还证明了 NF 与 TST 加上 “典型歧义” 公理模式是等一致的。此外，NF 还等一致于扩展了 “类型转换自同构” 的 TST，其中该自同构是一个理论外部的操作，它将每个类型映射到更高一级的类型，并保持相等性和成员关系不变。

　　 1983 年，马塞尔·克拉比（Marcel Crabbé）证明了一种他称为 NFI 的系统的一致性。该系统的公理包括不受限制的外延性公理，以及那些在理解公理的实例中，没有变量被赋予高于所断言存在的集合的类型。这是一种限定性的限制，尽管 NFI 并不是一个完全的限定性理论：它仍然允许足够的非限定性来定义自然数集（定义为所有归纳集的交集；需要注意的是，被量化的归纳集与所定义的自然数集属于相同的类型）。克拉比还讨论了 NFI 的一个子理论，其中在理解公理的实例中，只有参数（自由变量）可以具有被断言存在的集合的类型。他称该系统为 “限定性 NF”（NFP）。当然，如果一个理论允许自成员化的宇宙，那么它是否真正属于限定性理论是值得怀疑的。霍尔姆斯在[日期缺失] 证明，NFP 的一致性强度与《数学原理》（Principia Mathematica）的限定性类型论相同，但不包括可化公理。

　　 Metamath 数据库实现了 Hailperin 对新基础（NF）提出的有限公理化方案。[47]自 2015 年以来，兰德尔·霍尔姆斯（Randall Holmes）提出了多个 NF 一致性相对于 ZF 的候选证明，这些证明可在 arXiv 和他的个人主页上找到。他的证明方法是首先展示一种 “奇特” 的 TST 变体，即 “带 λ-类型的纠缠类型理论”（TTTλ）与 NF 是等一致的，然后再证明 TTTλ 在 ZF 带原子（ZFA）但无选择公理的情况下是一致的，方法是构造 ZFA 的类模型，其中包含在 ZF 带原子与选择公理（ZFA+C）中的 “基数的纠缠网”。然而，这些证明 “难以阅读、极度复杂，并涉及繁琐的细节记录，使得容易引入错误”。2024 年，Sky Wilshaw 使用 Lean 证明助理形式化了霍尔姆斯的一个证明版本，最终解决了 NF 一致性的问题。[48]蒂莫西·周评价 Wilshaw 的工作，认为这表明同行评审者对难以理解的证明感到迟疑的问题，可以借助证明助理来解决。[49]

6. 参见

• 替代集合论
• 公理化集合论
• 数学在集合论中的实现
• 正集合论
• 自然数的集合论定义

7. 注释

1. Hailperin 1944.
2. Holmes 1998，第 8 章。
3. Holmes 1998。
4. Holmes 1998，第 16 页。
5. Hailperin 1944，第 1.02 定义及公理 PId。
6. 例如，W. V. O. Quine 在 *Mathematical Logic*（1981）中使用了 “三种基本符号工具：成员关系、联合否定（joint denial）和量化”，然后按此方式定义了 "="（第 134–136 页）。
7. Holmes 1998，第 25 页。
8. Fenton 2015，ax-sn。
9. Holmes 1998，第 27 页。
10. Hailperin 1944，第 10 页，公理 P5。
11. Fenton 2015，ax-xp。
12. Holmes 1998，第 31 页。
13. Hailperin 1944，第 10 页，公理 P7。
14. Fenton 2015，ax-cnv。
15. Holmes 1998，第 32 页。
16. Hailperin 1944，第 10 页，公理 P2。
17. Fenton 2015，ax-si。
18. Hailperin 1944，第 10 页。
19. Holmes 1998，第 44 页。
20. Hailperin 1944，第 10 页，公理 P9。
21. Fenton 2015，ax-sset。
22. Holmes 1998，第 19 页。
23. Holmes 1998，第 20 页。
24. Holmes 1998，第 26–27 页。
25. Holmes 1998，第 30 页。
26. Holmes 1998，第 24 页。
27. Fenton 2015，ax-nin。
28. Hailperin 1944，第 10 页，公理 P8。
29. Fenton 2015，ax-1c。
30. Hailperin 1944，第 10 页，公理 P3、P4。
31. Fenton 2015，ax-ins2，ax-ins3。
32. Hailperin 1944，第 10 页，公理 P6。
33. Fenton 2015，ax-typlower。
34. Holmes & Wilshaw 2024。
35. Jensen 1969。
36. Holmes 2001。
37. Holmes 1998，第 12.1 节。
38. Specker 1953。
39. Holmes, M. Randall（2001 年 3 月）。"Strong axioms of infinity in NFU" (PDF). Journal of Symbolic Logic. 66 (1): 87–116. doi:10.2307/2694912. JSTOR 2694912。
40. Forster 2007。
41. Quine 1987。
42. Holmes 1998，第 17.5 节。
43. Smith, Peter（2024 年 4 月 21 日）。"NF really is consistent". Logic Matters. 2024 年 4 月 21 日检索。
44. Rosser 1942。
45. Wang 1950。
46. Grishin 1969。
47. Fenton 2015。
48. Smith, Peter（2024 年 4 月 21 日）。"NF really is consistent". Logic Matters. 2024 年 4 月 21 日检索。
49. Chow, Timothy（2024 年 5 月 3 日）。*"Timothy Chow on the NF consistency proof and Lean".* *Logic Matters.* 2024 年 5 月 3 日检索。

　　 1. 我们讨论的是自同构如何移动秩 $V_{\alpha }$，而不是序数 $\alpha$，因为我们不想假设模型中的每个序数都是某个秩的索引。

8. 参考文献

• Crabbé, Marcel (1982). "On the consistency of an impredicative fragment of Quine's NF". *The Journal of Symbolic Logic*. 47 (1): 131–136. doi:10.2307/2273386. JSTOR 2273386. S2CID 42174966.
• Fenton, Scott (2015). "New Foundations Explorer Home Page". *Metamath.* Retrieved 25 April 2024.
• Forster, Thomas (October 14, 2007). "Why the Sets of NF do not form a Cartesian-closed Category" (PDF). *www.dpmms.cam.ac.uk.*
• Forster, T. E. (2008). "The iterative conception of set" (PDF). *The Review of Symbolic Logic*. 1: 97–110. doi:10.1017/S1755020308080064. S2CID 15231169.
• Forster, T. E. (1992). *Set theory with a universal set. Exploring an untyped universe.* Oxford Science Publications, Oxford Logic Guides, vol. 20, New York: The Clarendon Press, Oxford University Press, ISBN 0-19-853395-0, MR 1166801.
• Forster, T. E. (2018). "Quine's New Foundations". *Stanford Encyclopedia of Philosophy.*
• Grishin, V. N. (1969). "Consistency of a fragment of Quine's NF system". *Dokl. Akad. Nauk SSSR.* 189 (2): 41–243.
• Hailperin, T. (1944). "A set of axioms for logic". *Journal of Symbolic Logic*. 9 (1): 1–19. doi:10.2307/2267307. JSTOR 2267307. S2CID 39672836.
• Holmes, M. Randall (1998). *Elementary set theory with a universal set* (PDF). *Cahiers du Centre de Logique*, vol. 10, Louvain-la-Neuve: Université Catholique de Louvain, Département de Philosophie, ISBN 2-87209-488-1, MR 1759289.
• Holmes, M. Randall (2008). "Symmetry as a Criterion for Comprehension Motivating Quine's 'New Foundations'". *Studia Logica*. 88 (2): 195–213. doi:10.1007/s11225-008-9107-8. S2CID 207242273.
• Holmes, M. Randall; Wilshaw, Sky (2024). *"New Foundations is consistent"* (PDF).
• Jensen, R. B. (1969), *"On the Consistency of a Slight(?) Modification of Quine's NF"*, *Synthese*, 19 (1/2): 250–263, doi:10.1007/bf00568059, JSTOR 20114640, S2CID 46960777. *附奎因的讨论*。
• Quine, W. V. (1937), *"New Foundations for Mathematical Logic"*, *The American Mathematical Monthly*, 44 (2), *Mathematical Association of America*: 70–80, doi:10.2307/2300564, JSTOR 2300564.
• Quine, Willard Van Orman (1940), *Mathematical Logic* (first ed.), New York: W. W. Norton & Co., Inc., MR 0002508.
• Quine, Willard Van Orman (1951), *Mathematical Logic* (Revised ed.), Cambridge, Mass.: Harvard University Press, ISBN 0-674-55451-5, MR 0045661.
• Quine, W. V. (1980), *"New Foundations for Mathematical Logic"* in *From a Logical Point of View*, 2nd ed., revised. Harvard Univ. Press: 80–101. *该版本是奎因 1937 年发表在《美国数学月刊》的论文的最终修订版*。
• Quine, Willard Van Orman (1987). *"The Inception of 'New Foundations'"*. *Selected Logic Papers - Enlarged Edition*. Harvard University Press. ISBN 9780674798373.
• Rosser, Barkley (1942), *"The Burali-Forti paradox"*, *Journal of Symbolic Logic*, 7 (1): 1–17, doi:10.2307/2267550, JSTOR 2267550, MR 0006327, S2CID 13389728.
• Specker, Ernst P. (1953). *"The axiom of choice in Quine's New Foundations for Mathematical Logic"*. *Proceedings of the National Academy of Sciences*. 39 (9). *National Academy of Sciences*: 972–975. Bibcode:1953PNAS...39..972S. doi:10.1073/pnas.39.9.972. PMC 1063889. PMID 16589362.
• Wang, Hao (1950), *"A formal system of logic"*, *Journal of Symbolic Logic*, 15 (1): 25–32, doi:10.2307/2268438, JSTOR 2268438, MR 0034733, S2CID 42852449.

9. 外部链接

• Solomon Feferman（2011）：《丰富的分层系统用于范畴论的基础》（"Enriched Stratified Systems for the Foundations of Category Theory")
• 斯坦福哲学百科全书（Stanford Encyclopedia of Philosophy）：
• 奎因的新基础（"Quine's New Foundations"*）——作者：Thomas Forster
• 替代公理化集合论（"Alternative axiomatic set theories"）——作者：Randall Holmes
• 新基础（NF）主页（"New Foundations Home Page"）
• 带有通用集合的集合论参考书目*（"Bibliography of Set Theory with a Universal Set"）
• NF 一致性证明的新尝试（"A new pass at the NF consistency proof"）