---
title: "A sequence for the constructible hierarchy"
module: L.Coding.HierarchySequence
lang: en
site: "Bedrock"
description: "A sequence for the constructible hierarchy"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 70
canonical: https://bedrock.institute/en/L.Coding.HierarchySequence.html
html: L.Coding.HierarchySequence.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/HierarchySequence.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Model, L.Coding.Expressions, L.Coding.DefinablePowerSet]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.HierarchySequence.md, https://bedrock.institute/ja/L.Coding.HierarchySequence.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# A sequence for the constructible hierarchy

This chapter describes successive definable-power-set stages by a function graph. It characterizes partial approximations to that function and packages the graph used later to recognize initial segments of the constructible hierarchy.

The tower is the one construction on this route that cannot be internalized the
way the satisfaction recursion was. A graph may not name the object it defines,
and the tower at a stage is built out of the tower below that stage, so a graph
written directly for the tower would have to name its own values at
sub-arguments. It has none to name.

What can be said instead is what an **approximation** is. A function `f` is an
approximation to the hierarchy on `a` when it is defined exactly on the members
of `a` and every value it records is the step at that argument computed from `f`
itself. The step consults `f` only below the argument, so the condition never
looks at a value the function does not already record, and the tower's own value
at `a` is then whatever the step from such an `f` yields. That is a sequence
characterization, and it is a first-order sentence about `f` alone.

Every slot in this chapter is represented by a variable. The approximation is
bound by the graph's one existential, the argument and the value are the graph's
two free variables, and nothing anywhere is a named constant, which is what lets
the whole description be stated where the hierarchy needs it: under the binder
that holds the stage. Every reading below is stated at a **variable**
environment, for the reason the last two chapters were: an adequacy discharged at a
concrete environment puts the construction of that environment inside a satisfaction, and
the same statement then costs minutes instead of seconds.

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Coding.HierarchySequence {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; _⇒̇_; ∃̇_; ∀̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ )
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; domAt; domAt-in; domAt-out; prAtL; prAtL-adequate )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-out; extAt-in; extAt-in-both )
open import L.Coding.DefinablePowerSet {ℓ} lem using ( DefAt; DefAt-in; DefAt-out )

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )

open hPropStructure 𝒮ʟ

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
```

## The successor-stage relation

`StepAt v b f` says that `v` is a successor argument in the domain of `f` and that the value of `f` there is the definable power set of its value at the predecessor `b`. `Records`, `StepOf`, and `PowOK` expose the three pieces of this claim.

`v` is the stage at `b`, given the approximation `f` below `b`, when the members
of `v` are exactly the sets lying in the definable powerset of some value `f`
records at some argument in `b`. Three adjacent existentials carry it: the
argument `c`, the value `w` the approximation records there, and the definable
powerset `d` of that value. The powerset has to be **bound**, because the
previous chapter delivers a description of it and not a term for it; `DefAt`
says that `d` is the definable powerset of `w`, so the only way to use it is to
quantify over the thing it describes.

The whole step is **one** `extAt`, and that is a decision rather than a
convenience. A stage is a set, and every clause of a set-valued recursion says
the same thing: this value is the set of exactly those things meeting a
condition. Written as a hand-made pair of inclusions the condition would appear
twice, once under each inclusion, so the three existentials would be duplicated,
every later change to them would have to be made in two places, and each reading
would have to be reassembled from two halves that are not each other's inverse.
`extAt` writes the condition once and hands the two readings back as
projections, which is exactly what it exists for.

One side condition travels with the step, and one hypothesis discharges it in
both directions. To satisfy the description one must produce the definable
powerset **as an element of the model**, since an object-language existential
ranges over `L`; to read the description back one needs the elimination of
`DefAt`, whose side condition is that the definable subsets of the carrier are
constructible. The first implies the second: if `𝒟ₒ w` is an element of `L` then
its members are constructible by transitivity of the class. So both directions
ask for the same thing, `PowOK`, and a consumer at a stage discharges it
with the successor identity.

```agda
private
  sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
  sh4 i = suc (suc (suc (suc i)))

StepBody : ∀ {n} → Fin n → Fin n → Formula S (suc (suc (suc (suc n))))
StepBody b f = (var (suc (suc zero)) ∈̇ var (sh4 b))
             ∧̇ ( appAt (sh4 f) (suc (suc zero)) (suc zero)
               ∧̇ ( DefAt zero (suc zero)
                 ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) )

StepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
StepAt v b f = extAt v (∃̇ (∃̇ (∃̇ (StepBody b f))))

Records : ∀ {n} → Fin n → Fin n → S ^ n → S → S → Type (ℓ-suc ℓ)
Records b f γ c w = ⟨ fst c ∈ fst (lookup b γ) ⟩
                  × ⟨ pr (fst c) (fst w) ∈ fst (lookup f γ) ⟩

StepOf : ∀ {n} → Fin n → Fin n → S ^ n → S → Type (ℓ-suc ℓ)
StepOf b f γ z = Σ[ c ∈ S ] Σ[ w ∈ S ]
                   (Records b f γ c w × ⟨ fst z ∈ 𝒟ₒ (fst w) ⟩)

PowOK : ∀ {n} → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ)
PowOK b f γ = (c w : S) → Records b f γ c w → ⟨ isL (𝒟ₒ (fst w)) ⟩
```

## Reading and constructing a hierarchy step

`StepAt-out` extracts the definable-power-set condition from a satisfied step, and `StepAt-in` constructs satisfaction from that condition together with the required domain data. `StepAt-back` retains the extracted condition in the form used by later proofs.

Reading the body is where the three existentials are spent, and each `PT.rec`
below names the type of its payload. That is the law the Powerset chapter was
written under and it is not a stylistic one: left to inference the payload is a
metavariable standing for the satisfaction of a formula the elaborator has not
committed to, and the same two lines then run past two minutes instead of two
seconds.

Assembling the body is the same three existentials filled in. The definable
powerset is supplied as the element of the model that `PowOK` provides,
its own coding equation is `refl` at that element, and the introduction
of `DefAt` needs nothing else. The readings of the step are then
`extAt`'s directions with those halves plugged in, and there are three of
them rather than two: `StepAt-out` reads a member of the step as a
payload, `StepAt-back` puts a payload back, and `StepAt-in` builds
the step from both directions at once, since a set built by extension has to be
re-entered member by member from both sides. The reading and the assembly of the
body are shared between all three, so each projection is one line.

```agda
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) where
  private
    Φ : Formula S (suc n)
    Φ = ∃̇ (∃̇ (∃̇ (StepBody b f)))

    readBody : PowOK b f γ → (z c w d : S)
             → ⟨ (d ∷ w ∷ c ∷ z ∷ γ) ⊨ StepBody b f ⟩ → StepOf b f γ z
    readBody ok z c w d (hb , (ha , (hd , hz))) =
      c , w , rec , subst (λ X → ⟨ fst z ∈ X ⟩) qd hz
      where
```

Perf: `env` spelled out at both ends; via an abbreviation, 15 s per conversion.

```agda
      rec : Records b f γ c w
      rec = hb , subst ⟨_⟩ (appAt-adequate
        (sh4 f) (suc (suc zero)) (suc zero) (d ∷ w ∷ c ∷ z ∷ γ)) ha

      qd : fst d ≡ 𝒟ₒ (fst w)
      qd = DefAt-out w zero (suc zero) (d ∷ w ∷ c ∷ z ∷ γ)
        (λ x x∈ → isL-trans {x = 𝒟ₒ (fst w)} {y = x} x∈ (ok c w rec)) refl hd

    unfold : PowOK b f γ → (z : S)
           → ⟨ (z ∷ γ) ⊨ Φ ⟩ → ∥ StepOf b f γ z ∥₁
    unfold ok z = PT.rec squash₁ viaArg
      where
      viaPow : (c w : S)
             → Σ[ d ∈ S ] ⟨ (d ∷ w ∷ c ∷ z ∷ γ) ⊨ StepBody b f ⟩
             → ∥ StepOf b f γ z ∥₁
      viaPow c w (d , hd) = ∣ readBody ok z c w d hd ∣₁

      viaVal : (c : S)
             → Σ[ w ∈ S ] ⟨ (w ∷ c ∷ z ∷ γ) ⊨ ∃̇ (StepBody b f) ⟩
             → ∥ StepOf b f γ z ∥₁
      viaVal c (w , hw) = PT.rec squash₁ (viaPow c w) hw

      viaArg : Σ[ c ∈ S ] ⟨ (c ∷ z ∷ γ) ⊨ ∃̇ (∃̇ (StepBody b f)) ⟩
             → ∥ StepOf b f γ z ∥₁
      viaArg (c , hc) = PT.rec squash₁ (viaVal c) hc

    fill : PowOK b f γ → (z : S) → StepOf b f γ z → ⟨ (z ∷ γ) ⊨ Φ ⟩
    fill ok z (c , (w , (rec , hz))) =
      ∣ c , ∣ w , ∣ D , (rec .fst , (ha , (hdef , hz))) ∣₁ ∣₁ ∣₁
      where
```

Perf: `env` spelled out at both ends; via an abbreviation, 15 s per conversion.

```agda
      D : S
      D = 𝒟ₒ (fst w) , ok c w rec

      ha : ⟨ (D ∷ w ∷ c ∷ z ∷ γ) ⊨ appAt (sh4 f) (suc (suc zero)) (suc zero) ⟩
      ha = subst ⟨_⟩ (sym (appAt-adequate
        (sh4 f) (suc (suc zero)) (suc zero) (D ∷ w ∷ c ∷ z ∷ γ))) (rec .snd)

      hdef : ⟨ (D ∷ w ∷ c ∷ z ∷ γ) ⊨ DefAt zero (suc zero) ⟩
      hdef = DefAt-in w zero (suc zero) (D ∷ w ∷ c ∷ z ∷ γ) refl refl

  StepAt-out : ⟨ γ ⊨ StepAt v b f ⟩ → PowOK b f γ
             → (z : S) → ⟨ fst z ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ z ∥₁
  StepAt-out h ok z z∈ = unfold ok z (extAt-out v Φ γ h z z∈)

  StepAt-back : ⟨ γ ⊨ StepAt v b f ⟩ → PowOK b f γ
              → (z : S) → StepOf b f γ z → ⟨ fst z ∈ fst (lookup v γ) ⟩
  StepAt-back h ok z s = extAt-in v Φ γ h z (fill ok z s)

  StepAt-in : PowOK b f γ
            → ((z : S) → ⟨ fst z ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ z ∥₁)
            → ((z : S) → StepOf b f γ z → ⟨ fst z ∈ fst (lookup v γ) ⟩)
            → ⟨ γ ⊨ StepAt v b f ⟩
  StepAt-in ok into back = extAt-in-both v Φ γ
    (λ z z∈ → PT.rec (snd ((z ∷ γ) ⊨ Φ)) (fill ok z) (into z z∈))
    (λ z h → PT.rec (snd (fst z ∈ fst (lookup v γ))) (back z) (unfold ok z h))
```

## Approximations to the hierarchy sequence

`ApproxAt f a` describes a function with ordinal domain `a`, the prescribed initial value, and every successor value related by `StepAt`. `GraphAt` existentially packages such a function, while its reading lemmas expose the domain, values, and step equations.

Two conjuncts, and there is no third. `f` is defined on `a`, and every value `f`
records is the step at that argument from `f` itself. The second conjunct needs
no guard saying the argument lies in `a`: the first conjunct already pins the
domain to `a` in both directions, so an argument at which anything is recorded
is a member of `a` and saying so again would only lengthen the sentence.

The pair is a membership **equivalence**, and that matters more than it looks.
Stated the other way, as "for each argument in `a` there merely is a value which
is the step there", the sentence permits `f` to hold junk pairs beside the right
ones, so it does not determine `f`, the existence claim is not a proposition,
and an induction against it needs an internal function-extensionality lemma to
get from two approximations to one. As an equivalence the motive is a
proposition and that lemma never has to be written.

There is deliberately **no single-valuedness conjunct**. It would assert nothing
the second conjunct does not already give: if two values are recorded at one
argument then both are the step at that argument, the step is a set identity,
and two sets with the same members are equal. Carrying it would put three
universal quantifiers under a satisfaction in exchange for a corollary.

The three projections are the three questions a consumer asks: an argument with
an entry is in the domain, an argument in the domain has an entry, and a
recorded value is a step. The introduction is here rather than at the call site
for the reason every reading is: it discharges an adequacy, and it must do so
at a variable environment.

```agda
private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

module RecShape (Step : ∀ {n} → Fin n → Fin n → Fin n → Formula S n) where

  Domain₀ : S → V ℓ → Type (ℓ-suc ℓ)
  Domain₀ h B = (c z : S) → ⟨ pr (fst c) (fst z) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩

  ApproxAt : ∀ {n} → Fin n → Fin n → Formula S n
  ApproxAt f a = domAt f a
               ∧̇ ∀̇ (∀̇ ( appAt (sh2 f) (suc zero) zero
                       ⇒̇ Step zero (suc zero) (sh2 f) ))

  GraphAt : ∀ {n} → Fin n → Fin n → Formula S n
  GraphAt w b = ∃̇ (ApproxAt zero (suc b) ∧̇ Step (suc w) (suc b) zero)

  module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where
    ApproxAt-dom : ⟨ γ ⊨ ApproxAt f a ⟩ → Domain₀ (lookup f γ) (fst (lookup a γ))
    ApproxAt-dom h = domAt-out f a γ (h .fst)

    ApproxAt-value : ⟨ γ ⊨ ApproxAt f a ⟩ → (c : S)
                   → ⟨ fst c ∈ fst (lookup a γ) ⟩
                   → ∥ (Σ[ z ∈ S ] ⟨ pr (fst c) (fst z) ∈ fst (lookup f γ) ⟩) ∥₁
    ApproxAt-value h = domAt-in f a γ (h .fst)

    ApproxAt-step : ⟨ γ ⊨ ApproxAt f a ⟩ → (c z : S)
                  → ⟨ pr (fst c) (fst z) ∈ fst (lookup f γ) ⟩
                  → ⟨ (z ∷ c ∷ γ) ⊨ Step zero (suc zero) (sh2 f) ⟩
    ApproxAt-step h c z p = h .snd c z
      (subst ⟨_⟩ (sym (appAt-adequate (sh2 f) (suc zero) zero (z ∷ c ∷ γ))) p)

    ApproxAt-in : ⟨ γ ⊨ domAt f a ⟩
                → ((c z : S) → ⟨ pr (fst c) (fst z) ∈ fst (lookup f γ) ⟩
                   → ⟨ (z ∷ c ∷ γ) ⊨ Step zero (suc zero) (sh2 f) ⟩)
                → ⟨ γ ⊨ ApproxAt f a ⟩
    ApproxAt-in hd hs = hd , λ c z p → hs c z
      (subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (z ∷ c ∷ γ)) p)

  module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
    GraphOf : Type (ℓ-suc ℓ)
    GraphOf = Σ[ f ∈ S ] ( ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
                         × ⟨ (f ∷ γ) ⊨ Step (suc w) (suc b) zero ⟩ )

    Graph-in : (f : S) → ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
             → ⟨ (f ∷ γ) ⊨ Step (suc w) (suc b) zero ⟩ → ⟨ γ ⊨ GraphAt w b ⟩
    Graph-in f ha hs = ∣ f , (ha , hs) ∣₁

    Graph-out : ⟨ γ ⊨ GraphAt w b ⟩ → ∥ GraphOf ∥₁
    Graph-out h = h

  PairGraphAt : ∀ {n} → Fin n → Fin n → Formula S n
  PairGraphAt e c = ∃̇ (prAtL (suc e) (suc c) zero ∧̇ GraphAt zero (suc c))

  module _ {n : ℕ} (e c : Fin n) (γ : S ^ n)
           (φ : Formula S n) (qφ : φ ≡ PairGraphAt e c) where
    PairOf : Type (ℓ-suc ℓ)
    PairOf = Σ[ z ∈ S ] ( (fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst z))
                        × ⟨ (z ∷ γ) ⊨ GraphAt zero (suc c) ⟩ )

    PairGraph-in : (z : S) → fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst z)
                 → ⟨ (z ∷ γ) ⊨ GraphAt zero (suc c) ⟩ → ⟨ γ ⊨ φ ⟩
    PairGraph-in z q hg = subst (λ ψ → ⟨ γ ⊨ ψ ⟩) (sym qφ)
      ∣ z , (subst ⟨_⟩
        (sym (prAtL-adequate (suc e) (suc c) zero (z ∷ γ))) q , hg) ∣₁

    PairGraph-out : ⟨ γ ⊨ φ ⟩ → ∥ PairOf ∥₁
    PairGraph-out h = PT.map
      (λ { (z , (hq , hg)) →
        z , (subst ⟨_⟩ (prAtL-adequate (suc e) (suc c) zero (z ∷ γ)) hq , hg) })
      (subst (λ ψ → ⟨ γ ⊨ ψ ⟩) qφ h)

open RecShape StepAt public renaming ( GraphAt to LsetGraphAt
                                     ; Graph-in to LsetGraph-in
                                     ; Graph-out to LsetGraph-out )
```

## The graph of a hierarchy approximation

`PairGraphAt` recognizes a pair of an ordinal argument and the value assigned by an approximation. The final graph formula collects exactly these pairs, turning the pointwise approximation into a set that represents the hierarchy sequence.

One existential over the approximation, and under it the two conjuncts the
chapter was written for: `f` is an approximation on the argument, and the value
is the step at that argument from `f`. The value stands at the first slot and
the argument at the second, which is the order the model's replacement field
reads a graph in, and `LsetGraph` is the sentence with those two slots
filled in.

The approximation is bound, and it has to be. A graph may not name the object it
defines, and it may assert the existence of something only when that something
is already known to be an element of `L`, since satisfaction is read at the
model. An approximation is such a thing: it is a set of pairs collected by
replacement from arguments below, not the tower it is used to describe. The
consumer supplies one; the graph merely says there merely is one.

Both readings are one line each, because a satisfied existential **is** a
truncated sigma and a satisfied conjunction **is** a pair. What they buy is not
proof, it is the name and the slot. `GraphOf` writes the payload type out
rather than leaving it to inference, and both readings stand at **variable**
slots in a variable environment, so a consumer instantiates them rather than
converting against them.

The naming is the whole cost of this section, and the figure is worth keeping
because the first diagnosis of it was wrong. Stated with the graph named by its
closed-sentence alias, the same two lines took 98 seconds of the chapter's 130.
The slots were blamed and they are innocent: an isolating measurement in the next
chapter puts a reading at fully concrete slots at fifteen milliseconds and the
same reading against an alias at fifty-one seconds. What costs is deciding a
satisfaction of the alias against a satisfaction of its expansion, which Agda
settles by normalizing a satisfaction that carries the entire
definable-powerset description inside it. Generic in the slots the readings never
meet that question, and the closed sentence is one unfolding away,
and the concrete sentence is one unfolding away.

## Recap

The resulting set-coded graph records the successive constructible stages up to an ordinal bound, with the step relation already expressed by the definable-power-set formula needed for later internal descriptions.

`LsetGraph` is the object-language sentence "the value is the stage at
the argument", written without naming a stage, a tower, or an ordinal.
`StepAt` is one `extAt` over three adjacent existentials, the
argument, the value recorded there and its definable powerset;
`ApproxAt` is two conjuncts, the domain and the step condition, and no
more.

Nothing here is proved twice. The definable powerset arrives from the previous
chapter as a description at a slot and is used exactly as it was delivered, the
function machinery is read off `appAt` and `domAt`, and the step's
two readings are `extAt`'s own two. What the chapter contributes is the
shape: a graph that consults an approximation rather than the tower, which is
the only shape a graph is allowed to have.

Two rulings are recorded where a reader meets them. The step is a membership
equivalence rather than a one-directional collection, which keeps the motive of
the induction to come a proposition and removes an internal
function-extensionality lemma from the route entirely. And there is no
single-valuedness conjunct, because the step condition already pins every value
recorded at an argument, so single-valuedness is a corollary and not a
hypothesis.

One measurement, and the chapter after this one corrected its diagnosis. Every
second this chapter ever cost was a conversion between two spellings of the same
thing, and every time Agda answered it by normalizing a satisfaction with the
whole definable-powerset description inside: 98 seconds for two readings taken
against the graph's closed-sentence alias, and 15 seconds at each place where a
hypothesis carried an environment written out while the application named it
behind an abbreviation. Concrete slots are not the mechanism and cost nothing.
Written so that the two sides are the same expression, the chapter checks in
under two seconds rather than 130, with no change to the mathematics. The law
the preceding coding chapters were written under, that an adequacy is discharged at a
variable argument, holds for a **statement** exactly as it does for a
substitution.