可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

交互式目录 · 依赖图

固定宇宙层级 ℓ 与这一条经典假设。描述中使用的每个对象，从可构造集合到编码后的公式键，都处在相应层级，因此结论不引入更强的经典假设。

module L.GCH.SatisfactionDescription {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

外部语义递归已经构造出统一满足关系表。现在的问题是，在 L 中解释的公式如何把一个候选集合识别为同一张图。我们将把环境塔、公式码域、表的两条定义域条件与十条递归构造子子句封装成一条有界描述，供后续公式量化。

这一构造仍以层级 ℓ-suc ℓ 上的排中律为条件。该假设支撑下文使用的编码与满足关系构造，但不会变成候选表的一项额外性质，而是始终显式携带。

最终描述由三个公式合取而成。其句法目标是一个 Δ₀ 证书，也就是描述中的每个量词都保持有界。正是这一有界性，使后文能够比较 L 内部与外围层级中的满足关系。

三类编码数据必须彼此一致。公式键属于典范集合 AllCodes W；元数 k 指向环境集 envSet W k；有序对则把键与其语义值包装在一起。AllCodes W 的元素只能在命题截断下显露为某个公式键，后面的每一步解码都保留这一边界。

对每个真实公式键，语义递归产生满足集 SatW ψ，函数表则记录相应取值。有界描述并不在内部重新运行这项递归，而是列出十条局部构造子子句，再用结构论证表明：任何满足这些子句的候选表，在每个真实键处都被钉扎到外部定义的取值。

只有先控制定义域，才能读取构造子子句。候选码域必须包含全部真实公式键，并且只容纳这样的键；环境塔则把每个自然数元数与该长度的环境联系起来。这两项描述恰好为归纳提供所需的子公式键与环境。

剩下的对象是统一满足关系表的图。它的条目是由公式键与满足集组成的编码对。十条有界子句描述第二分量如何依赖第一分量所编码的构造子，而真实图将为这些子句提供完备性见证。

解释环境是可构造集合组成的有限向量，其中的索引标识表、工作集、码域、塔与数码标签。依赖对表达各读式返回的见证。只要见证处在命题截断下，它就只能用于证明另一个命题，不能成为全局选定的数据。

自然数元数在累积层级内部表示为数码 # k。因此环境塔的条目被编码为 # k 与 envSet W k 的有序对。这里的等式始终陈述于底层的层级集合之间，这正是编码定理工作的层面。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_ )

以 S 表示可构造结构的载体。S 的元素由一个底层层级集合及其可构造性证据组成。表的读式比较的是底层集合，并不主张随附的可构造性证据相等。

open hPropView 𝒮ʟ using ( S )

本章的公式在 L 内部解释，其有限环境取值于 S。这些公式的有界性使后文能够与外围层级比较，但眼下的可靠性论证首先完全在这一内部满足关系中进行。

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

有界描述的可靠性

为证明可靠性，固定候选集合 T、C、E、工作集 W、十个数码标签，以及读取它们的环境。分别假设塔、码域与表的描述成立，并且只把工作集槽与 W 对齐。这三项描述假设中，没有一项由另外两项推出。

module SatSound {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m) (W : S)
  (qw : (lookup w γ) .fst ≡ W .fst) (tg : Tags γ N)
  (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩) (hC : ⟨ γ ⊨ codesAt C w E N ⟩)
  (hT : ⟨ γ ⊨ tableAt T w C E N ⟩) where

open Alphabet W

用 Tv、Cv、Ev 表示候选表、码域与环境塔所呈现的底层集合。子句语义提供一座桥，把关于这些集合的有界公式转换为结构论证所需的外围成员关系与等式事实。

open Bridge W
private
  Tv = (lookup T γ) .fst
  Cv = (lookup C γ) .fst
  Ev = (lookup E γ) .fst

设 Ev 的一个条目已经呈现为 n 与 F 的编码对。读取环境塔会在命题截断下给出元数 k 及等式 n = # k；忘去同时得到的 F = envSet W k，便得到分析候选公式键恰好所需的元数事实。反向的塔读式把每个真实元数条目放入 Ev，因而也能把真实键插入 Cv。

  module TR = TowerRead E w (N f0) γ W qw (tg f0) hE
  arity : (n F : S) → ⟨ pr (n .fst) (F .fst) ∈ Ev ⟩ → ∥ Σ[ k ∶ ℕ ] (n .fst ≡ # k) ∥₁
  arity n F q∈ = map₁ (λ { (k , (qk , _)) → k , qk }) (TR.entry-out n F q∈)
  module CS = CodesSound C w E N γ W qw tg arity (hC .fst)
  module CC = CodesComplete C w E N γ W qw tg TR.entry-in (hC .snd)

前提 hT 由全定义性、定义域条件与十条构造子子句组成，Frame 则提供它们的语义读式。SatSoundC 中的钉扎论证把全定义性和十条子句与环境塔事实、候选码域的封闭性结合起来。该论证不需要定义域条件，因为要被钉扎的表项已经作为真实公式键处的一个配对给出；后面读取任意已呈现的表配对时，才会使用定义域条件。

  module Fr = Frame T w C E N γ tg
  module SC = SatSoundC T w C E N γ W qw tg hE CS.closed hT

两条定义域条件具有互补的形式。全定义性对 Cv 中每个 c 仅给出经命题截断的存在性：有某个 y 使 pr c y 属于 Tv。定义域条件则从 Tv 的任意元素 e 出发，同样在命题截断下把它分解为 pr c y，并给出 c 属于 Cv。两者都不在全局选定取值或配对分量，单凭其中任何一条也不能使该表成为单值关系。

  hTot = hT .fst
  hOn = hT .snd .fst

利用码域完备性把公式 a 的真实键放入 Cv，再对此键应用全域性。结论仅仅说某个值与该键组成的对属于 Tv，见证仍处在命题截断下。这里没有选定值，也没有解码函数；后文只会把它消去到命题中。

  sub : ∀ {n} (a : Formula Ab n) → ∥ Σ[ ya ∶ S ] ⟨ pr ((keyS W a) .fst) (ya .fst) ∈ Tv ⟩ ∥₁
  sub a = Fr.total-out hTot (keyS W a) (CC.key-in a)

钉扎谓词说：只要值 y 与 ψ 的键组成的对属于候选表，y 的底层集就等于 ψ 的递归满足集。它只钉扎底层集；y 的可构造性证书与公式本身都不由它固定。

Pinned : ∀ {n} (ψ : Formula Ab n) → Type (ℓ-suc ℓ)
Pinned ψ = (y : S) → ⟨ pr ((keyS W ψ) .fst) (y .fst) ∈ Tv ⟩ → y .fst ≡ (SatW ψ) .fst

证明对 ψ 作结构递归。Cv 的封闭性给出直接子公式的键，全定义性则只在命题截断下给出这些键处的表取值。递归假设钉扎这些子取值；相应的构造子子句随后给出与语义递归相同的外延条件，因此外延性钉扎父公式的取值。事实 CC.key-in ψ 则提供从 ψ 的键开始这项论证所需的候选码域成员关系。

pinned : ∀ {n} (ψ : Formula Ab n) → Pinned ψ
pinned ψ = SC.pinned ψ (CC.key-in ψ)

候选码域的每个元素都属于典范码集。候选键读式只在命题截断下显露元数、公式与键等式。由于目标的典范成员关系是命题，可以把见证消去到该目标，并沿等式搬运成员关系；这一论证没有选定公式。

C-out : (c : S) → ⟨ c .fst ∈ Cv ⟩ → ⟨ c .fst ∈ (AllCodes W) .fst ⟩
C-out c c∈ = rec₁ ((c .fst ∈ (AllCodes W) .fst) .snd)
  (λ { (k , ψ , e) → subst (λ u → ⟨ u ∈ (AllCodes W) .fst ⟩) (sym e) (key∈AllCodes W ψ) })
  (CS.key-out c c∈)

反过来，典范码集的每个元素都属于 Cv。典范成员关系在命题截断下给出公式键的呈现，码域完备性再把该键插入候选域。这里仍只用见证证明成员关系，而不据此定义解码器。

C-in : (c : S) → ⟨ c .fst ∈ (AllCodes W) .fst ⟩ → ⟨ c .fst ∈ Cv ⟩
C-in c c∈ = rec₁ ((c .fst ∈ Cv) .snd)
  (λ { (k , ψ , e) → subst (λ u → ⟨ u ∈ Cv ⟩) (sym e) (CC.key-in ψ) })
  (AllCodes-out W c c∈)

环境塔的向外读式只处理已经呈现为 pr n F 的条目。它在命题截断下给出自然数 k，使 n = # k 且 F = envSet W k。它既不全局选定 k，也不声称仅凭本引理就能把 Ev 的任意元素呈现为编码对。

E-out : (n F : S) → ⟨ pr (n .fst) (F .fst) ∈ Ev ⟩
      → ∥ Σ[ k ∶ ℕ ] ((n .fst ≡ # k) × (F .fst ≡ (envSet W k) .fst)) ∥₁
E-out = TR.entry-out

环境塔的向内读式给出互补事实，而且无需命题截断：对每个给定的自然数 k，标准条目 pr (# k) (envSet W k) 都属于 Ev。它与上一条读式共同双向控制标准编码条目，但不主张为塔的每个任意元素选定元数。

E-in : (k : ℕ) → ⟨ pr (# k) ((envSet W k) .fst) ∈ Ev ⟩
E-in = TR.entry-in

表的读取是可靠性方向的核心。它只对已经呈现为 x 与 y 的有序对的成员关系陈述；候选表的任意元素不在本引理覆盖范围内。

T-out : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ Tv ⟩
      → Σ[ mx ∶ ⟨ x .fst ∈ (AllCodes W) .fst ⟩ ] (y .fst ≡ (Table.val W W x mx) .fst)
T-out x y h = rec₁ (isPropΣ ((x .fst ∈ (AllCodes W) .fst) .snd) (λ mx → setIsSet _ _))
  (λ { (c , yc , (ee , c∈)) → rec₁ (isPropΣ ((x .fst ∈ (AllCodes W) .fst) .snd) (λ mx → setIsSet _ _))
    (λ { (k , ψ , e) →

配对等式拆分出两侧的第一分量，码等式把被记录的键认同为某条解码公式的键；该公式键属于典范码集则由搬运得到。

      let q = pr-inj ee
          qx : x .fst ≡ (keyS W ψ) .fst
          qx = q .fst ∙ e
          mx : ⟨ x .fst ∈ (AllCodes W) .fst ⟩
          mx = subst (λ u → ⟨ u ∈ (AllCodes W) .fst ⟩) (sym qx) (key∈AllCodes W ψ)

钉扎先把被记录值与递归满足集认同，val-at 再把该集合与同一键处的函数表取值认同。结论由典范码集成员关系及底层集合等式组成。虽然它本身没有命题截断，但整个依赖对本身是命题，所以可以从命题截断下的解码中得到；这并不是计算性的解码。

      in mx , ( pinned ψ y (subst (λ u → ⟨ u ∈ Tv ⟩) (cong (λ a → pr a (y .fst)) qx) h)
              ∙ sym (cong (λ p → p .fst) (val-at W W ψ x mx qx)) ) })
    (CS.key-out c c∈) })
  (Fr.onC-out hOn (down (lookup T γ) (pr (x .fst) (y .fst)) h) h)

为得到表的反向读式，从一个指定的典范码 x 出发。它在 AllCodes W 中的成员关系在命题截断下给出公式 ψ，其键就是 x。全域性随后再次在命题截断下给出该公式键处记录的某个候选值。

T-in : (x : S) (mx : ⟨ x .fst ∈ (AllCodes W) .fst ⟩) → ⟨ pr (x .fst) ((Table.val W W x mx) .fst) ∈ Tv ⟩
T-in x mx = rec₁ ((pr (x .fst) ((Table.val W W x mx) .fst) ∈ Tv) .snd)
  (λ { (k , ψ , e) → rec₁ ((pr (x .fst) ((Table.val W W x mx) .fst) ∈ Tv) .snd)
    (λ { (y , my) →
      subst (λ u → ⟨ u ∈ Tv ⟩)

候选值被钉扎到递归满足集，值引理把它与函数表值对齐；成员关系随即沿有序对等式搬运。两次消去都落在表成员关系这一命题上。

        (cong₂ pr (sym e) (pinned ψ y my ∙ sym (cong (λ p → p .fst) (val-at W W ψ x mx e))))
        my })
    (sub ψ) })
  (AllCodes-out W x mx)

完备性与两种读法

完备性从具体的语义对象出发，而不是从任意候选出发。环境中的四个槽分别与 W、真实图 SatGraph.pairs W、典范码集 AllCodes W、真实塔 Tower.tower W 对齐，十个标签也被固定。这些对齐是前提，不是有界子句的结论。

module SatHolds {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m) (W : S)
  (qw : (lookup w γ) .fst ≡ W .fst) (qT : (lookup T γ) .fst ≡ (SatGraph.pairs W) .fst)
  (qC : (lookup C γ) .fst ≡ (AllCodes W) .fst) (qE : (lookup E γ) .fst ≡ (Tower.tower W) .fst)
  (tg : Tags γ N) where

open Alphabet W

记表槽与码域槽中的底层集合为 Tv 与 Cv。对齐 qT 与 qC 把它们的成员关系事实分别搬运到真实图与典范码集中。因此，已呈现的表配对可以用真实图的读式处理，而公式码的解码仍只在命题截断下成立。下面每条等式依然只比较底层层级集合。

open Bridge W
private
  Tv = (lookup T γ) .fst
  Cv = (lookup C γ) .fst

在与公式键同一视的码处的表值，等于该公式的递归满足集。证明从真实满足图读出该对，沿「被呈现键与公式键」的同一视搬运第二分量，最后以值引理收尾。

  val≡ : ∀ {n} (ψ : Formula Ab n) (c yc : S) → c .fst ≡ (keyS W ψ) .fst
       → ⟨ pr (c .fst) (yc .fst) ∈ Tv ⟩ → yc .fst ≡ (SatW ψ) .fst
  val≡ ψ c yc qc h =
    let p = SatGraph.pairs-out W c yc (subst (λ u → ⟨ pr (c .fst) (yc .fst) ∈ u ⟩) qT h)
    in p .snd ∙ cong (λ p → p .fst) (SatGraph.valOf≡ W c (p .fst)) ∙ cong (λ p → p .fst) (val-at W W ψ c (p .fst) qc)

若码域元素呈现为 pr (# n) z，把它搬入 AllCodes W 后便可在命题截断下解码：存在某条公式 ψ : Formula Ab n，其载荷为 z。这里既没有选定公式，也没有解码唯一性，因而没有定义出解码函数。

  decode : (c : S) → ⟨ c .fst ∈ Cv ⟩ → (n : ℕ) (z : V ℓ) → c .fst ≡ pr (# n) z
         → ∥ Σ[ ψ ∶ Formula Ab n ] (z ≡ cd ψ) ∥₁
  decode c c∈ = Match.decodeAll W c (subst (λ u → ⟨ c .fst ∈ u ⟩) qC c∈)

对候选码 c，它与典范码集的对齐使 c 成为真实图的合法输入。真实图在此码处的取值给出一个表项，再沿 Tv 与 SatGraph.pairs W 的对齐搬回。所得存在陈述仍处在命题截断下，恰好符合全域性子句的要求。

  tot : (c : S) → ⟨ c .fst ∈ Cv ⟩ → ∥ Σ[ yc ∶ S ] ⟨ pr (c .fst) (yc .fst) ∈ Tv ⟩ ∥₁
  tot c c∈ =
    let mx = subst (λ u → ⟨ c .fst ∈ u ⟩) qC c∈
    in ∣ SatGraph.valOf W c mx , subst (λ u → ⟨ pr (c .fst) ((SatGraph.valOf W c mx) .fst) ∈ u ⟩) (sym qT) (SatGraph.pairs-in W c mx) ∣₁

真实图还给出任意表元素所需的形状。在命题截断下，每个这样的元素都是某个码与其图取值组成的编码对，而且该码属于 Cv。这只是存在性的分解，并没有为每个元素选定分量。

  onc : (e : S) → ⟨ e .fst ∈ Tv ⟩
      → ∥ Σ[ c ∶ S ] Σ[ yc ∶ S ] ((e .fst ≡ pr (c .fst) (yc .fst)) × ⟨ c .fst ∈ Cv ⟩) ∥₁
  onc e e∈ = map₁
    (λ { (x , mx , ee) → x , SatGraph.valOf W x mx , (ee , subst (λ u → ⟨ x .fst ∈ u ⟩) (sym qC) mx) })
    (SatGraph.pairs-shape W e (subst (λ u → ⟨ e .fst ∈ u ⟩) qT e∈))

SatHoldsC.holds 的各项输入分工明确。真实环境塔提供环境行，val≡ 识别真实公式键处的取值，decode 只从具有指定形状的码中解出经命题截断的公式，tot 与 onc 则建立两条定义域条件。结构论证随后验证全部十条构造子子句。它每次使用经命题截断的元数、公式或分解时，都只把见证消去到「相应子句得到满足」这一命题中，不会产生全局解码器或表取值的选择。

holds : ⟨ γ ⊨ tableAt T w C E N ⟩
holds = SatHoldsC.holds W T w C E N γ qw tg
  (TowerHolds.holds E w (N f0) γ W qw qE (tg f0)) val≡ decode tot onc

密封公式 satAt 封装三条彼此独立的描述：towerAt、codesAt 与 tableAt。环境塔分量接收标签槽 N f0，Tags 把该槽识别为数码零；码域分量与表分量则接收完整的十槽族 N。这项合取本身不会给出候选对象与典范环境塔、码集或满足关系图之间的等式。

opaque
  satAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
  satAt T w C E N = towerAt E w (N f0) ∧̇ (codesAt C w E N ∧̇ tableAt T w C E N)

后续论证可以把 satAt 当作一个完整的有界谓词，无需反复展开它的三个分量。检查它是否属于 Lévy 层级等句法性质时，定义只在受控范围内展开；语义上的使用则通过下面的投影与完备性结果进行。不透明性只标出这道证明边界，并不增加任何模型论性质。

opaque
  unfolding satAt

证书 Δ₀-satAt 利用有界片段对合取的封闭性，把三个分量的证书组合起来。它只建立 satAt 的句法有界性，尚未说明哪些集合满足该公式。后面的 SatRead 与 sat-complete 才分别提供语义上的两个方向。

  Δ₀-satAt : ∀ {m} (T w C E : Fin m) (N : Fin 10 → Fin m) → Δ₀ (satAt T w C E N)
  Δ₀-satAt T w C E N = δ-∧ (Δ₀-towerAt E w (N f0)) (δ-∧ (Δ₀-codesAt C w E N) (Δ₀-tableAt T w C E N))

从 satAt 的证明中可以取回可靠性所需的三项精确前提：环境塔描述、码域描述与表描述。这一投影不增加语义结论，也不给出候选对象与典范对象的等式。

  satAt-out : ∀ {m} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m)
            → ⟨ γ ⊨ satAt T w C E N ⟩
            → ⟨ γ ⊨ towerAt E w (N f0) ⟩ × (⟨ γ ⊨ codesAt C w E N ⟩ × ⟨ γ ⊨ tableAt T w C E N ⟩)
  satAt-out T w C E N γ h = h

反过来，这三项描述的证明组合起来便得到 satAt。这一构造只是合取：每个分量都必须独立给出，表子句不能补偿缺失的塔子句或码域子句。

  satAt-in : ∀ {m} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m)
           → ⟨ γ ⊨ towerAt E w (N f0) ⟩ → ⟨ γ ⊨ codesAt C w E N ⟩ → ⟨ γ ⊨ tableAt T w C E N ⟩
           → ⟨ γ ⊨ satAt T w C E N ⟩
  satAt-in T w C E N γ hE hC hT = hE , (hC , hT)

SatRead 是面向可靠性方向的候选对象接口。只有工作集槽已与 W 对齐、Tags 已校准数码槽且候选对象满足 satAt 时，它才适用，并公开上文证得的六条精确向外与向内规则。这些规则保留原有的结论形状：该接口既不把它们改写成笼统的集合等式，也不暴露选定的解码结果或见证。

module SatRead {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m) (W : S)
  (qw : (lookup w γ) .fst ≡ W .fst) (tg : Tags γ N) (h : ⟨ γ ⊨ satAt T w C E N ⟩) where

private module SS = SatSound T w C E N γ W qw tg
          (satAt-out T w C E N γ h .fst) (satAt-out T w C E N γ h .snd .fst) (satAt-out T w C E N γ h .snd .snd)

对码而言，两个方向比较其与 AllCodes W 的成员关系。对塔条目而言，两个方向读取或插入标准有序对 pr (# k) (envSet W k)。对表项而言，它们把一个已呈现的有序对与典范码处的函数表取值比较。保持这三类结论的形状彼此有别，可以避免无依据的更强唯一性主张。

open SS public using ( C-out; C-in; E-out; E-in; T-out; T-in )

反向定理假设四个槽已经呈现预定对象：W、它的满足关系图、完整码集与环境塔；同时还假设十个正确的数码标签。这些对齐是完备性的输入数据，并不是从 satAt 中恢复出来的。

sat-complete : ∀ {m} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m) (W : S)
             → (lookup w γ) .fst ≡ W .fst
             → (lookup T γ) .fst ≡ (SatGraph.pairs W) .fst
             → (lookup C γ) .fst ≡ (AllCodes W) .fst
             → (lookup E γ) .fst ≡ (Tower.tower W) .fst

结论是这个已对齐环境对 satAt 的满足证明。证明先由 qw、qE、qC 与已校准的标签填入环境塔分量和码域分量；这些对齐在整个论证中始终是前提。此步不会引入新环境塔、码集或图的存在见证，也不主张每个满足 satAt 的四元组都唯一地等于典范四元组。

             → Tags γ N → ⟨ γ ⊨ satAt T w C E N ⟩
sat-complete T w C E N γ W qw qT qC qE tg =
  satAt-in T w C E N γ
    (TowerHolds.holds E w (N f0) γ W qw qE (tg f0))
    (CodesHolds.holds C w E N γ W qw qC qE tg)

最后一行重用 SatHolds.holds 来填入表这一合取项。如上所证，它建立的是 tableAt 的全部内容，即两条定义域条件与十条构造子子句，而不只是后十条子句。satAt-in 再把它与环境塔合取项、码域合取项组合起来。因此，sat-complete 是把已对齐的典范数据写入有界描述的方向；表证明内部使用的命题截断解码不会对外给出全局解码器或选定取值。

    (SatHolds.holds T w C E N γ W qw qT qC qE tg)