基本介紹
- 中文名:層化
- 外文名:stratification
- 套用學科:數理邏輯
- 相關術語:弱層化
- 所屬領域:數學和天文學
- 定義:保證邏輯理論存在唯一形式釋義
數理邏輯中,新基礎中,
數理邏輯中
(A) 如果謂詞 P 是肯定的推導自謂詞 Q,則 P 的層化數必定大於等於 Q 的層化數,簡寫為
。

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

新基礎中
在帶有等式和成員關係的一階邏輯的語言中,一個公式
對新基礎和有關集合論被稱為是層化的,若且唯若有一個函式
以如下方式映射在
中出現的每個變數(考慮為一個語法單位)到一個自然數(如果所有整數都使用則運做相當良好),
中出現的任何原子公式
滿足
而在
中出現的任何原子公式 x=y滿足
。








顯然要求只在原子公式是約束於要考慮的集合抽象
中的時候滿足這些條件就足夠了。滿足這個弱條件的集合抽象被稱成弱層化。

新基礎的層化推廣到了帶有更多謂詞和帶有項構造的語言。每個基本謂詞都需要規定所需要的
在(弱)層化公式中的(約束)參數上的值之間的置換(displacement)。在帶有項構造的語言中,項自身需要被指派在
下的值,帶有它在(弱)層化公式中的每個(約束)參數上的值的固定置換。定義的項構造(可能只是含蓄的)使用描述理論來巧妙的處理: 項
(x 使得
) 必須被指派在
下同變數 x 同樣的值。





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