描述满足关系表

对象语言不能直接调用宿主语言中关于公式的递归，因此需要用有界方式描述该递归应产生的图。本章把 T 视为由公式键与环境集组成的候选关系，并追问每个匹配条目应服从哪些局部方程。答案由十条构造子子句和关于 T 第一投影的两项条件组成；语义正确性、唯一性、码域闭包以及典范数据的存在都还需要后续论证。

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

这项描述涉及两个层次。Agda 提供检查构造的元理论，而下文构造的公式属于可构造结构的一阶对象语言。本章不假设排中律：它只用直觉主义有效的运算组合公式，并证明一项句法有界性陈述。

open import Base.Prelude
module L.Coding.SatisfactionClauses {ℓ : Level} where

带有 j 个自由槽的公式，要在这些槽取得可构造载体中的元素后才得到解释。隶属、相等、命题联结词与有界量词足以表述下文全部子句。末尾的 Δ₀ 见证只涉及这种对象语言构文；它本身既不解释子句，也不给出子句中的任何见证。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; Term; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊤̇; ⊥̇; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀ )
open import L.Constructible {ℓ} using ( 𝒮ʟ )

候选关系借助编码有序对来表达。全章由三种形状组织：环境塔条目把元数 ar 与环境集 F 配对；公式键把同一元数与带标签的载荷配对；T 的成员再把该键与候选值集配对。有界配对读式暴露这些分量，而后继谓词与 cons 谓词分别描述元数提升和编码环境的延拓。

open import L.Coding.Model {ℓ} using ( prAtL )
open import L.Coding.Expressions {ℓ} using ( sucAtL; consAtL )
open import L.Coding.Quantification {ℓ} using
  ( f0; f1; i0; i1; i2; i3; i4; i5; i6; i8; i9; i11; i12; i14; i16; i17; i19; sh
  ; sndEx; sndAll; bothEx; bothAll; bigAnd )

公式构造子恰有十个位置，由 Fin 10 索引。把这样的索引转换为自然数，就能让同一个族分派到相应子句。此处标签槽中存放的值仍只是任意参数；后续的 Tags 假设才会把每个槽与预期的标准数码同一视。

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.Unit using ( tt )

对象语言的所有变元都在可构造结构的载体 S 上取值。T、C 或 w 这样的槽只命名赋值中的位置；经过求值后，该位置才指称一个可构造集。区分这两层，可以避免把句法子句误当成在元理论中构造满足关系表或码集。

open hPropStructure 𝒮ʟ using ( S )

表框架及其十条子句

第一个可复用思想是精确的外延条件。给定候选集 y、参照集 F 与性质 φ，extB 的前半部说 y 的每个成员都属于 F 且满足 φ，因而给出一个包含方向；后半部说 F 中每个满足 φ 的成员都属于 y，给出反向包含。因此，extB 把 y 外延刻画为 F 中由 φ 截出的子集，但既不构造这个集合，也不断言它存在。

extB : ∀ {j} → Fin j → Fin j → Formula S ( + j) → Formula S j
extB y F φ = ∀̇∈ (var y) ((var i0 ∈̇ var (sh  F)) ∧̇ φ)
           ∧̇ ∀̇∈ (var F) (φ ⇒̇ (var i0 ∈̇ var (sh  y)))

当编码对的第二分量 v 已知时，fstAll 在配对编码所用的容纳集合中作全称遍历。只要配对谓词识别出一个候选第一分量，主体就必须在把该分量加入赋值后成立。两层有界全称服务于有序对的集合论表示；数学上，这只是对第一分量的一次带守卫读取，并作用于每一种可能分解。

fstAll : ∀ {j} → Fin j → Fin j → Formula S ( + j) → Formula S j
fstAll x v body = ∀̇∈ (var x) (∀̇∈ (var i0) (prAtL (sh  x) i0 (sh  v) ⇒̇ body))

公式递归首先需要同元数读取。subAt T ar a body 要求：对于 T 中键为配对 (ar,a) 的每个条目，body 都成立。它是关于全部匹配条目的全称蕴涵，因此既不选取条目，也不证明取值唯一。若该键没有条目，条件可能真空成立；后续要取得条目，还需同时使用全定义性以及子键属于码域的独立证明。

subAt : ∀ {j} → Fin j → Fin j → Fin j → Formula S ( + j) → Formula S j
subAt T ar a body = ∀̇∈ (var T) (bothAll i0 (prAtL i1 (sh  ar) (sh  a) ⇒̇ body))

量化公式的主体多出一个可用变元，因此递归读取必须改变元数。subSucAt T ar a body 考察键为 (ar',a) 的每个表条目，并加入守卫 ar' = suc ar；只有满足该守卫时才要求 body。与同元数读式一样，条目及其分解都受全称量化。该公式既不选择 ar' 或某个取值，也不保证提升后的子键出现在 T 中。

subSucAt : ∀ {j} → Fin j → Fin j → Fin j → Formula S ( + j) → Formula S j
subSucAt T ar a body =
  ∀̇∈ (var T) (bothAll i0 (fstAll i1 (sh  a) (sucAtL (sh  ar) i0 ⇒̇ body)))

词项求值有两种码形状。tmIs t z v N0 N1 说：t 或是携带 v 的常元码，或是携带索引 i 的变元码，并且编码环境 z 含有图条目 (i,v)。析取和变元索引见证都在命题截断下解释。此外，在后续 Tags 假设把 N0、N1 与零号、一号数码同一视之前，它们只是标签槽；对于任意多值关系 z，同一个变元码可能验证多个候选值。

tmIs : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Fin j → Formula S j
tmIs t z v N0 N1 =
  prAtL t N0 v ∨̇ sndEx t N1 (∃̇∈ (var (sh  z)) (prAtL i0 i1 (sh  v)))

下文五种构造子关系共享三个参数：候选关系 T、载体界限 w 与十个标签槽组成的族 N。局部名称 N0、N1 只把前两个标签槽移过新绑定的变元。这项簿记保持槽位指称不变，并不添加把它们识别为标准数码的等式。

module Rel {m : ℕ} (T w : Fin m) (N : Fin  → Fin m) where
  private
    N0 N1 : ∀ {j} → Fin (j + m)
    N0 {j} = sh j (N f0)
    N1 {j} = sh j (N f1)

读出两个子公式取值 ya、yb 后，二元子句要判断同一个编码环境 z 与它们的关系。两个命题就是 z ∈ ya 与 z ∈ yb，参数 op 再把它们组合起来。把 op 分别实例化为合取、析取或蕴涵，就会保留相应极性，而不会把三种联结词压成同一种条件。

  binBody : (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S ( + m)
  binBody op = op (var i0 ∈̇ var i5) (var i0 ∈̇ var i1)

对于被编码公式中的非有界量词，描述公式用 w 作为显式界限。当 q 实例化为 ∃[]-syntax 时，它只在命题截断下断言某个 x ∈ w 可行；当 q 实例化为 ∀[]-syntax 时，每个 x ∈ w 都必须可行。无论哪种情形，内层条件都只要求命题截断地存在主体取值集中的编码延拓 e'，使 e' 由把 x cons 到 z 前端得到；这里不会给出全局选定的延拓函数。

  quBody : (∀ {j} → Term S j → Formula S (suc j) → Formula S j) → Formula S ( + m)
  quBody q = q (var (sh  w)) (∃̇∈ (var i4) (consAtL i0 i1 i2))

有界量词还必须求出界词项的值。全称情形以 ∀[]-syntax 配合蕴涵，要求 tmIs 验证的每个候选值 v，以及 w 中属于 v 的每个 x，都有一个命题截断地存在于主体取值集中的编码延拓。存在情形则以 ∃[]-syntax 配合合取，只要求命题截断地存在这样的 v、x 与延拓。若编码环境关系是多值的，这两种极性仍有实质差别；本子句不会修复该关系，也不证明词项值唯一。

  bqBody : (∀ {j} → Term S j → Formula S (suc j) → Formula S j)
         → (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S ( + m)
  bqBody q c =
    q (var (sh  w)) (c (tmIs i9 i1 i0 N0 N1)
      (q (var (sh  w)) (c (var i0 ∈̇ var i1) (∃̇∈ (var i5) (consAtL i0 i1 i3)))))

原子公式不对子公式作递归。它的载荷由两个词项码组成，因此原子主体只在命题截断下要求存在两个由 tmIs 验证的值 v,x ∈ w，再在其上检验指定的原子关系。隶属情形使用 v ∈ x，相等情形比较 v 与 x；词项值直接来自常元或变元码形状，而不是来自 T 的条目。

  atomBody : Formula S ( + m) → Formula S ( + m)
  atomBody rel =
    ∃̇∈ (var (sh  w)) (∃̇∈ (var (sh  w))
      (tmIs i4 i2 i1 N0 N1 ∧̇ (tmIs i3 i2 i0 N0 N1 ∧̇ rel)))

假命题给出最简单的外延方程。它的性质不可能成立，所以正向包含说明候选值 yc 没有成员；反向包含则因 F 中没有成员能满足假命题而立即成立。因此，这条子句把 yc 刻画为空，却不构造空值或表条目。

  botRel : Formula S ( + m)
  botRel = extB i0 i8 ⊥̇

对于二元联结词，载荷先分解为两个公式码 a、b。随后，两次同元数读取遍历 T 中与子键 (ar,a)、(ar,b) 匹配的每个取值。对于所得子值的每一种组合，extB 都借助二元主体刻画 yc。因此，多值候选关系会对所有组合施加方程；这个关系构造子既不假设子值存在，也不假设它们唯一。

  binRel : (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S ( + m)
  binRel op =
    bothAll i3 (subAt (sh  T) i12 i1 (subAt (sh  T) i16 i4 (extB i11 i19 (binBody op))))

非有界量化公式的载荷就是其主体码。该关系只在后继元数处读取这个码，再用 extB 比较候选值与满足量词主体的环境。被编码量词在语义上遍历整个预期载体，而描述公式则以显式集合 w 为界遍历；正因如此，描述仍保持有界。

  quRel : (∀ {j} → Term S j → Formula S (suc j) → Formula S j) → Formula S ( + m)
  quRel q = subSucAt (sh  T) i9 i3 (extB i6 i14 (quBody q))

有界量词的载荷是由界词项码与主体码组成的配对 (t,a)。只有 a 会在后继元数处接受递归读取；t 则由 tmIs 在局部求值。两个参数随后给出精确极性：有界全称使用 ∀[]-syntax 配合蕴涵，有界存在使用 ∃[]-syntax 配合合取。

  bqRel : (∀ {j} → Term S j → Formula S (suc j) → Formula S j)
        → (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S ( + m)
  bqRel q c = bothAll i3 (subSucAt (sh  T) i12 i0 (extB i9 i17 (bqBody q c)))

对于原子载荷，配对读式暴露两个词项码，extB 再把原子主体用于 F 中每个候选编码环境。这里不会从 T 读取任何子键。这一区分反映了语法树：公式沿直接子公式递归，而这个很小的词项语言则直接按两种码形状解释。

  atomRel : Formula S ( + m) → Formula S ( + m)
  atomRel rel = bothAll i3 (extB i3 i11 (atomBody rel))

前四个标签给出四种精确真值条件。在 Tags 校准标签槽之后，标签 0 是隶属原子：若 v 与 x 分别是第一、第二个词项的值，则要求 v ∈ x。标签 1 是相等原子，要求 v = x。标签 2、3 分别用合取与析取组合两个同元数子公式的断言 z ∈ ya 与 z ∈ yb。在校准之前，这些只是由相应标签槽选出的子句，不能据此断言槽中已经放置标准数码。

  relN : ℕ → Formula S ( + m)
  relN  = atomRel (var i1 ∈̇ var i0)
  relN  = atomRel (var i1 ≐ var i0)
  relN  = binRel _∧̇_
  relN  = binRel _∨̇_

标签 4 给出余下的二元极性：z ∈ ya 从左子公式向右子公式蕴涵 z ∈ yb。标签 5 使假命题具有空外延。标签 6、7 都在后继元数处读取一个主体；标签 6 在 w 上使用 ∃[]-syntax，标签 7 使用 ∀[]-syntax。标签 8 是有界全称。对每个 v ∈ w，tmIs 作为前件验证 v 是界词项的值；随后对每个 x ∈ w，成员关系 x ∈ v 又作为前件，要求命题截断地存在主体取值集中的编码延拓。

  relN  = binRel _⇒̇_
  relN  = botRel
  relN  = quRel ∃̇∈
  relN  = quRel ∀̇∈
  relN  = bqRel ∀̇∈ _⇒̇_

标签 9 具有存在极性。它用 ∃[]-syntax 配合合取，只要求命题截断地存在由 tmIs 验证的某个 v ∈ w、满足 x ∈ v 的某个 x ∈ w，以及主体取值集中的某个编码延拓。至此得到编号 0 至 9 的十种情形。对不小于 10 的自然数，relN 返回真；但最后这条方程不会给表规格增加任何情形，因为当 k : Fin 10 时，toℕ k 必在 0 至 9 之间。

  relN  = bqRel ∃̇∈ _∧̇_
  relN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) = ⊤̇

现在可以把构造子关系放入共同框架。需要连接的数据包括一个环境塔配对、一个具有相同元数与带标签载荷的公式码，以及 T 在该码处的候选条目。这里复用同一个局部关系模块，使每个标签都在相同的 T、w 与两个词项码标签解释下接受判断。

module Clause {m : ℕ} (T w C E : Fin m) (N : Fin  → Fin m) where
  private
    module R = Rel T w N

固定 k 后，子句沿一条精确链条展开。它考察每个 q ∈ E 及其每种分解 q=(ar,F)；每个满足 c=(ar,p) 的 c ∈ C；每种分解 p=(N k,r)；以及每个满足 e=(c,yc) 的 e ∈ T。在每个完整匹配的框架上，yc 都必须满足 relN (toℕ k)。每次分解都由全称蕴涵守卫，因此该子句并不断言这些框架数据存在。它也只把 F 与 N k 当作给定值，并不把它们认同为真实环境集或 k 对应的数码。

  clause : Fin  → Formula S m
  clause k =
    ∀̇∈ (var E) (bothAll i0 (∀̇∈ (var (sh  C)) (sndAll i0 i2 (sndAll i0 (sh  (N k))
      (∀̇∈ (var (sh  T)) (sndAll i0 i5 (R.relN (toℕ k))))))))

两条定义域条件补充全称局部子句本身没有给出的存在性。total 说：对于每个 c ∈ C，命题截断地存在 yc，使 (c,yc) ∈ T；表成员及其配对分解都留在命题截断内。反过来，onC 说每个 e ∈ T 都命题截断地分解为 (c,yc)，且 c ∈ C。二者合起来把 T 的第一投影定义域确定为 C，但不给出选择函数，也不使 T 成为单值关系。

  total onC : Formula S m
  total = ∀̇∈ (var C) (∃̇∈ (var (sh  T)) (sndEx i0 i1 ⊤̇))
  onC = ∀̇∈ (var T) (bothEx i0 (var i1 ∈̇ var (sh  C)))

十条局部子句由一个有限合取收集。参数 9 意味着索引类型是 Fin (suc 9)，也就是 Fin 10，并没有漏掉一种情形。普通合取与这个有限合取都不会在各子句已有的命题截断之外引入新的命题截断。

  ten : Formula S m
  ten = bigAnd  clause

公式 tableAt 现在合取三项要求：在 C 上经过命题截断的全定义性、每个表成员的键都属于 C 的限制，以及全部十条构造子子句。这是一条关于候选关系的局部有界规格。它不证明 C 对子公式码封闭，不证明 E 是预期的环境塔，不校准标签，不证明取值唯一，也不把候选关系认同为典范满足关系表。后续章节会分别给出环境塔与码域描述、标签校准、语义桥接和钉扎论证，从而把适当候选对象与典范数据联系起来。

tableAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
tableAt T w C E N = Clause.total T w C E N ∧̇ (Clause.onC T w C E N ∧̇ Clause.ten T w C E N)

最后，结构检查器给出 tableAt 属于 Δ₀ 的见证。每一处看似搜索的量化都受 T、C、E、w、某个配对容纳集合或候选值集限制，因此描述公式没有引入非有界量词。这个结论只分类句法：它既不证明合适的表存在，也不证明任何候选对象满足这些子句，更不建立语义正确性、绝对性或完备性定理。

Δ₀-tableAt : ∀ {m} (T w C E : Fin m) (N : Fin  → Fin m) → Δ₀ (tableAt T w C E N)
Δ₀-tableAt T w C E N = checkΔ₀ (tableAt T w C E N) tt

小结

公式 tableAt 是 total、onC 与由 ten 收集的十条局部构造子子句之合取。其中，total 只给出 C 中每个码的表取值在命题截断下的存在性；onC 把第一投影定义域限制为 C；十条子句则施加全称的局部外延方程。定理 Δ₀-tableAt 只证明这份描述在句法上有界。

后续论证仍需把 E 认同为预期环境塔，证明 C 含有所需的子公式码，通过 Tags 校准标签槽，并建立双向语义读式、钉扎与完备性，才能得到典范图与总体谓词 satAt。这些结论以及满足关系表或全局选定的取值都不是本章构造的对象。