Uniform satisfaction over all codes

Recursion on AllCodes A produces one satisfaction assignment whose value at every formula key agrees with the explicit satisfaction table for that formula. This makes satisfaction available uniformly across formulas and arities.

Consumers of internal satisfaction arrive holding a code, not the formula from which it came. The internal definable powerset ranges over all arity-one codes at a stage, while the well-order may compare codes that are not subcodes of any common formula. The recursion therefore needs one table whose visible domain is the whole stage code set. AllCodes supplies exactly those keys, at every arity.

The graph itself binds a table and a qualifying index set existentially. To show that a member has a graph value, funct may use the member's own subformula slot, whose closed, total, clause-satisfying table was certified by the preceding coding chapters. Uniformity then says that these local witnesses cohere into the value read from the whole code set.

A second bridge is needed because the code set uses the hierarchy's coding over a stage alphabet, whereas the recursive table uses the model's coding over the model language. This chapter identifies the two presentations and exports the uniform satisfaction table consumed by powerset and Choice.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp )
open import FOL.Manipulation.Relabelling using ( ⊨-map )
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.Definability {ℓ} using ( module DefOf )
open import L.Coding.Model {ℓ} using ( domAt; domAt-intro; domAt-out )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
open import L.Coding.SatisfactionBridge {ℓ} lem
  using ( intoL; asConst; Sat-spec ) renaming ( graph to envGraph )
open import L.Coding.SatisfactionTable {ℓ} lem
  using ( keyʟ; slot; satTable; total; inSlot; entry-in )
open import L.Coding.SlotClosure {ℓ} lem using ( slotClosed )
open import L.Coding.EnvironmentTower {ℓ} lem using ( towerAt; module Tower; module TowerHolds )
open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SlotHolds ) renaming ( keyBridge to keyBridge' )
open import L.Coding.SatisfactionGraph {ℓ} lem using
  ( satGraph; graph-in; graph-out; Bi; Ti; Ci; Ei; NN; ev; numν; numTags )
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.Nat using ( _+_ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Vec using ( _∷_; [] )
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 hPropStructure 𝒮ʟ

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

Naming a member of the code set

The specification of AllCodes A turns any member into a formula over members of A whose key is that member. The construction keyIn packages the resulting key as an element of L for use by the recursion.

Three lines, and they are the only one-time decision in this chapter. 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 made opaque where it is made. As an opaque definition, 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 this opaque name is the only thing that would need unfolding, and no step unfolds 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 ψ

Relating external and internal formula keys

keyBridge proves that coding a formula over members of A directly gives the same underlying key as first translating its constants into L and then using the model-internal key. The accompanying frame fixes the numeral tags, tower, and code domain needed by the graph formula.

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 not been used 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 = keyBridge' A

module _ (B : S) where
  fr : ∀ {m n} (φ : Formula S m) (γ : S ^ n) → S ^ ( + n)
  fr φ γ = ev numν (Tower.tower B) (slot B φ) (satTable B φ) B γ

  frTags : ∀ {m n} (φ : Formula S m) (γ : S ^ n) → Tags (fr φ γ) NN
  frTags φ γ = numTags (Tower.tower B) (slot B φ) (satTable B φ) B γ

  frTow : ∀ {m n} (φ : Formula S m) (γ : S ^ n) → ⟨ fr φ γ ⊨ towerAt Ei Bi (NN f0) ⟩
  frTow φ γ = TowerHolds.holds Ei Bi (NN f0) (fr φ γ) B refl refl refl

  frDom : ∀ {m n} (φ : Formula S m) (γ : S ^ n) → ⟨ fr φ γ ⊨ domAt Ti Ci ⟩
  frDom φ γ = domAt-intro Ti Ci (fr φ γ)
    (λ 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))

module _ (A B : S) where
  private

Existence and uniqueness at a named formula

For the formula named by a member of AllCodes B, its explicit satisfaction table supplies an output at the corresponding key. The table’s key-determinacy theorem proves that any two outputs there are equal, giving the two hypotheses required by recursion.

Both halves come from 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.

The change does not affect uniqueness 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 ten 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.

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

    exists : ∀ {n} (ψ : Formula ⟪ fst B ⟫ n) (x : S) → fst x ≡ fst (keyʟ (toB ψ))
           → ⟨ (Sat B (toB ψ) ∷ x ∷ []) ⊨ satGraph B ⟩
    exists {n} ψ x k = graph-in B x (Sat B (toB ψ))
      ∣ numν
      , (Tower.tower B
      , (slot B (toB ψ)
      , (satTable B (toB ψ)
      , (B
      , (refl
      , (frTags B (toB ψ) δ2
      , (frTow B (toB ψ) δ2
      , (slotClosed B (toB ψ) (Tower.tower B ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3
            ∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ Sat B (toB ψ) ∷ x ∷ [])
      , (frDom B (toB ψ) δ2
      , (subst (λ w → ⟨ pr w (fst (Sat B (toB ψ))) ∈ fst (satTable B (toB ψ)) ⟩) (sym k)
            (entry-in B (toB ψ))
      , SlotHolds.holds B Ti Bi Ci Ei NN (fr B (toB ψ) δ2) refl
          (frTags B (toB ψ) δ2) (frTow B (toB ψ) δ2) ψ refl refl)))))))))) ∣₁
      where δ2 = Sat B (toB ψ) ∷ x ∷ []

    unique : ∀ {n} (ψ : Formula ⟪ fst B ⟫ n) (x : S) → fst x ≡ fst (keyʟ (toB ψ))
           → (y : S) → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩ → y ≡ Sat B (toB ψ)
    unique {n} ψ x k y hy = Σ≡Prop (λ v → snd (isL v))
      (PT.rec (setIsSet (fst y) (fst (Sat B (toB ψ))))
        (λ { (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) →
          SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b (y ∷ x ∷ [])) B eb tg hE hc h12
            ψ (subst (λ u → ⟨ u ∈ fst C ⟩) (k ∙ sym (keyBridge' B ψ))
                 (domAt-out Ti Ci (ev ν E C T b (y ∷ x ∷ [])) hd x y ha)) y
            (subst (λ u → ⟨ pr u (fst y) ∈ fst T ⟩) (k ∙ sym (keyBridge' B ψ)) ha) })
        (graph-out B x y hy))

Recursion on the whole code set

satRec instantiates the abstract recursion theorem with AllCodes B, the satisfaction graph, closure under subformulas, and the preceding existence-and-uniqueness proof. Its value function is the uniform satisfaction assignment used below.

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 B
  Recursion.graph satRec = satGraph B
  Recursion.funct satRec x x∈ = mereFunct (satGraph B) x
    (PT.map
      (λ { (n , ψ , q) → Sat B (toB ψ)
         , ( exists ψ x (q ∙ keyBridge' B ψ)
           , unique ψ x (q ∙ keyBridge' B ψ) ) })
      (AllCodes-out B x x∈))

  module Table = Of satRec

Identifying each recursive value

val-at identifies the recursive value at a formula key with the explicit Sat value already known to satisfy the clauses. The theorem val-sat then reads membership in that value as satisfaction of the represented formula under its encoded environment.

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 B ⟫ n) (x : S) (x∈ : ⟨ x ∈ˢ AllCodes B ⟩)
         → fst x ≡ fst (keyS B ψ)
         → Table.val x x∈ ≡ Sat B (toB ψ)
  val-at ψ x x∈ q =
    Table.val-uniq x x∈ (Sat B (toB ψ)) (exists ψ x (q ∙ keyBridge' B ψ))

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 DA.𝒮M DA.ι id ψ δ

Recap

The construction yields one graph over all formula codes, while val-at and val-sat ensure that each of its values is the intended satisfaction set rather than merely a solution of the recursion equations.

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, and val-sat says that value is satisfaction over the carrier.

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 ten 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.