---
title: "The Lévy hierarchy"
module: FOL.LevyHierarchy
lang: en
site: "Bedrock"
description: "The Lévy hierarchy"
stage: "First-order logic"
reading_order: 9
canonical: https://bedrock.institute/en/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/zh/FOL.LevyHierarchy.md, https://bedrock.institute/ja/FOL.LevyHierarchy.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

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

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.

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

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

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.

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

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.

```agda
δ-¬ 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.

```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 ψ
```

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.

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

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

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.

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

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.

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

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.

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

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

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

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

`Πₙ` 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`.

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

## 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.