The Levy hierarchy

Not every formula travels equally well. Take a set x in some sub-world 𝒮 ↾ M of a model (the structure chapter's restriction), and ask one question twice: inside M, and in the full world. "Is x empty?" gets the same answer in both places whenever members of members stay inside M: the formula ∀̇∈ x ⊥̇ interrogates only the members of x, and none of them has escaped. But "is some set disjoint from x?" quantifies over everything, and the witness the full world has in mind may simply be missing from M. The difference shows in the syntax alone: the first formula's quantifier is bounded, the second's is not. The Levy hierarchy grades formulas by exactly this: Δ₀ allows only bounded quantifiers, Σ₁ prefixes existentials to a Δ₀ core, Π₁ prefixes universals. This chapter makes the grades witnesses: inductive data, purely syntactic, portable across any constant domain, travelling with the formula they certify; the next chapter proves the travel theorems they enable.

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

module FOL.LevyHierarchy where

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

The Δ₀ witness

One constructor per permitted formula shape, and none for ∃̇ or ∀̇: absence is the classification. A Δ₀ φ inhabitant is a machine-checkable witness that every quantifier in φ is bounded.

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 φ)

Σ₁ and Π₁

One unbounded quantifier kind each, stacked on a Δ₀ core.

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)} → Π₁ φ → Π₁ (∀̇ φ)

The general hierarchy

Σ₁ and Π₁ are the first floor of an alternating tower: Σₙ₊₁ stacks existential blocks on Πₙ, Πₙ₊₁ stacks universal blocks on Σₙ, and Δ₀ sits inside every level. Part 4's reflection arguments will climb this tower level by level; the constructors follow the same one-quantifier-per-step pattern, with σ-Π and π-Σ providing the alternation.

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) (∀̇ φ)

Recap

The Levy hierarchy lives as inductive witnesses, Δ₀ by the absence of unbounded constructors, Σ₁/Π₁ and the alternating Σₙ/Πₙ tower above it. The witnesses are pure syntax, and they stay put under a change of constant domain, a fact catalogued with the relabelling kit at the book's tail. The theorem that gives them their force is next.