A formula for the definable power set

Read this chapter directly, or use the reading guide and dependency map to choose another route.

Reading guide · Dependency map

This chapter combines formula codes with uniform satisfaction to define a first-order predicate for membership in a carrier’s definable power set, and proves that the predicate selects exactly the subsets defined by one-variable formulas.

This is the step the whole route exists for. Every chapter before it built a component at a carrier the caller holds: a set of L, named in a formula as a constant. The internal hierarchy cannot hold its stage that way. Its graph binds the stage, because a graph may not name the object it defines, and a set enters a formula only by being named. So the description of the definable powerset has to be speakable under that binder, with the carrier occupying a slot of the ambient environment and nothing else.

What the description says is what the operator is. u is the definable powerset of the carrier when its members are exactly the sets carved out of the carrier by a formula: there merely is a code c over the carrier and a value v, the value is what the satisfaction recursion records at that code, and u's member is the set of members of the carrier whose one-entry environment lies in v. Three conjuncts, and each is a chapter already delivered, read at a slot rather than at a constant.

One shape correction is forced and it is worth stating before the formula appears. The code and the value are bound by adjacent existentials, with no conjunct between them. Nested through an intervening conjunct the two hypotheses land at different environments, and the route would acquire a weakening lemma it otherwise never needs: the same formula, the same conjunct count, the same depth, and a lemma's worth of difference.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ∃̇_ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; 𝒟ₒ; 𝒟ₒ-intro; 𝒟ₒ-inv )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Axioms.Basic {ℓ} using ( 𝒟ₒ→isL; LsetS )
open import L.Coding.Model {ℓ} using ( domAt-out )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-out; extAt-in; extAt-in-both; tagAtL; tagAtL-adequate )
open import L.Coding.Environment {ℓ} using ( env )
open import L.Coding.FormulaRecovery {ℓ} using ( keyOf; keyOf-fst )
open import L.Coding.CodeSet {ℓ} lem
  using ( keyArityAtL; keyArityAtL-in; keyArityAtL-out; hasWitnessAt
        ; codeS; keyS; witnessAt-in; witnessAt-out )
open import L.Coding.SatisfactionGraph {ℓ} lem
  using ( satGraphAt; GraphWitAt; graphAt-in; graphAt-out
        ; Bi; Ti; Ci; Ei; NN; ev; numν )
open import L.Coding.EnvironmentTower {ℓ} lem using ( module Tower )
open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SlotHolds )
open import L.Coding.SatisfactionTable {ℓ} lem
  using ( keyʟ; slot; satTable; entry-in )
open import L.Coding.SlotClosure {ℓ} lem using ( slotClosed )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst; defSet-Sat )
open import L.Coding.UniformSatisfaction {ℓ} lem using ( keyBridge; fr; frTags; frTow; frDom )

open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_ )

open hPropStructure 𝒮ʟ

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

The environment with one entry

envOne v is the graph assigning the sole free variable to v. The formula envOneAt e y recognizes exactly this graph, with envOneAt-in and envOneAt-out proving both directions.

Definability at arity one asks whether a formula holds of a single member, and the satisfaction recursion answers at environments, so the two are joined by the environment that assigns that member to the only variable there is. An environment is its graph, and a graph of length one is a single pair: the numeral zero with the value.

That makes the reader one line. "The set at this slot has exactly the pairs (0, y) as members" is extAt applied to the tag reader, and the tag reader already delivers the equation between underlying sets, so nothing has to be proved about pairs here at all.

Its two directions are hand-written over the one-element index type, and that is a measurement rather than a taste. Reading a membership in a one-entry set back is a two-case split, one case impossible; through a library round trip between finite functions and vectors the same statement walled a chapter at over eight minutes, and the chapter that met it wrote its two clauses by hand instead. This one does the same.

envOne : V ℓ → V ℓ
envOne y = env {1} (λ _ → y)

envOneAt : ∀ {n} → Fin n → Fin n → Formula S n
envOneAt e y = extAt e (tagAtL zero 0 (suc y))

module _ {n : ℕ} (e y : Fin n) (γ : S ^ n) where
  private
    E : S
    E = lookup e γ

    v : V ℓ
    v = fst (lookup y γ)

    readEntry : (z : S) → ⟨ fst z ∈ envOne v ⟩ → fst z ≡ pr (# 0) v
    readEntry z = PT.rec (setIsSet (fst z) (pr (# 0) v))
      (λ { (lift zero , q) → sym q ; (lift (suc ()) , _) })

    entry∈ : (z : S) → fst z ≡ pr (# 0) v → ⟨ fst z ∈ envOne v ⟩
    entry∈ z q = ∣ lift zero , sym q ∣₁

  envOneAt-in : fst E ≡ envOne v → ⟨ γ ⊨ envOneAt e y ⟩
  envOneAt-in q = extAt-in-both e (tagAtL zero 0 (suc y)) γ fwd bwd
    where
    fwd : (z : S) → ⟨ fst z ∈ fst E ⟩ → ⟨ (z ∷ γ) ⊨ tagAtL zero 0 (suc y) ⟩
    fwd z z∈ = subst ⟨_⟩ (sym (tagAtL-adequate zero 0 (suc y) (z ∷ γ)))
      (readEntry z (subst (λ w → ⟨ fst z ∈ w ⟩) q z∈))

    bwd : (z : S) → ⟨ (z ∷ γ) ⊨ tagAtL zero 0 (suc y) ⟩ → ⟨ fst z ∈ fst E ⟩
    bwd z h = subst (λ w → ⟨ fst z ∈ w ⟩) (sym q)
      (entry∈ z (subst ⟨_⟩ (tagAtL-adequate zero 0 (suc y) (z ∷ γ)) h))

  envOneAt-out : ⟨ γ ⊨ envOneAt e y ⟩ → fst E ≡ envOne v
  envOneAt-out h = extensionalV (λ w → ⇔toPath (sub₁ w) (sub₂ w))
    where
    sub₁ : (w : V ℓ) → ⟨ w ∈ fst E ⟩ → ⟨ w ∈ envOne v ⟩
    sub₁ w w∈ = entry∈ wS (subst ⟨_⟩
        (tagAtL-adequate zero 0 (suc y) (wS ∷ γ))
        (extAt-out e (tagAtL zero 0 (suc y)) γ h wS w∈))
      where
      wS : S
      wS = w , isL-trans {x = fst E} {y = w} w∈ (snd E)

    sub₂ : (w : V ℓ) → ⟨ w ∈ envOne v ⟩ → ⟨ w ∈ fst E ⟩
    sub₂ w = PT.rec (snd (w ∈ fst E))
        (λ { (lift zero , q) →
               subst (λ u → ⟨ u ∈ fst E ⟩) (keyOf-fst 0 (lookup y γ) ∙ q) hasKey
           ; (lift (suc ()) , _) })
      where
      hasKey : ⟨ fst (keyOf 0 (lookup y γ)) ∈ fst E ⟩
      hasKey = extAt-in e (tagAtL zero 0 (suc y)) γ h (keyOf 0 (lookup y γ))
        (subst ⟨_⟩
          (sym (tagAtL-adequate zero 0 (suc y) (keyOf 0 (lookup y γ) ∷ γ)))
          (keyOf-fst 0 (lookup y γ)))

Recognizing the subset defined by a code

DefinesAt x w v says that x contains exactly those elements whose one-entry environments occur in the satisfaction value v attached to code w. Its three reading lemmas expose each direction and their equivalence.

The third conjunct, alone, at three slots: the member, the carrier and the value the satisfaction recursion recorded. It says that the member is the set of those members of the carrier whose one-entry environment lies in that value, which is the definable subset spelled out with the recursion in the place of satisfaction.

The condition is a conjunction rather than one clause because the carrier's bound is not implied by the rest. A member of the recursion's value is an environment, not a set of the carrier, so the second half alone would say nothing about where the member came from; the definable subset is cut out of the carrier and the formula has to say so.

Its two directions are extAt's own two, and the existential inside the condition is read by the previous section. Nothing here inspects the value, which is why this section knows nothing about codes.

DefinesAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
DefinesAt x w v = extAt x ( (var zero ∈̇ var (suc w))
                          ∧̇ ∃̇ ( envOneAt zero (suc zero)
                               ∧̇ (var zero ∈̇ var (suc (suc v))) ) )

module _ {n : ℕ} (x w v : Fin n) (γ : S ^ n) where
  private
    inner : Formula S (suc n)
    inner = ∃̇ (envOneAt zero (suc zero) ∧̇ (var zero ∈̇ var (suc (suc v))))

    body : Formula S (suc n)
    body = (var zero ∈̇ var (suc w)) ∧̇ inner

    Holds : S → Type (ℓ-suc ℓ)
    Holds z = ⟨ fst z ∈ fst (lookup w γ) ⟩
              × ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩

    readInner : (z : S) → ⟨ (z ∷ γ) ⊨ inner ⟩
              → ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩
    readInner z = PT.rec (snd (envOne (fst z) ∈ fst (lookup v γ))) step
      where
      step : Σ[ E ∈ S ] ⟨ (E ∷ z ∷ γ)
               ⊨ (envOneAt zero (suc zero) ∧̇ (var zero ∈̇ var (suc (suc v)))) ⟩
           → ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩
      step (E , (hE , E∈)) = subst (λ u → ⟨ u ∈ fst (lookup v γ) ⟩)
        (envOneAt-out zero (suc zero) (E ∷ z ∷ γ) hE) E∈

    fillInner : (z : S) → ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩
              → ⟨ (z ∷ γ) ⊨ inner ⟩
    fillInner z h =
      ∣ E , (envOneAt-in zero (suc zero) (E ∷ z ∷ γ) refl , h) ∣₁
      where
      E : S
      E = envOne (fst z)
        , isL-trans {x = fst (lookup v γ)} {y = envOne (fst z)} h
            (snd (lookup v γ))

  DefinesAt-out : ⟨ γ ⊨ DefinesAt x w v ⟩
                → (z : S) → ⟨ fst z ∈ fst (lookup x γ) ⟩ → Holds z
  DefinesAt-out h z z∈ = hz .fst , readInner z (hz .snd)
    where
    hz : ⟨ (z ∷ γ) ⊨ body ⟩
    hz = extAt-out x body γ h z z∈

  DefinesAt-in : ⟨ γ ⊨ DefinesAt x w v ⟩
               → (z : S) → Holds z → ⟨ fst z ∈ fst (lookup x γ) ⟩
  DefinesAt-in h z (hw , hv) =
    extAt-in x body γ h z (hw , fillInner z hv)

  DefinesAt-both : ((z : S) → ⟨ fst z ∈ fst (lookup x γ) ⟩ → Holds z)
                 → ((z : S) → Holds z → ⟨ fst z ∈ fst (lookup x γ) ⟩)
                 → ⟨ γ ⊨ DefinesAt x w v ⟩
  DefinesAt-both f g = extAt-in-both x body γ
    (λ z z∈ → f z z∈ .fst , fillInner z (f z z∈ .snd))
    (λ z h → g z (h .fst , readInner z (h .snd)))

Recognizing codes over a variable carrier

isCodeAt c w recognizes when c is the key of a one-variable formula whose constants are members of the carrier at slot w. The introduction and elimination lemmas translate this formula to an explicit coded formula.

Two conjuncts, both already proved, and this is only where they meet: the argument is a key at arity one, and it has a closed, shaped witness at the carrier the slot holds. The first is what tells the decode which arity to answer at; the second is what the decode runs on. Neither names a set, so the pair can be stated under any binder.

The pinned predicate of the code-set chapter is this same pair with one binder on top, and that binder is the only thing separating a predicate a stage can hold from a predicate a bound variable can carry.

isCodeAt : ∀ {n} → Fin n → Fin n → Formula S n
isCodeAt c w = keyArityAtL c 1 ∧̇ hasWitnessAt w c

module _ (A : S) where
  codeAt-in : ∀ {n} (c w : Fin n) (γ : S ^ n)
            → fst (lookup w γ) ≡ fst A
            → (ψ : Formula ⟪ fst A ⟫ 1) → fst (lookup c γ) ≡ fst (keyS A ψ)
            → ⟨ γ ⊨ isCodeAt c w ⟩
  codeAt-in c w γ qw ψ qc =
    keyArityAtL-in c 1 γ (codeS A ψ) qc , witnessAt-in A w c γ ψ qw qc

  codeAt-out : ∀ {n} (c w : Fin n) (γ : S ^ n)
             → fst (lookup w γ) ≡ fst A
             → ⟨ γ ⊨ isCodeAt c w ⟩
             → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ]
                   (fst (lookup c γ) ≡ fst (keyS A ψ))) ∥₁
  codeAt-out c w γ qw (hk , hw) =
    PT.rec squash₁ step (keyArityAtL-out c 1 γ hk)
    where
    step : Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# 1) (fst z))
         → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ]
               (fst (lookup c γ) ≡ fst (keyS A ψ))) ∥₁
    step (z , qz) = witnessAt-out A w c γ qw hw 1 z qz

Satisfaction over a variable carrier

Given a formula over members of the carrier stored at w, graphAt-holds supplies its formula key and uniform satisfaction value in the graph, while graphAt-unique proves that this value is unique.

The satisfaction recursion's graph was generalized to take its carrier as a slot, and its two halves are the existence and uniqueness the recursion was built from, restated at that slot and at a variable environment. Nothing is proved here that was not proved then: existence hands over the subformula slot, the table over it, and the ten clauses, all three of which take the ambient environment as an argument already; uniqueness reads the graph's own bound index set and table back and applies the pinning theorem at the carrier the graph bound.

Both are stated with the code and the value reached by equations rather than named, which is the law the value theorems were written under: naming a key puts its construction inside a satisfaction, and the same statement then costs minutes instead of seconds.

module _ (B : S) where
  private
    toB : ∀ {n} → Formula ⟪ fst B ⟫ n → Formula S n
    toB = mapFo (asConst B)

  graphAt-holds : ∀ {m n} (ψ : Formula ⟪ fst B ⟫ m) (w c v : Fin n) (γ : S ^ n)
                → fst (lookup w γ) ≡ fst B
                → fst (lookup c γ) ≡ fst (keyʟ (toB ψ))
                → fst (lookup v γ) ≡ fst (Sat B (toB ψ))
                → ⟨ γ ⊨ satGraphAt w c v ⟩
  graphAt-holds {m} {n} ψ w c v γ qw qc qv = graphAt-in w c v γ
    ∣ numν
    , (Tower.tower B
    , (slot B φ
    , (satTable B φ
    , (B
    , (sym qw
    , (frTags B φ γ
    , (frTow B φ γ
    , (slotClosed B φ (Tower.tower B ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3
         ∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ γ)
    , (frDom B φ γ
    , (entry
    , SlotHolds.holds B Ti Bi Ci Ei NN (fr B φ γ) refl
        (frTags B φ γ) (frTow B φ γ) ψ refl refl)))))))))) ∣₁
    where
    φ : Formula S m
    φ = toB ψ

    entry : ⟨ pr (fst (lookup c γ)) (fst (lookup v γ)) ∈ fst (satTable B φ) ⟩
    entry = subst2 (λ a b → ⟨ pr a b ∈ fst (satTable B φ) ⟩)
      (sym qc) (sym qv) (entry-in B φ)

  graphAt-unique : ∀ {m n} (ψ : Formula ⟪ fst B ⟫ m) (w c v : Fin n) (γ : S ^ n)
                 → fst (lookup w γ) ≡ fst B
                 → fst (lookup c γ) ≡ fst (keyʟ (toB ψ))
                 → ⟨ γ ⊨ satGraphAt w c v ⟩
                 → fst (lookup v γ) ≡ fst (Sat B (toB ψ))
  graphAt-unique {m} {n} ψ w c v γ qw qc h =
    PT.rec (setIsSet (fst (lookup v γ)) (fst (Sat B (toB ψ)))) step
      (graphAt-out w c v γ h)
    where
    step : GraphWitAt w c v γ → fst (lookup v γ) ≡ fst (Sat B (toB ψ))
    step (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12)))))))))))
      = SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b γ) B (eb ∙ qw) tg hE hc h12
          ψ (subst (λ u → ⟨ u ∈ fst C ⟩) (qc ∙ sym (keyBridge B ψ))
               (domAt-out Ti Ci (ev ν E C T b γ) hd (lookup c γ) (lookup v γ) ha))
          (lookup v γ)
          (subst (λ u → ⟨ pr u (fst (lookup v γ)) ∈ fst T ⟩)
             (qc ∙ sym (keyBridge B ψ)) ha)

The definable-power-set description

DefAt u w says that every member of u is defined over the carrier at w by some one-variable code and its graph value. DefOK records the constructibility condition required to interpret this description for a general carrier.

The three conjuncts, under two adjacent existentials, under one extension: u is the set of exactly those x for which there merely are a code c over the carrier and a value v such that the recursion records v at c and x is what v defines. That is the definable powerset, said in the object language, with the carrier at a slot throughout.

The side condition is about what an object-language quantifier can reach. Every existential in the description ranges over L, so the set the description picks out can only contain constructible sets. If some definable subset of the carrier were not constructible, the description would still be satisfied, by the set of the constructible ones, and it would then hold of something that is not the definable powerset. DefOK is exactly the absence of that gap.

A carrier the caller holds needs no such condition stated, because a caller that holds the carrier holds the theorem about it too. A carrier at a slot is whatever the ambient environment puts there, and no theorem about it is available under the binder, so the fact has to travel as a hypothesis and be discharged where the slot is filled. It is a hypothesis of the elimination only: the introduction is given that u is the definable powerset, and u is an element of L, so its members are constructible already and the condition it would have needed is implied by its own hypothesis.

private
  sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n)))
  sh3 i = suc (suc (suc i))

DefBody : ∀ {n} → Fin n → Formula S (suc (suc (suc n)))
DefBody w = isCodeAt (suc zero) (sh3 w)
            ∧̇ ( satGraphAt (sh3 w) (suc zero) zero
              ∧̇ DefinesAt (suc (suc zero)) (sh3 w) zero )

DefAt : ∀ {n} → Fin n → Fin n → Formula S n
DefAt u w = extAt u (∃̇ (∃̇ (DefBody w)))

DefOK : S → Type (ℓ-suc ℓ)
DefOK A = (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (fst A) ⟩ → ⟨ isL x ⟩

One defining formula in both directions

For a fixed one-variable formula, fill builds witnesses showing that its definable subset satisfies DefAt, and read recovers from such witnesses equality with the corresponding definable subset.

The two halves of the description at a single formula, which is what the adequacy is assembled from. Supplying the three conjuncts for a formula ψ is supplying its key for the code and the recursion's value for the value; reading them back is decoding the code to a formula, pinning the value to the recursion's own, and then reading the third conjunct as a set identity.

Everything here is stated at a variable carrier reached by an equation, and that is what keeps the stage out of the proof. The instantiation at a stage is an equation the caller supplies, and neither Lset nor an ordinal appears anywhere below.

module _ (A : S) where
  private
    module DA = DefOf (fst A)

    toS : Formula ⟪ fst A ⟫ 1 → Formula S 1
    toS ψ = mapFo (asConst A) ψ

    defined-membership : (ψ : Formula ⟪ fst A ⟫ 1) (y : V ℓ)
                       → (y ∈ DA.defSet ψ)
                       ≡ ((y ∈ fst A) ⊓ (envOne y ∈ fst (Sat A (toS ψ))))
    defined-membership ψ y = ⇔toPath out inn
      where
      at : ⟨ y ∈ fst A ⟩ → (y ∈ DA.defSet ψ) ≡ (envOne y ∈ fst (Sat A (toS ψ)))
      at hy = cong (λ u → u ∈ DA.defSet ψ) (sym e)
        ∙ defSet-Sat A ψ m ∙ cong (λ u → envOne u ∈ fst (Sat A (toS ψ))) e
        where
        m = ∈-asFiber {a = y} {b = fst A} hy .fst
        e = ∈-asFiber {a = y} {b = fst A} hy .snd
      out : ⟨ y ∈ DA.defSet ψ ⟩ → ⟨ y ∈ fst A ⟩ × ⟨ envOne y ∈ fst (Sat A (toS ψ)) ⟩
      out h = DA.defSet⊆A ψ y h , subst ⟨_⟩ (at (DA.defSet⊆A ψ y h)) h
      inn : ⟨ y ∈ fst A ⟩ × ⟨ envOne y ∈ fst (Sat A (toS ψ)) ⟩ → ⟨ y ∈ DA.defSet ψ ⟩
      inn (hy , h) = subst ⟨_⟩ (sym (at hy)) h

  fill : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
       → (z : S) (ψ : Formula ⟪ fst A ⟫ 1) → DA.defSet ψ ≡ fst z
       → ⟨ (Sat A (toS ψ) ∷ keyS A ψ ∷ z ∷ γ) ⊨ DefBody w ⟩
  fill {n} w γ qw z ψ qz = hcode , (hgraph , hdef)
    where
    δ : S ^ (suc (suc (suc n)))
    δ = Sat A (toS ψ) ∷ keyS A ψ ∷ z ∷ γ

    hcode : ⟨ δ ⊨ isCodeAt (suc zero) (sh3 w) ⟩
    hcode = codeAt-in A (suc zero) (sh3 w) δ qw ψ refl

    hgraph : ⟨ δ ⊨ satGraphAt (sh3 w) (suc zero) zero ⟩
    hgraph = graphAt-holds A ψ (sh3 w) (suc zero) zero δ qw
               (keyBridge A ψ) refl

    Holds : S → Type (ℓ-suc ℓ)
    Holds y = ⟨ fst y ∈ fst (lookup w γ) ⟩
              × ⟨ envOne (fst y) ∈ fst (Sat A (toS ψ)) ⟩

    agrees : (y : S) → (fst y ∈ fst z)
           ≡ ((fst y ∈ fst (lookup w γ)) ⊓ (envOne (fst y) ∈ fst (Sat A (toS ψ))))
    agrees y = cong (λ X → fst y ∈ X) (sym qz)
      ∙ defined-membership ψ (fst y)
      ∙ cong (λ X → (fst y ∈ X) ⊓ (envOne (fst y) ∈ fst (Sat A (toS ψ)))) (sym qw)

    into : (y : S) → ⟨ fst y ∈ fst z ⟩ → Holds y
    into y = subst ⟨_⟩ (agrees y)

    back : (y : S) → Holds y → ⟨ fst y ∈ fst z ⟩
    back y = subst ⟨_⟩ (sym (agrees y))

    hdef : ⟨ δ ⊨ DefinesAt (suc (suc zero)) (sh3 w) zero ⟩
    hdef = DefinesAt-both (suc (suc zero)) (sh3 w) zero δ into back

  read : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
       → (z c v : S) → ⟨ (v ∷ c ∷ z ∷ γ) ⊨ DefBody w ⟩
       → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁
  read {n} w γ qw z c v (hcode , (hgraph , hdef)) =
    PT.rec squash₁ step (codeAt-out A (suc zero) (sh3 w) δ qw hcode)
    where
    δ : S ^ (suc (suc (suc n)))
    δ = v ∷ c ∷ z ∷ γ

    step : Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (fst c ≡ fst (keyS A ψ))
         → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁
    step (ψ , qc) = ∣ ψ , extensionalV (λ y → ⇔toPath (into y) (back y)) ∣₁
      where
      qv : fst v ≡ fst (Sat A (toS ψ))
      qv = graphAt-unique A ψ (sh3 w) (suc zero) zero δ qw
             (qc ∙ keyBridge A ψ) hgraph

      into : (y : V ℓ) → ⟨ y ∈ DA.defSet ψ ⟩ → ⟨ y ∈ fst z ⟩
      into y hy = DefinesAt-in (suc (suc zero)) (sh3 w) zero δ hdef
        (y , isL-trans (DA.defSet⊆A ψ y hy) (snd A))
        (subst (λ X → ⟨ y ∈ X ⟩) (sym qw) (h .fst)
        , subst (λ X → ⟨ envOne y ∈ X ⟩) (sym qv) (h .snd))
        where h = subst ⟨_⟩ (defined-membership ψ y) hy

      back : (y : V ℓ) → ⟨ y ∈ fst z ⟩ → ⟨ y ∈ DA.defSet ψ ⟩
      back y hy = subst ⟨_⟩ (sym (defined-membership ψ y))
        (subst (λ X → ⟨ y ∈ X ⟩) qw (h .fst)
        , subst (λ X → ⟨ envOne y ∈ X ⟩) qv (h .snd))
        where
        h = DefinesAt-out (suc (suc zero)) (sh3 w) zero δ hdef
          (y , isL-trans hy (snd z)) hy

Reading and assembling the description

The describe argument reads a DefAt witness through its satisfaction value, while assemble starts from an explicit defining formula. Together they prove the introduction and elimination specifications for the complete description.

Assembling and describing are the per-member halves, and the two readings are those under extAt's own two directions. The introduction says that the definable powerset satisfies the description: every member of it is a definable subset, and the three conjuncts are supplied for the formula that defines it. The elimination says that nothing else does, and it is the direction the side condition is for, since a set the description holds of has to be re-entered member by member, and each member either is an element of L or is absent altogether.

  private
    describe : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
             → (z : S) → ⟨ (z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)) ⟩
             → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁
    describe w γ qw z = PT.rec squash₁ viaCode
      where
      Target : Type (ℓ-suc ℓ)
      Target = ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁

      viaValue : (c : S)
               → Σ[ v ∈ S ] ⟨ (v ∷ c ∷ z ∷ γ) ⊨ DefBody w ⟩ → Target
      viaValue c (v , hv) = read w γ qw z c v hv

      viaCode : Σ[ c ∈ S ] ⟨ (c ∷ z ∷ γ) ⊨ ∃̇ (DefBody w) ⟩ → Target
      viaCode (c , hc) = PT.rec squash₁ (viaValue c) hc

    assemble : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
             → (z : S)
             → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁
             → ⟨ (z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)) ⟩
    assemble w γ qw z = PT.rec (snd ((z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)))) step
      where
      step : Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)
           → ⟨ (z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)) ⟩
      step (ψ , qψ) = ∣ keyS A ψ , ∣ Sat A (toS ψ) , fill w γ qw z ψ qψ ∣₁ ∣₁

  DefAt-in : ∀ {n} (u w : Fin n) (γ : S ^ n)
           → fst (lookup w γ) ≡ fst A
           → fst (lookup u γ) ≡ 𝒟ₒ (fst A)
           → ⟨ γ ⊨ DefAt u w ⟩
  DefAt-in {n} u w γ qw qu = extAt-in-both u Φ γ f g
    where
    Φ : Formula S (suc n)
    Φ = ∃̇ (∃̇ (DefBody w))

    f : (z : S) → ⟨ fst z ∈ fst (lookup u γ) ⟩ → ⟨ (z ∷ γ) ⊨ Φ ⟩
    f z z∈ = assemble w γ qw z
      (𝒟ₒ-inv (fst A) (fst z) (subst (λ X → ⟨ fst z ∈ X ⟩) qu z∈))

    g : (z : S) → ⟨ (z ∷ γ) ⊨ Φ ⟩ → ⟨ fst z ∈ fst (lookup u γ) ⟩
    g z hz = subst (λ X → ⟨ fst z ∈ X ⟩) (sym qu)
      (𝒟ₒ-intro (fst A) (fst z) (describe w γ qw z hz))

  DefAt-out : ∀ {n} (u w : Fin n) (γ : S ^ n) → DefOK A
            → fst (lookup w γ) ≡ fst A
            → ⟨ γ ⊨ DefAt u w ⟩
            → fst (lookup u γ) ≡ 𝒟ₒ (fst A)
  DefAt-out {n} u w γ ok qw h =
    extensionalV (λ y → ⇔toPath (sub₁ y) (sub₂ y))
    where
    Φ : Formula S (suc n)
    Φ = ∃̇ (∃̇ (DefBody w))

    sub₁ : (y : V ℓ) → ⟨ y ∈ fst (lookup u γ) ⟩ → ⟨ y ∈ 𝒟ₒ (fst A) ⟩
    sub₁ y y∈ = 𝒟ₒ-intro (fst A) y (describe w γ qw yS (extAt-out u Φ γ h yS y∈))
      where
      yS : S
      yS = y , isL-trans {x = fst (lookup u γ)} {y = y} y∈ (snd (lookup u γ))

    sub₂ : (y : V ℓ) → ⟨ y ∈ 𝒟ₒ (fst A) ⟩ → ⟨ y ∈ fst (lookup u γ) ⟩
    sub₂ y y∈ = extAt-in u Φ γ h yS (assemble w γ qw yS (𝒟ₒ-inv (fst A) y y∈))
      where
      yS : S
      yS = y , ok y y∈

Definable power sets at constructible stages

When the carrier is a constructible stage, its formula codes and uniform satisfaction objects already belong to L, so DefOK is discharged. The resulting specialization says directly that DefAt defines the stage’s definable power set.

The instantiation is just one equation. A stage is an element of L, its definable subsets are constructible because a stage is constructible one stage later, and those two facts are what the successor identity delivers at every stage at once. So the side condition is discharged for good, and what is left is an equivalence of truth values: at a carrier holding a stage, the description holds of a set exactly when that set is the definable powerset of that stage. It holds of 𝒟ₒS and of nothing else.

Neither statement mentions the stage as anything but the value of a slot, which is what the internal hierarchy needs: the description will be spoken under a binder, and the equation the caller supplies is the only thing that connects it to a stage at all.

DefAt-stage : (β : V ℓ) (oβ : IsOrd β) → ∀ {n} (u w : Fin n) (γ : S ^ n)
            → fst (lookup w γ) ≡ Lset β
            → (γ ⊨ DefAt u w)
              ≡ ( (fst (lookup u γ) ≡ 𝒟ₒ (Lset β))
                , setIsSet (fst (lookup u γ)) (𝒟ₒ (Lset β)) )
DefAt-stage β oβ u w γ qw = ⇔toPath
  (DefAt-out (LsetS β oβ) u w γ (𝒟ₒ→isL β oβ) qw)
  (DefAt-in (LsetS β oβ) u w γ qw)

Recap

The chapter has produced a bounded formula whose extension over a constructible stage is exactly the collection of subsets definable over that stage with parameters from it.

DefAt is the definable powerset described in the object language at a carrier that is a slot, and DefAt-in and DefAt-out are its two readings: the operator satisfies the description, and under DefOK nothing else does. DefAt-stage instantiates both readings at a stage, where the side condition is discharged once and for all and the description becomes an equation between truth values.

Three chapters meet here and not one of them is re-proved. The code predicate is read at a slot, the satisfaction graph is read at a slot, and the definable subset is read through the bridge that says the recursion's value is satisfaction over the carrier. What is new is only the joining: envOneAt, one line, because an environment of length one is a single pair, and DefinesAt, which is extAt over a two-part condition.

Two measurements are worth recording. The adjacency correction was adopted before the first line was written and it cost nothing, so no weakening lemma exists anywhere on this route. And the one difficulty met while writing was not in the mathematics at all: the code predicate's elimination at a pinned carrier, with the truncation's payload left to inference, ran past 140 seconds and was terminated there, while the same two lines with the payload type written out check in two seconds. Every PT.rec here names its payload, and that is why this chapter checks in half a minute rather than not at all.