新基础

在数理逻辑中，新基础（NF）是一种公理集合理论，由威拉德-范-奥曼-奎因设想为《数学原理》中类型理论的简化。奎因在1937年一篇题为《数学逻辑的新基础》的文章中首次提出了NF，因此得名。本条目的大部分内容讨论了NFU，这是NF的一个重要变体，归功于詹森（1969），并由霍姆斯（1998）澄清。在1940年和1951年的修订中，奎因引入了NF的扩展，有时被称为数理逻辑或ML，它包括适当的类以及集合。新基础有一个普遍的集合，所以它是一个非井底的集合理论。也就是说，它是一个公理集合理论，允许无限的成员递减链，如......xn∈xn-1∈......∈x2∈x1。它避免了罗素悖论，只允许用理解力的公理模式来定义可分层的公式。例如，x∈y是一个可分层的公式，但x∈x则不是。

罗素未定型集合理论（TST）的基本谓词，即类型理论的精简版，是平等().TST有一个线性的类型层次：类型0包括其他未描述的个体。对于每个（元）自然数n，类型n+1对象是类型n对象的集合；类型n的集合有类型n-1的成员。通过身份连接的对象必须具有相同的类型。下面两个原子公式简洁地描述了类型化规则。延伸性：具有相同成员的相同（正）类型的集合是相等的；一个理解性公理模式，即：如果{displaystylephi(x{n})}是一个公式，那么这个集合的成员就有可能是一个相同的成员。是一个公式，那么这个集合{displaystyle{x{n}mid`phi(x{n})}{n+1}!换句话说，给定任何公式这种类型的理论比最早在《数学原理》中提出的理论要简单得多，因为后者包括关系的类型，其参数不一定都是相同的类型。1914年，诺伯特-维纳(NorbertWiener)展示了如何将有序对作为集合的编码，使得消除关系类型而支持这里描述的集合的线性层次成为可能。

公理和分层NewFoundations(NF)的良好形式公式与TST的良好形式公式相同，但抹去了类型注释。NF的公理是。延伸性。具有相同元素的两个对象是同一个对象；一个理解性模式。按照惯例，NF的理解模式是用分层公式的概念来表述的，没有直接提到类型。一个公式如果存在一个函数f，从j的片断出发，就可以说是分层的。

的句法到自然数的函数，这样对于任何原子子formula即使是隐含在分层概念中的对类型的间接引用也可以被消除。TheodoreHailperin在1944年表明，Comprehension等同于其实例的有限联结，因此NF可以被有限公理化，而无需提及类型的概念。Comprehension似乎与天真的集合理论中的问题相类似，但事实并非如此。

关系和函数在TST（以及NF和NFU）中以通常的方式定义为有序对的集合。有序对的通常定义是由Kuratowski在1921年首次提出的，对于NF和相关理论来说有一个严重的缺点：所产生的有序对必然有一个比其参数类型高两倍的类型（它是左和右的投影）。