層化

在數理邏輯中，層化是保證一個邏輯理論存在唯一形式釋義的任何一致的數到謂詞符號的指派。特別是，對於Horn子句理論，我們稱一個理論是層化的，當且僅當有一個層化指派 S 滿足下列條件:

(A) 如果謂詞 P 是肯定的推導自謂詞 Q，則 P 的層化數必定大於等於 Q 的層化數，簡寫為

。

(B) 如果謂詞 P 推導自否定的謂詞 Q，則 P 的層化數必定大於 Q 的層化數，簡寫為

。

層化只保證 Horn 子句理論的唯一釋義。它被蒯因(1937年)用來解決羅素悖論，它破壞了弗雷格的中心著作《Grundgesetze der Arithmetik》 (1902年)。

在帶有等式和成員關係的一階邏輯的語言中，一個公式

對新基礎和有關集合論被稱為是層化的，當且僅當有一個函數

以如下方式映射在

中出現的每個變量(考慮為一個語法單位)到一個自然數(如果所有整數都使用則運做相當良好)，

中出現的任何原子公式

滿足

而在

中出現的任何原子公式 x=y滿足

。 ^[1] 

顯然要求只在原子公式是約束於要考慮的集合抽象

中的時候滿足這些條件就足夠了。滿足這個弱條件的集合抽象被稱成弱層化。

新基礎的層化推廣到了帶有更多謂詞和帶有項構造的語言。每個基本謂詞都需要規定所需要的

在(弱)層化公式中的(約束)參數上的值之間的置換(displacement)。在帶有項構造的語言中，項自身需要被指派在

下的值，帶有它在(弱)層化公式中的每個(約束)參數上的值的固定置換。定義的項構造(可能只是含蓄的)使用描述理論來巧妙的處理: 項

(x 使得

) 必須被指派在

下同變量 x 同樣的值。

一個公式是層化的，當且僅當有可能指派類型給在公式中出現的所有變量，以在新基礎文章中描述的 TST 版本的類型論中有意義的方式。