新基础集合论

在数理逻辑中，新基础集合论（NF）是公理化集合论的一种，由蒯因构想出来作为对《数学原理》中类型论的简化。蒯因1937年于《数理逻辑的新基础》一文中首次提及NF（此即其名称的由来）。请注意，此条目大多是在谈论NFU，这是Jensen于1969年所提出，并由Holmes于1998年阐述的一重要变体。

改进版本的类型论TST的基本谓词是等于和成员关系。TST有一个线性的类型层次：类型0由不加描述的个体组成。对于每个（元-）自然数，类型+1的对象是类型对象的集合；类型的集合有类型为-1的成员。用等号连接的对象必须有相同的类型。下列两个原子公式简洁的描述了定类型规则：${\displaystyle x^n=y^n}$，使得对于任何${\displaystyle \mathrm{\varphi <!--\; \varphi \; -->}}$() = () + 1；而对于任何${\displaystyle \mathrm{\varphi <!--\; \varphi \; -->}}$() = ()。概括接着变成：

对于朴素集合论概括好像是不自洽的，但是在这里不是。例如，不可能的罗素类${\displaystyle \{x\mid <!--\; \mid \; -->x\notin x\}}$上的限制，则不只是康托尔式的而且是强康托尔式的。

下面是关于最大序数的布拉利-福尔蒂悖论。我们定义(跟从朴素集合论)序数是良序排序在相似性下的等价类。在序数上有一个明显的自然的良序排序；因为它是良序排序所以它属于一个序数${\displaystyle \mathrm{\Omega <!--\; \Omega \; -->}}$是NFU的模型，尽管是集合，因为成员关系不是集合关系。

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

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