统一满足关系的内部图

设 W 是一个可构造集合，它既充当公式常元取值的字母表，也充当环境中各项的取值范围。统一满足关系构造为 AllCodes W 中的每个公式码指派一个集合，即满足该码所编码公式的所有环境。本章证明，这一指派本身在 L 内具有图：存在一个集合，其成员恰好是公式码与相应满足关系集组成的有序对。数学上的关键是替换公理。统一的图公式在每个公式码上都有唯一取值，因此它在集合 AllCodes W 上的像可以收集成集合。

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

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

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

固定这样的可构造集合 W，并假设在编码构造所需的命题层上成立排中律。有序对在外围层级中构造，而定义域、取值与图本身都属于可构造论域 S。

open import FOL.ZFStructure using ( module hPropStructure )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )

定义域 AllCodes W 是可构造集合，由字母表取自 W 的良构公式码组成。公式语法给出图公式的类型；依值对的外延性随后用于证明「解及其满足证书」所组成的依值对具有唯一性。

open import L.Coding.CodeSet {ℓ} lem using ( AllCodes )

open import FOL.Syntax using ( Formula )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Vec using ( _∷_; [] )

累积层级中的成员关系表达截断的存在，因此任意图成员的最终刻画也采用截断形式。论域 S 来自可构造结构 𝒮ʟ；它的每个元素都由外围集合及其可构造性证书组成。

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )

open hPropStructure 𝒮ʟ using ( S )

这里使用的满足关系，是限制结构 𝒮ᵥ ↾ isL 上的内层语义，而这个限制结构就是可构造结构 𝒮ʟ。常元由其论域上的恒等映射解释。因此，_⊨_ 直接表示公式在 L 中满足；本章不使用它与外围语义之间的比较定理。

module AbsSF = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsSF using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )

对固定的 W，统一构造的两个参数都取这个集合，因此编码字母表与环境取值范围都是 W。Table.graph W W 是一条统一适用于 AllCodes W 全体成员的二元公式，用来描述取值关系；Table.val W W x mx 则是它在特定公式码 x 处的唯一取值。

open import L.Coding.UniformSatisfaction {ℓ} lem using ( module Table )
open import L.Recursion {ℓ} lem using ( Recursion )
open import L.Recursion.Graph {ℓ} lem using () renaming ( module Graph to MapGraph )

module SatGraph (W : S) where

给定公式码 x 及其成员证书 mx，把这个唯一取值记作 valOf x mx。等式 valOf≡ 在定义上把它识别为 Table.val W W x mx。这个记号单独标出将要收集其图的数学函数：每个定义域成员被送到相应的满足关系集。

  opaque
    valOf : (x : S) → ⟨ fst x ∈ fst (AllCodes W) ⟩ → S
    valOf x mx = Table.val W W x mx

    valOf≡ : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) → valOf x mx ≡ Table.val W W x mx
    valOf≡ x mx = refl

令 gr 为同一条二元公式 Table.graph W W。它的第一个自由位置放置候选满足关系集，第二个自由位置放置公式码。因此，它定义的关系正是公式码与取值之间的候选图关系。

  private
    opaque
      unfolding valOf
      gr : Formula S 
      gr = Table.graph W W

两条事实使 gr 成为函数图。存在性说明表中的取值与其公式码满足 gr，见证取自 Table.funct；唯一性说明任何满足同一图公式的 y 都等于 valOf x mx，它由表的唯一性定理取对称得到。

      defines' : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) → ⟨ (valOf x mx ∷ x ∷ []) ⊨ gr ⟩
      defines' x mx = Table.funct W W x mx .fst .snd

      only' : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ gr ⟩ → y ≡ valOf x mx
      only' x mx y h = sym (Table.val-uniq W W x mx y h)

对每个公式码，满足 gr 的解类型都是可缩的。它的中心是依值对，由取值 valOf x mx 与该取值满足 gr 的证明 defines' 组成。若另有解 (y , h)，only' 先识别两个取值；余下的分量都是同一命题的证明，因而 Σ≡Prop 把取值的相等提升为两个完整依值对的相等。这个可缩性正是应用替换所需的函数性前提。

    M : Recursion
    M = record
      { dom = AllCodes W ; graph = gr
      ; funct = λ x mx → (valOf x mx , defines' x mx)
          , λ { (y , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ gr)) (sym (only' x mx y h)) } }

现在可以对可构造集合 AllCodes W 上的函数关系 gr 应用替换。它把有序对 pr (fst x) (fst (valOf x mx)) 收集成可构造集合，记作 pairs。因此这张图位于 L 内部：定义域及每个取值都是可构造的，替换把它们的配对关系组成一个集合。

    module G = MapGraph M using ( F; F-in; pair-out )

  opaque
    pairs : S
    pairs = G.F

AllCodes W 中的每个公式码都贡献一个图上的有序对。具体而言，pairs-in 证明由底层公式码与底层满足关系集组成的有序对属于 pairs。

    pairs-in : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) → ⟨ pr (fst x) (fst (valOf x mx)) ∈ fst pairs ⟩
    pairs-in = G.F-in

反过来，假设有序对 pr (fst x) (fst y) 属于 pairs。替换像的纤维取值于命题，因此可以把截断见证消去到这样一个依值对：x 属于 AllCodes W，并且 y 等于该处的唯一取值。这就是 pairs-out 给出的未截断结论。

    pairs-out : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst pairs ⟩
              → Σ[ mx ∈ ⟨ fst x ∈ fst (AllCodes W) ⟩ ] (fst y ≡ fst (valOf x mx))
    pairs-out = G.pair-out

pairs 的任意成员未必已经以有序对的形式给出。因此，一般的像定理只产生截断的刻画：仅仅存在公式码 x、成员证书 mx 以及一个等式，把该成员呈现为 x 与其取值组成的有序对。这正是 pairs-shape；其中的截断来自替换像的成员关系。

    pairs-shape : (e : S) → ⟨ fst e ∈ fst pairs ⟩
                → ∥ Σ[ x ∈ S ] Σ[ mx ∈ ⟨ fst x ∈ fst (AllCodes W) ⟩ ] (fst e ≡ pr (fst x) (fst (valOf x mx))) ∥₁
    pairs-shape e h = MapGraph.F-out M (fst e) h

因此，pairs 是统一满足关系的内部图，其中公式常元与环境取值都取自 W。统一取值的存在唯一性使关系成为函数；替换把这个关系化为 L 中的集合；三条成员定理则分别针对已经呈现的有序对和任意成员刻画这个集合。