6.2 宇宙公理與古典相容#
本章導讀#
上一節建立了命題即型別的樂觀對應 ， 本章要誠實面對它的邊界 。 核心問題有三個 ， 型別能裝下自己嗎 ， 命題證明是否唯一 ， 需要哪些公理 。 學完本章 ， 你能解釋宇宙分層 ， 並說出三個古典公理的用途 。 我們會以 Russell 悖論為反面教材 ， 看宇宙如何擋下自我指涉 。 本章結束後 ， 第 5 章與第 6 章的理論篇即告一段落 。
淺顯說明#
把宇宙想成圖書館的樓層 ， 地面是 \(Type\_0\) ， 二樓是 \(Type\_1\) ， 依此類推 。 每一層的住戶名冊都放在上一層 ， 所以名冊永遠比住戶高一層 。 自然數 \(Nat\) 住在地面 ， 而地面的名冊本身住在二樓 。 命題宇宙 \(Prop\) 則像特別閱覽室 ， 每個座位最多只認一種借閱證 。 這就是證明無關性 ， 同一命題的兩個證明沒有可觀察的差別 。 三個古典公理像是館方外掛 ， 啟用後查詢更方便 ， 但不再是純構造借閱 。 商型別則像併桌服務 ， 按等價關係把同桌的讀者視為同一組 。 而 Russell 悖論就像要求一本收錄所有不收錄自己的目錄 ， 館方用樓層制度拒絕它 。 因為目錄與被收錄的書不能住在同一層 ， 悖論的自我指涉無法成形 。
正規理論#
宇宙分層的核心是以下兩條判斷 ， 每一層都住在更高一層之中 。
依此類推形成無窮階梯 ， 從而避免型別包含自身的循環 。 下表整理各宇宙層級及其典型居民 。
| 層級 | 典型居民 | 說明 |
|---|---|---|
| \(Prop\) | \(True\) ， \(False\) ，等式命題 | 證明無關的命題宇宙 |
| \(Type\_0\) | \(Nat\) ， \(Bool\) ， \(List\) | 日常資料型別的家 |
| \(Type\_1\) | \(Type\_0\) 本身 | 名冊住在上一層 |
證明無關性可用獨立公式表達如下 ， 同一命題的證明彼此相等 。
命題即型別的構造核心只需要以上機制 ， 但古典數學還需要三條公理 。
| 公理 | 內容 | 用途 | 構造性 |
|---|---|---|---|
| \(propext\) | 互推命題彼此相等 | 命題層的等價代換 | 非構造 |
| \(funext\) | 逐點相等則函數相等 | 函數層的等價代換 | 非構造 |
| \(choice\) | 由存在性取出選擇函數 | 從規格得到實作 | 非構造 |
商型別 \(Quot\) 允許按等價關係把元素黏成同一點 ， 其消去子要求函數尊重等價關係 。 Russell 構造的核心集合可用以下公式表示 ， 關鍵在於無層級的概括公理 。
在無宇宙的集合論中 ， 由 \(R\) 可推出矛盾的等價式 ， 故理論不一致 。 而在分層宇宙中 ， 概括公理的每一次收集都被固定在某一層之內 。 集合 \(R\) 若在第 \(n\) 層 ， 其成員條件只能談論低於 \(n\) 層的對象 。 自我成員判斷 \(R\in R\) 因而不再是良形公式 ， 悖論在成形前即被樓層制度攔下 。
簡易範例#
下面程式示範宇宙分層的查詢 ， 以及三公理的典型使用骨架 。 請在 Lean 中逐行執行 #check ， 觀察宇宙標號的變化 。
#check Type -- 第一宇宙
#check Prop -- 命題宇宙
#check (Type : Type 1) -- 分層證據
variable {p q : Prop}
variable {α β : Type} {f g : α → β}
-- 命題外延性
example (h : p ↔ q) : p = q := propext h
-- 函數外延性
example (h : ∀ x, f x = g x) : f = g := funext h
-- 選擇公理
#check @Classical.choice
-- 商型別構造子
#check @Quot
第一組查詢顯示 \(Type\) 其實是 \(Type\_0\) 的省略寫法 ， 而它住在 \(Type\_1\) 之中 。 \(propext\) 把邏輯等價提升為相等 ， 是命題層最常用的代換工具 。 \(funext\) 把逐點相等提升為函數相等 ， 沒有它就無法證明多數函數等式 。 \(choice\) 則從存在敘述中取出函數 ， 代價是超出純構造範疇 。 商型別 \(Quot\) 把以上能力再推一步 ， 允許自訂相等關係 。 關於 Russell 的實驗 ， 可試著在注釋中寫下無層級的概括 ， 體會它為何無法通過宇宙檢查 。
歷史典故#
宇宙分層的源頭是 Church 簡單型別理論 。 該卷宗以型別階層馴服了無型別演算中的自我套用 。 分層思想的集大成者是 CoC 與 CIC 。 構造演算用宇宙階梯同時容納程式 ， 命題與證明 ， 又避開悖論 。 公理一側的后續發展 ， 則通向 HoTT 同倫型別論 。 同倫觀點重新詮釋了相等與等價 ， 讓 \(funext\) 與商型別有了幾何意義 。 而工程一側的里程碑是 Coq 誕生 。 它證明分層宇宙與古典公理可以在同一系統中和平共存 。 讀本章時 ， 不妨把宇宙看成防火牆 ， 把公理看成經審查的通行證 。
習題#
- 用
#check觀察 \(Nat\) ， \(Type\) 與 \(Prop\) 各自的宇宙 ， 並用樓層比喻解釋為何 \(Type\) 不能住在自己裡面 。 - 分別舉一個必須使用 \(propext\) 與 \(funext\) 的證明場景 ， 並說明不用它們時證明會卡在哪一步 。
- 仿照 \(R\) 的定義寫出理髮師版本 ， 即為全城不為自己理髮的人理髮 ， 並說明宇宙分層在哪一步擋下這個定義 。