BedrockSatisfaction over the whole code set
The instance of the previous chapter is indexed by slot B φ, the keys of one formula and its subformulas. Nothing downstream can use it. A consumer arrives holding a code, not the formula the code came from: the internal definable powerset ranges over the codes of arity one at a stage, and the well-order compares two codes that are subcodes of no common formula. Indexed by one formula's slot there is a table per formula, and "what does the table say at this code" has no answer until someone produces a formula the code is a subcode of.
The domain that answers is the code set at a stage, and the previous goal built it. AllCodes holds the keys of the formulas over the carrier at every arity, which is exactly what a consumer arrives holding.
Closedness of the whole code set is not what discharges the graph's demand on an index set, and it is worth saying so, because that theorem is what the previous goal was registered for. The graph binds its table and its index set existentially, so funct owes only some qualifying set containing the member, and the smallest one is the member's own formula's slot, closed by the chapter that built it. Nothing anywhere consumed it, and it has since been retired.
What the change costs is the whole content of this chapter, and it is almost nothing, for a reason worth stating before any of it. The graph binds its table existentially. So funct at a member does not have to exhibit a table over the whole domain; it has to exhibit some closed, total, clause-satisfying table holding that member, and the smallest such table is the subformula slot of the member's own formula, which four earlier chapters already built and certified. The recursion changes its domain and nothing else changes:
Table, Slot, Sound and Unique are untouched statement for statement, and the per-formula instance keeps working beside this one.
One thing here is genuinely new, and it is not about recursion at all. The code set's members are keys taken in the hierarchy's coding over the stage's own alphabet; everything the recursion speaks is keys taken in the model's coding over the model's language. Those are the same construction at two alphabets, and no theorem connected them.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Coding.Uniform {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula ) open import FOL.Manipulation.Relabelling using ( mapFo; mapFo-comp; ⊨-map ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; module VCode ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Definability {ℓ} using ( module DefOf ) open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst ) open import L.Coding.Model {ℓ} using ( module LCode; prʟ-fst; codeBridge; domAt; domAt-intro; domAt-out ) open import L.Coding.EnvSet {ℓ} lem using ( envS ) open import L.Coding.Sat {ℓ} lem using ( Sat ) open import L.Coding.Bridge {ℓ} lem using ( intoL; asConst; Sat-spec; defSet-Sat ) renaming ( graph to envGraph ) open import L.Coding.Table {ℓ} lem using ( keyʟ; slot; satTable; total; inSlot; entry-in ) open import L.Coding.Slot {ℓ} lem using ( slotClosed ) open import L.Coding.Sound {ℓ} lem using ( soundness ) open import L.Coding.Unique {ℓ} lem using ( module Good ) open import L.Coding.Graph {ℓ} lem using ( satGraph; graph-in; graph-out ) open import L.Coding.CodeSet {ℓ} lem using ( keyS; AllCodes; AllCodes-out; key∈AllCodes ) open import L.Recursion {ℓ} lem using ( Recursion; mereFunct; module Of ) open import Cubical.Data.Sigma using ( Σ≡Prop ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_ ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
A member, named
Three lines, and they are the chapter's one performance decision. A consumer that wants the value at a particular formula has to name the member the value is taken at, and the obvious name is the key itself; naming it that way does not elaborate, because the key unfolds into a pair of a numeral with a code and that construction then sits inside the recursion's domain and inside a satisfaction.
So the name is sealed where it is made. Sealed, it is an element of L that a type can mention without unfolding, and the two facts a consumer needs come out with it: it lies in the domain, and it is the key of the formula it was made from. Everything below is stated at a variable member and reaches its key by an equation, so the seal is the only thing that has to be opened, and nothing opens it.
module _ (A : S) where opaque keyIn : ∀ {n} → Formula ⟪ fst A ⟫ n → S keyIn ψ = keyS A ψ keyIn≡ : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n) → fst (keyIn ψ) ≡ fst (keyS A ψ) keyIn≡ ψ = refl keyIn∈ : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n) → ⟨ keyIn ψ ∈ˢ AllCodes A ⟩ keyIn∈ ψ = key∈AllCodes A ψ
The two codings meet
A key in the hierarchy's coding is the arity numeral paired with the code of the formula relabelled along the alphabet's embedding; a key in the model's coding is the numeral of L paired with the code taken in L. codeBridge equates the two codes, one clause per constructor. It was written in the model chapter and has had no consumer since, because this is the statement it was written for.
What it does not supply is the relabelling. The set's formulas are over the alphabet ⟪ A ⟫ and the recursion's formulas are over L, so the two sides pass through two different maps and their composite has to be recognized as one map. That is functoriality of relabelling, which belongs where relabelling is defined and is now there, so the whole bridge is four rewrites and no induction.
The map into the model is not built here either. It is the bridge chapter's own
asConst, the alphabet's embedding followed by the class inclusion, and taking that one rather than an equal one is what lets the last section quote the adequacy without a translation step.
The bridge takes the alphabet and nothing else. The set the environments range over never appears in it, so it is stated one parameter short of the recursion below, and a later chapter that needs the two codings to agree at a carrier held in a slot can use it without supplying a second carrier it does not have.
module _ (A : S) where keyBridge : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n) → fst (keyS A ψ) ≡ fst (keyʟ (mapFo (asConst A) ψ)) keyBridge {n} ψ = cong (pr (# n)) ( cong (λ χ → VCode.⌜ χ ⌝) (sym (mapFo-comp (asConst A) fst ψ)) ∙ sym (codeBridge (mapFo (asConst A) ψ)) ) ∙ cong (λ w → pr w (fst LCode.⌜ mapFo (asConst A) ψ ⌝)) (sym (numeralL-fst n)) ∙ sym (prʟ-fst (numeralL n) LCode.⌜ mapFo (asConst A) ψ ⌝) module _ (A B : S) where private toS : ∀ {n} → Formula ⟪ fst A ⟫ n → Formula S n toS = mapFo (asConst A)
Both halves, at the formula the code names
Both are the previous chapters', applied at the formula the member is the key of rather than at an ambient formula, and the change makes existence shorter. The per-formula instance had to transport a subformula's entry along the inclusion of its own subtree into the ambient table; here the recovered formula is the formula whose table is being handed over, so entry-in applies directly and the transport is gone.
Uniqueness does not notice the change at all, and the reason is structural.
Pinned speaks about the index set and the table the graph produced, which are bound variables of the caller's environment, never about the recursion's domain. The domain occurs nowhere in it, nor in the twelve clauses, so changing what the recursion is indexed by cannot reach uniqueness.
Only the totality hypothesis is written out here, and its environment is written out with it. Left to inference, the graph's three existentially bound slots determine nothing and six metavariables survive; naming the environment costs one line and is the difference between elaborating and not.
Ci Ti : Fin 5 Ci = suc (suc zero) Ti = suc zero hdom : ∀ {n} (φ : Formula S n) (x y : S) → ⟨ (B ∷ satTable B φ ∷ slot B φ ∷ y ∷ x ∷ []) ⊨ domAt Ti Ci ⟩ hdom φ x y = domAt-intro Ti Ci (B ∷ satTable B φ ∷ slot B φ ∷ y ∷ x ∷ []) (λ z → (λ h → PT.rec (snd (fst z ∈ fst (slot B φ))) (λ { (w , hw) → inSlot B φ (fst z) (fst w) hw }) h) , (λ h → total B φ (fst z) h)) exists : ∀ {n} (φ : Formula S n) (x : S) → fst x ≡ fst (keyʟ φ) → ⟨ (Sat B φ ∷ x ∷ []) ⊨ satGraph B ⟩ exists φ x k = graph-in B x (Sat B φ) ∣ slot B φ , (satTable B φ , (B , (refl , ( slotClosed B φ (Sat B φ ∷ x ∷ []) , ( hdom φ x (Sat B φ) , ( subst (λ w → ⟨ pr w (fst (Sat B φ)) ∈ fst (satTable B φ) ⟩) (sym k) (entry-in B φ) , soundness B φ (Sat B φ ∷ x ∷ []) )))))) ∣₁ unique : ∀ {n} (φ : Formula S n) (x : S) → fst x ≡ fst (keyʟ φ) → (y : S) → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩ → y ≡ Sat B φ unique φ x k y hy = Σ≡Prop (λ v → snd (isL v)) (PT.rec (setIsSet (fst y) (fst (Sat B φ))) (λ { (C , (T , (b , (eb , (hc , (hd , (ha , h12))))))) → Good.pinned (b ∷ T ∷ C ∷ y ∷ x ∷ []) Ci Ti zero hc hd h12 φ x y k (domAt-out Ti Ci (b ∷ T ∷ C ∷ y ∷ x ∷ []) hd x y ha) ha ∙ cong (λ w → fst (Sat w φ)) (Σ≡Prop (λ v → snd (isL v)) eb) }) (graph-out B x y hy))
The instance
The domain is the code set at the stage, the graph is the one two chapters back, and funct is filled through mereFunct, because a merely existing unique solution is a contractible one. A member arrives as a mere key of a formula over the alphabet, the bridge turns its equation into one about the model's key, and the two halves above are applied at that key.
The two carriers are independent parameters and stay so. A is the alphabet the codes' constants are drawn from; B is the set the environments range over; nothing in the recursion relates them, and charging the recursion for a relation it does not use would be stating a weaker theorem. They are pinned together in the next section, and only there, because that is where satisfaction acquires a meaning.
satRec : Recursion Recursion.dom satRec = AllCodes A Recursion.graph satRec = satGraph B Recursion.funct satRec x x∈ = mereFunct (satGraph B) x (PT.map (λ { (n , ψ , q) → Sat B (toS ψ) , ( exists (toS ψ) x (q ∙ keyBridge A ψ) , unique (toS ψ) x (q ∙ keyBridge A ψ) ) }) (AllCodes-out A x x∈)) module Table = Of satRec
What the value is
A recursion connected to nothing defines nothing, so the value is stated twice.
Against the recursion's own construction first, and that is uniqueness spent in the other direction: the value at a member that is the key of a formula is the set the meta-level recursion built at that formula, because the existence half exhibits that set as a solution and the recursion's value is the only solution. This is the reading a consumer needs to get anything out of the table at all, since the value function comes from a contractibility and computes to nothing on its own.
The member is a variable and its key is reached by an equation, and that is a measurement, not a taste. Stated at the key itself, the value function's argument is a concrete code construction, which puts that construction inside the graph satisfaction the value is defined from; the statement that costs four seconds at a variable ran past six minutes at the key and was abandoned, and so did the same statement written as a corollary of the variable one, which shows the cost is in the statement and not in the proof. The uniqueness chapter recorded this law at its first case and it holds here unchanged.
Nothing is lost, in either direction. A consumer holding a member holds it as a member, with its key equation beside it; and a consumer that wants to name the member gets the convenient form back through the sealed name, at no cost, because what the type mentions there does not unfold.
val-at : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n) (x : S) (x∈ : ⟨ x ∈ˢ AllCodes A ⟩) → fst x ≡ fst (keyS A ψ) → Table.val x x∈ ≡ Sat B (toS ψ) val-at ψ x x∈ q = Table.val-uniq x x∈ (Sat B (toS ψ)) (exists (toS ψ) x (q ∙ keyBridge A ψ)) val-key : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n) → Table.val (keyIn A ψ) (keyIn∈ A ψ) ≡ Sat B (toS ψ) val-key ψ = val-at ψ (keyIn A ψ) (keyIn∈ A ψ) (keyIn≡ A ψ)
And against satisfaction, which is the reason to have the goal. The bridge chapter proved that a member of the meta-level value is an environment satisfying the formula in the world (B, ∈); composing it with the reading above says the same of the table this recursion produces. At arity one it specializes to the definable subset the definable powerset means, so the table read at a member that is the key of a formula is that formula's definable subset, which is the statement the internal hierarchy will read Def off.
The two carriers meet here because this is where they have to. A formula whose constants are members of the carrier is one the inner world can read; a formula naming an arbitrary element of L is not, and the bridge chapter says so about itself. So the two theorems below are stated at the one carrier, which is the instantiation the consumer wants anyway: the codes at a stage, satisfied over that same stage.
module _ (A : S) where module DA = DefOf (fst A) open DA using ( _⊨ᵐ_ ) val-sat : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n) (x : S) (x∈ : ⟨ x ∈ˢ AllCodes A ⟩) → fst x ≡ fst (keyS A ψ) → (δ : DA.SM ^ n) (z : S) → fst z ≡ envGraph A δ → (z ∈ˢ Table.val A A x x∈) ≡ (δ ⊨ᵐ ψ) val-sat ψ x x∈ q δ z qz = cong (z ∈ˢ_) (val-at A A ψ x x∈ q ∙ cong (Sat A) (sym (mapFo-comp DA.ι (intoL A) ψ))) ∙ Sat-spec A (mapFo DA.ι ψ) δ z qz ∙ ⊨-map (hPropAlgebra (ℓ-suc ℓ)) DA.𝒮M DA.ι id ψ δ val-defSet : (ψ : Formula ⟪ fst A ⟫ 1) (m : ⟪ fst A ⟫) (x : S) (x∈ : ⟨ x ∈ˢ AllCodes A ⟩) → fst x ≡ fst (keyS A ψ) → (⟪ fst A ⟫↪ m ∈ DA.defSet ψ) ≡ (envS A (λ _ → m) ∈ˢ Table.val A A x x∈) val-defSet ψ m x x∈ q = defSet-Sat A ψ m ∙ cong (envS A (λ _ → m) ∈ˢ_) (sym (val-at A A ψ x x∈ q))
Recap
satRec is satisfaction as an internalized recursion over the codes at a stage, not over one formula's subformulas, and Table is the table it yields. val-at reads a value out at a member given as a key, with
val-key the same reading at the sealed name of a formula's own key;
val-sat says that value is satisfaction over the carrier; and
val-defSet spends both on the definable powerset at arity one, which is the form the internal hierarchy consumes.
Nothing below was re-indexed and nothing was weakened. The registered risk for this goal was that the domain or its well-formedness predicate would need the carrier as a constant somewhere it cannot be a slot, which would have re-indexed the slot, the table, totality and membership at a pair of a carrier and a key, and charged the two halves a transport for each of their twelve cases. It did not fire, and the direct evidence is that slot, satTable,
total, inSlot, slotClosed, soundness and
Good.pinned are all applied above at their existing types. The code carrier never reaches the graph: it is bound and pinned inside the code set's own predicate, and what comes out is an element of L, which is all a domain is.
What made this cheap is the existential in the graph, and it is worth keeping as a design fact rather than an accident. A graph that quantifies its table existentially lets a value be justified by any admissible table, so an instance may answer at each index with the smallest table that reaches it. Had the graph named its table, the domain and the table would have had to grow together and every earlier chapter would have moved.
The one cost that was not predicted is in the statements, not in the proofs, and it is the chapter's measurement. A value read at a key written out does not elaborate, at any length of proof, because the key's construction lands inside a satisfaction; the reading that costs four seconds at a variable member ran past six minutes at the key, and so did the same statement written as a corollary of the variable one. Two things fix it and they are the two recorded laws, one each: every reading takes the member as a variable and reaches its key by an equation, and the name a consumer would write instead is sealed where it is built. The first is the uniqueness chapter's law, met again where nothing is being proved by induction; the second is the law about a construction appearing in a goal, met at a goal that is a plain equation.