Can you summarize the following document?
        
  改進版本的型別論TST的基本謂詞是等於和成員關係。TST有一個線性的型別層次:型別0由不加描述的個體組成。對於每個(元-)自然數"n",型別"n"+1的物件是型別"n"物件的集合;型別"n"的集合有型別為"n"-1的成員。用等號連線的物件必須有相同的型別。下列兩個原子公式簡潔的描述了定型別規則:formula_1和formula_2(符號仍可改進)。  TST的公理是:  這個型別論比於《數學原理》首次發表的型別論簡單許多,因為它還得包括其引數不必然都有同樣型別的關係型別。在1914年,諾伯特·維納展示瞭如何把有序對編碼為集合的集合。這使得以這裡描述的集合層次的方式消除了關係型別。

  

  新基礎(NF)是通過放棄TST的型別區別而獲得的。NF的公理有:  通過約定,NF的概括模式使用層化公式的概念來陳述,而不直接提及型別。一個公式formula_8被稱為是層化的,如果存在從語法片段到自然數的一個函式"f",使得對於任何formula_8的原子子公式formula_10有"f"("y") = "f"("x") + 1;而對於任何formula_8的原子子公式formula_12,有"f"("x") = "f"("y")。概括接著變成:  對於樸素集合論概括好像是不自洽的,但是在這裡不是。例如,不可能的羅素類formula_15不是NF集合,因為formula_16不能被層化。

  關係和函式在TST(以及NF和NFU)中以通常的方式定義為有序對。首先由Kuratowski在1921年提議的有序對常用的定義對於NF和相關理論有個嚴重缺陷:結果的有序對必定有比它的引數(它的左和右投影)的型別高2的型別。所以為了決定分層,函式有比它的域的成員高3的型別。  如果能以其型別是同它的引數一樣的型別的方式定義對(導致一個型別齊平有序對),則關係或函式有隻比它的域的成員的型別高1的型別。所以NF和相關理論通常採用蒯因的有序對的集合論定義,這樣得出的是型別的型別-齊平的有序對。Holmes(1998)把有序對與它的左和右投影定為原始概念。幸運的是,無論有序對是通過定義或通過假定(就是作為原始概念)而型別齊平,通常是不重要的。  型別齊平有序對的存在蘊涵了“無窮公理”,而NFU +“無窮公理”解釋了NFU +“存在著型別齊平的有序對”(它們不是同樣的理論,但是區別無關緊要)。反過來,NFU +“無窮公理”+“選擇公理”證明了型別齊平有序對的存在。

  NF(以及NFU +“無窮公理”+“選擇公理”,下面描述並已知是相容的)允許構造兩種集合,它們都是ZFC和它的真擴充套件所不允許的,因為“太大”的緣故(某些集合論在真類的名義下接受這些實體):

  NF清除了三個周知的集合論悖論。NFU這個{相對}相容的理論也避免了這些悖論,增強了我們對這些理論的信心。  羅素悖論:formula_20不是層化公式,所以不會通過概括的任何推論得出formula_15的存在性。蒯因構造NF的時候大概最關注於這個悖論。  關於最大基數的康托爾悖論利用了康托爾定理對全集的應用。康托爾定理聲稱(假定ZFC)任何集合的formula_22的冪集formula_23大於formula_22(沒有從formula_23到formula_22的單射函式)。但如果formula_27是全集的話,當然有從formula_28到formula_27的單射。為了解決這個問題,我們需要注意到formula_30在型別論中沒有意義:formula_23的型別比formula_22的型別高1。正確的有型別版本(它是在型別論中的定理,成立的原因就像康托爾定理在ZF中成立那樣)是formula_33,這裡的formula_34是formula_22的單元素子集的集合。在這個定理中,使我們感興趣的特殊例項是formula_36:單元素集合們少於集合們(因此一個元素的集合們少於全體物件,如果我們在NFU中的話)。從全集到這些單元素集合明顯的雙射formula_37不是一個集合;它不是集合是因為它的定義是非層化的。注意在所有已知的NFU的模型中formula_38都成立;“選擇公理”允許我們不只證明有基本元素,而且在formula_39和formula_40之間有很多基數。  我們現在引入某些有用的概念。若集合formula_22滿足formula_42,就被稱為康托爾式的:康托爾式集合滿足通常形式的康托爾定理。集合formula_22滿足進一步條件formula_44,即單元素集合對映在"A"上的限制,則不只是康托爾式的而且是強康托爾式的。  下面是關於最大序數的布拉利-福爾蒂悖論。我們定義(跟從樸素集合論)序數是良序排序在相似性下的等價類。在序數上有一個明顯的自然的良序排序;因為它是良序排序所以它屬於一個序數formula_45。(通過超限歸納法)可直接證明在小於一個給定序數formula_46的序數們上的自然次序的序型別是formula_46自身。但是這意味著formula_45是小於formula_49的序數們的序型別,因此它嚴格小於所有序數的序型別 -- 但是通過定義,後者是formula_45自身!  在NF(U)中對這個悖論的解決開始於觀察到在小於formula_46的序數們上的自然次序的序型別的型別比formula_46的型別高。因此型別齊平有序對的型別比它的引數的型別高1,而常規的Kuratowski有序對高3。對於任何序型別formula_46,我們可以定義比formula_46的型別高1的序型別:如果formula_55,則formula_56是次序formula_57的序型別。T運算的煩瑣只是外觀上的;可以輕易的證明T是在序數們上的嚴格的單調(序保持)運算。  我們可以用層化的方式重申關於序型別的引理:在小於formula_46的序數們上的自然次序的序型別是formula_59或formula_60,依賴於使用哪個有序對定義(我們在下文中假定型別齊平有序對)。從此我們可演繹出在小於formula_49的序數們上的序型別是formula_62,從它我們演繹出formula_63。因此T運算不是個函式;我們不能有從序數到序數的嚴格單調集合對映,它向下對映一個序數!因為T是單調的,我們有formula_64,在序數們中的“遞減序列”不能是集合。  某些人已經斷言這個結果證實了沒有NF(U)的模型是“標準”的,因此在任何NFU的模型中序數們外在的不是不是良序的。我們不接受這種立場,而我們注意到還有一個NFU的定理,任何NFU的集合模型都有非良序的“序數”;NFU不結論出全集"V"是NFU的模型,儘管"V"是集合,因為成員關係不是集合關係。  關於數學在NFU中的進一步開發,和與在ZFC中相同的開發的比較,請參見數學的集合論實現()。  蒯因在1940年第一版的《數理邏輯》的集合論中,結合了von Neumann-Bernays-Gödel集合論的真類於NF,併為真類包括了一個無限制概括的公理模式。在1942年,J. Barkley Rosser證明了蒯因的集合論遭受Burali-Forti悖論。在1950年,Hao Wang展示瞭如何修正蒯因的公理來避免這個問題,蒯因在1951年第二和最終版本的《數理邏輯》中包括了結果的公理化。
在數理邏輯中,新基礎集合論(NF)是公理化集合論的一種,由蒯因構想出來作為對《數學原理》中型別論的簡化。蒯因1937年於《數理邏輯的新基礎》一文中首次提及NF(此即其名稱的由來)。請注意,此條目大多是在談論NFU,這是Jensen於1969年所提出,並由Holmes於1998年闡述的一重要變體。