Bedrock描述封闭的公式码定义域
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图Agda 已经给出公式的归纳类型，以及在外部把集合指定为公式码的运算。然而，要在集合论内部推理句法，模型还需要用自身语言中的公式描述一个候选公式键集合。本章构造这份有界描述：形状半边读取候选域中已有键的直接结构，闭包半边则由合法组成部分生成复合键。
{-# OPTIONS --cubical --safe --guardedness #-}
这份描述是构造性的。它只记录有界隶属、配对、标签与公式键的直接组成部分，因此其定义不需要排中律实例。
open import Base.Prelude
固定一个宇宙层级。下文的主要参数是候选码域 C、提供常元的工作集 w、预期存放环境塔条目的集合 E，以及十个构造子标签的具名位置 N。预期的 E 条目把元数与相应环境集配成一对，但这里定义的公式本身并不断言 E 就是典范环境塔；这一事实由后续充分性证明的假设提供。
module L.Coding.CodeDomain {ℓ : Level} where
目标是由隶属、相等、联结词与有界量词组成的对象语言公式。其中的量词只在描述中已经命名的集合，或拆解有序对所用的小容器上取值。正因这一句法限制，最终公式才能获得 Δ₀ 认证。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇∈; ∀̇∈ ) open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀ )
所有公式都在可构造载体上解释。有序对谓词与编码图应用谓词使内部语言能够检查形如「元数与带标签载荷的对」的键，而无须假定集合编码的有序对具有原始投影。
import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( prAtL; appAt ) open import L.Coding.Expressions {ℓ} using ( sucAtL )
嵌套的有界量词会在环境前端引入临时见证。具名的有穷槽位及其移位，使 C、w、元数与全部十个标签在拆解这些见证时始终指向原来的值。
import L.Coding.Expressions {ℓ} as CodingExpressions module E = CodingExpressions.PairExpression open import L.Coding.Quantification {ℓ} using ( i0; i1; i2; i3; i4; i5; i6; i7; i8; sh ; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9
有序对读式在保持所有见证有界的同时显露两个分量。随后，一个有穷析取把十种可能的最外层构造子合成一项形状检验；相应的有界全称读式则对所有合法输入表达封闭性。
; sndEx; sndAll; bothEx; bothAll; bigOr )
有穷索引与集合论数码在这里承担不同角色。映射 N 指出外围环境中的十个位置，toℕ 则确定每个标签位置应放置零至九中的哪个数码。当有界见证扩展环境时，移位会保持这些引用不变。此处尚未认证 E 的条目中记录的元数是自然数码；这一认同要由后续的环境塔假设给出。
open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.FinData using ( toℕ ) open import Cubical.Data.Unit using ( tt ) open import Cubical.Data.Vec using ( lookup ) open import Cubical.HITs.CumulativeHierarchy.Constructions
十个构造子标签由零至九的冯・诺伊曼数码表示。数码之间的区分将在后文辨别两个原子关系、三个二元联结词、假与四个量词。
using ( module InfinitySet ) open InfinitySet {ℓ} using ( #_ )
以 S 表示可构造集合的载体。解释对象语言公式时，候选域、其中的键、工作集与环境塔条目都取自这一载体。
open hPropStructure 𝒮ʟ using ( S )
因此，下文构造的公式可以在可构造元素组成的有限环境中读取。先从最小的局部问题开始：在固定元数处，哪些带标签集合算作词项码？
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ ) open AbsL using ( _^_ )
描述形状与封闭性
词项谓词接受两类表示：标签取槽位 N0 且载荷属于工作集 w 的对，或标签取槽位 N1 且载荷属于元数集合 ar 的对。在预期的标签赋值下，它们分别表示常元与自由变元。此处 ar 仍只是一个集合；要把它认同为自然数码，还需后文使用的环境塔事实。
isTm : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m isTm t ar w N0 N1 = sndEx t N0 (var i0 ∈̇ var (sh 2 w)) ∨̇ sndEx t N1 (var i0 ∈̇ var (sh 2 ar))
对固定载荷 r，keyUp C ar r 断言完整键 (ar + 1, r) 属于 C，其中 ar + 1 由内部后继关系表达。量词的形状子句用它处理主体。该谓词只断言这个固定的加一元数键属于域，并不独立检查 r 的形状，也不证明 ar 是数码。
keyUp : ∀ {m} → Fin m → Fin m → Fin m → Formula S m keyUp C ar r = ∃̇∈ (var C) (∃̇∈ (var i0) (∃̇∈ (var i0) (prAtL i2 i0 (sh 3 r) ∧̇ sucAtL (sh 3 ar) i0)))
公式键统一具有 (ar, (N, p)) 的形状：ar 是元数，N 是构造子标签，p 是载荷。构造时先形成内层的带标签载荷 (N, p)，再把它与元数配对。不同构造子改变的是 p 的结构，而最外层布局保持不变。
keyExpr : ∀ {m} → Fin m → Fin m → E.Expr m → E.Expr m keyExpr ar N p = E.pair (E.slot ar) (E.pair (E.slot N) p)
对任一原子关系，载荷都具有 ((Nx, x), (Ny, y)) 的形状。每个内层对同时记录词项的种类与载荷，因此左右词项可以分别取常元或变元，而原子公式仍保持统一的键形状。
atomKeyExpr : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → E.Expr m atomKeyExpr ar N Nx x Ny y = keyExpr ar N (E.pair (E.pair (E.slot Nx) (E.slot x)) (E.pair (E.slot Ny) (E.slot y)))
有界量词载荷把带标签界词项 (Nx, x) 与主体载荷 a 配成一对。外围键记录当前元数；另行给出的 keyUp 条件才要求主体的完整键 (元数 + 1, a) 属于定义域。
bndKeyExpr : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → E.Expr m bndKeyExpr ar N Nx x a = keyExpr ar N (E.pair (E.pair (E.slot Nx) (E.slot x)) (E.slot a))
第一个隶属模板断言嵌套对 (ar, (N, a)) 属于候选域。它只记录这项集合隶属；N 是否是适当的一元构造子标签、a 是否为合法组成部分，都由外围子句另行规定。
unKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Formula S m unKey C ar N a = E.member (keyExpr ar N (E.slot a)) (var C)
二元模板把一元载荷换成对 (a, b)。后文先另行要求两个同元数子键属于 C，再用这个模板处理合取、析取与蕴涵。
binKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m binKey C ar N a b = E.member (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C)
原子模板把两个带标签词项载荷放入键中。这里仍然只断言其属于 C；原子的形状与闭包子句会给出词项的界，并为最外层关系选择标签零或一。
atomKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m atomKey C ar N Nx x Ny y = E.member (atomKeyExpr ar N Nx x Ny y) (var C)
有界量词与无界量词的区别在于，它除主体外还携带一个界词项。载荷 ((Nx, x), a) 记录带标签的界词项与主体载荷，但这个隶属模板本身并不断言二者合法。外围形状条件检查词项在当前元数处合法，并检查主体的完整键位于后继元数处；闭包条件则沿生成方向使用同样两个组成部分。
bndKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m bndKey C ar N Nx x a = E.member (bndKeyExpr ar N Nx x a) (var C)
标签一致要求十个槽位恰取数码零至九，每个槽位对应其位置。正因如此，后文每个公式说「隶属原子的标签」时，指的都是同一个槽位。
Tags : ∀ {m} (γ : S ^ m) (N : Fin 10 → Fin m) → Type (ℓ-suc ℓ) Tags γ N = (k : Fin 10) → fst (lookup (N k) γ) ≡ # (toℕ k)
当公式在添入受界变元后的环境中读取时，十个标签槽位随环境移位；移位后的命名使每条子句仍与相同的标签对齐。
shN : ∀ {m} (j : ℕ) → (Fin 10 → Fin m) → Fin 10 → Fin (j + m) shN j N k = sh j (N k)
现在可以对候选域的成员提出向内的问题：什么证据表明其载荷属于允许的构造子形状之一？虽然构造子标签共有十个，载荷条件却只需分成五类，因为两个原子关系、三个二元联结词、两个无界量词与两个有界量词分别共用各自的组成模式。
module Shape {m : ℕ} (C w : Fin m) (N : Fin 10 → Fin m) where private C9 w9 : Fin (9 + m) C9 = sh 9 C w9 = sh 9 w
五种载荷形状被写出。原子载荷要求两个合法词项；二元载荷要求两个已在定义域中的同元数子键；假值的载荷是数码零；无界量词载荷要求后继元数处的主体键。
atomPay binPay conPay quPay bqPay : Formula S (9 + m) atomPay = bothEx i0 (isTm i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) ∧̇ isTm i0 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1))) binPay = bothEx i0 (appAt (sh 12 C) i8 i1 ∧̇ appAt (sh 12 C) i8 i0) conPay = var i0 ≐ var (sh 9 (N f0)) quPay = keyUp C9 i5 i0
对有界量词，载荷包含当前元数处的合法界词项，以及一个主体载荷，而该主体在元数加一处的完整键须属于定义域。合取同时记录这两项义务，但不会选出一条解码后的主体公式。
bqPay = bothEx i0 (isTm i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) ∧̇ keyUp (sh 12 C) i8 i0)
前四个标签区分两个原子关系与前两个二元联结词：标签零是隶属，标签一是相等，标签二是合取，标签三是析取。前一对共用原子载荷条件，后一对共用二元载荷条件；不同数码仍然保留了最外层构造子的区别。
payN : ℕ → Formula S (9 + m) payN 0 = atomPay payN 1 = atomPay payN 2 = binPay payN 3 = binPay
标签四是蕴涵，标签五是假，标签六与七分别是无界存在量词和无界全称量词，标签八是有界全称量词。相应载荷条件依次为两个同元数子键、固定数码零、后继元数处的主体键，以及当前元数处的界词项与这种主体的组合。
payN 4 = binPay payN 5 = conPay payN 6 = quPay payN 7 = quPay payN 8 = bqPay
标签九是有界存在量词，与标签八共用有界量词载荷条件。末条等式在九以上返回假，使 payN 成为自然数上的全函数；由于 pay 只通过 Fin 10 中的索引调用它，这个后备分支不会出现在十路形状检验中。
payN 9 = bqPay payN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) = ⊥̇
至此，十个标签各自都有对应的载荷检验。下一步要把由 k 索引的检验与实际的带标签载荷联系起来，再把十个索引分支合成形状条件。
pay : Fin 10 → Formula S (9 + m) pay k = payN (toℕ k)
对选定的构造子索引 k，最外层载荷必须分解为 (N k, r)，余下分量 r 则须满足该标签的载荷条件。元数已由外围形状公式显露；本子句拆解的是带标签载荷，而不是在元数的成员上作量化。
at : Fin 10 → Formula S (7 + m) at k = sndEx i0 (sh 7 (N k)) (pay k)
十条形状子句被收集为一个有穷析取。因此，单一公式便能陈述带标签载荷至少匹配十种构造子形状之一，而无须引入额外的无界量词。
ten : Formula S (7 + m) ten = bigOr 9 at
形状半边从候选域中每个已有成员 c 出发。它从 E 选择条目 (ar, F)，把 c 分解为 (ar, p)，并要求 p 匹配十种带标签载荷形状之一。复合形状已经要求其直接公式子键属于 C。在语义解释中，这些有界存在见证经过命题截断，因此该条件既不提供选定的分解，也不声称解码唯一。
shapeAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m shapeAt C w E N = ∀̇∈ (var C) (∃̇∈ (var (sh 1 E)) (bothEx i0 (sndEx i4 i1 (Shape.ten C w N))))
第二个半边转向向外的问题。固定 E 的一个条目，并把其第一分量作为共同元数。闭包子句陈述：只要词项在该元数处合法，且直接公式键已在所需的当前元数或后继元数处属于 C，哪些复合键就必须进入 C。
module Close {m : ℕ} (C w : Fin m) (N : Fin 10 → Fin m) where private C4 w4 : Fin (4 + m) C4 = sh 4 C w4 = sh 4 w
一条原子生成子句固定最外层关系标签，并为两个词项各固定一个标签。它让两个载荷分别在界 X 与 Y 中取值，再要求所得原子键属于 C。后面的八个实例让每个词项标签在常元与变元之间选择，并相应把 X、Y 取为工作集或当前元数。
atomClose : (k Nx Ny : Fin 10) (X : Fin (4 + m)) (Y : Fin (5 + m)) → Formula S (4 + m) atomClose k Nx Ny X Y = ∀̇∈ (var X) (∀̇∈ (var Y) (atomKey (sh 6 C) i3 (sh 6 (N k)) (sh 6 (N Nx)) i1 (sh 6 (N Ny)) i0))
二元闭包要求：定义域中任意两个同元数成员生成以其为子键的每个二元联结词的键。
binClose : (k : Fin 10) → Formula S (4 + m) binClose k = ∀̇∈ (var C4) (sndAll i0 i2 (∀̇∈ (var (sh 7 C)) (sndAll i0 i5 (binKey (sh 10 C) i7 (sh 10 (N k)) i3 i0))))
假值闭包把带零载荷的假符号之键放入定义域。
conClose : (k : Fin 10) → Formula S (4 + m) conClose k = unKey C4 i1 (sh 4 (N k)) (sh 4 (N f0))
对无界量词，任取 C 中一个可分解为元数 ar + 1 处主体键的成员。该子句随即要求元数 ar 处相应的量化公式键属于 C。这是从已有直接组成部分到复合公式的生成方向。
quClose : (k : Fin 10) → Formula S (4 + m) quClose k = ∀̇∈ (var C4) (bothAll i0 (sucAtL i5 i1 ⇒̇ unKey (sh 8 C) i5 (sh 8 (N k)) i0))
有界量词子句再加入当前元数处的界词项。一旦 C 的某个成员被认作元数 ar + 1 处的主体键，所选词项界 X 中的每个载荷都会在元数 ar 处生成有界量词键；后面的实例分别选择常元与变元情形。
bqClose : (k Nx : Fin 10) (X : Fin (8 + m)) → Formula S (4 + m) bqClose k Nx X = ∀̇∈ (var C4) (bothAll i0 (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh 9 C) i6 (sh 9 (N k)) (sh 9 (N Nx)) i0 i1)))
闭包合取以八条原子子句开场：两个原子符号各有两个词项槽，每槽取常元或变元，共八种组合。
all : Formula S (4 + m) all = atomClose f0 f0 f0 w4 (sh 1 w4) ∧̇ (atomClose f0 f0 f1 w4 i2 ∧̇ (atomClose f0 f1 f0 i1 (sh 1 w4) ∧̇ (atomClose f0 f1 f1 i1 i2 ∧̇ (atomClose f1 f0 f0 w4 (sh 1 w4) ∧̇ (atomClose f1 f0 f1 w4 i2
这个合取先接上最后两条原子子句，从而补全相等原子的四种词项形状组合；随后加入三条二元子句、一条假子句、两条无界量词子句与四条有界量词子句。因此总数是八条原子、三条二元、一条假、两条无界与四条有界子句，合计十八条。
∧̇ (atomClose f1 f1 f0 i1 (sh 1 w4) ∧̇ (atomClose f1 f1 f1 i1 i2 ∧̇ (binClose f2 ∧̇ (binClose f3 ∧̇ (binClose f4 ∧̇ (conClose f5 ∧̇ (quClose f6 ∧̇ (quClose f7 ∧̇ (bqClose f8 f0 (sh 8 w) ∧̇ (bqClose f8 f1 i5 ∧̇ (bqClose f9 f0 (sh 8 w) ∧̇ bqClose f9 f1 i5))))))))))))))))
闭包半边在 E 所指集合的每个条目处施加全部十八条生成子句。条目拆开后，其第一分量为各构造规则提供共同元数。这个公式并不认证这些条目构成典范环境塔，甚至不认证每个记录元数都是自然数码；这些事实由后续假设提供。在任一合法塔条目处，其方向始终是由合法组成部分生成相应复合键，而不是从 C 的任意成员反向恢复其组成部分。
closeAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m closeAt C w E N = ∀̇∈ (var E) (bothAll i0 (Close.all C w N))
完整描述合取两个方向。shapeAt 从每个已有成员向内读取，并要求其直接子键仍在候选域中；closeAt 则从合法组成部分出发，生成相应的复合键。任一条件单独都不够：只有形状条件时可能漏掉真实键，只有闭包条件时可能容许额外成员。这个合取仍只是相对于 w、E 与 N 的规格；它自身既不构造码域，也不证明码域就是典范集合。
codesAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m codesAt C w E N = shapeAt C w E N ∧̇ closeAt C w E N
最后的计算给出一份证书，确认 codesAt 中每个量词都有界，因而 codesAt 属于 Δ₀ 类。这是对描述候选域的对象语言公式所作的分类；它既不是把单个码分类为 Δ₀ 对象，也不会单独证明所描述码域的存在性、典范性或绝对性定理。
Δ₀-codesAt : ∀ {m} (C w E : Fin m) (N : Fin 10 → Fin m) → Δ₀ (codesAt C w E N) Δ₀-codesAt C w E N = checkΔ₀ (codesAt C w E N) tt
小结
候选码域规格包含两个互补方向。shapeAt 把每个已有成员读成十种带标签构造形状之一，并要求该形状所需的每个直接公式子键都属于 C；closeAt 则把十八条生成子句打包起来，由合法词项与当前元数或后继元数处已有的子键构造相应公式键。二者的合取是相对于 w、E 与 N 的有界规格。
有界存在量词隐藏的语义见证只能在命题截断下取得，因此这份规格既不选定分解，也不给出解码函数。下一章将在正确的字母表、标签与环境塔假设以及排中律下分别证明两项充分性结论：候选域的每个成员纯粹地可解码为真实公式键，而对外部公式作归纳则把每个真实键放入候选域。外部编码的单射性随后可以证明固定元数下恢复出的两条公式相同，但这一独立结果并不会使 codesAt 成为选定的或全局唯一的句法解码器。