The Lévy hierarchy

A first-order formula can quantify in two ways: boundedly, as in "for all $x$ in $t$", or unboundedly, over the whole universe. The Lévy hierarchy measures a formula's syntactic complexity by its unbounded quantifiers: Δ₀ formulas use only bounded quantifiers, Σ₁ formulas prefix a block of unbounded existentials to a Δ₀ core, and Π₁ formulas prefix a block of unbounded universals. Membership in these classes matters because later chapters prove Δ₀-absoluteness and run definability arguments over the constructible universe by structural induction on quantifier shape. Rather than inspect formulas over and over, this chapter turns the classification itself into data: a witness is an inductive datum indexed by a formula, available for any constant domain K, so a formula can carry proof of its own complexity class alongside its syntax. The chapter builds the Δ₀ witness, a Boolean checker that recognizes bounded formulas, and the extension to every finite level Σₙ/Πₙ.

The chapter relies on one bridge between computation and proof. The type Bool has the two values true and false, and _and_ conjoins two Boolean results. The operation Bool→Type sends a Boolean to a type: true goes to a one-point type and false to the empty type. Hence an element of Bool→Type b exists exactly when b is true. This is what lets a computed answer later serve as a proof obligation: a program can first decide a Boolean question about syntax, and the assertion that the answer came out true is itself a type one can inhabit.

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

module FOL.LevyHierarchy where

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

The formulas being classified come from the object language of FOL.Syntax: terms, the atomic relations _∈̇_ and _≐_, the connectives, and two distinct pairs of quantifier forms. The bounded quantifiers ∀̇∈ and ∃̇∈ name their bound as a term of the language, while ∀̇_ and ∃̇_ quantify without one. Keeping the two kinds syntactically separate is what makes the whole classification possible: every family defined below is indexed by a Formula K n, so the Lévy hierarchy here is a predicate on syntax itself, never on semantic values.

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

The Δ₀ witness

Δ₀ is an inductive family indexed by formulas: an inhabitant of Δ₀ φ is a witness, as explicit data, that every quantifier occurring in φ is bounded. The definition admits one constructor for each permitted formula shape and none for ∃̇ or ∀̇; this absence is the classification. The family is parameterized by the constant domain K at some universe level ℓc but otherwise only by syntax, so the same witness type is available over any domain.

The guiding invariant of the Δ₀ family is: bounded quantifiers preserve boundedness, and unbounded quantifiers break it. The declaration realizes this as an inductive family Δ₀ indexed by formulas of every arity n, living at the same universe level as K, so a witness is small data. An atomic formula such as t ∈̇ u is accepted outright: it contains no quantifier at all, so δ-∈ (and its equality companion δ-≐) takes no argument. The class is then closed under the binary connectives, with δ-∧ and δ-∨ each demanding a witness for both components of the compound.

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} → Δ₀ φ → Δ₀ ψ → Δ₀ (φ ∨̇ ψ)

Implication δ-⇒ and falsity δ-⊥, which carries no quantifier, complete the quantifier-free shapes. The decisive rows are the bounded quantifiers: δ-∀∈ and δ-∃∈ take a witness for a body φ of arity suc n and return one for ∀̇∈ t φ or ∃̇∈ t φ, where the bound is the term t. Boundedness thus travels through a bounded quantifier unchanged. Equally decisive is what the list omits: no constructor mentions the unbounded ∃̇ or ∀̇. A formula with an unbounded quantifier, such as ∃̇ (x₀ ∈̇ x₁), falls under no constructor, so no inhabitant of Δ₀ at that index can ever be assembled. This refusal is the classification, not a theorem about it.

  δ-⇒  : ∀ {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} → Δ₀ φ → Δ₀ (¬̇ φ)

Negation and truth need no special treatment because they are not primitive: in this syntax ¬̇ φ is defined as φ ⇒̇ ⊥̇ and ⊤̇ as ⊥̇ ⇒̇ ⊥̇. Since implication and falsity already carry witnesses, boundedness of the defined formulas follows by the δ-⇒ constructor. The derived witness δ-¬ d packages the witness d with δ-⊥, and δ-⊤ places δ-⊥ on both sides of an implication. These are lemmas about the existing family, not new constructors, and they let later code certify negated and trivial formulas without new case analysis.

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

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

Checking concrete formulas

Reading a formula against the constructor list by hand is unnecessary: the function bounded traverses the syntax and returns true exactly when no unbounded quantifier is met, and checkΔ₀ converts the assertion that this Boolean came out true into an actual Δ₀ witness. The proved direction is one-way: Boolean success yields a witness. The definition is not claimed to be a decision procedure in the opposite direction, and no completeness result is proved here.

Building Δ₀ witnesses by hand is unnecessary once the invariant can be checked mechanically. The function bounded walks through a formula and reports a Bool: atomic formulas and falsity report true outright, while each binary connective conjoins the results of its two subformulas with _and_. At this stage the check simply mirrors the shapes that Δ₀ accepts, one recursion per formula constructor.

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 ψ

Here the invariant does real work. Both unbounded quantifiers return false, so a single unbounded occurrence anywhere in a formula spoils the whole check, whatever its subformulas look like. The bounded quantifiers behave oppositely: the recursion just continues into the body, because the bound t is a term of the syntax and cannot conceal a quantifier. The rule bounded (∀̇∈ t φ) = bounded φ is the computational counterpart of the Δ₀ constructor that let boundedness pass through.

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

A Boolean true at a conjunction means two things at once, and the private helper and-out takes it apart. Given a b : Bool and an inhabitant of Bool→Type (a and b), it returns a pair of inhabitants, one for Bool→Type a and one for Bool→Type b. When a is false, the input would have to inhabit Bool→Type false, an empty type, so the case is discharged by the absurd pattern (). When a is true, the unit element tt proves the first conjunct and the given h already is the second.

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

The function checkΔ₀ is where the Boolean decision becomes evidence. It takes a formula φ and an inhabitant of Bool→Type (bounded φ), which can exist only if the traversal computed true, and produces an actual Δ₀ φ witness. The atomic cases return the corresponding constructors directly, with the hypothesis h unused. For a conjunction, bounded (φ ∧̇ ψ) computes to bounded φ and bounded ψ, so and-out splits h into the two per-conjunct proofs p .fst and p .snd, and the recursive calls supply the sub-witnesses that δ-∧ reassembles.

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

Disjunction and implication repeat the same move: each splits h with and-out, runs the two recursive calls, and recombines with δ-∨ or δ-⇒. Falsity needs only δ-⊥. With these clauses, every quantifier-free shape that Δ₀ accepts has a route from the Boolean result to a witness.

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 = δ-⊥

The remaining clauses close the argument. For the unbounded quantifiers, bounded (∃̇ φ) and bounded (∀̇ φ) both compute to false, so the hypothesis h would have to inhabit Bool→Type false, an empty type; the absurd pattern () accepts the case precisely because no such inhabitant exists. For the bounded quantifiers, bounded (∀̇∈ t φ) computes to bounded φ, so h passes unchanged to the body and the recursive result is wrapped with δ-∀∈ or δ-∃∈. In total the clauses establish bounded φ ≡ true → Δ₀ φ for every formula: computational success yields evidence. The terms t and u never influence the outcome, and the converse direction is not claimed anywhere here.

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

Σ₁ and Π₁

Once formulas can be unboundedly quantified, the natural next question is how many unbounded quantifiers, and of which kind, a formula may contain. Σ₁ and Π₁ answer for exactly one block: a Σ₁ witness is either a Δ₀ witness, or one more unbounded existential applied to a Σ₁ witness for the body. So Σ₁-witnesses form a type nested over itself, recording any finite run of existentials over a Δ₀ core, and Π₁ is the same construction with the polarity flipped. Neither class allows the two quantifier kinds to alternate, and each binder consumes a body of arity suc n while producing a formula of arity n. The two families here stand alone; the next section reorganizes the same idea into a uniform hierarchy indexed by a level.

The nesting is visible in the two constructors of Σ₁. The base σ-Δ₀ embeds any Δ₀ witness unchanged, so every bounded formula counts as Σ₁ with no extra quantifiers. The step σ-∃ prepends one unbounded existential: from a Σ₁ witness for a body of arity suc n it builds one for ∃̇ φ. Applying σ-∃ repeatedly builds a finite block of existentials, and the block must end in a σ-Δ₀ core; there is no way to introduce a universal quantifier along the way.

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

Π₁ is the mirror image: π-Δ₀ shares the same Δ₀ base, and π-∀ prepends one unbounded universal, again from a body of arity suc n. The two families are built by the same nesting pattern with the quantifier polarity reversed, and this difference in polarity is exactly what later absoluteness arguments will read off the witnesses.

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

The general hierarchy

One fixed block of unbounded quantifiers is only the first rung. The general Lévy hierarchy grades formulas by how often the polarity of their unbounded quantifiers alternates, and this chapter encodes the grading with two mutually defined inductive families, Σₙ and Πₙ, each carrying a natural number level k. The index k is a bound supplied by the witness itself: a witness at level k may use up to k alternations, but need not use exactly k, because Δ₀ formulas embed at every level. The implicit n remains the formula's arity, a separate bookkeeping that must not be confused with k. Each family closes under its own unbounded quantifier at a fixed level, while σ-Π and π-Σ are the two alternation steps that raise the index by crossing between the families.

The two families must refer to each other, since an alternation is precisely a change of family, so they are declared in one mutual block. Σₙ carries the level index k before the formula index. The base σ-Δ₀ lets a Δ₀ formula sit at any level k, which is why the level records an upper bound rather than an exact count. The alternation step σ-Π promotes a Πₙ k witness to Σₙ (suc k), paying one increment of level for crossing polarity. Finally σ-∃ extends a witness at level suc k by one more existential at that same level, the body's arity suc n shrinking back to 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) (∃̇ φ)

Πₙ is declared in the same mutual block with the dual shape: π-Δ₀ embeds Δ₀ at every level, π-Σ lifts a Σₙ k witness to Πₙ (suc k), and π-∀ closes level suc k under unbounded universals. Together the two families record finite quantifier blocks whose cores alternate as often as the level permits. The separately defined Σ₁/Π₁ families of the previous section correspond in shape to Σₙ 1 and Πₙ 1, that is suc zero: at level zero only the Δ₀ constructor is available, while the quantifier constructors require 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 Lévy hierarchy is now represented by inductive witnesses. A Δ₀ witness excludes unbounded quantifiers by construction; Σ₁ and Π₁ add a finite block of one polarity; and the mutually defined Σₙ and Πₙ families bound further alternation independently of formula arity. Because each witness exposes the permitted outer shape, later induction arguments can treat bounded, existential, and universal cases separately.