BedrockThe hierarchy, said as a sequence
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 a slot. 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 spoken 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.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Coding.Sequence {ℓ : 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 ( extAt; extAt-out; extAt-in; extAt-in-both; appAt; appAt-adequate ; domAt; domAt-in; domAt-out ) open import L.Coding.Powerset {ℓ} lem using ( DefAt; DefAt-in; DefAt-out ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
What the step at an argument says
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.
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)) ⟩
The step, both ways
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 last 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.
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 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 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))
What it is to be an approximation
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.
private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i) ApproxAt : ∀ {n} → Fin n → Fin n → Formula S n ApproxAt f a = domAt f a ∧̇ ∀̇ (∀̇ ( appAt (sh2 f) (suc zero) zero ⇒̇ StepAt zero (suc zero) (sh2 f) )) module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where ApproxAt-dom : ⟨ γ ⊨ ApproxAt f a ⟩ → (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ fst x ∈ fst (lookup a γ) ⟩ ApproxAt-dom h = domAt-out f a γ (h .fst) ApproxAt-value : ⟨ γ ⊨ ApproxAt f a ⟩ → (x : S) → ⟨ fst x ∈ fst (lookup a γ) ⟩ → ∥ (Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩) ∥₁ ApproxAt-value h = domAt-in f a γ (h .fst) ApproxAt-step : ⟨ γ ⊨ ApproxAt f a ⟩ → (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ (y ∷ x ∷ γ) ⊨ StepAt zero (suc zero) (sh2 f) ⟩ ApproxAt-step h x y p = h .snd x y (subst ⟨_⟩ (sym (appAt-adequate (sh2 f) (suc zero) zero (y ∷ x ∷ γ))) p) ApproxAt-in : ⟨ γ ⊨ domAt f a ⟩ → ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ (y ∷ x ∷ γ) ⊨ StepAt zero (suc zero) (sh2 f) ⟩) → ⟨ γ ⊨ ApproxAt f a ⟩ ApproxAt-in hd hs = hd , λ x y p → hs x y (subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (y ∷ x ∷ γ)) p)
The graph
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.
LsetGraphAt : ∀ {n} → Fin n → Fin n → Formula S n LsetGraphAt y x = ∃̇ (ApproxAt zero (suc x) ∧̇ StepAt (suc y) (suc x) zero) LsetGraph : Formula S 2 LsetGraph = LsetGraphAt zero (suc zero) module _ {n : ℕ} (y x : Fin n) (γ : S ^ n) where GraphOf : Type (ℓ-suc ℓ) GraphOf = Σ[ f ∈ S ] ( ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc x) ⟩ × ⟨ (f ∷ γ) ⊨ StepAt (suc y) (suc x) zero ⟩ ) LsetGraph-in : (f : S) → ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc x) ⟩ → ⟨ (f ∷ γ) ⊨ StepAt (suc y) (suc x) zero ⟩ → ⟨ γ ⊨ LsetGraphAt y x ⟩ LsetGraph-in f ha hs = ∣ f , (ha , hs) ∣₁ LsetGraph-out : ⟨ γ ⊨ LsetGraphAt y x ⟩ → ∥ GraphOf ∥₁ LsetGraph-out h = h
Recap
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 last chapters were written under, that an adequacy is discharged at a variable argument, holds for a statement exactly as it does for a substitution.