--- title: "The set of all formula codes" module: L.Coding.CodeSet lang: en site: "Bedrock" description: "The set of all formula codes" stage: "Internal coding: tables and uniform satisfaction" reading_order: 61 canonical: https://bedrock.institute/en/L.Coding.CodeSet.html html: L.Coding.CodeSet.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/CodeSet.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, V.Coding, L.Constructible, L.Recursion, L.Axioms.Full, L.Axioms.Numerals, L.Axioms.Infinity, L.Coding.Model, L.Coding.Expressions, L.Coding.Closure, L.Coding.CodeConstructibility, L.Coding.SubformulaClosure, L.Coding.CodeShape, L.Coding.FormulaRecovery] routes: [internal-satisfaction] translations: [https://bedrock.institute/zh/L.Coding.CodeSet.md, https://bedrock.institute/ja/L.Coding.CodeSet.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # The set of all formula codes Using the closed code domain, this chapter separates one constructible set containing exactly the formula codes, across all arities, that carry the required shape and closure witnesses. Its membership theorems move between a code, its arity numeral, and the decoded formula. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Coding.CodeSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ∃̇_ ) open import FOL.Manipulation.ConstantMapping using ( mapFo ) import FOL.Absoluteness import FOL.ZFModel open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; module VCode ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Recursion {ℓ} lem using ( smallDom ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst ) open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL ) open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate ) open import L.Coding.Expressions {ℓ} using ( tagAtL; tagAtL-adequate ) open import L.Coding.Closure {ℓ} using ( closedAt ) open import L.Coding.CodeConstructibility {ℓ} using ( key; keyL; codeL; key∈closure ) open import L.Coding.SubformulaClosure {ℓ} using ( clo; closureClosed ) open import L.Coding.CodeShape {ℓ} using ( shapedAt; closureShaped ) open import L.Coding.FormulaRecovery {ℓ} using ( keyOf-fst; module Decode ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_; ∈-asFiber ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_ ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open hPropStructure 𝒮ʟ module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) ``` ## Is a key at a stated arity One reader, and it is the only new piece of object language the chapter needs. A key at arity `k` is a pair whose first component is the numeral `k`, and the tag reader already says exactly that of a *named* second component. What is wanted here is the second component left unnamed, so the reader is the tag reader under one existential, and its two directions are the existential's two directions with the tag reader's adequacy equation discharged inside. The equation is discharged with the index, the numeral and the environment all still variables; keeping them as variables is what avoids the extra conversion-checking overhead that later instantiation would otherwise incur. ```agda keyArityAtL : ∀ {n} → Fin n → ℕ → Formula S n keyArityAtL c k = ∃̇ (tagAtL (suc c) k zero) keyArityAtL-out : ∀ {n} (c : Fin n) (k : ℕ) (γ : S ^ n) → ⟨ γ ⊨ keyArityAtL c k ⟩ → ∥ (Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# k) (fst z))) ∥₁ keyArityAtL-out c k γ = PT.map (λ { (z , hz) → z , subst ⟨_⟩ (tagAtL-adequate (suc c) k zero (z ∷ γ)) hz }) keyArityAtL-in : ∀ {n} (c : Fin n) (k : ℕ) (γ : S ^ n) (z : S) → fst (lookup c γ) ≡ pr (# k) (fst z) → ⟨ γ ⊨ keyArityAtL c k ⟩ keyArityAtL-in c k γ z e = ∣ z , subst ⟨_⟩ (sym (tagAtL-adequate (suc c) k zero (z ∷ γ))) e ∣₁ ``` ## Is a key at some arity The reader above names its arity as a metalevel numeral, which is what pins the arity to one; a set that has to hold subcodes cannot do that, because a quantifier's subformula lives one arity up. So the arity has to become a bound set, and something has to say of that set what `# k` gives directly: that it is a numeral. Stating it takes one constant. `ωʟ` is an element of `L` whose members are exactly the numerals, so "the arity component lies in `ωʟ`" *is* the condition, written with the same unbounded membership the second conjunct already uses. The whole formula has two existentials, one for the arity and one for the payload, the pair reader between them, and the membership on the arity. Reading it in the other direction is where the choice takes effect. `ω-specL` is an equation between propositions, not an implication, so a member of `ωʟ` *is* a truncated natural number, and one composition with the chain's projection equation turns it into the metalevel `# m` that `recover` takes as its arity argument. Neither direction needs induction; the numeral chapter already did that work. ```agda arityNumAtL : ∀ {n} → Fin n → Formula S n arityNumAtL c = ∃̇ (∃̇ (prAtL (suc (suc c)) (suc zero) zero ∧̇ (var (suc zero) ∈̇ con ωʟ))) arityNumAtL-out : ∀ {n} (c : Fin n) (γ : S ^ n) → ⟨ γ ⊨ arityNumAtL c ⟩ → ∥ (Σ[ m ∈ ℕ ] Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# m) (fst z))) ∥₁ arityNumAtL-out c γ = PT.rec squash₁ (λ { (ar , h) → PT.rec squash₁ (λ { (z , (hp , hω)) → PT.map (λ { (m , qm) → lower m , z , ( subst ⟨_⟩ (prAtL-adequate (suc (suc c)) (suc zero) zero (z ∷ ar ∷ γ)) hp ∙ cong (λ w → pr w (fst z)) (qm ∙ numeralL-fst (lower m)) ) }) (subst ⟨_⟩ (ω-specL ar) hω) }) h }) arityNumAtL-in : ∀ {n} (c : Fin n) (γ : S ^ n) (m : ℕ) (z : S) → fst (lookup c γ) ≡ pr (# m) (fst z) → ⟨ γ ⊨ arityNumAtL c ⟩ arityNumAtL-in c γ m z e = ∣ numeralL m , ∣ z , ( subst ⟨_⟩ (sym (prAtL-adequate (suc (suc c)) (suc zero) zero (z ∷ numeralL m ∷ γ))) (e ∙ cong (λ w → pr w (fst z)) (sym (numeralL-fst m))) , subst ⟨_⟩ (sym (ω-specL (numeralL m))) ∣ lift m , refl ∣₁ ) ∣₁ ∣₁ ``` ## The predicate Two conjuncts, at one free variable. The first pins the arity from outside, which is the conjunct the previous chapter asked for by name. The second is a witness for the decode's two hypotheses: a set holding the argument, closed and shaped. Nothing in the second conjunct is bounded, and nothing has to be. The witness is produced from a formula's own subformula closure in the introduction, and consumed as a set of `L` in the elimination, and the class model is where both readings happen. The second conjunct is written twice: once at two slots, the carrier and the argument, and once with the carrier pinned to a constant. The general one is a single existential, for the set; the pinned one wraps it in the binder that names `A`, and that binder is the entire difference between them. ```agda hasWitnessAt : ∀ {n} → Fin n → Fin n → Formula S n hasWitnessAt A x = ∃̇ ((var (suc x) ∈̇ var zero) ∧̇ (closedAt zero ∧̇ shapedAt zero (suc A))) hasWitness : S → Formula S 1 hasWitness A = ∃̇ ((var zero ≐ con A) ∧̇ hasWitnessAt zero (suc zero)) isCodeAny : S → Formula S 1 isCodeAny A = arityNumAtL zero ∧̇ hasWitness A ``` ## The superset, and the set The carrier is fixed, and the consumer will fix it at a stage. Its members are the alphabet, exactly as the coding chapters' two parameters expect: the embedding into the hierarchy, and the certificate that what it lands on is constructible. The second is transitivity of `L` applied once, and the membership it is applied to is named separately, because the shape predicate now asks for it in its own right. Then the superset. `smallDom` asks for a small family of elements of `L` and returns a stage containing all of it; the family is indexed by the pairs of an arity and a formula at it. The type is of the right size because syntax is an inductive type at the alphabet's own level, and the arity is a natural number, which costs no level at all. What comes back contains every key and much else, and separation removes the else. The set is sealed where it is built. Unsealed, every later type mentioning it would carry the separation instrument's unfolding into conversion, and the facts exported here are all any consumer needs. Only the ones that read a separation are inside a seal; the directions back and the equations they compose into are outside, since none of them needs to know what the set was cut out of. ```agda module _ (A : S) where private ι : ⟪ fst A ⟫ → V ℓ ι = ⟪ fst A ⟫↪ ι∈ : (m : ⟪ fst A ⟫) → ⟨ ι m ∈ fst A ⟩ ι∈ m = ∈∈ₛ {a = ι m} {b = fst A} .snd (∈ₛ⟪ fst A ⟫↪ m) ιL : (m : ⟪ fst A ⟫) → ⟨ isL (ι m) ⟩ ιL m = isL-trans {x = fst A} {y = ι m} (ι∈ m) (A .snd) codeS : ∀ {n} → Formula ⟪ fst A ⟫ n → S codeS φ = VCode.⌜ mapFo ι φ ⌝ , codeL ι ιL φ keyS : ∀ {n} → Formula ⟪ fst A ⟫ n → S keyS φ = key ι ιL φ , keyL ι ιL φ private smallAny : Σ[ d ∈ S ] ((p : Σ[ n ∈ ℕ ] Formula ⟪ fst A ⟫ n) → ⟨ keyS (snd p) ∈ˢ d ⟩) smallAny = smallDom (Σ[ n ∈ ℕ ] Formula ⟪ fst A ⟫ n) (λ p → keyS (snd p)) sepAny : isContr (SetOf (λ x → (x ∈ˢ smallAny .fst) ⊓ ((x ∷ []) ⊨ isCodeAny A))) sepAny = hasSeparationL (smallAny .fst) (isCodeAny A) ``` ## The witness, in and out Both halves of the second conjunct are proved here, once, at a variable arity, a variable carrier slot and a variable environment, and everything below applies them. The arity may be variable because the conjunct never mentions it: the introduction produces a closed, shaped set for a formula of any arity, and the elimination consumes one and calls the decode, which took the arity as an argument from the start. The carrier and the environment may be variable because every lemma the two halves are built from already takes them so. Introduction is the half that adds nothing beyond what is given. The witness is the subformula closure, whose three obligations are `key∈closure`, `closureClosed` and `closureShaped`, one chapter each and all already discharged. The last of them asks for one thing more, that every constant is a member of the carrier, and at this alphabet that is the fact the alphabet was defined by, carried across the slot's equation. Elimination is the other half, and it starts from the member already in key form at a stated arity, which is what `recover` demands and what nothing in the second conjunct would supply. The carrier slot's equation turns a membership in whatever that slot holds into a membership in `A`, which is what makes the decode's hypothesis dischargeable: `A`'s members are exactly the image of `⟪ A ⟫`, by the presentation of a set by its own members. Read the existential and a closed, shaped set arrives with it. Then the decode runs, and its answer is a formula over the carrier, at the arity it was handed. The pinned pair is these two at the environment the naming binder makes, and that is the whole of what pinning costs: introduction supplies `A` for the binder and `refl` for its equation, elimination reads the binder off and hands what it holds to the general form. **Reading it off is where the payload has to be named.** Left to inference, the truncation's payload at a pinned carrier is a metavariable standing for the satisfaction of a formula the elaborator has not committed to, and the same two lines that check in two seconds with the type written out ran past 140 seconds without it and were killed there. This is the law the recursion's totality hypothesis recorded, met again in a different place: it is not about the graph, it is about `PT.rec` at a concrete environment. ```agda witnessAt-in : ∀ {n k} (b c : Fin n) (γ : S ^ n) (φ : Formula ⟪ fst A ⟫ k) → fst (lookup b γ) ≡ fst A → fst (lookup c γ) ≡ fst (keyS φ) → ⟨ γ ⊨ hasWitnessAt b c ⟩ witnessAt-in b c γ φ qb qc = ∣ clo ι ιL φ , ( subst (λ w → ⟨ w ∈ fst (clo ι ιL φ) ⟩) (sym qc) (key∈closure ι ιL φ) , ( closureClosed ι ιL φ γ , closureShaped ι ιL φ b γ (λ m → subst (λ w → ⟨ ι m ∈ w ⟩) (sym qb) (ι∈ m)) ) ) ∣₁ witnessAt-out : ∀ {n} (b c : Fin n) (γ : S ^ n) → fst (lookup b γ) ≡ fst A → ⟨ γ ⊨ hasWitnessAt b c ⟩ → (k : ℕ) (z : S) → fst (lookup c γ) ≡ pr (# k) (fst z) → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst (lookup c γ) ≡ fst (keyS ψ))) ∥₁ witnessAt-out b c γ qb hw k z qz = PT.rec squash₁ viaSlot hw where Target : Type (ℓ-suc ℓ) Target = ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst (lookup c γ) ≡ fst (keyS ψ))) ∥₁ onto : (y : V ℓ) → ⟨ y ∈ fst (lookup b γ) ⟩ → ∥ Σ[ m ∈ ⟪ fst A ⟫ ] (ι m ≡ y) ∥₁ onto y y∈ = ∣ ∈-asFiber {a = y} {b = fst A} (subst (λ w → ⟨ y ∈ w ⟩) qb y∈) ∣₁ viaSlot : Σ[ C ∈ S ] ⟨ (C ∷ γ) ⊨ ((var (suc c) ∈̇ var zero) ∧̇ (closedAt zero ∧̇ shapedAt zero (suc b))) ⟩ → Target viaSlot (C , (x∈C , (hcl , hsh))) = PT.map (λ { (ψ , qψ) → ψ , (qz ∙ cong (pr (# k)) (sym qψ)) }) (Decode.recover ι zero (suc b) (C ∷ γ) onto hcl hsh k z (subst (λ w → ⟨ w ∈ fst C ⟩) (qz ∙ sym (keyOf-fst k z)) x∈C)) private witness-in : ∀ {n} (φ : Formula ⟪ fst A ⟫ n) → ⟨ (keyS φ ∷ []) ⊨ hasWitness A ⟩ witness-in φ = ∣ A , ( refl , witnessAt-in zero (suc zero) (A ∷ keyS φ ∷ []) φ refl refl ) ∣₁ witness-out : (x : S) → ⟨ (x ∷ []) ⊨ hasWitness A ⟩ → (k : ℕ) (z : S) → fst x ≡ pr (# k) (fst z) → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst x ≡ fst (keyS ψ))) ∥₁ witness-out x hw k z qz = PT.rec squash₁ viaCarrier hw where viaCarrier : Σ[ B ∈ S ] ⟨ (B ∷ x ∷ []) ⊨ ((var zero ≐ con A) ∧̇ hasWitnessAt zero (suc zero)) ⟩ → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst x ≡ fst (keyS ψ))) ∥₁ viaCarrier (B , (qB , hB)) = witnessAt-out zero (suc zero) (B ∷ x ∷ []) qB hB k z qz ``` ## The set at every arity What comes out is the class of keys of formulas over the carrier **at any arity**, which is the class a recursion over subcodes has to be indexed by, because a quantifier's subformula lives one arity up and the arity-one class does not contain it. ```agda IsKeyOverAny : S → hProp (ℓ-suc ℓ) IsKeyOverAny x = ∥ (Σ[ n ∈ ℕ ] Σ[ ψ ∈ Formula ⟪ fst A ⟫ n ] (fst x ≡ fst (keyS ψ))) ∥₁ , squash₁ opaque AllCodes : S AllCodes = sepAny .fst .fst key∈AllCodes : ∀ {n} (φ : Formula ⟪ fst A ⟫ n) → ⟨ keyS φ ∈ˢ AllCodes ⟩ key∈AllCodes {n} φ = subst ⟨_⟩ (sym (sepAny .fst .snd (keyS φ))) ( smallAny .snd (n , φ) , ( arityNumAtL-in zero (keyS φ ∷ []) n (codeS φ) refl , witness-in φ ) ) AllCodes-out : (x : S) → ⟨ x ∈ˢ AllCodes ⟩ → ⟨ IsKeyOverAny x ⟩ AllCodes-out x x∈ = PT.rec squash₁ (λ { (k , z , qz) → PT.map (λ { (ψ , q) → k , ψ , q }) (witness-out x (sat .snd) k z qz) }) (arityNumAtL-out zero (x ∷ []) (sat .fst)) where sat : ⟨ (x ∷ []) ⊨ isCodeAny A ⟩ sat = subst ⟨_⟩ (sepAny .fst .snd x) x∈ .snd AllCodes-in : (x : S) → ⟨ IsKeyOverAny x ⟩ → ⟨ x ∈ˢ AllCodes ⟩ AllCodes-in x = PT.rec (snd (x ∈ˢ AllCodes)) (λ { (n , ψ , q) → subst (λ w → ⟨ w ∈ fst AllCodes ⟩) (sym q) (key∈AllCodes ψ) }) ``` ## Recap One set, one predicate. `AllCodes` is an element of `L` whose members are exactly the keys of the formulas over the carrier, at every arity, by `AllCodes-out` and `AllCodes-in`. The whole content is in two conjuncts, and both are of the same kind. Closedness and shapedness together recognize the *shape* of a code and say nothing about the arity a key carries or the alphabet its constants come from, so a decode written against them has to be handed both, and a set built from them has to state both. `smallDom` and general-formula separation do the rest, and neither needed anything the earlier chapters had not already established. The set exists for the *class* it characterizes, not for a theorem about it. A recursion over codes has to answer at a code's subcodes, a quantifier's subformula lives one arity up, and the arity-one class does not contain it, so the domain has to be the keys at every arity.