Lévy 层级

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

阅读指南 · 依赖地图

一阶公式有两种量化方式：有界的，如「对所有 $x$ 属于 $t$」；以及在整个宇宙上取量的无界量化。Lévy 层级按无界量词衡量公式的语法复杂度：Δ₀ 公式只用有界量词，Σ₁ 公式在 Δ₀ 核心之前加一段无界存在量词，Π₁ 公式则加一段无界全称量词。这些类的归属之所以重要，是因为后面的章节要证明 Δ₀ 绝对性，并在可构造宇宙上按量词形状做结构归纳的可定义性论证。与其反复去检查公式，本章干脆把分类本身做成数据：见证是以公式为下标的归纳数据，对任意常元域 K 都可用，于是一个公式可以在语法之外同时携带其复杂度类的证明。本章构造 Δ₀ 见证、一个识别有界公式的布尔检查器，以及推广到每个有限层级 Σₙ/Πₙ 的分类。

本章依赖一条从计算到证明的桥梁。类型 Bool 有 true 与 false 两个值，_and_ 合取两个布尔结果。运算 Bool→Type 把布尔值送到一个类型：true 对应单点类型，false 对应空类型。于是 Bool→Type b 有元素当且仅当 b 为 true。这正是让计算结果日后能兼作证明义务的机制：程序可以先对语法作出布尔判定，而「答案为 true」这个断言本身就是一个可以有元素的类型。

{-# OPTIONS --cubical --safe --guardedness #-}

module FOL.LevyHierarchy where

open import Base.Prelude
open import Cubical.Data.Bool using ( Bool; true; false; _and_; Bool→Type )

被分类的公式来自 FOL.Syntax 的对象语言：词项、原子关系 _∈̇_ 与 _≐_、联结词，以及两对不同的量词形式。有界量词 ∀̇∈ 与 ∃̇∈ 把界限写成语言中的词项，而 ∀̇_ 与 ∃̇_ 则不带界限地量化。两种量词在语法上分离，正是整个分类得以进行的前提：下面定义的每个族都以 Formula K n 为下标，所以这里的Lévy 层级是语法本身的谓词，而不是语义值的谓词。

open import Cubical.Data.Unit using ( tt )
open import FOL.Syntax using
  ( Term; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

Δ₀ 见证

Δ₀ 是以公式为下标的归纳族：Δ₀ φ 的一个元素就是一份显式数据的见证，证明 φ 中出现的每个量词都有界。定义对每个获准的公式形状给一个构造子，而不给 ∃̇ 与 ∀̇ 任何构造子；缺席即分类。该族除在某个宇宙层级 ℓc 上以常元域 K 为参数外，只由语法决定，所以同一见证类型对任意常元域都可用。

Δ₀ 族的指引性不变量是：有界量词保持有界性，无界量词破坏它。声明把它实现为以每个元数 n 的公式为下标的归纳族 Δ₀，与 K 同处一个宇宙层级，故见证是小数据。像 t ∈̇ u 这样的原子公式被直接接受：它根本不含量词，所以 δ-∈ (以及等式的同伴 δ-≐) 不带参数。该类随后对二元联结词封闭，δ-∧ 与 δ-∨ 各自要求复合公式两个成分都有见证。

data Δ₀ {ℓc} {K : Type ℓc} : ∀ {n} → Formula K n → Type ℓc where
  δ-∈  : ∀ {n} {t u : Term K n} → Δ₀ (t ∈̇ u)
  δ-≐  : ∀ {n} {t u : Term K n} → Δ₀ (t ≐ u)
  δ-∧  : ∀ {n} {φ ψ : Formula K n} → Δ₀ φ → Δ₀ ψ → Δ₀ (φ ∧̇ ψ)
  δ-∨  : ∀ {n} {φ ψ : Formula K n} → Δ₀ φ → Δ₀ ψ → Δ₀ (φ ∨̇ ψ)

蕴涵 δ-⇒ 与不带量词的伪式 δ-⊥ 补齐了无量词的形状。决定性的行是有界量词：δ-∀∈ 与 δ-∃∈ 取元数 suc n 的体 φ 的见证，返回 ∀̇∈ t φ 或 ∃̇∈ t φ 的见证，其界限是词项 t。于是有界性原封不动地穿过有界量词。同样决定性的是清单所省略者：没有任何构造子提到无界的 ∃̇ 或 ∀̇。像 ∃̇ (x₀ ∈̇ x₁) 这样含无界量词的公式不落入任何构造子，所以在该下标处根本拼不出 Δ₀ 的元素。这种拒绝本身就是分类，而不是关于分类的定理。

  δ-⇒  : ∀ {n} {φ ψ : Formula K n} → Δ₀ φ → Δ₀ ψ → Δ₀ (φ ⇒̇ ψ)
  δ-⊥  : ∀ {n} → Δ₀ {n = n} ⊥̇
  δ-∀∈ : ∀ {n} {t : Term K n} {φ : Formula K (suc n)} → Δ₀ φ → Δ₀ (∀̇∈ t φ)
  δ-∃∈ : ∀ {n} {t : Term K n} {φ : Formula K (suc n)} → Δ₀ φ → Δ₀ (∃̇∈ t φ)

δ-¬ : ∀ {ℓc} {K : Type ℓc} {n} {φ : Formula K n} → Δ₀ φ → Δ₀ (¬̇ φ)

否定与真无需特殊处理，因为它们不是原始的：在这套语法中，¬̇ φ 定义为 φ ⇒̇ ⊥̇，⊤̇ 定义为 ⊥̇ ⇒̇ ⊥̇。既然蕴涵与伪式已有见证，被定义公式的有界性便由 δ-⇒ 构造子推出。派生见证 δ-¬ d 把见证 d 与 δ-⊥ 打包，δ-⊤ 则把 δ-⊥ 放在蕴涵两端。它们是关于既有族的引理而非新构造子，使后面的代码无需新的分情形即可证明否定式与平凡式。

δ-¬ d = δ-⇒ d δ-⊥

δ-⊤ : ∀ {ℓc} {K : Type ℓc} {n} → Δ₀ {K = K} {n = n} ⊤̇
δ-⊤ = δ-⇒ δ-⊥ δ-⊥

检查具体公式

逐条对照构造子清单去读一个公式并无必要：函数 bounded 遍历语法，恰在未遇到无界量词时返回 true；checkΔ₀ 再把「这个布尔值为 true」这一断言转成真正的 Δ₀ 见证。已证明的方向是单向的：布尔成功给出见证。这里并未声称该定义是反方向的判定过程，也没有证明任何完备性结果。

一旦不变量可以机械地检查，手工构造 Δ₀ 见证就不必要了。函数 bounded 遍历公式并报告一个 Bool：原子公式与伪式直接报告 true，每个二元联结词则用 _and_ 合取两个子公式的结果。此阶段的检查只是逐个公式构造子地镜像 Δ₀ 所接受的形状。

bounded : ∀ {ℓc} {K : Type ℓc} {n} → Formula K n → Bool
bounded (t ∈̇ u) = true
bounded (t ≐ u) = true
bounded (φ ∧̇ ψ) = bounded φ and bounded ψ
bounded (φ ∨̇ ψ) = bounded φ and bounded ψ

不变量在这里真正发挥作用。两个无界量词都返回 false，所以公式中任何一处出现无界量词，无论子公式如何，整个检查即告失败。有界量词则相反：递归直接进入体公式，因为界限 t 是语法中的词项，藏不住量词。规则 bounded (∀̇∈ t φ) = bounded φ 正是那条允许有界性穿过的 Δ₀ 构造子的计算对应物。

bounded (φ ⇒̇ ψ) = bounded φ and bounded ψ
bounded ⊥̇ = true
bounded (∃̇ φ) = false
bounded (∀̇ φ) = false
bounded (∀̇∈ t φ) = bounded φ

合取处的布尔值 true 意味着两件事，私有辅助函数 and-out 把它拆开。给定 a b : Bool 与 Bool→Type (a and b) 的一个元素，它返回一对元素，分别属于 Bool→Type a 与 Bool→Type b。当 a 为 false 时，输入将不得不落入空类型 Bool→Type false，所以该情形由荒谬模式 () 直接打发。当 a 为 true 时，单位元 tt 证明第一个合取支，而给定的 h 本身就是第二个。

bounded (∃̇∈ t φ) = bounded φ

private
  and-out : (a b : Bool) → Bool→Type (a and b) → Bool→Type a × Bool→Type b
  and-out false b ()
  and-out true b h = tt , h

函数 checkΔ₀ 正是布尔判定变成证据之处。它取公式 φ 与 Bool→Type (bounded φ) 的一个元素，后者只有在遍历算出 true 时才可能存在，并产出真正的 Δ₀ φ 见证。原子情形直接返回相应构造子，前提 h 用不上。合取情形中，bounded (φ ∧̇ ψ) 计算为 bounded φ and bounded ψ，于是 and-out 把 h 拆成两个逐支证明 p .fst 与 p .snd，递归调用给出子见证，再由 δ-∧ 重组。

checkΔ₀ : ∀ {ℓc} {K : Type ℓc} {n} (φ : Formula K n) → Bool→Type (bounded φ) → Δ₀ φ
checkΔ₀ (t ∈̇ u) h = δ-∈
checkΔ₀ (t ≐ u) h = δ-≐
checkΔ₀ (φ ∧̇ ψ) h = δ-∧ (checkΔ₀ φ (p .fst)) (checkΔ₀ ψ (p .snd))
  where p = and-out (bounded φ) (bounded ψ) h

析取与蕴涵重复同一动作：各自用 and-out 拆开 h，运行两次递归调用，再以 δ-∨ 或 δ-⇒ 重组。伪式只需 δ-⊥。有了这些子句，Δ₀ 接受的每个无量词形状都有了从布尔结果到见证的路径。

checkΔ₀ (φ ∨̇ ψ) h = δ-∨ (checkΔ₀ φ (p .fst)) (checkΔ₀ ψ (p .snd))
  where p = and-out (bounded φ) (bounded ψ) h
checkΔ₀ (φ ⇒̇ ψ) h = δ-⇒ (checkΔ₀ φ (p .fst)) (checkΔ₀ ψ (p .snd))
  where p = and-out (bounded φ) (bounded ψ) h
checkΔ₀ ⊥̇ h = δ-⊥

余下的子句收束论证。对无界量词，bounded (∃̇ φ) 与 bounded (∀̇ φ) 都计算为 false，于是前提 h 将不得不落入空类型 Bool→Type false；荒谬模式 () 之所以能接受该情形，正因为这样的元素不存在。对有界量词，bounded (∀̇∈ t φ) 计算为 bounded φ，于是 h 原样传给体公式，递归结果用 δ-∀∈ 或 δ-∃∈ 包住。合起来，这些子句对每个公式确立 bounded φ ≡ true → Δ₀ φ：计算上的成功给出证据。词项 t 与 u 从不影响结果，而相反方向在这里任何地方都未被声称。

checkΔ₀ (∃̇ φ) ()
checkΔ₀ (∀̇ φ) ()
checkΔ₀ (∀̇∈ t φ) h = δ-∀∈ (checkΔ₀ φ h)
checkΔ₀ (∃̇∈ t φ) h = δ-∃∈ (checkΔ₀ φ h)

Σ₁ 与 Π₁

公式既然可以无界量化，下一个自然的问题是：公式可以含多少个无界量词、是哪种。Σ₁ 与 Π₁ 恰好对一段量词作出回答：Σ₁ 见证要么是 Δ₀ 见证，要么是对某个 Σ₁ 见证 (其体公式) 再多施加一个无界存在量词。因此 Σ₁ 见证构成一个套在自己之上的类型，记录 Δ₀ 核心之上任意有限段存在量词；Π₁ 则是同一构造、极性翻转。两类都不允许两种量词交替，且每个约束词消耗元数 suc n 的体、产出元数 n 的公式。这里的两族是独立定义的；下一节把同一想法重组成按层级下标的统一层级。

这种嵌套在 Σ₁ 的两个构造子中清晰可见。基座 σ-Δ₀ 原样嵌入任何 Δ₀ 见证，于是每个有界公式都算 Σ₁，不带额外量词。台阶 σ-∃ 前置一个无界存在量词：从元数 suc n 的体的 Σ₁ 见证构造出 ∃̇ φ 的见证。反复使用 σ-∃ 便得到有限段存在量词，而这一段必须终于 σ-Δ₀ 核心；途中没有办法引入全称量词。

data Σ₁ {ℓc} {K : Type ℓc} : ∀ {n} → Formula K n → Type ℓc where
  σ-Δ₀ : ∀ {n} {φ : Formula K n} → Δ₀ φ → Σ₁ φ
  σ-∃  : ∀ {n} {φ : Formula K (suc n)} → Σ₁ φ → Σ₁ (∃̇ φ)

Π₁ 是其镜像：π-Δ₀ 共享同一个 Δ₀ 基座，π-∀ 前置一个无界全称量词，同样取自元数 suc n 的体。两族由同一嵌套模式构成，只是量词极性相反，而这一极性之差正是后面绝对性论证要从见证中读出的东西。

data Π₁ {ℓc} {K : Type ℓc} : ∀ {n} → Formula K n → Type ℓc where
  π-Δ₀ : ∀ {n} {φ : Formula K n} → Δ₀ φ → Π₁ φ
  π-∀  : ∀ {n} {φ : Formula K (suc n)} → Π₁ φ → Π₁ (∀̇ φ)

一般层级

一段固定的无界量词只是第一级。一般Lévy 层级按无界量词极性交替的次数为公式分级，本章用两个互定义的归纳族 Σₙ 与 Πₙ 来编码这种分级，各带自然数层级 k。下标 k 是由见证自身提供的一个界：层级 k 的见证至多可用 k 次交替，但不必恰好用 k 次，因为 Δ₀ 公式在每个层级都有嵌入。隐含的 n 仍是公式的元数，是另一回事，不可与 k 混淆。每个族在固定层级上对自己那种无界量词封闭，而 σ-Π 与 π-Σ 则是跨越两族、抬升下标的两个交替步骤。

两族必须互相引用，因为交替恰恰就是换族，所以它们在一个 mutual 块中声明。Σₙ 在公式下标之前带上层级下标 k。基座 σ-Δ₀ 允许 Δ₀ 公式处于任何层级 k，这正是层级记录上界而非确切次数的原因。交替台阶 σ-Π 把 Πₙ k 的见证提升为 Σₙ (suc k)，为跨越极性付出一级层。最后，σ-∃ 在同一层级 suc k 上用多一个存在量词扩展见证，体的元数 suc n 缩回到 n。

mutual
  data Σₙ {ℓc} {K : Type ℓc} : ℕ → ∀ {n} → Formula K n → Type ℓc where
    σ-Δ₀ : ∀ {k n} {φ : Formula K n} → Δ₀ φ → Σₙ k φ
    σ-Π  : ∀ {k n} {φ : Formula K n} → Πₙ k φ → Σₙ (suc k) φ
    σ-∃  : ∀ {k n} {φ : Formula K (suc n)} → Σₙ (suc k) φ → Σₙ (suc k) (∃̇ φ)

Πₙ 在同一互定义块中以对偶形状声明：π-Δ₀ 在每个层级嵌入 Δ₀，π-Σ 把 Σₙ k 的见证提升为 Πₙ (suc k)，π-∀ 使层级 suc k 对无界全称量词封闭。两族合起来记录了核心按层级所允许的次数交替的有限量词段。上一节独立定义的 Σ₁/Π₁ 两族在形状上对应 Σₙ 1 与 Πₙ 1，即 suc zero：零层级只有 Δ₀ 构造子可用，而量词构造子都要求 suc k。

  data Πₙ {ℓc} {K : Type ℓc} : ℕ → ∀ {n} → Formula K n → Type ℓc where
    π-Δ₀ : ∀ {k n} {φ : Formula K n} → Δ₀ φ → Πₙ k φ
    π-Σ  : ∀ {k n} {φ : Formula K n} → Σₙ k φ → Πₙ (suc k) φ
    π-∀  : ∀ {k n} {φ : Formula K (suc n)} → Πₙ (suc k) φ → Πₙ (suc k) (∀̇ φ)

小结

Lévy 层级现在由归纳见证表示。Δ₀ 见证从构造上排除无界量词；Σ₁ 与 Π₁ 各加入一段有限的单一极性量词；互定义的 Σₙ 与 Πₙ 族则把更高的交替层级同公式元数分开控制。每个见证都显露获准的外层形状，因此后续归纳论证可以分别处理有界、存在与全称情形。