全部编码上的一致满足关系

在 AllCodes A 上递归产生一个统一的满足关系赋值，它在每个公式键处的值都与该公式的显式满足关系表相符。于是满足关系可以跨公式与元数一致地使用。

内部满足关系的使用者直接面对的是一个码，而非该码所出自的公式。内部可定义幂集会遍历某层处全部元数一的码，良序也可能比较不属于任何共同公式的两个子码。因此递归需要一张定义域为整个层码集的表；AllCodes 恰好对每个元数都给出这些键。

图以存在方式把表与合格的索引集绑定起来。为了证明某个成员有图值，funct 可以取该成员自己的子公式槽；前面的编码章节已经证明那张槽表封闭、全且满足诸子句。统一性随后说明这些局部见证与从整个码集读出的取值相容。

除此之外还需另一个衔接：码集使用层级在层字母表上的编码，而递归表使用模型在模型语言上的编码。本章认同这两种呈现，并导出供幂集与 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 _⊨_ )

命名编码集的成员

AllCodes A 的规格把任意成员化为一个常元取自 A 的成员且以该成员为键的公式。构造 keyIn 再把所得键封装为 L 的元素，供递归使用。

这三行是本章仅有的一次性决定。想要某条特定公式处取值的使用者，必须指明「取值所在的那个成员」，而显而易见的名字就是那个键本身；可是这样一来名字无法展开，因为键会展开成「数码与码之对」，而这个构造随后就进入了递归的定义域，也进入了一个满足关系。

因此，这个名字在构造处被封装为不透明定义。封装后，它是 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 ψ

关联外部与内部公式键

keyBridge 证明：把一个常元取自 A 成员的公式直接编码，与先把常元翻译进 L 再取模型内部的公式键，两者所得的底层键相同。随后的框架固定图公式所需的数码标签、塔与编码域。

层级编码里的一个键，是元数数码与「沿字母表的嵌入重标之后那条公式的码」之对；模型编码里的一个键，是 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 = 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

命名公式处的存在性与唯一性

对 AllCodes B 的成员所命名的公式，其显式满足关系表在相应键处给出一个输出。满足关系表的键确定性定理证明该处任意两个输出相等，从而给出递归所需的存在性与唯一性。

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

这次更换完全不影响唯一性，理由是结构性的。Pinned 谈的是「图所产出的索引集与表」，那是调用方环境里的被绑定变元，从不涉及递归的定义域。定义域既不出现在它里面，也不出现在十条子句里，因此更换递归的索引触及不到唯一性。

此处把全性那条假设连同它的环境一并显式写出。若交由推断，图上三个存在绑定的槽位确定不了任何内容，会剩下六个元变元；而点名环境只需一行，那正是「能否被展开求解」的分水岭。

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

全部编码集上的递归

satRec 以 AllCodes B、满足关系图、对子公式的封闭性以及上一节的存在唯一性证明来实例化抽象递归定理；其取值函数就是下文使用的一致满足关系赋值。

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

两个载体是彼此独立的参数，且始终如此。A 是诸码的常元所取自的字母表；B 是诸环境所属的集合；递归中没有任何东西把它们联系起来，而要求递归带上一个用不上的关系，只会得到一条更弱的定理。两者在下一节、且只在下一节才被结合起来，因为只有在那里满足关系才获得含义。

  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

逐个识别递归取值

val-at 把公式键处的递归取值等同于已经证明满足诸子句的显式 Sat 值。随后，val-sat 把「属于该值」读成：所表示的公式在其编码环境下得到满足。

与任何东西都不相连的递归定义不了任何东西，故这个取值要陈述两遍。

先对照递归自身的构造来读，这里用到的正是唯一性：在「是某条公式之键」的那个成员处，取值就是元语言递归在那条公式处造出的那个集合，因为存在性那一半给出以该集合为一个解，而递归的取值是唯一的解。后续使用这张表的证明要从其中取出任何内容，所需的正是这条读式，因为那个值函数来自一次可缩性，自身化简不出任何东西。

那个成员是变元，其键通过一条等式给出；这是测量所得的选择，而非表述偏好。若直接在该键上陈述，值函数的实参就是具体的码构造，该构造也会进入「定义该值的图的满足关系」中。同一陈述以变元书写时耗时四秒，直接写在键上则运行超过六分钟后被放弃；把它改写成变元版本的推论时结果相同。这说明代价来自陈述而非证明。唯一性一章在第一个情形中记录的规则，在此原样适用。

两个方向都没有丢失内容。已经持有一个成员的使用者，同时持有该成员及其键等式；需要点名该成员时，则可通过前面封装的不透明名字取得方便的形式，而且无需展开，因为类型中提到该名字不会触发其定义。

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

再对照满足关系，这是本目标存在的理由。桥那一章证过：元语言那个取值的成员，就是在世界 (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 DA.𝒮M DA.ι id ψ δ

小结

这一构造得到覆盖全部公式编码的一张图，而 val-at 与 val-sat 保证其中每个取值都是预期的满足关系集，而不只是递归方程的某个解。

satRec 作为已内化递归的满足关系，定义在某层处的诸码之上，而非定义在一条公式的诸子公式之上，而 Table 是它产出的那张表。val-at 在一个以键的形式给出的成员处读出取值；val-sat 说那个取值就是载体之上的满足关系。

这里没有任何内容被重新索引或削弱。预先记录的风险是：定义域或其良构谓词可能在无法使用槽位的位置要求把载体作为常元；那样就必须在「载体与键」的对上重新索引槽、表、全性与隶属，并在两个方向的十个情形中逐一改写。该风险没有发生：slot、satTable、total、inSlot、slotClosed、soundness 与 Good.pinned 在上文都按原有类型直接使用。码载体不会进入那个图；它在码集自身的谓词中被绑定并固定，所得是 L 的一个元素，而这正是递归的定义域。

这一切之所以便宜，靠的是图中的那个存在量词；这应当视为一项设计事实，而非侥幸留存的结果。一个以存在量词存放自己的表的图，允许取值由任意一张合格的表来担保，因此实例在每个索引处都能用可给出该取值的最小的表作答。倘若图中写明了具体的表，定义域与表就得一起扩大，而前面每一章都要随之修改。

唯一未曾预料的代价出现在陈述中，而不在证明中；本章的测量说明了这一点。在一个完全展开的键处读取取值时，键的构造会进入满足关系，因此证明再长也无法使它顺利展开。同一读式在变元成员上检查需四秒，直接写在键上则运行超过六分钟；把它写成变元版本的推论时也有同样差别。解决办法正是两条既有规则：每条读式都以成员为变元，再通过等式转到它的键；调用方需要点名的名字则在构造处封装为不透明定义。前一规则来自唯一性一章，在这里虽无归纳证明仍然适用；后一规则针对出现在目标中的构造，在这里只有一条等式的目标上同样适用。