新基础集合论

改进版本的类型论TST的基本谓词是等於和成员关系。TST有一个线性的类型层次：类型0由不加描述的个体组成。对于每个（元-）自然数n，类型n+1的对象是类型n对象的集合；类型n的集合有类型为n-1的成员。用等號连接的對象必须有相同的类型。下列两个原子公式简洁的描述了定类型规则：${\displaystyle x^{n}=y^{n}\ }$和${\displaystyle x^{n}\in y^{n+1}}$（符号仍可改进）。

TST的公理是：

• 外延性：带有相同成员的相同（正数）类型的集合是相等的；
• 概括公理模式，也就是：

如果${\displaystyle \phi (x^{n})\ }$是公式，则集合${\displaystyle \{x^{n}\mid \phi (x^{n})\}^{n+1}}$存在。

换句话说，给定任何公式${\displaystyle \phi (x^{n})\ }$，存在集合${\displaystyle A^{n+1}\ }$使得${\displaystyle \forall x^{n}\exists A^{n+1}[x^{n}\in A^{n+1}\leftrightarrow \phi (x^{n})]}$为真。

这个类型论比于《数学原理》首次发表的类型论簡單許多，因為它還得包括其参数不必然都有同样类型的关系类型。在1914年，諾伯特·維納展示了如何把有序对编码为集合的集合。这使得以这里描述的集合层次的方式消除了关系类型。

NF清除了三个周知的集合论悖论。NFU這個{相对}相容的理论也避免了这些悖论，增强了我们對這些理論的信心。

罗素悖论：${\displaystyle x\not \in x}$不是层化公式，所以不會通過概括的任何推論得出${\displaystyle \{x\mid x\not \in x\}}$的存在性。蒯因构造NF的时候大概最关注于这个悖论。

关于最大基数的康托尔悖论利用了康托尔定理对全集的应用。康托尔定理声称（假定ZFC）任何集合的${\displaystyle A\ }$的幂集${\displaystyle P(A)\ }$大于${\displaystyle A\ }$（没有从${\displaystyle P(A)\ }$到${\displaystyle A\ }$的单射函数）。但如果${\displaystyle V\ }$是全集的话，当然有从${\displaystyle P(V)\ }$到${\displaystyle V\ }$的单射。為了解决这个问题，我们需要注意到${\displaystyle |A|<|P(A)|\ }$在类型论中没有意义：${\displaystyle P(A)\ }$的类型比${\displaystyle A\ }$的类型高1。正确的有类型版本（它是在类型论中的定理，成立的原因就像康托尔定理在ZF中成立那樣）是${\displaystyle |P_{1}(A)|<|P(A)|\ }$，这里的${\displaystyle P_{1}(A)\ }$是${\displaystyle A\ }$的單元素子集的集合。在这个定理中，使我们感兴趣的特殊实例是${\displaystyle |P_{1}(V)|<|P(V)|\ }$：單元素集合们少于集合们（因此一个元素的集合们少于全体对象，如果我们在NFU中的话）。从全集到这些單元素集合明显的双射${\displaystyle x\mapsto \{x\}\ }$不是一个集合；它不是集合是因为它的定义是非层化的。注意在所有已知的NFU的模型中${\displaystyle |P_{1}(V)|<|P(V)|<<|V|\ }$都成立；“选择公理”允许我们不只证明有基本元素，而且在${\displaystyle |P(V)|\ }$和${\displaystyle |V|\ }$之间有很多基数。

我们现在引入某些有用的概念。若集合${\displaystyle A\ }$满足${\displaystyle |A|=|P_{1}(A)|\ }$，就被称为康托尔式的：康托尔式集合满足通常形式的康托尔定理。集合${\displaystyle A\ }$满足进一步条件${\displaystyle (x\mapsto \{x\})\lceil A\ }$，即单元素集合映射在A上的限制，则不只是康托尔式的而且是强康托尔式的。

下面是关于最大序数的布拉利-福尔蒂悖论。我们定义(跟从朴素集合论)序数是良序排序在相似性下的等价类。在序数上有一个明显的自然的良序排序；因为它是良序排序所以它属于一个序数${\displaystyle \Omega \ }$。(通过超限归纳法)可直接证明在小于一个给定序数${\displaystyle \alpha \ }$的序数们上的自然次序的序类型是${\displaystyle \alpha \ }$自身。但是这意味着${\displaystyle \Omega \ }$是小于${\displaystyle \Omega \ }$的序数们的序类型，因此它严格小于所有序数的序类型 -- 但是通过定义，后者是${\displaystyle \Omega \ }$自身！

在NF(U)中对这个悖论的解决开始于观察到在小于${\displaystyle \alpha \ }$的序数们上的自然次序的序类型的类型比${\displaystyle \alpha \ }$的类型高。因此类型齐平有序对的类型比它的参数的类型高1，而常规的Kuratowski有序对高3。对于任何序类型${\displaystyle \alpha \ }$，我们可以定义比${\displaystyle \alpha \ }$的类型高1的序类型：如果${\displaystyle W\in \alpha \ }$，则${\displaystyle T(\alpha )\ }$是次序${\displaystyle W^{\iota }=\{(\{x\},\{y\})\mid xWy\}}$的序类型。T运算的烦琐只是外观上的；可以轻易的证明T是在序数们上的严格的单调(序保持)运算。

我们可以用层化的方式重申关于序类型的引理：在小于${\displaystyle \alpha \ }$的序数们上的自然次序的序类型是${\displaystyle T^{2}(\alpha )\ }$或${\displaystyle T^{4}(\alpha )\ }$，依赖于使用哪个有序对定义(我们在下文中假定类型齐平有序对)。从此我们可演绎出在小于${\displaystyle \Omega \ }$的序数们上的序类型是${\displaystyle T^{2}(\Omega )\ }$，从它我们演绎出${\displaystyle T^{2}(\Omega )<\Omega \ }$。因此T运算不是个函数；我们不能有从序数到序数的严格单调集合映射，它向下映射一个序数！因为T是单调的，我们有${\displaystyle \Omega >T^{2}(\Omega )>T^{4}(\Omega )\ldots }$，在序数们中的“递减序列”不能是集合。

某些人已经断言这个结果证实了没有NF(U)的模型是“标准”的，因此在任何NFU的模型中序数们外在的不是不是良序的。我们不接受这种立场，而我们注意到还有一个NFU的定理，任何NFU的集合模型都有非良序的“序数”；NFU不结论出全集V是NFU的模型，尽管V是集合，因为成员关系不是集合关系。

关于数学在NFU中的进一步开发，和与在ZFC中相同的开发的比较，请参见数学的集合论实现（en:Implementation of mathematics in set theory）。

蒯因在1940年第一版的《数理逻辑》的集合论中，结合了von Neumann-Bernays-Gödel集合论的真类于NF，并为真类包括了一个无限制概括的公理模式。在1942年，J. Barkley Rosser证明了蒯因的集合论遭受Burali-Forti悖论。在1950年，王浩展示了如何修正蒯因的公理来避免这个问题，蒯因在1951年第二和最终版本的《数理逻辑》中包括了结果的公理化。

• 公理化集合论
• 罗素公理体系
• ZFC
• 数学的集合论实现
• 自然数的集合论定义
• 正集合论
• 可替代的集合论

• Holmes, Randall, 1998. Elementary Set Theory with a Universal Set. Academia-Bruylant. The publisher has graciously consented to permit diffusion of this introduction to NFU via the web. Copyright is reserved.
• Jensen, R. B., 1969, "On the Consistency of a Slight(?) Modification of Quine's NF," Synthese 19: 250-63. With discussion by Quine.
• Quine, W. V., 1980, "New Foundations for Mathematical Logic" in From a Logical Point of View, 2nd ed., revised. Harvard Univ. Press: 80-101. The definitive version of where it all began, namely Quine's 1937 paper in the American Mathematical Monthly.

• Stanford Encyclopedia of Philosophy:
  • Quine's New Foundations -- by Thomas Forster.
  • Alternative axiomatic set theories -- by Randall Holmes.
• Randall Holmes: New Foundations Home Page.
• Randall Holmes: Bibliography of Set Theory with a Universal Set.