The Levy hierarchy

公式的旅行能力并不平等。取模型某个子世界 𝒮 ↾ M (结构章的限制) 中的一个集合 x，同一个问题问两遍：一遍在 M 里问，一遍在全世界问。「x 空吗？」只要成员的成员不出 M，两处答案就一致：公式 ∀̇∈ x ⊥̇ 只盘问 x 的成员，而它们谁也没有逃走。可「有集合与 x 不相交吗？」对一切量化，全世界心里想的那个见证可能恰好不在 M 中。这份差别单看语法就能看出：前一条公式的量词有界，后一条无界。Lévy 层级恰按此给公式分级：Δ₀ 只许有界量词，Σ₁ 在 Δ₀ 核心之前加存在量词，Π₁ 加全称量词。本章把级别做成见证：纯语法的归纳数据，对任意常量域可携，随其所证的公式旅行；它们所解锁的旅行定理由下一章证明。

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

module FOL.LevyHierarchy where

open import Base.Prelude
open import Base.Truth
open import FOL.Syntax using
  ( Term; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

Δ₀ 见证

每个获准的公式形状一个构造子，而 ∃̇ 与 ∀̇ 没有：缺席即分类。Δ₀ φ 的居民就是「φ 的每个量词都有界」的机器可查见证。

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} → Δ₀ φ → Δ₀ ψ → Δ₀ (φ ∨̇ ψ)
  δ-⇒  : ∀ {n} {φ ψ : Formula K n} → Δ₀ φ → Δ₀ ψ → Δ₀ (φ ⇒̇ ψ)
  δ-¬  : ∀ {n} {φ : Formula K n} → Δ₀ φ → Δ₀ (¬̇ φ)
  δ-⊤  : ∀ {n} → Δ₀ {n = n} ⊤̇
  δ-⊥  : ∀ {n} → Δ₀ {n = n} ⊥̇
  δ-∀∈ : ∀ {n} {t : Term K n} {φ : Formula K (suc n)} → Δ₀ φ → Δ₀ (∀̇∈ t φ)
  δ-∃∈ : ∀ {n} {t : Term K n} {φ : Formula K (suc n)} → Δ₀ φ → Δ₀ (∃̇∈ t φ)

Σ₁ 与 Π₁

各在 Δ₀ 核心之上叠一种无界量词。

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

data Π₁ {ℓc} {K : Type ℓc} : ∀ {n} → Formula K n → Type ℓc where
  π-Δ₀ : ∀ {n} {φ : Formula K n} → Δ₀ φ → Π₁ φ
  π-∀  : ∀ {n} {φ : Formula K (suc 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) (∃̇ φ)

  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 层级以归纳见证的形态存在：Δ₀ 靠无界构造子的缺席，其上是 Σ₁/Π₁ 与交替的 Σₙ/Πₙ 之塔。这些见证是纯语法，且在常量变换下纹丝不动，这一事实编在书末的常量变换工具组里。赋予它们力量的定理在下一章。