在数理逻辑中，新基础集合论(NF)是公理化集合论的一种，由蒯因构想出来作为对英国哲学家罗素和其老师怀特海的巨著《数学原理》中逻辑类型论的简化。蒯因 1937 年于《数理逻辑的新基础》一文中首次提及NF（此即其名称的由来）。请注意，此条目大多是在谈论 NFU，这是Jensen于1969年所提出，并由Holmes于1998年阐述的一重要变体。
简介
在数理逻辑中，新基础集合论(NF)是公理化集合论的一种，由蒯因构想出来作为对英国哲学家罗素和其老师怀特海的巨著《数学原理》中逻辑类型论的简化。蒯因 1937 年于《数理逻辑的新基础》一文中首次提及NF（此即其名称的由来）。请注意，此条目大多是在谈论 NFU，这是Jensen于1969年所提出，并由Holmes于1998年阐述的一重要变体。
注意事项
在数理逻辑中，新基础集合论(NF)是公理化集合论的一种，由蒯因构想出来作为对英国哲学家罗素和其老师怀特海的巨著《数学原理》中逻辑类型论的简化。蒯因 1937 年于《数理逻辑的新基础》一文中首次提及NF（此即其名称的由来）。请注意，此条目大多是在谈论 NFU，这是Jensen于1969年所提出，并由Holmes于1998年阐述的一重要变体。
TST公理
外延性：带有相同成员的相同(正数)类型的集合是相等的；
概括公理模式，也就是：如果Φ（x^n）是公式，则集合{x^n | Φ（x^n）}^(n+1)存在。换句话说，给定任何公式Φ（x^n），存在集合A^(n+1)使得∀x^n∃A^(n+1) [x^n∈A^(n+1) ↔ Φ（x^n）]为真。
这个类型论比起罗素和怀特海的《数学原理》首次发表的
逻辑类型论简单了许多，它包括其参数不必然都有同样类型的关系类型。在1914年，诺伯特·维纳展示了如何把有序对编码为集合的集合。这使得以这里描述的集合层次的方式消除了关系类型。
蒯因集合论
公理和层化
新基础(NF)是通过放弃TST的类型区别而获得的。NF的公理有：
外延性：有相同元素的两个对象是同一个对象；
概括模式：所有TST的概括实例，但去掉了类型索引(并且不用介入在变量之间新的同一性)。
通过约定，NF的概括模式是使用层化公式的概念而陈述的，而不直接提及类型。一个公式Φ被称为是层化的，如果存在从语法片段到自然数的一个函数f，使得对于任何Φ的原子子公式x∈y有f(y)=f(x)+1，而对于任何Φ的原子子公式x=y，有f(x)=f(y)。概括接着变成：
对于每个层化公式Φ存在{x|Φ}。
甚至在层化概念内隐含的对类型的间接提及也可以消除。Hailperin在1944年证实了概括等价于它的实例的有限合取，所以NF可以有限的公理化，而不提及类型的概念。
对于
朴素集合论概括好像是不自洽的，但是在这里不是。例如，不可能的罗素类{x|x￠x}不是NF集合，因为x￠x不能被层化。
有序对
关系和函数在TST(与NF和NFU)中以通常的方式定义为有序对。首先由Kuratowski在1921年提议的有序对常用的定义对于NF和相关理论有个严重缺陷：结果的有序对必定有比它的参数(它的左和右投影)的类型高2的类型。所以用途是决定分层的函数有比它的域的成员高3的类型。
如果能以其类型是同它的参数一样的类型的方式定义对(导致一个类型-齐平有序对)，则关系或函数有只比它的域的成员的类型高1的类型。所以NF和相关理论通常采用蒯因的有序对的集合论定义，它生成类型的类型-齐平的有序对。Holmes(1998)把有序对与它的左和右投影接受为基本的。幸运的是，有序对是否通过的定义或通过假定(就是接受为基本的)而是类型-齐平，通常是不重要的。
类型-级别有序对的存在蕴涵了“无穷”，而NFU+“无穷”解释了NFU+“存在着类型齐平的有序对”(它们不是同样的理论，但是区别无关紧要)。反过来，NFU+“无穷”+“选择”证明了类型-齐平有序对的存在。
有用的大集合的可容纳性
NF (和NFU+“无穷”+“选择”，下面描述并已知是相容的)允许构造ZFC和它的真扩展因为“太大”而不允许的两种集合(某些集合论在真类的名义下接受这些实体)：
全集V：因为 x = x 是层化公式，通过概括存在全集V={x|x=x}。直接的推论是所有集合都有补集，而在NF下的整个集合论全集有一个布尔结构。
基数和序数：在NF(和TST)中，存在n个元素的所有集合的集合(这里循环性只是外观上的)。所以弗雷格的基数定义在NF和NFU中可行：基数是集合在等势关系下的等价类：集合 A 和 B 是等势的，如果存在它们之间的双射，在这种情况下我们写为A~B。类似的，序数是良序集合在相似关系下的等价类。
怎样避免
NF 清除了三个周知的
集合论悖论，即：“罗素悖论”、“康托尔悖论”和“布拉利-福尔蒂悖论”NFU是(相对)相容的理论也避免了这些悖论，增强了我们在这个事实上的信心。
罗素悖论
x￠x不是层化公式，所以{x|x￠x}的存在不被任何概括的实例所断言。蒯因构造NF的时候大概最关注于这个悖论。
康托尔悖论
关于最大基数的康托尔悖论利用了
康托尔定理对全集的应用。康托尔定理声称(假定 ZFC)任何集合的A的幂集P(A)>A[没有从P(A)到A的单射函数(一一映射)]。当然有从P(V)到V的单射，如果V是全集的话！解决这个问题需要我们观察到 |A|<|P(A)| 在类型论中没有意义：P(A)的类型高1于A的类型。正确的有类型版本(它是与在ZF中工作的最初形式的康托尔定理本质上同样道理的类型论中的定理)是 |P1(A)|<|P(A)|，这里的P1(A)是A的一个元素的子集的集合。我们感兴趣的这个定理的特殊实例是 |P1(V)|<|P(V)|：一个元素的集合们少于集合们(因此一个元素的集合们少于全体对象，如果我们在NFU中的话)。从全集到这些一个元素集合明显的双射x→{x}不是一个集合；它不是集合是因为它的定义是非层化的。注意在所有已知的NFU的模型中 |P1(V)|<|P(V)|<<|V| 都成立；“选择”允许我们不只证明有基本元素而且在 |P(V)| 和 |V| 之间有很多基数。 我们现在介入某些有用的概念。集合A满足直觉上吸引人的 |A|=|P1(A)| 就被称为康托尔式的：康托尔式集合满足通常形式的康托尔定理。集合A满足进一步条件（x→{x}）ΓA，即
单元素集合映射于A的限制，则不仅仅是康托尔式的，而且是强康托尔式的。
布拉利-福尔蒂悖论
下面是关于最大序数的布拉利-福尔蒂悖论。我们定义(跟从
朴素集合论)序数是良序排序在相似性下的等价类。在序数上有一个明显的自然的良序排序；因为它是良序排序所以它属于一个序数Ω。(通过
超限归纳法)可直接证明在小于一个给定序数α的序数们上的自然次序的序类型是α自身。但是这意味着Ω是小于Ω 的序数们的序类型，因此它严格小于所有序数的序类型——但是通过定义，后者是Ω自身！
在 NF(U) 中对这个悖论的解决开始于观察到：在小于α的序数们上的自然次序的序类型的类型比α的类型高。
因此类型齐平有序对的类型比它的参数的类型高1，而常规的Kuratowski有序对高3。
对于任何序类型α，我们可以定义比α的类型高1的序类型：如果 W∈α，则T(α)是次序W^t={（{x},{y}）| xWy}的序类型。T运算的烦琐只是外观上的；可以轻易的证明T是在序数们上的严格的单调(序保持)运算。
序类型的引理
我们可以用层化的方式重申关于序类型的引理：在小于α的序数们上的自然次序的序类型是T^2(α)或T^4(α)，依赖于使用哪个有序对定义(我们在下文中假定类型齐平有序对)。
从此我们可演绎出：在小于Ω的序数们上的序类型是T^2(Ω)，从它我们演绎出T^2(Ω)<Ω。因此T运算不是个函数；我们不能有从序数到序数的严格单调集合映射，它向下映射一个序数！因为T是单调的，我们有 Ω>T^2(α)>T^4(α)···，在序数们中的“递减序列”不能是集合。
某些人已经断言这个结果证实了没有NF(U)的模型是“标准”的，因此在任何NFU的模型中序数们外在的不是良序的。我们不接受这种立场，而我们注意到还有一个NFU的定理，任何NFU的集合模型都有非良序的“序数”；NFU推不出全集V是NFU的模型，尽管V是集合，因为成员关系不是集合关系。
缺陷及修正
蒯因在 1940 年第一版的《数理逻辑》的集合论中，结合了von Neumann-Bernays-Godel Set Theory（冯·诺伊曼-博内斯-哥德尔集合论）的真类于NF中，并为真类包括了一个无限制概括的公理模式。在1942年，J.Barkley Rosser 证明了蒯因的集合论遭受Burali-Forti悖论。在1950年，蒯因的学生王浩（Hao Wang）展示了如何修正蒯因的公理来避免这个问题，蒯因在 1951 年第二和最终版本的《数理逻辑》中包括了结果的公理化。