Satisfaction over the whole code set

上一章那个实例以 slot B φ 为索引，即一条公式及其诸子公式的诸键。下游没有任何东西用得上它。消费方到场时手里握着的是一个码，而不是该码所出自的那条公式：内部可定义幂集在某阶段处元数一的诸码上取值，而良序要比较的两个码并非任何共同公式的子码。以一条公式的槽为索引，就是一条公式一张表，而「这张表在这个码处说什么」在有人拿出「该码是其子码」的某条公式之前，根本没有答案。

作答的那个定义域是某阶段处的码集，而上一个目标已经把它造好。AllCodes 持有载体之上诸公式在每个元数处的诸键，而那恰是消费方到场时手里握着的东西。

整个码集的封闭性不是打发图对索引集之要求的那个东西，而这件事值得说出来，因为那条定理正是上一个目标为之登记的。图把自己的表与索引集都作存在绑定，故 funct 只欠「某个装着该成员的合格集合」，而最小的那个就是该成员自己那条公式的槽，其封闭性由造出它的那一章给出。它在任何地方都不被消费，故此后已予撤除。

这次更换的代价就是本章的全部内容，而它几乎为零；理由值得在一切之前说明。那个图把自己的表存在绑定。故 funct 在一个成员处不必拿出一张覆盖整个定义域的表；它只需拿出「某张封闭、全的、满足诸子句的、装着该成员的表」，而最小的这样一张，就是该成员自己那条公式的子公式槽，而它已由前面四章造好并认证。这场递归换掉它的定义域，其余一概不变：Table、Slot、Sound 与 Unique 逐条陈述原封不动，而按公式索引的那个实例继续在这一个旁边有效。

此处确有一件全新的东西，而它压根与递归无关。码集的诸成员是在层级的编码里、在该阶段自己的字母表之上取的键；而这场递归所说的一切，是在模型的编码里、在模型的语言之上取的键。两者是同一套构造落在两个字母表上，而没有任何定理把它们接上。

{-# 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 _⊨_ )

点名一个成员

三行，而它们是本章唯一的一次性能决定。想要某条特定公式处的取值的消费方，必须为「取值所在的那个成员」点名，而显而易见的名字就是那个键本身；可是那样点名展开不了，因为键会展成「数码与码之对」，而那个构造随后就坐进了递归的定义域里、也坐进了一个满足关系里面。

于是那个名字在它被造出之处封印。封印之后，它是 L 的一个元素，类型可以提它而不必展开，而消费方所需的两条事实随之出来：它落在定义域中，且它是「造它时所用的那条公式」的键。下面的一切都陈述在变元成员上、并经一条等式抵达它的键，故需要被打开的只有这个封印，而没有任何东西打开它。

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 ψ

两套编码的会合

层级编码里的一个键，是元数数码与「沿字母表的嵌入重标之后那条公式的码」之对；模型编码里的一个键，是 L 的数码与「在 L 里取的码」之对。codeBridge 把这两个码等同起来，一构造子一子句。它写在模型那一章，此后一直没有消费方，因为它当初就是为这条陈述而写的。

它供不出的是那次重标。集合那边的公式在字母表 ⟪ A ⟫ 之上，递归这边的公式在 L 之上，故两侧经过的是两个不同的映射，而它们的复合必须被认出为一个映射。那是重标的函子性，它归属于重标被定义之处，而如今就在那里；于是整座桥是四次改写，没有归纳。

通往模型的那个映射也不在此处造。它就是桥那一章自己的 asConst，即字母表的嵌入接上类包含；而取它、而非取一个与它相等的映射，正是使最后一节能够径直引用那条适足性、无须任何翻译步骤的原因。

这座桥只取字母表，别无其他。诸环境所落之上的那个集合在它里面从未出现，故它比下面那场递归少一个参数；而后面某一章若需要两套编码在「握在一位上的载体」处相符，便可以直接用它，无须供上一个它并不拥有的第二载体。

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)

两半，落在那个码所命名的公式上

两半都是前几章的，只是施于「该成员是其键的那条公式」而非某条周遭公式，而这次更换使存在性更短。按公式索引的那个实例得把一条子公式的条目沿「它自己的子树到周遭表的包含」搬过去；此处被还原出来的那条公式就是其表正被递出的那条公式，故 entry-in 直接适用，那次搬运消失了。

唯一性压根察觉不到这次更换，而理由是结构性的。Pinned 谈的是「图所产出的索引集与表」，那是调用方环境里的被绑定变元，从不谈递归的定义域。定义域既不出现在它里面，也不出现在十二条子句里，故更换递归的索引，够不着唯一性。

此处只把全性那条假设写出来，而它的环境也一并写出。若交给推断，图那三个存在绑定的槽位什么也决定不了，会剩下六个元变元；把环境点名只花一行，而那正是「能否被展开求解」的分水岭。

    Ci Ti : Fin 
    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))

那个实例

定义域是该阶段处的码集，图是两章之前的那一个，而 funct 经 mereFunct 交付，因为「仅仅存在的唯一解」就是可缩解。一个成员以「字母表之上某条公式的键」这种仅仅存在的形式到场，那座桥把它的等式变成一条关于模型之键的等式，而上面两半就施于那个键。

两个载体是彼此独立的参数，且保持如此。A 是诸码的常元所取自的字母表；B 是诸环境所落之上的集合；递归里没有任何东西把它们联系起来，而为一个用不上的关系向递归收费，等于陈述一条更弱的定理。它们在下一节、且只在那里被钉在一起，因为那才是满足关系获得含义的地方。

  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

那个取值是什么

一场与任何东西都不相连的递归什么也没定义，故那个取值陈述两遍。

先对着递归自己的构造，而那是唯一性反过来花掉：在「是某条公式之键」的那个成员处，取值就是元语言递归在那条公式处造出的那个集合，因为存在性那一半把那个集合作为一个解拿了出来，而递归的取值是唯一的解。这就是消费方要从这张表里取出任何东西所需的读式，因为那个值函数来自一次可缩性，自身不化简出任何东西。

那个成员是变元，而它的键经一条等式抵达；这是一次测量，不是口味。若径直陈述在那个键上，值函数的实参就是一个具体的码构造，也就把那个构造塞进了「值据以定义的那个图的满足关系」里；在变元上花四秒的那条陈述，写在键上跑过了六分钟并被放弃，而把它写成变元版本的推论时同样如此，这说明代价在陈述里、不在证明里。唯一性那一章在它的第一个情形上记下了这条规矩，而它在此处原样成立。

两个方向都什么也没有失去。手里握着一个成员的消费方，握着的就是一个成员，外加它的键等式；而想把那个成员点名的消费方，可经那个封印过的名字把方便的形式拿回来，且分文不花，因为类型在那里所提的东西不会展开。

  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 ψ)

再对着满足关系，而那是这个目标存在的理由。桥那一章证过：元语言那个取值的成员，就是在世界 (B, ∈) 中满足该公式的一个环境；把它与上面那条读式复合，同一句话便落到这场递归所产出的表上。在元数一处它特化为可定义幂集所指的那个可定义子集，故在「是某条公式之键」的那个成员处读出的那张表，就是该公式的可定义子集，而那正是内部层级将据以读出 Def 的陈述。

两个载体在此会合，因为此处是它们非会合不可的地方。常元皆为载体成员的公式，内层世界读得了；点名了 L 的任意元素的公式则不然，而桥那一章对自己就是这么说的。故下面两条定理陈述在同一个载体上，而那本来也是消费方想要的实例化：某阶段处的诸码，在同一个阶段之上被满足。

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 ⟫ ) (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))

小结

satRec 是作为已内化递归的满足关系，跑在某阶段处的诸码之上，而非跑在一条公式的诸子公式之上，而 Table 是它产出的那张表。val-at 在一个以键的形式给出的成员处读出取值，而 val-key 是同一条读式落在「一条公式自己的键」那个封印过的名字上；val-sat 说那个取值就是载体之上的满足关系；而 val-defSet 把两者花在元数一处的可定义幂集上，那正是内部层级所消费的形式。

底下没有任何东西被重新索引，也没有任何东西被削弱。本目标登记在案的风险是：定义域或它的良构谓词会在某个不能取作槽位之处、把载体当作常元来要；那将把槽、表、全性与隶属重新索引在「载体与键」之对上，并为两半的十二个情形各记一笔搬运。它没有引爆，而直接的证据是：slot、satTable、total、inSlot、slotClosed、soundness 与 Good.pinned 在上面全都是按它们既有的类型施用的。码载体压根到不了那个图：它在码集自己的谓词里被绑定、被钉住，而出来的是 L 的一个元素，而定义域无非就是这个。

使这一切便宜的是图里的那个存在量词，而这值得当作一项设计事实、而非一次偶然留存下来。一个把自己的表存在量化的图，允许一个取值由任意一张合格的表来担保，故实例可以在每个索引处用「够得着它的最小的表」作答。倘若那个图把自己的表点了名，定义域与表就得一起长大，而前面每一章都要动。

唯一没被预料到的代价落在诸陈述里、不落在诸证明里，而它就是本章的那次测量。在一个写开了的键处读出的取值，无论证明写多长都展开不了，因为那个键的构造落进了一个满足关系里面；在变元成员上花四秒的那条读式，写在键上跑过了六分钟，而把它写成变元版本的推论时同样如此。修好它的有两件事，恰是登记在案的两条规矩、一条一件：每条读式都把成员取作变元、并经一条等式抵达它的键；而消费方本会写下的那个名字，在它被造出之处封印。前者是唯一性那一章的规矩，此番出现在一个压根没有在作归纳证明的地方；后者是「关于出现在目标里的构造」的那条规矩，此番出现在一个只是一条等式的目标上。