码化递归所用的公式表达式

码化的满足关系递归要在 L 内部判定形如「环境 γ 是否满足码 c 所示公式」的问题。要用有界公式识别 Kuratowski 对这样的复合取值，其见证本身必须是模型元素。对分量 u、v 的配对 q，需要一个可构造集合 s，使 s 属于 q，而 u、v 属于 s；读式一次性绑定这三者，并在「v, u, s 接原赋值」的扩展赋值中求取两个分量条件，原槽位在移位下保持不变。

本章把这件事一次做好：在由赋值槽位、可构造字面常元、数码与 Kuratowski 对组成的小表达式语言上建立一条结构读式，并证明其双向充分性。向外方向从满足判断出发，把三层截断存在消去到取值为命题的路径中，再将配对等式与递归的分量路径串联。向内方向为两个子表达式选定显式的内部元素，并取得它们共同的可构造容器，而不从任何截断中抽取选择。

同一读式随后沿几个方向特化。表达式取值属于词项所指的隶属关系使用 L 的传递性：该周遭取值属于词项的可构造解释这一事实证明了取值可构造，故它能充当模型元素；这是一次真正的构造，与「截断只能消去到取值为命题的目标」这一限制不同。外延集合描述是一对普通的全称蕴含，外层没有截断；它刻画一个候选集合，而不构造它。元数标签识别器读取两层嵌套的配对：元数与「标签加载荷」之对。最后，后继公式与环境扩展公式经有界绝对性抬升，其转换立足于既有的传递模型设置，以及查值在投影下的相容性。本章以环境扩展公式收尾。

要让复合集合取值的一阶描述留在有界片段中，固定部件由常元命名，每个见证都受集合界定。这里的一切都固定在一个层 ℓ 上：周遭层级是 V ℓ，有界量词所遍历其元素的模型，是栖身于其中的可构造模型。由于满足判断比较的是真值，这些公式所断言的事实便是hProp (ℓ-suc ℓ) 中的命题。

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

open import Base.Prelude

module L.Coding.Expressions {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

一条区分的两面贯穿全章。在层级之外，结构 𝒮ᵥ 在 V ℓ 上解释一阶语言，那里的 Kuratowski 配对正是运算 pr。在模型之内，同一语言被重新解释于可构造集合之上。因此，识别复合取值的一条子句必须能同时在两处读出；而下面的每条充分性陈述说的恰是这件事：内部公式在模型中读出的真值，作为一条路径，被等同于关于 pr 与投影赋值的相应周遭陈述。

open import FOL.Syntax
  using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _⇒̇_; ∀̇_; ∃̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )

可构造模型的一个元素是「周遭集合连同它可构造的证明」。L 的传递性使有界见证能在两侧之间移动：由 isL-trans，可构造集合的成员本身可构造，因而自己就能充当模型元素。有界绝对性则为公式做相应的工作：一条关于层级、且所有常元都命名可构造集合的 Δ₀ 公式，在 L 内意义不变；BoundedFo 数据记录的常元有界性正是这一转换所需的前提。后继公式与环境扩展公式已在层级一侧证得，把它们抬入模型只需施用这一转换。

open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import FOL.Manipulation.ConstantBounding using ( BoundedFo )
open import L.Absoluteness {ℓ} using ( InL; liftFo; transferFo )
open import L.Coding.Environment {ℓ}
  using ( sucAt; Δ₀-sucAt; sucAt-adequate; consAt; Δ₀-consAt; consAt-adequate

数码需要一条相容性事实。内部数码 numeralL k 在模型内实现冯·诺伊曼自然数 k，而 numeralL-fst 把它的投影与周遭的 # k 等同起来；数码子句的两个方向都依赖于此。由于若干子句要同时对有穷多个槽位量化，环境沿槽位的重标定而移动。一种逻辑形式贯穿全章：充分性陈述是由命题等价的两个蕴含得到的真值路径，而对象语言的有界量词被读作截断存在。

        ; env; cons; shiftPairAt; sgl0At; pair0At; tag0At )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )

open import Cubical.Data.Vec using ( map )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Functions.Logic using ( ⇔toPath; ∃[∶]-syntax )

周遭层级 V ℓ 是一个 h-集合，故其中两个集合的相等是命题，可以放进真值之内；这正是下文打包等式得以成立的原因。自然数以集合身份进入：# k 是层级中的冯·诺伊曼数码，sucV 是其后继运算，它既不同于任何宇宙层级，也不同于码所带的元数指标。命题截断给出单纯存在，其消去只在取值为命题的目标中合法；配对读式的向外证明将显式遵守这一限制。

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )

这里使用的真值是层 ℓ-suc ℓ 的 hProp 命题，每个都连同「它是命题」的证明打包，联结词与量词直接作用在这些命题上。模型的载体 S 由「周遭集合配可构造性证书」的对组成。绝对性机制针对这一情形一次性设立：被相对化的结构是层级 𝒮ᵥ，挑选子模型的类是 isL，传递性使 Δ₀ 公式保持绝对；满足记作 ⊨，词项解释记作 ⟦_⟧，环境是模型元素的向量。

open hPropStructure 𝒮ʟ using ( S )

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

open import L.Coding.Model {ℓ}

模型词典中有一件东西对主要构造至关重要：配对形状的事实。模型的配对 prʟ 经 prʟ-fst 投影为周遭配对，其有界读式是 prAtL；记录 Container 连同 container 为等于某个对的取值造出一个容纳两个分量的可构造集合。用有界公式读取一个对，需要的恰是这样的中间集合；而 lookup-fst 与 envOverAt 则是同一词典中稍后用到的投影与环境事实。

  using ( lookup-fst; prʟ; prʟ-fst; prAtL; prAtL-adequate; envOverAt
        ; Container; container )

模型中的有界量词遍历 S 的元素，因此公式要识别的任何复合取值，都必须能由本身是模型元素的有界见证来匹配。本节建立一般工具：一个归纳语言 Expr，其取值由赋值槽位、可构造字面常元、数码与 Kuratowski 对组装而成；连同一条把表达式变成公式的结构读式，以及一个双向的充分性定理，它把公式的含义与表达式所指的值等同起来。本章其余的一切都是这一读式的特例。

本节以两件小准备开篇。PairIs a p 把「周遭取值 a 等于 p」这一陈述打包成真值：由于层级是 h-集合，该相等类型是命题，与 setIsSet 配对后便是 hProp (ℓ-suc ℓ) 的元素。此后充分性陈述都将沿路径把满足判断与这些打包的等式相比较。表达式语言本身以自然数 n 为指标，确定可用的自由变元槽位数；某个槽位完全可以不被使用。

private
  PairIs : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
  PairIs a p = (a ≡ p) , setIsSet a p

module PairExpression where
  data Expr (n : ℕ) : Type (ℓ-suc ℓ) where

表达式语言由四个构造子确定，每个构造子对应复合取值向公式呈现自身的一种方式。slot i 引用周遭赋值的第 i 项，相当于变元；literal a 一次性命名模型的一个完整元素，连同其可构造性证书，故其行为如对象语言常元；numeral k 命名冯·诺伊曼自然数 k；pair 把两个子表达式合成一个 Kuratowski 对。表达式是取值的有穷描述，本身不是集合，因此它容许两种独立的读法，而目标正是证明二者一致。

    slot : Fin n → Expr n
    literal : S → Expr n
    numeral : ℕ → Expr n
    pair : Expr n → Expr n → Expr n

  value : ∀ {n} → Expr n → (Fin n → V ℓ) → V ℓ

第一种读法是周遭的。给定把层级集合指派给各槽位，value 计算表达式所指的集合：槽位按查值，字面常元经 fst 投影掉其证书，数码变为 # k，配对则是两个所指集合的 Kuratowski 对 pr。充分性定理将在右侧恢复的正是这种读法：一条有界公式的意义，就在于从模型内部识别出一个天然描述于外的取值。

  value (slot i) γ = γ i
  value (literal a) γ = fst a
  value (numeral k) γ = # k
  value (pair a b) γ = pr (value a γ) (value b γ)

  element : ∀ {n} → Expr n → (Fin n → S) → S

第二种读法停留在模型内部。给定把 S 的元素指派给各槽位，element 计算出一个 S 的元素：字面常元本就是带证书的模型元素，数码用内部数码 numeralL，配对由模型自己的配对 prʟ 生成。两种读法逐条款平行，而这种平行性正是二者之间的桥梁可证的原因：比较它们时只需逐情形对应地比。

  element (slot i) γ = γ i
  element (literal a) γ = a
  element (numeral k) γ = numeralL k
  element (pair a b) γ = prʟ (element a γ) (element b γ)

  element-fst : ∀ {n} (e : Expr n) (γ : Fin n → S)

桥梁是 element-fst：投影一个内部元素，作为一条路径，恰好等于在投影后赋值处的周遭取值。对槽位与字面常元，两种读法逐字重合，故证明即 refl。数码是第一个实质情形：其内部形式经 numeralL-fst 投影为周遭形式，这正是数码一章给出的内部数码与周遭数码之间的相容性事实。注意方向，它将贯穿全章：路径从内部取值的投影出发，指向周遭取值。

              → fst (element e γ) ≡ value e (λ i → fst (γ i))
  element-fst (slot i) γ = refl
  element-fst (literal a) γ = refl
  element-fst (numeral k) γ = numeralL-fst k
  element-fst (pair a b) γ = prʟ-fst (element a γ) (element b γ)

配对情形把两条独立的相容性串联起来：模型的配对经 prʟ-fst 投影为周遭配对，而每个分量的投影律正是递归的事实。在 pr 之下的同余把两条分量路径合成一条，嵌套表达式的投影律便由归纳成立。在语法一侧，lift3 是配对读式所需的重标定：它把每个旧槽位上移三位，即 lift3 ρ i = suc (suc (suc (ρ i)))，既保留每个槽位所指的旧条目，又为三个新变元腾出位置。

    ∙ cong₂ pr (element-fst a γ) (element-fst b γ)

  lift3 : ∀ {n m} → (Fin n → Fin m) → Fin n → Fin ( + m)
  lift3 ρ i = suc (suc (suc (ρ i)))

  read : ∀ {n m} → Expr n → (Fin n → Fin m) → Fin m → Formula S m
  read (slot i) ρ q = var q ≐ var (ρ i)

读式 read 把槽位 q 处的表达式变成一条有界公式。槽位要求与相应的重标定变元相等，字面常元要求与其常元相等，数码要求与命名其内部数码的常元相等。配对情形才有数学内容：它用三条有界存在绑定 q 处集合中的集合 s，以及 s 中的元素 u、v，使 s 属于 q 处的条目，而 u、v 属于 s；再借模型的配对读式 prAtL 断言 q 处的条目等于对 pr u v。随后在移位槽位处递归读出两个分量条件，这正是 lift3 所提供的。于是，一个复合取值是从模型内部、经由一个容纳两个 Kuratowski 分量的可构造中间集合来识别的。

  read (literal a) ρ q = var q ≐ con a
  read (numeral k) ρ q = var q ≐ con (numeralL k)
  read (pair a b) ρ q = ∃̇∈ (var q) (∃̇∈ (var zero) (∃̇∈ (var (suc zero))
    (prAtL (suc (suc (suc q))) (suc zero) zero
      ∧̇ (read a (lift3 ρ) (suc zero) ∧̇ read b (lift3 ρ) zero))))

充分性分为两个方向，out 是可靠性证明所用的方向：从满足判断的一个证明出发，产出「槽位 q 处的条目投影后等于所指的值」这条路径。槽位与字面常元按定义本就是这样的路径，数码情形则把前提与 numeralL-fst 复合，方向与 element-fst 相同。实质工作在配对情形，它占了接下来的两步。

  out : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
       → ⟨ γ ⊨ read e ρ q ⟩ → fst (lookup q γ) ≡ value e (λ i → fst (lookup (ρ i) γ))
  out (slot i) ρ q γ h = h
  out (literal a) ρ q γ h = h
  out (numeral k) ρ q γ h = h ∙ numeralL-fst k

配对情形的前提是一个具有三层的截断有界存在，故证明逐层消去它们，而每次消去都需要取值为命题的目标。这正是 setIsSet 进入之处：结论是层级 (一个 h-集合) 中的一条路径，因此目标是命题，消去合法。截断给了什么、没给什么，值得直说：见证 s、u、v 作为元素到达，数学可以继续使用它们，但前提断言的只是它们的单纯存在：没有唯一性，也没有被选出的代表。

  out (pair a b) ρ q γ = PT.rec (setIsSet _ _) (λ { (s , s∈ , hs) →
    PT.rec (setIsSet _ _) (λ { (u , u∈ , hu) →
      PT.rec (setIsSet _ _) (λ { (v , v∈ , p , ha , hb) →
        subst ⟨_⟩ (prAtL-adequate (suc (suc (suc q))) (suc zero) zero (v ∷ u ∷ s ∷ γ)) p
        ∙ cong₂ pr (out a (lift3 ρ) (suc zero) (v ∷ u ∷ s ∷ γ) ha)

拿到三个见证后，最内层公式由配对读式自身的充分性展开：把 p 沿 prAtL-adequate 传输，配对断言便变成等式 fst (lookup q γ) ≡ pr (fst u) (fst v)。两个递归前提随即给出分量在一号与零号槽位处的投影，即 fst u ≡ value a 与 fst v ≡ value b；再经 pr 之下的同余，右侧被改写为 pr (value a) (value b)，恰是该配对表达式的取值。内层证明因此是一次传输加一次同余。

                   (out b (lift3 ρ) zero (v ∷ u ∷ s ∷ γ) hb) }) hu }) hs })

  into : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
        → fst (lookup q γ) ≡ value e (λ i → fst (lookup (ρ i) γ)) → ⟨ γ ⊨ read e ρ q ⟩
  into (slot i) ρ q γ h = h
  into (literal a) ρ q γ h = h

逆向的 into 从裸等式出发构造满足判断的一个证明。槽位与字面常元直接可得；数码情形与 numeralL-fst 的对称复合，调转了前述相容性的方向。配对情形须一次性给出全部三个截断层，而此处并非从截断中抽取任何东西：见证是直接构造的。内部元素 u 与 v 取为重标定赋值下的 element a 与 element b，而 Container 与 container 用调整后的路径 e 造出一个同时容纳两者的可构造集合 s，连同全部隶属证书。这是对 L 传递性的一次独立运用，与上文使消去得以合法的「取值为命题」是两回事：那里消去的是截断，这里产出的是具体的元素。

  into (numeral k) ρ q γ h = h ∙ sym (numeralL-fst k)
  into {n} {m} (pair a b) ρ q γ h = ∣ s , c .snd .fst , ∣ u , c .snd .snd .fst ,
    ∣ v , c .snd .snd .snd ,
      subst ⟨_⟩ (sym (prAtL-adequate (suc (suc (suc q))) (suc zero) zero δ)) e
      , into a (lift3 ρ) (suc zero) δ (element-fst a η)

扩展赋值 δ 就是 v ∷ u ∷ s ∷ γ，它的布局就是这一构造的全部簿记：

配对公式断言 s ∈ q、u ∈ s、v ∈ s，以及 q ≡ pr u v；由于 u 位于一号槽位、v 位于零号槽位，经 lift3 后，在一号槽位处的 read a 与零号槽位处的 read b 所查询的恰是原来的槽位。每个子证明由 into 自身在移位槽位处组装，喂入被读分量的投影路径 element-fst；最后，三个嵌套的截断存在各以一个显式的 ∣_∣₁ 封口。

      , into b (lift3 ρ) zero δ (element-fst b η) ∣₁ ∣₁ ∣₁
    where
    η : Fin n → S
    η i = lookup (ρ i) γ
    u v : S

其余的局部定义记录这一构造的算术。η 把旧赋值限制到重标定后的槽位，u 与 v 是两个子表达式在其下的显式内部元素；它们是直接选定的，并非从任何截断中提取。路径 e 随后陈述：q 处的条目等于周遭配对 pr (fst u) (fst v)。它的方向很重要：前提 h 说条目等于整个配对所指的值，与分量的投影同余 element-fst 的对称复合后，得到的恰是容器构造所预期的目标。

    u = element a η
    v = element b η
    e : fst (lookup q γ) ≡ pr (fst u) (fst v)
    e = h ∙ sym (cong₂ pr (element-fst a η) (element-fst b η))
    c : Container (lookup q γ) u v

容器由路径 e 造出，其第一个分量正是所需的可构造集合 s，它是到达两个 Kuratowski 分量的公共中间体：s 是 q 处条目的成员，而 u 与 v 是 s 的成员。把 v、u、s 依次推到 γ 的最前，便得到比原来多元数三的扩展赋值 δ。此后内向构造所需的每个材料都不再是游离的元素，而是 δ 的一个条目。

    c = container (lookup q γ) u v e
    s : S
    s = c .fst
    δ : S ^ (suc (suc (suc m)))
    δ = v ∷ u ∷ s ∷ γ

两个方向组装成所宣称的形状。adequate 陈述：在 γ 处的满足判断，作为一个真值，等于「q 处条目的投影」与「周遭所指」之间打包后的等式；⇔toPath 把 out 与 into 这对蕴含变成这条路径。作为第一个应用，member e C 说表达式 e 的取值属于词项 C 的所指：它对 C 所指的成员作有界量化，并要求在该成员扩展后的赋值处成立表达式读式，其中表达式被移入首位槽位。

  adequate : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
            → (γ ⊨ read e ρ q) ≡ PairIs (fst (lookup q γ)) (value e (λ i → fst (lookup (ρ i) γ)))
  adequate e ρ q γ = ⇔toPath (out e ρ q γ) (into e ρ q γ)

  member : ∀ {n} → Expr n → Term S n → Formula S n
  member e C = ∃̇∈ C (read e suc zero)

member 的向外读式消去截断的有界存在，得到成员 x、其隶属证明 h，以及「x 的扩展赋值满足表达式读式」的证明 p。把充分性沿向外方向施于 p，得到等式 fst x ≡ value e ...；再沿这条等式搬运 h，便把 fst x 的隶属变成所指取值的隶属。目标正是隶属命题 value e ... ∈ fst (⟦ C ⟧ γ)，其第二分量给出 PT.rec 所需的命题性证明。

  member-out : ∀ {n} (e : Expr n) (C : Term S n) (γ : S ^ n)
              → ⟨ γ ⊨ member e C ⟩ → ⟨ value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ) ⟩
  member-out e C γ = PT.rec (snd (value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ)))
    (λ { (x , h , p) → subst (λ v → ⟨ v ∈ fst (⟦ C ⟧ γ) ⟩) (out e suc zero (x ∷ γ) p) h })

  member-in : ∀ {n} (e : Expr n) (C : Term S n) (γ : S ^ n)

向内读式必须给出那个成员，而表达式 e 的取值本身即可充当，只需先把它变成模型的元素。由前提它是 fst (⟦ C ⟧ γ) 的成员，而该词项的解释可构造，于是 L 的传递性给出该取值的可构造性证书：这正是 isL-trans 在此处所做的事。这里没有消去截断；证书与周遭取值组成显式的模型元素 x，作为有界存在的见证。扩展赋值处的首项按定义投影为该取值，故递归的 into 收到路径 refl。

             → ⟨ value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ) ⟩ → ⟨ γ ⊨ member e C ⟩
  member-in e C γ h = ∣ x , h , into e suc zero (x ∷ γ) refl ∣₁
    where
    x : S
    x = value e (λ i → fst (lookup i γ)) , isL-trans h (snd (⟦ C ⟧ γ))

第一个特化把一般读式变成标签识别器。tagAtL s k x 在槽位 s 处读取「数码 k 与槽位 x 配对」的表达式，因而是一条有界公式，断言 s 处的条目是 # k 与 x 处条目的有序对。递归中的码都带有一个与载荷配对的数字标签，而这正是那个形状。

tagAtL : ∀ {n} → Fin n → ℕ → Fin n → Formula S n
tagAtL s k x = PairExpression.read
  (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot x)) id s

tagAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (x : Fin n) (γ : S ^ n)
  → (γ ⊨ tagAtL s k x)

它的充分性引理无需新证明：在这一表达式处以恒等改名实例化一般充分性，其计算结果已经是「满足判断等同于投影条目与 pr (# k) 投影载荷的 PairIs」。这是全节的模式：选定一个表达式，引用 PairExpression.adequate，子句的含义便被读出。

  ≡ PairIs (fst (lookup s γ)) (pr (# k) (fst (lookup x γ)))
tagAtL-adequate s k x γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot x)) id s γ

tagPairAtL : ∀ {n} → Fin n → ℕ → Fin n → Fin n → Formula S n
tagPairAtL s k a b = PairExpression.read

第二个特化处理本身是对形式的载荷，两层配对嵌套在表达式之内。tagPairAtL s k a b 读取「数码 k 与槽位 a、b 之对配对」的表达式，故识别形如 pr (# k) (pr (entry a) (entry b)) 的条目：一个标签架在双分量载荷之上。

  (PairExpression.pair (PairExpression.numeral k)
    (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b))) id s

tagPairAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ tagPairAtL s k a b)
  ≡ PairIs (fst (lookup s γ))

充分性引理再次由一般引理直接计算而得，恢复全部三个分量：标签数码，以及投影后的两个载荷条目。嵌套完全在表达式读式内部处理；在这一层子句上，除表达式形状外什么都看不见。

      (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ))))
tagPairAtL-adequate s k a b γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.numeral k)
    (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b))) id s γ

以外延给出集合

上一节的结构读式经由 Kuratowski 配对层识别取值；而许多递归子句要说的却是「一个集合的成员是什么」。二者是同类陈述：模型中的一条一阶公式，读回周遭层级后，恰能指认槽位中的取值。本节构造外延形状。

extAt y φ 对槽位 y 中的集合断言：其成员恰为满足一元条件 φ 的对象。它的外层结构是两条无界全称量词经普通合取相连：一条从属于该集合推出 φ，一条反向。extAt 自身不引入新的命题截断，但参数 φ 是任意公式，内部可以含有自己的量词与截断存在。由于外层的证据只是普通的合取，它的两种读法就是该合取的两个投影，而它的引入也就是二者的有序对。这正是一条描述所需的强度：该公式刻画一个候选集合，对这样的集合是否存在不置一词；存在与否，属于日后给出该取值的构造的事。

该定义为候选者绑定一个新变元，整体是两条无界全称量词的合取：槽位 y 中集合的每个成员满足 φ，而每个满足者也属于该集合。外层的联结词是普通合取，extAt 不把任何一条蕴含包进截断，但条件 φ 按原样传入，可以是任何公式，内部含有量词或截断存在均可。extAt 自身固定的只是外层形状：量词之下的一对蕴含，每侧都是模型元素及其满足证明上的函数。这正是该公式得以充当描述的原因：它约束一个取值，却从不断言取值的存在。

extAt : ∀ {n} → Fin n → Formula S (suc n) → Formula S n
extAt y φ = ∀̇ ((var zero ∈̇ var (suc y)) ⇒̇ φ)
         ∧̇ ∀̇ (φ ⇒̇ (var zero ∈̇ var (suc y)))

module _ {n : ℕ} (y : Fin n) (φ : Formula S (suc n)) (γ : S ^ n) where
  extAt-out : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)

两个读式就是外层合取的两个投影。由 extAt y φ 的一个证明出发，extAt-out 取第一分量：它对每个模型元素 z 给出一条蕴含，从 fst z 属于槽位 y 处集合，到扩展环境中 φ 成立；extAt-in 取第二分量，给出反方向的同一条蕴含。两个读式都不消去截断、不选取见证、也不沿路径搬运；无论 φ 内部含有什么，在这一外层上证据就是一个有序对，而每个读式恰是它的投影。

            → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩
  extAt-out h = h .fst

  extAt-in : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)
           → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩
  extAt-in h = h .snd

引入把两个投影反向运行，就是那两条蕴含的有序对，各以函数形式给出。于是有 extAt-in-both：一个能同时建立其条件两个方向的子句，只需把两个函数配成对，便满足这条公式，外层无须再做任何事；量词或截断的工作都发生在 φ 内部，并在那里完成。这条陈述本身值得细读：它从两个函数造出满足判断的一个证明，而对「成员满足 φ 的集合是否存在」不作任何断言。这样的集合是否真的被给出，由构造取值之处决定，与此处无关。

  extAt-in-both : ((z : S) → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩)
                → ((z : S) → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩)
                → ⟨ γ ⊨ extAt y φ ⟩
  extAt-in-both f g = f , g

分两层读一个键

满足关系递归的键是一个由两层嵌套配对组装而成的集合：元数与一个码配成对，而码本身又是标签数码与载荷之对。因此用有界公式识别一个键，就意味着检查这两层配对；而结构读式本就处理任意嵌套的表达式，恰好胜任。于是下面的每条公式都是把该读式用于相应的表达式，每条充分性引理也都是 PairExpression.adequate 的相应特例。元数被有意保留为变元槽位而非固定为某个数码，因为那些会产出不同元数子公式的构造子，其子句需要谈论元数值本身。

arityTagPairAtL c ar k a b 断言槽位 c 中的集合是一个有序对：第一分量是槽位 ar 中的集合，第二分量本身又是一个配对，即数码 # k 与槽位 a、b 中集合之对的配对。定义表达式为 pair (slot ar) (pair (numeral k) (pair (slot a) (slot b)))，在恒等改名下于 c 处读取；这正是载荷为双槽位码的键的形状。

arityTagPairAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Fin n → Formula S n
arityTagPairAtL c ar k a b = PairExpression.read
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k)
      (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b)))) id c

充分性陈述把该公式的真值等同于命题 PairIs (fst (lookup c γ)) (...)，这是周遭层级中的一条路径，断言 c 处的集合等于由各槽位投影构造的嵌套 Kuratowski 对。各分量便可从右边读出：标签数码 # k 是固定的，而 ar、a 与 b 各自贡献其查得的值。由于该陈述是真理值之间的路径而非单向蕴含，后续证明可以在任一方向上用它改写。

arityTagPairAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagPairAtL c ar k a b)
  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ))
        (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ)))))

证明是 PairExpression.adequate 对同一表达式、同一改名与同一槽位的一行特例。有界见证、截断存在的消去与引入、以及沿 prAtL 充分性的搬运，都已在结构定理中一次性完成，故这里不再出现新的语义论证。双槽位载荷的情形就绪之后，单载荷变体 arityTagAtL c ar k a 以同样方式定义，唯一差别是最内层表达式是单个槽位 a，而非两个槽位之对。

arityTagPairAtL-adequate c ar k a b γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k)
      (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b)))) id c γ

arityTagAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Formula S n

主体是在恒等改名下于 c 处应用结构读式，充分性陈述同样取 PairIs 路径的形式：c 处的集合等于元数值与「# k 与 a 处的值之对」的配对。当码的载荷是单个槽位而非两个时，需要的正是这个形状，例如一个变元指标或一个子公式槽位。

arityTagAtL c ar k a = PairExpression.read
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot a))) id c

arityTagAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagAtL c ar k a)

充分性证明再次在同样的表达式与槽位上引用 PairExpression.adequate，与配对情形如出一辙。因此两个元数标签公式与两个充分性引理都立足于那一个结构定理，这正是把读式写成通用形式所得到的回报。至于恢复出的元数值之后如何使用，属于满足关系递归的子句，它们陈述于 L.Coding.SatisfactionClauses；本章给出的正是那些子句所读取的形状。

  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ)) (pr (# k) (fst (lookup a γ))))
arityTagAtL-adequate c ar k a γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot a))) id c γ

在表中查一个子码

满足关系表的一个条目记录的是：对由元数与码组成的键，满足该公式的环境之集。因此读取一个子公式的取值，意味着在对象语言内部构造那个键：把元数与子码配成对，并断言其与一个候选集合相等。在子公式自身的元数处，公式全称遍历表中条目，并以键相等作为蕴含的前件来选出相符条目；当子公式绑定变元时，同样的查表发生在下一个元数处，该元数由下一节的后继公式在内部给出见证。

一条子句的形状

递归的一条子句绑定码、其元数、其载荷分量以及表在该码处记录的取值，然后断言码的带标签形状，并在被记录的取值之间陈述一条构造子特有的条件。把子句读回去，是沿本章建立的诸充分性引理作一串改写；而组装一条子句，就是把这些改写反向运行。

正的联结词

对合取与析取而言，那条构造子特有的条件很小：码处的取值是两个子取值的逐点合取，或逐点析取，都从同一元数处的表读出。该条件之外子句所需的一切，就是上面的查表机制。

周遭环境集

envSetAt 以外延刻画描述一个集合：以一个槽位所存元数为元数、相对于另一槽位中的载体的环境之集。它刻画这个集合，而不构造它。

该定义把外延刻画施于槽位 E，条件取为环境谓词 envOverAt。这个谓词相对于一个定义域与一个值域，对单个候选环境加以分类，因此 extAt 新绑定的变元 (位于扩展环境的零号位置) 就扮演候选者的角色。定义域与值域的参数写作 suc ar 与 suc B，因为条件是在扩展环境中求值的，比公式自身绑定的槽位高一个元数。由投影 extAt-out 与 extAt-in，envSetAt E ar B 的证明恰给出一对蕴含：E 处的集合恰含那些以 ar 处记录的元数为元数、且为 B 处载体所容纳的候选环境。这条公式只描述集合；其构造发生在构造满足关系表之处。

envSetAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
envSetAt E ar B = extAt E (envOverAt zero (suc ar) (suc B))

蕴含与底

在诸逻辑子句之中，蕴含与底在取值形状上不同于正的联结词。底没有子码，并在共同的外延框架中以假为条件，故其取值为空；它仍使用框架所绑定的周遭环境集。蕴含则在该码元数处的全体环境之集上解释，故其子句必须点名那个周遭集合，并以外延方式约束它；这也正是上一节的环境之集存在的原因。蕴含写成蕴含式，而非「前件之补与后件之并」，才与hProp 上的函数空间蕴涵相合；直接使用蕴含正合构造性语义，并不调用排中律。

下一个元数

sucAtL 是断言槽位 j 中的集合等于槽位 i 中集合之 sucV 的内部公式；其充分性引理适用于任意集合，并不假定两者是数码或序数。

当子公式比原式高一个元数时，子句必须在受约束为当前元数后继的元数处查询表。层级一侧的公式 sucAt 表达这一集合等式，且不点名常元。抬升它需要 liftFo 所要求的 BoundedFo InL 参数；另一个独立定理 Δ₀-sucAt 则稍后交给 transferFo，用来证明有界绝对性。

定义为 sucAtL i j = liftFo (sucAt i j) _。由于 sucAt 不含常元，其 BoundedFo InL 参数没有非平凡的常元可构造性见证。在充分性证明中，transferFo 分别接收这个参数与 Δ₀-sucAt i j，后者才是层级一侧的 Δ₀ 证书。所得路径把满足等同于 PairIs (fst (lookup j γ)) (sucV (fst (lookup i γ)))：即槽位 j 的集合是槽位 i 集合的后继集这一命题。

sucAtL : ∀ {n} → Fin n → Fin n → Formula S n
sucAtL i j = liftFo (sucAt i j) _

sucAtL-adequate : ∀ {n} (i j : Fin n) (γ : S ^ n)
  → (γ ⊨ sucAtL i j) ≡ PairIs (fst (lookup j γ)) (sucV (fst (lookup i γ)))
sucAtL-adequate i j γ =

证明串联三条路径。转换引理先借有界性证书，把抬升公式在 L 中的满足等同于 sucAt i j 在投影赋值 map fst γ 处的周遭满足；该转换立足于既有的传递模型设置。层级一侧的充分性定理 sucAt-adequate 随后把那个满足改写为被解释取值之间的等式。最后，lookup-fst 把投影赋值处的两次查表换成 γ 中查表后的投影，同余把 sucV 移到内部，再由 cong₂ 在 PairIs 之下重新组装等式。所得即所陈述的等同。

    transferFo (sucAt i j) _ (Δ₀-sucAt i j) γ
  ∙ sucAt-adequate i j (map fst γ)
  ∙ cong₂ PairIs (lookup-fst j γ) (cong sucV (lookup-fst i γ))

扩展一个环境

consAtL 描述以一个新的首值扩展环境，其充分性引理准确对应所得的码化环境。

量词主体在当前环境前添入一个取值后求值。层级一侧的公式 consAt 已刻画这一运算，consAtL 则要在可构造模型内部表达同一刻画。抬升所需的有界性证书分别对应组成码化扩展的单集、配对、标签和键移位关系。这些关系没有引入常元数码：指定标签是空集，而新的首值从槽位 m 读取。紧接着在此定义的独立引理 numL 记录周遭数码的可构造性，供确实点名数码的其他有界公式使用。

numL k 在此定义，并证明周遭数码 # k 可构造。内部数码 numeralL k 已带有其投影可构造的证明，numeralL-fst k 把该投影与 # k 等同；沿此路径搬运证书，便得到 ⟨ isL (# k) ⟩。随后的私有定义为识别空标签的公式提供 BoundedFo InL 数据：既记录有界形状，也为其中出现的常元给出可构造性见证。其中 sgl0At k 把槽位 k 中的集合刻画为 {∅}：它有一个空成员，并且每个成员都是空的。bddSgl0 给出这种组合数据，而不是一条独立的 Δ₀ 定理。

numL : (k : ℕ) → InL (# k)
numL k = subst (λ w → ⟨ isL w ⟩) (numeralL-fst k) (numeralL k .snd)

private
  bddSgl0 : ∀ {n} (k : Fin n) → BoundedFo InL (sgl0At k)
  bddSgl0 k = (_ , (_ , _)) , (_ , (_ , _))

pair0At k j 把槽位 k 中的集合刻画为无序对 {∅, W}，其中 W 是原赋值槽位 j 的取值；进入内部量词后，同一取值由 suc j 指向。它并不是两个槽位取值的 Kuratowski 对。tag0At s x 再组合 sgl0At 与 pair0At：两个指定成员分别是 {∅} 与 {∅, W}，所以槽位 s 中的集合就是 Kuratowski 对 pr ∅ W。bddPair0 与 bddTag0 为这些描述给出 BoundedFo InL 数据，其中包括所需的常元可构造性见证。

  bddPair0 : ∀ {n} (k j : Fin n) → BoundedFo InL (pair0At k j)
  bddPair0 k j = (_ , (_ , _)) , ((_ , _) , (_ , ((_ , _) , (_ , _))))

  bddTag0 : ∀ {n} (s x : Fin n) → BoundedFo InL (tag0At s x)
  bddTag0 {n} s x =
      (_ , bddSgl0 {suc n} zero)

bddTag0 的其余部分把用于空集标签本身的单集证书，与外、内两层配对的证书配成对。其后 bddShift 为 shiftPairAt p' p 作证：p' 处的条目是由 p 处的条目把其数码键换成其后继、而配对的值保持不变所得；这里证书写成一个占位符，因为该公式的有界子公式仍是已被覆盖的叶子与有界量词。

    , ( (_ , bddPair0 {suc n} zero (suc x))
      , (_ , (bddSgl0 {suc n} zero , bddPair0 {suc n} zero (suc x))) )

  bddShift : ∀ {n} (p' p : Fin n) → BoundedFo InL (shiftPairAt p' p)
  bddShift p' p = _

  bddCons : ∀ {n} (e' m e : Fin n) → BoundedFo InL (consAt e' m e)

bddCons 装配扩展公式所需的一切。按其三个合取项来读：扩展后的图持有一个条目，即架在 m 处之值上的空集标签，也就是新的首条目，由移位槽位处的 bddTag0 作证；旧图的每个条目带其后移的键重现，由高两个元数处的 bddShift 作证；其余合取项为从扩展中向外读出的隶属方向重复这两个证书。每个合取项的证书位于其量词所创造的深度，这正说明注记中的元数增长到 suc (suc n)。

  bddCons {n} e' m e =
      (_ , bddTag0 {suc n} zero (suc m))
    , ( (_ , (_ , bddShift {suc (suc n)} zero (suc zero)))
      , (_ , ( bddTag0 {suc n} zero (suc m)
             , (_ , bddShift {suc (suc n)} (suc zero) zero) )) )

有界性证书装配齐备之后，consAtL e' m e 就是层级一侧公式 consAt e' m e 经 liftFo 的抬升，其证书由 bddCons 提供。它的充分性陈述带有一个后继情形所没有的条件：给定一个族 g : Fin k → V ℓ，以及「槽位 e 中的集合是码化环境 env g」的证明 hE。在该假设下，consAtL e' m e 的满足作为一个真值被等同于 PairIs (fst (lookup e' γ)) (env (cons (fst (lookup m γ)) g))：e' 处的集合恰是把 m 处的取值推到 g 前端所得的码化环境。这条公式是针对一个已被码化的环境作分类，而非构造环境；关于旧环境的那个假设，正是使这一分类适定的前提。

consAtL : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
consAtL e' m e = liftFo (consAt e' m e) (bddCons e' m e)

consAtL-adequate : ∀ {n} (e' m e : Fin n) (γ : S ^ n)
  {k : ℕ} (g : Fin k → V ℓ)
  → fst (lookup e γ) ≡ env g

证明以转换引理开场，一次给足它的全部输入：公式 consAt e' m e、其有界性证书 bddCons、以及层级一侧记录的 Δ₀ 证书 Δ₀-consAt。这一步是有界绝对性的实际运用，并依赖于既已建立的传递模型设置：由于 L 传递、且公式点名的每个常元都可构造，抬升公式在载体中的满足，就移为原公式在投影赋值 map fst γ 处的满足，而在那里周遭的事实可以直接陈述。

  → (γ ⊨ consAtL e' m e)
  ≡ PairIs (fst (lookup e' γ)) (env (cons (fst (lookup m γ)) g))
consAtL-adequate e' m e γ g hE =
    transferFo (consAt e' m e) (bddCons e' m e) (Δ₀-consAt e' m e) γ
  ∙ consAt-adequate e' m e (map fst γ) g

层级一侧的充分性定理 consAt-adequate 随后把周遭满足改写为新槽位与扩展后的码化环境的等同。它需要假设以投影形式给出，这正是入口处把 lookup-fst e γ 与 hE 串联的原因：e 处条目的投影等于 env g。接着，同余移走剩下的两次查表：e' 处的取值由 lookup-fst 处理，m 处的取值在函数 λ w → env (cons w g) 之下由 cong 处理。路径链条的终点恰是所允诺的 PairIs 等同。本章自身的数学至此收束：识别语法形状、元数、环境及其扩展所需的每条内部公式都已就位。

      (lookup-fst e γ ∙ hE)
  ∙ cong₂ PairIs (lookup-fst e' γ)
      (cong (λ w → env (cons w g)) (lookup-fst m γ))

无界量词

两条无界量词子句使用共同的有界框架 extB；它先绑定周遭环境集 F 与扩展数据，再应用量词专有的主体。在 quBody q 中，参数 q 是遍历载体集 w 的外层量词：存在情形取有界存在，全称情形取有界全称。内部公式 ∃̇∈ ya (consAtL ...) 表示扩展环境出现在主体所记录的取值中，在两种情形下都不改变。因此，全称情形只把外层量词改成蕴含语义，并没有把某个最内层合取改成蕴含。

求一个词项的值，与两个原子

一个词项是变元或常元，故求值码化词项的子句有两种情形：变元的取值是环境在其键处记录的东西，而常元的取值就是那个常元，在任何环境中都一样。两个原子随后求出两个词项码的值并在模型中比较所得，其一断言隶属，另一断言相等；它们的载荷是一对词项码，满足关系表在该处没有条目，这正是该子句自行构造查表、而不由框架代劳的原因。

有界量词

有界量词的载荷是「词项码与公式码的对」。界由两情形的求值读式在环境中求值，主体的取值在高一个元数处读出，而被推入的取值同时限于载体与所得界中的元素。同时遍历载体与那个界并非冗余：参照语义是在载体上作量化、再以「属于那个界」设防，而一个界完全可以有落在载体之外的成员；只在那个界上作量化，就会索要表所没有的条目。

小结

本章建立了码化满足关系的子句在 L 内部识别复合取值所需的一阶公式。支撑它的是三类陈述。表达式读式的结构充分性在两个方向上把「关于槽位、字面常元、数码与 Kuratowski 对的公式」的满足，等同于「投影条目与所指周遭取值」的相等，配对情形经由一个可构造的中间集合完成。外延刻画 extAt 是两条全称蕴含的普通合取，其读法与引入就是投影与配对。内部的后继公式与环境扩展公式由传递模型上的有界绝对性抬升，其充分性路径由转换后的满足、层级一侧的定理、以及查值在投影下的相容性串联而成。码化满足关系递归的诸子句形状正立足于此。