---
title: "Lévy 层级"
module: FOL.LevyHierarchy
lang: zh
site: "Bedrock"
description: "Lévy 层级"
stage: "一阶逻辑"
reading_order: 9
canonical: https://bedrock.institute/zh/FOL.LevyHierarchy.html
html: FOL.LevyHierarchy.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/LevyHierarchy.lagda.md
prerequisites: [Base.Prelude, FOL.Syntax]
routes: [common-foundations]
translations: [https://bedrock.institute/en/FOL.LevyHierarchy.md, https://bedrock.institute/ja/FOL.LevyHierarchy.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Lévy 层级

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

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

```agda
{-# 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 层级是语法本身的谓词，而不是语义值的谓词。

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

## Δ₀ 见证

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

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

```agda
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₁)` 这样含无界量词的公式不落入任何构造子，所以在该下标处根本拼不出 `Δ₀` 的元素。这种拒绝本身就是分类，而不是关于分类的定理。

```agda
  δ-⇒  : ∀ {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` 与 `δ-⊥` 打包，`δ-⊤` 则把 `δ-⊥` 放在蕴涵两端。它们是关于既有族的引理而非新构造子，使后面的代码无需新的分情形即可证明否定式与平凡式。

```agda
δ-¬ d = δ-⇒ d δ-⊥

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

## 检查具体公式

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

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

```agda
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 φ` 正是那条允许有界性穿过的 Δ₀ 构造子的计算对应物。

```agda
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` 本身就是第二个。

```agda
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`，递归调用给出子见证，再由 `δ-∧` 重组。

```agda
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`，运行两次递归调用，再以 `δ-∨` 或 `δ-⇒` 重组。伪式只需 `δ-⊥`。有了这些子句，Δ₀ 接受的每个无量词形状都有了从布尔结果到见证的路径。

```agda
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` 从不影响结果，而相反方向在这里任何地方都未被声称。

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

## Σ₁ 与 Π₁

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

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

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

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

```agda
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`。

```agda
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`。

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