贡献者： 待更新
本文根据 CC-BY-SA 协议转载翻译自维基百科相关文章。
在数学逻辑中，新基础（New Foundations，简称 NF）是一种非良基、可有限公理化的集合论，由威拉德·范·奥曼·奎因构思，旨在简化《数学原理》中的类型论。
NF 的良构公式是命题演算的标准公式，具有两个基本谓词：相等（\(=\)）和成员关系（\(\in\)）。NF 可以仅通过两个公理模式来表述：
一个公式 \( \phi \) 被称为分层的，如果存在一个从 \( \phi \) 的语法结构的各部分到自然数的函数 \( f \)，使得：对于 \( \phi \) 中的任意原子子公式 \( x \in y \)，满足 \( f(y) = f(x) + 1 \)；对于 \( \phi \) 中的任意原子子公式 \( x = y \)，满足 \( f(x) = f(y) \)。
NF 可以被有限公理化。[1] 这种有限公理化的一个优点是，它消除了分层性的概念。有限公理化中的公理对应于一些自然的基本构造，而分层理解公理虽然强大，但不一定直观。在其入门书籍中，Holmes 选择将有限公理化作为基本框架，并将分层理解公理作为一个定理来证明。[2]
具体的公理集合可能有所不同，但通常包含以下大部分公理，而其余的可以作为定理证明：[3][1]
新基础集合论与拉塞尔型的非分层类型化集合论密切相关。TST 是《数学原理》中类型论的简化版本，采用线性类型层次结构。在这种多排序理论（many-sorted theory）中，每个变量和集合都被赋予一个类型（type）。通常，类型指数使用上标表示：\(x^n\) 表示类型为 \( n \) 的变量。类型0由未进一步描述的个体组成。对于每个（元）自然数 \( n \)，类型 \( n+1 \) 的对象是类型 \( n \) 对象的集合。相等关系仅适用于相同类型的对象。类型 \( n \) 的集合仅包含类型 \( n-1 \) 的成员。TST 的公理包括：外延性：适用于相同（正）类型的集合。理解公理：如果 \( \phi(x^n) \) 是一个公式，则集合 \(\{x^n \mid \phi(x^n)\}^{n+1}\) 存在，即：\(\exists A^{n+1}\forall x^n [x^n \in A^{n+1} \leftrightarrow \phi(x^n)]\) 是一个公理，其中 \( A^{n+1} \) 代表集合 \(\{x^n \mid \phi(x^n)\}^{n+1}\)，并且 \( A^{n+1} \) 在 \( \phi(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]
带有基数元素的新基础集合论是 NF 的一个重要变种，由 Jensen 提出，[35]并由 Holmes 进一步澄清。[3]基数元素是不是集合的对象：它们不包含任何元素，但可以被包含在集合中。在 NFU 最简单的公理化形式之一中，基数元素被视为多个不同的空集，从而削弱了 NF 的外延性公理，改为：
这意味着：对于非空集合，外延性仍然成立。对于空集和基数元素，外延性不适用，它们可以是多个不同的对象。在这种公理化下：理解模式保持不变。但是，如果某个集合的定义公式 \(\phi(x)\) 无解（即不可满足），则集合 \(\{x \mid \phi(x)\}\) 可能不是唯一的（即它可以对应多个不同的基数元素）。
然而，为了方便使用，通常更希望有一个唯一的、“标准” 空集。这可以通过引入集合性谓词 \( \text{set}(x)\) 来区分集合和基数元素（原子）。 其公理如下：[36]
\(NF_3\)：NF 的一个子理论，仅允许最多三种类型的分层公式（即 \(x, y, z\) 这样的最多三层类型）。\(NF_4\)：与完整的 NF 等价，即没有基数元素，并且允许所有满足分层性条件的理解公理。
数学逻辑（Mathematical Logic, ML）是 NF 的扩展，它不仅包含集合，还包含适当的类。ML 由 Quine 提出，并由 Hao Wang 修订。Wang 证明，NF 与修订后的 ML 具有等一致性，即它们的一致性（无矛盾性）是等价的。
本节讨论 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 的公理化中：理解模式——即对于任意分层公式 \(\phi\)，集合 \(\{x \mid \phi(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 \land 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 及其变种中证明无穷公理，在这些情况下，它可能被称为无穷定理：
更强的无穷公理：可以假设自然数集合是一个强康托尔集合。NFUM（即 NFU + Infinity + Large Ordinals + Small Ordinals）等价于 Morse–Kelley 集合论（Morse–Kelley Set Theory, MK），再加上一个对适当类的谓词，该谓词是一个κ-完备的非主超滤，定义在适当类的序数 \(\kappa\) 上。[39]
NF（以及 NFU + Infinity + Choice，它已知是一致的）允许构造两类在 ZFC 及其扩展中被禁止的集合，因为它们 “过大”（在某些集合论中，这些对象被视为适当类）。
在 NF 中，以集合作为对象、以这些集合之间的函数作为箭头构成的范畴不是笛卡尔封闭的。[40]由于 NF 不满足笛卡尔封闭性：并非所有函数都可以柯里化，这与直觉上的期望不同。NF 不是一个拓扑斯。
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, \quad 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 悖论在 NF（New Foundations）中以相反的方式得到解决：在 NF 中，即使可以访问序数的集合，也无法构造出 “最大序数”。人们可以构造出对应于所有序数的自然良序的序数 \( \Omega \)，但这并不意味着 \(\Omega \) 比所有这些序数都大。
要在 NF 中形式化 Burali-Forti 悖论，首先需要对序数的概念进行形式化。在 NF 中，序数的定义方式与朴素集合论相同，即它们被定义为良序集在同构关系下的等价类。这是一个分层的定义，因此可以无问题地定义序数的集合 \( \mathrm{Ord} \)。在 NF 中，超限归纳适用于分层陈述，这使得可以证明序数的自然序关系是 \( \mathrm{Ord} \) 上的一个良序。具体来说：\(\alpha \leq \beta \iff \text{ 存在良序关系 } R \in \alpha, S \in \beta \text{，使得 } S \text{ 是 } R \text{的延续}\) 根据序数的定义，这个良序关系本身也属于某个序数 \(\Omega \in \mathrm{Ord}\)。在朴素集合论中，通常可以通过超限归纳证明：每个序数 \( \alpha \) 的序型正好是所有小于 \( \alpha \) 的序数的自然序关系的序型。但如果在 NF 中应用这一点，就会导致矛盾：因为按照定义，\( \Omega \) 是所有序数的序型，而不是它们的某个真初始片段的序型。这就导致了 Burali-Forti 悖论。
然而，陈述 “\( \alpha \) 是所有小于 \( \alpha \) 的序数的自然序关系的序型” 并不是分层的，因此超限归纳在 NF 中无法使用。实际上，“小于 \( \alpha \) 的序数的自然序关系 \( R_{\alpha} \) 的序型 \( \beta \)” 的类型至少比 \( \alpha \) 高出两层：关系 \( R_{\alpha} = \{(x, y) \mid x \leq 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 x W y\}\) 现在，可以以分层的方式重新表述关于序型的引理。
所有 \(<\alpha \) 的序数在自然序关系下的序型是 \( T^2(\alpha) \) 或 \( T^4(\alpha) \)，具体取决于所使用的有序对的定义。这两个版本的陈述都可以通过超限归纳来证明；在下文中，我们假设使用类型层次上的有序对。这意味着：\(T^2(\alpha) < \Omega\) 其中，\( \Omega \) 是所有序数的序型。特别地，有：\(T^2(\Omega) < \Omega\)
另一个可以通过超限归纳证明的分层陈述是，\( T \) 运算在序数上是严格单调的，即它是保持序关系的运算：\(T(\alpha) < T(\beta) \iff \alpha < \beta\) 因此，T 运算不是一个函数：序数的集合 \(\{\alpha \mid T(\alpha) < \alpha\}\) 不可能有最小元素，因此它不能构成一个集合。更具体地说，T 运算的单调性意味着存在如下的 “递降序列”：\(\Omega > T^2(\Omega) > T^4(\Omega) > \dots\) 在序数中，这样的序列不能构成一个集合。
有人可能会认为，这一结果表明 NF(U) 的任何模型都不是 “标准”，因为在任何 NFU 的模型中，外部看来序数并非良序。然而，这是一个哲学性问题，而不是形式化理论内部可以证明的问题。需要注意的是，即使在 NFU 内部，也可以证明任何 NFU 的集合模型都包含非良序的 “序数”。但 NFU 并不得出结论，认为整个宇宙 \( V \) 是 NFU 的一个模型，尽管 \( V \) 是一个集合，因为归属关系并不是一个集合关系。
一些数学家曾质疑 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 + 选择公理 下是必要的。
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 的一个模型。设 \( \phi \) 是 NFU 语言中的一个分层公式。选择一个类型分配，为公式中的所有变量赋予类型，使其满足分层性。然后选择一个自然数 \( N \)，使其大于该分层中分配给所有变量的类型。
步骤 1：将 NFU 公式翻译到 Zermelo 集合论的非标准模型,使用 NFU 模型中归属关系的定义，将公式 \( \phi \) 展开为 Zermelo 集合论非标准模型（带有自同构 \( j \) 中的公式 \( \phi_1 \)。由于 \( j \) 是自同构，对等式或归属语句的两边同时应用任何幂次的 \( j \)，都不会改变其真值。
步骤 2：调整公式，使所有变量的类型一致,对公式 \( \phi_1 \) 的每个原子公式应用 \( j \)，使得每个分配类型 \( i \) 的变量 \( x \) 被应用 \( j^{N-i} \)。这样，每个变量的类型都会对齐到相同的层次。由于所有 NFU 归属语句转化出的原子归属语句的形式，以及公式本身是分层的，这种变换是可行的。此时，每个全称量化语句 \(\forall x \in V_{\alpha}.\psi(j^{N-i}(x))\) 可以转换为 \(\forall x \in j^{N-i}(V_{\alpha}).\psi(x)\) 存在量化的情况也类似。
步骤 3：消去公式中的 \( j \) 应用执行上述变换，使得在公式 \( \phi_2 \) 中，\( j \) 不再应用于任何约束变量。选择 \( \phi \) 中一个被分配类型 \( i \) 的自由变量 \( y \)，对整个公式统一应用 \( j^{i-N} \)，得到新的公式 \( \phi_3 \)，其中 \( y \) 不再带有任何 \( j \) 的应用。
步骤 4：构造 NFU 模型中的集合,集合 \(\{ y \in V_{\alpha} \mid \phi_3 \}\) 在外部模型中存在（因为 \( j \) 只作用于自由变量和常量），并且属于 \(V_{\alpha+1} \)。它包含了所有在 NFU 模型中满足原始公式 \( \phi \) 的 \( y \)。由于 NFU 模型的归属关系不同，\( j \) 在 NFU 模型中的应用方式会对其进行修正，即：\(j(\{ y \in V_{\alpha} \mid \phi_3 \})\) 在 NFU 模型中具有正确的外延。
结论：分层理解公理成立.通过上述构造，可以得出 NFU 模型中满足分层理解公理，从而证明该模型确实是 NFU 的一个有效模型。
要验证弱外延性成立是直接的：每个非空元素 \( V_{j(\alpha)+1} \) 都从非标准模型继承了一个唯一的外延。空集也继承了它通常的外延。所有其他对象被视为无元素个体。
如果 \( \alpha \) 是一个自然数 \( n \)，那么所得的 NFU 模型 声称整个宇宙是有限的（当然，从外部来看它仍然是无限的）。如果 \( \alpha \) 是无限的，且非标准 ZFC 模型中满足选择公理，那么构造出的 NFU 模型将满足：\(\text{NFU} + \text{Infinity} + \text{Choice}\).
出于哲学原因，需要注意的是，要完成这一证明，并不需要在 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 \) 与 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 \) 都成立。该函数可以在宇宙上定义一个类型级别的 “成员” 关系，从而重现原始非标准模型中的成员关系。
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]
1. 我们讨论的是自同构如何移动秩 \( V_{\alpha} \)，而不是序数 \( \alpha \)，因为我们不想假设模型中的每个序数都是某个秩的索引。
友情链接： 超理论坛 | ©小时科技 保留一切权利