概述
在數理邏輯中，新基礎集合論(NF)是公理化集合論的一種，由蒯因構想出來作為對英國哲學家羅素和其老師懷特海的巨著《數學原理》中邏輯類型論的簡化。蒯因 1937 年於《數理邏輯的新基礎》一文中首次提及NF（此即其名稱的由來）。請注意，此條目大多是在談論 NFU，這是Jensen於1969年所提出，並由Holmes於1998年闡述的一重要變體。
本詞條的注意事項在本詞條中由於無法顯示部分數學和邏輯符號，故用符號 ^ 表示次方，用 ￠ 表示邏輯中的“不屬於”意義，符號 |P1(A)| 和 |P1(V)| 中的1是下標。特此說明。
類型論TST
改進版本的類型論TST的基本謂詞是等式和成員關係。TST有一個線性的類型層次：類型0由不加描述的個體組成。對於每個(元-)自然數n，類型n+1的對象是類型n對象的集合；類型n的集合有類型為n-1的成員。用等式連線的類型必須有相同的類型。下列兩個原子公式簡潔的描述了定類型規則：
x^n=y^n 和x^n∈y^(n+1)，符號仍可改進。
外延性：帶有相同成員的相同(正數)類型的集合是相等的；
概括公理模式，也就是：如果Φ（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(U) 如何避免集合論悖論
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 年第二和最終版本的《數理邏輯》中包括了結果的公理化。
