λ→ à la Church 學習筆記-6（邏輯的表示）
目錄：類型論驛站寫作計劃
前一篇：λ→ à la Church 學習筆記-5（λ立方體的強正規性）
後一篇：λ→ à la Church 學習筆記-7（數據類型的表示）
這篇筆記大部分內容是由R Markdown生成的。曾經用知乎編輯器編寫了前半部分，但內容慘遭丟失。
λ 立方體中的八個系統對應著八個直覺主義邏輯系統。這就是 Barendregt 提出的「邏輯立方體」。
邏輯立方體里不同邏輯系統的具體名稱分別是：
- PROP：命題邏輯/命題演算
- PROP2：二階命題邏輯
- PROP
：弱高階命題邏輯
- PROPω ：高階命題邏輯
- PRED：謂詞邏輯/謂詞演算
- PRED2：二階謂詞邏輯
- PRED
- PREDω ：高階謂詞邏輯
這些系統都是「最小邏輯」，也就是說唯一的兩個邏輯運算元分別是→ 和 ? . 但對於二階與高階邏輯系統來說，其他的邏輯運算元，以及萊布尼茲等於關係（Leibnizs equality）是可以通過這兩個運算元來定義的。如果在邏輯立方體的系統里加上公理?α.??α→α ，那麼我們就得到了「經典邏輯立方體」。
在邏輯立方體的邏輯系統 中，公式 A 可以被解釋為λ 立方體中
系統里的類型[[A]]. 這種解釋被稱為「命題作為類型」釋義（propositions-as-types interpretation），最早由Bruijn（1970）和Howard（1980）提出。
「命題作為類型」釋義滿足健全性/可靠性（soundness）：如果 A 在PRED中是可證明的，那麼[[A]]在λP 中是被棲居（inhabited）的。
多類別謂詞邏輯
定義6（典型語境和翻譯）
和定義1中所定義的結構 相對應的典型語境（canonical context），記為
，定義如下：
對於項 ，我們歸納地定義
的典型翻譯（canonical translation），記為
，如下：
對於邏輯式 ，我們歸納地定義
的典型翻譯，記為
，如下：
引理7
1.
2.
定義8（定義3的重新描述）
在PRED中， 的推導（derivation)
，記為
定義如下：
表示映射，
表示引入（introduction），
表示推廣（generalization）。
定義9
1. 設 ，那麼
的典型翻譯，記為
，是如下定義的語境（context）：
2. 在PRED里，設 ，
的典型翻譯，記為
，以及
的典型語境，記為
，歸納地定義如下：
定義16
1. PROP定義如下：
PROP2定義如下：
PROP
定義如下：
PROP
定義如下：
2. PRED 定義如下：
PRED2 定義如下：
PRED
定義如下：
PRED
定義如下：
新的PTS立方體如下圖所示：
定義17（邏輯運算的二階可定義性）
1. 對於 ，我們定義：
2. 對於 ，我們定義：
3. 對於 ，我們定義：
「邏輯立方體- 立方體」里的所有系統對子（二元組）都滿足健全性，但並非所有對子都滿足完全性（completeness）。此外，邏輯PTS立方體中的所有系統的推導都是強正規的。
目錄：類型論驛站寫作計劃
前一篇：λ→ à la Church 學習筆記-5（λ立方體的強正規性）
後一篇：λ→ à la Church 學習筆記-7（數據類型的表示）
推薦閱讀：