Bedrock绝对性
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图若一条公式在传递子结构中的解释与在外围结构中的解释具有相同真值，就称它是绝对的。这里子结构的载体是 𝒮 ↾ M，其元素由一个外围元素及其属于类 M 的证据组成；外围解释则在用 fst 投影这些序对后使用同一套语法。传递性提供关键一步：若某个界属于 M，那么该界的每个成员也属于 M。
本章通过归纳证明每条 Δ₀ 公式的内外真值相等。原子公式归结为词项求值的一致，联结词保持归纳假设，而有界量词必须把外围成员变成子结构元素时才需要传递性。最后再把这一等式推广为两个单向规律：Σ₁ 真值从子结构向上传递到外围结构，Π₁ 真值则从外围结构向下传递到子结构。
这里的结构是命题值的：ZFStructure 的载体带有取值于 hProp ℓ 的等词与成员关系，因此一条满足陈述是带有底层类型的命题，两条满足陈述可以用路径相等来比较。另有两个概念承载数学内容。其一是 Transitive，即闭合条件 y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M：M 中元素的成员仍属于 M。其二是 _↾_，它把结构限制到一个类，新载体由「元素配上其属于该类的证据」的对组成；改变的是什么算作元素，而各关系沿第一投影继承。
{-# OPTIONS --cubical --safe --guardedness #-} module FOL.Absoluteness where open import Base.Prelude open import FOL.ZFStructure using ( ZFStructure; Transitive; _↾_ )
句法方面，公式有常元 con、变量 var，以及两个有界量词 ∀̇∈ 与 ∃̇∈，其范围是某词项取值的成员。Lévy 层谱以归纳刻画的方式进入：Δ₀ 是由原子成员关系与等词出发、经命题联结词与有界量词生成的公式的归纳类，构造子名为 δ-。Σ₁ 与 Π₁ 建立其上：要么是一条 Δ₀ 公式，要么是一个无界存在 (相应地全称) 量词、其母式仍为 Σ₁ (相应地 Π₁)，由 σ-∃ 与 π-∀ 见证。这些见证正是绝对性证明将要消耗的归纳数据。
open import FOL.Syntax using ( Term; con; var; Formula; ∀̇∈; ∃̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ ; Σ₁; σ-Δ₀; σ-∃; Π₁; π-Δ₀; π-∀ ) import FOL.Semantics
语义是泛型的，因此本章将在同一套语法上使用它两次，每个世界一次。三个记号服务于后续证明：map 把第一投影作用到整个环境，⇔toPath 把两个蕴涵合成真值的路径，而截断工具以 PT 出现：无界存在量词的满足是仅要求存在的类型，因此见证在两个世界之间的转移发生在截断之下。
open import Cubical.Data.Vec using ( map ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.HITs.PropositionalTruncation as PT
设置：一套语法，两套语义
固定环境结构 𝒮 与传递类 M；内层世界是限制结构 𝒮 ↾ M，其载体 SM 由 M 的成员组成。语法取 K := SM：公式中的常元必须是 M 的成员，参数须满足的规则由类型强制保证。同一族公式于是得到两套语义：在外层 𝒮 中求值，常元经 fst 解释；在内层 𝒮 ↾ M 中求值，常元即其自身。相对化因此不是句法操作，而是同一泛型语义的两种读法；满足符号上的上标 ᵛ 与 ᵐ 读作「在哪里求值」。
本节在三个固定参数下工作：结构 𝒮、其载体上取值于 hProp ℓ 的类 M、以及传递性的证明 trans。载体 S 与真值关系 _∈ˢ_、_≈ˢ_ 属于 𝒮；hProp 上的直接运算 ⊓、⊔、⇒ 解释各联结词。目前只用到 M 是一个类这一事实；传递性进入的是定理的证明，而不是陈述定理的定义。
module Single {ℓ} (𝒮 : ZFStructure ℓ) (M : ZFStructure.S 𝒮 → hProp ℓ) (trans : Transitive 𝒮 M) where open ZFStructure 𝒮
内层世界的载体是 Σ 类型 SM：S 的一个元素配上它属于 M 的证据。由于 𝒮 ↾ M 的关系都在第一投影上解释，就 𝒮 而言，内层元素与其 fst 像指称 S 中同一个 inhabitant。泛型语义于是在这个载体上使用两次：一次在外层结构 𝒮 中求值，一次在限制结构 𝒮M 中求值。两种读法共享语法，因为常元域都取 SM；差别只在结构与常元解释。
SM : Type ℓ SM = Σ[ x ∈ S ] (x ∈ᶜ M) 𝒮M : ZFStructure ℓ 𝒮M = 𝒮 ↾ M module SemV = FOL.Semantics 𝒮
外层读法采用常元解释 ι := fst：命名某个 M 成员的常元在 𝒮 中就指那个成员本身。固定记号为：𝒮 中的满足写作 _⊨ᵛ_，词项取值写作 ⟦_⟧ᵛ；环境记号 _^_ 在全章可用。
module SemM = FOL.Semantics 𝒮M open SemV using ( _^_ ) public open module V = SemV.At SM fst public renaming ( _⊨_ to _⊨ᵛ_ ; ⟦_⟧ to ⟦_⟧ᵛ ) open module Mse = SemM.At SM id public
内层读法采用 ι := id：在 𝒮 ↾ M 中，常元就是它所命名的对，而限制结构的关系读出该对的第一投影。于是内层的原子命题 xm ∈ˢ ym 恰好意味着 𝒮 中的 fst xm ∈ˢ fst ym，这正是两条满足关系能够比较的原因。记号为 _⊨ᵐ_ 与 ⟦_⟧ᵐ，因此每条公式既可读作内层的 δ ⊨ᵐ φ，也可读作外层的 (map fst δ) ⊨ᵛ φ。
renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )
两个世界的差别只在环境的读法：内层环境 δ : SM ^ n 经 fst 给出外层的取值，map fst δ 就是相应的外层环境。两条引理连接两侧的词项求值。常元在两侧都取自己的第一投影为值，变量在两个世界都只是一次查表，因此词典问题在原子层面就已解决。
第一条引理使查表与投影逐项交换：读取投影后环境的第 i 项，等于投影第 i 项。证明对下标分情形：表头处是 refl，尾部递归，因为 lookup 与 map 都是逐项计算的。
private lookup-fst : ∀ {n} (i : Fin n) (δ : SM ^ n) → lookup i (map fst δ) ≡ fst (lookup i δ) lookup-fst zero (m ∷ δ) = refl lookup-fst (suc i) (m ∷ δ) = lookup-fst i δ
第二条引理把这一点提升到词项：在内层求值再投影，等于在投影后的环境中求值。常元情形，两侧按各自的解释 id 与 fst 都计算到 fst m，refl 即可。变量情形，外层值是对 map fst δ 的查表，第一条引理把它改写为内层查表的投影；sym 把等式摆到所需方向。任何词项都由这两种情形生成，词典于是完备。
⟦⟧-fst : ∀ {n} (t : Term SM n) (δ : SM ^ n)
→ fst (⟦ t ⟧ᵐ δ) ≡ ⟦ t ⟧ᵛ (map fst δ)
⟦⟧-fst (con m) δ = refl
⟦⟧-fst (var i) δ = sym (lookup-fst i δ)
定理
Δ₀ 的绝对性由对 Δ₀ 见证的结构归纳证明。原子与联结词情形只是记账：原子情形使用前节的词项引理，每个联结词由部分的真值算出整体的真值，因此部分相等会传递到整体相等。有界全称才是数学发生的地方。向外时，界的外层成员 x 必须重新包装成 M 的成员交给内层语义；由于界的取值属于 M，x ∈ ⟦ t ⟧ 配上 ⟦ t ⟧ ∈ᶜ M 经传递性正好给出 x ∈ᶜ M。反向只需投影。有界存在是对偶论证，在命题截断之下进行。当证明必须把裸的外层元素变成内层元素时才使用传递性：对有界全称是从内到外的方向，对有界存在则是从外到内的方向。
定理陈述的是真值的路径，而不仅是蕴涵：对每条证明 φ 是 Δ₀ 的见证 d 及指向 SM 的每个环境 δ，内层满足 δ ⊨ᵐ φ 作为类型等于投影后环境下的外层满足。原子情形中，词项引理对两侧求值：∈ 读结构字段 _∈ˢ_，≐ 读 _≈ˢ_，cong₂ 把两个词项值的相等沿关系搬运。联结词 ∧、∨、⇒ 的语义分别是 ⊓、⊔、⇒，因此把 abs₀ 作用于两个子见证、再交给 cong₂，即是整个情形：这些运算是函数，因而保持相等。
abs₀ : ∀ {n} {φ : Formula SM n} → Δ₀ φ → (δ : SM ^ n) → (δ ⊨ᵐ φ) ≡ ((map fst δ) ⊨ᵛ φ) abs₀ (δ-∈ {t = t} {u}) δ = cong₂ _∈ˢ_ (⟦⟧-fst t δ) (⟦⟧-fst u δ) abs₀ (δ-≐ {t = t} {u}) δ = cong₂ _≈ˢ_ (⟦⟧-fst t δ) (⟦⟧-fst u δ) abs₀ (δ-∧ d e) δ = cong₂ _⊓_ (abs₀ d δ) (abs₀ e δ)
荒谬无需工作：δ-⊥ 两侧都是 ⊥，所需路径即 refl。剩下的是两个有界量词：其范围 ⟦ t ⟧ 生活在外层世界，而内层量化遍历的是「值配上其属于 M 的证据」的对。下面的分块逐个方向展开。
abs₀ (δ-∨ d e) δ = cong₂ _⊔_ (abs₀ d δ) (abs₀ e δ) abs₀ (δ-⇒ d e) δ = cong₂ _⇒_ (abs₀ d δ) (abs₀ e δ) abs₀ δ-⊥ δ = refl abs₀ (δ-∀∈ {t = t} {φ = φ} d) δ = ⇔toPath fwd bwd where
对 ∀̇∈，两个方向由 ⇔toPath 打包成一条路径。先做两个缩写：tm 是界定词项的内层取值，p 是词项引理 fst tm ≡ ⟦ t ⟧ᵛ (map fst δ) 在其上的特化，即内层范围 (一个对) 与外层范围 (其第一投影) 之间的桥。
tm : SM tm = ⟦ t ⟧ᵐ δ p : fst tm ≡ ⟦ t ⟧ᵛ (map fst δ) p = ⟦⟧-fst t δ fwd : ⟨ δ ⊨ᵐ (∀̇∈ t φ) ⟩ → ⟨ (map fst δ) ⊨ᵛ (∀̇∈ t φ) ⟩
正向取内层的验证者 h，须对每个满足 x ∈ˢ ⟦ t ⟧ᵛ (map fst δ) 的外层 x 给出母式的外层真值。这里的 x 只是裸元素而非 M 的成员，必须先重新包装。沿 sym p 的传输把成员证据搬到内层范围 fst tm，随后传递性生效：x ∈ fst tm 配上 fst tm ∈ᶜ M 得到 x ∈ᶜ M，于是 xm := x , trans hx' (snd tm) 是合法的内层元素。在 xm 处运行 h 得到母式的内层真值，归纳假设 abs₀ d (xm ∷ δ) 再把它运到外层。整条归纳中唯有这一步使用前提 trans。
fwd h x hx = let hx' = subst (λ s → ⟨ x ∈ˢ s ⟩) (sym p) hx xm = x , trans hx' (snd tm) in subst ⟨_⟩ (abs₀ d (xm ∷ δ)) (h xm hx') bwd : ⟨ (map fst δ) ⊨ᵛ (∀̇∈ t φ) ⟩ → ⟨ δ ⊨ᵐ (∀̇∈ t φ) ⟩
反向沿另一方向进行：外层验证者 g 遍历裸元素，而内层子句期待一个自带成员证据的对 xm。投影 fst xm 是外层元素，词项引理把其成员关系从 fst tm 运到 ⟦ t ⟧ᵛ (map fst δ)，恰是 g 期待的形式。调用 g 得到外层真值，abs₀ d (xm ∷ δ) 再沿 sym 运回内层。这一方向不需要传递性：对 xm 是带着证据到达的。
bwd g xm hxm = subst ⟨_⟩ (sym (abs₀ d (xm ∷ δ))) (g (fst xm) (subst (λ s → ⟨ fst xm ∈ˢ s ⟩) p hxm)) abs₀ (δ-∃∈ {t = t} {φ = φ} d) δ = ⇔toPath fwd bwd where
存在情形 ∃̇∈ 镜像全称情形，仅有一处结构差异：存在量词的满足定义为载体上的上确界，即盖过所有逐元素贡献的最小真值，而被截断命题的上确界生活在命题截断之下，因此两个方向都经 PT.map 运作。缩写 tm 与 p 同样在作用域内；把见证经范围重新包装的数学与全称情形完全相同。
tm : SM tm = ⟦ t ⟧ᵐ δ p : fst tm ≡ ⟦ t ⟧ᵛ (map fst δ) p = ⟦⟧-fst t δ fwd : ⟨ δ ⊨ᵐ (∃̇∈ t φ) ⟩ → ⟨ (map fst δ) ⊨ᵛ (∃̇∈ t φ) ⟩
正向，截断下的内层见证是一个三元组：范围内的内层元素 xm、其成员证据、母式的内层真值。map 把它送到 fst xm，沿 p 把成员关系运到外层，成为 ⟨ fst xm ∈ˢ ⟦ t ⟧ᵛ (map fst δ) ⟩ 的形状，再经归纳假设 abs₀ d (xm ∷ δ) 把母式真值运到外层。见证本身只在截断之内使用，从不被提取。
fwd = PT.map λ { (xm , hxm , hφ) → fst xm , subst (λ s → ⟨ fst xm ∈ˢ s ⟩) p hxm , subst ⟨_⟩ (abs₀ d (xm ∷ δ)) hφ } bwd : ⟨ (map fst δ) ⊨ᵛ (∃̇∈ t φ) ⟩ → ⟨ δ ⊨ᵐ (∃̇∈ t φ) ⟩
反向，外层见证是三元组：裸元素 x、其在外层范围中的成员关系、母式的外层真值。沿 sym p 的传输把成员关系拉回内层范围，传递性随后证明 x ∈ᶜ M，使 xm 成为内层元素，母式真值再经 sym (abs₀ d (xm ∷ δ)) 运入内层。截断的输出同样由 PT.map 组装，因此全程未使用任何选择公理：两个有界量词情形在两侧都只以仅要求存在的见证成立。
bwd = PT.map λ { (x , hx , hφ) → let hx' = subst (λ s → ⟨ x ∈ˢ s ⟩) (sym p) hx xm = x , trans hx' (snd tm) in xm , hx' , subst ⟨_⟩ (sym (abs₀ d (xm ∷ δ))) hφ }
Σ₁ 向上，Π₁ 向下
越出 Δ₀ 之外，绝对性变成单向的，且两个方向对偶：内层为真的 Σ₁ 公式在外层为真，外层为真的 Π₁ 公式在内层为真。不对称源于量词的变异性。Σ₁ 见证可以在 Δ₀ 核之上由任意有限串的无界存在量词构造，内层的存在见证经 fst 送到外层。Π₁ 见证同样可由无界全称构造，外层验证者在每一步被特化到内层元素的 fst 上。这些无界步骤不再使用传递性；但每条归纳的 Δ₀ 基础仍依赖绝对性定理，因而依赖传递性前提。
在 Δ₀ 基础情形中，abs₀ d δ 是内外真值之间的路径，subst 沿这条路径把内层真值的证明传输到外层。这个基础情形本身不引入命题截断。Σ₁ 情形 σ-∃ 是载体上的无界存在，其满足是命题截断下的上确界，因此 PT.map 作用于截断的对：内层见证 xm 配上母式的内层真值 h，被送到外层元素 fst xm，而递归调用 σ₁-up s (xm ∷ δ) h 用完整的对扩展环境，让见证在内层保留到基础情形丢弃包装为止。
σ₁-up : ∀ {n} {φ : Formula SM n} → Σ₁ φ → (δ : SM ^ n) → ⟨ δ ⊨ᵐ φ ⟩ → ⟨ (map fst δ) ⊨ᵛ φ ⟩ σ₁-up (σ-Δ₀ d) δ = subst ⟨_⟩ (abs₀ d δ) σ₁-up (σ-∃ s) δ = PT.map λ { (xm , h) → fst xm , σ₁-up s (xm ∷ δ) h } π₁-down : ∀ {n} {φ : Formula SM n} → Π₁ φ → (δ : SM ^ n)
向下律是它的镜像。Δ₀ 情形沿 sym (abs₀ d δ) 传输；Π₁ 情形 π-∀ 是无界全称：给定外层验证者 h，对每个内层元素 xm 在 fst xm 处实例化，递归调用在扩展后的环境中证明母式。这里不出现截断，因为全称的满足是一个下确界，即低于所有逐元素贡献的最大真值，直接给出验证者即可显式验证；无界步骤不使用传递性，因为无界量词遍历整个载体，在那里对构造与投影本就可用。
→ ⟨ (map fst δ) ⊨ᵛ φ ⟩ → ⟨ δ ⊨ᵐ φ ⟩ π₁-down (π-Δ₀ d) δ = subst ⟨_⟩ (sym (abs₀ d δ)) π₁-down (π-∀ s) δ h xm = π₁-down s (xm ∷ δ) (h (fst xm))
小结
边界是精确的。在传递性之下，Δ₀ 真值在 𝒮 ↾ M 与 𝒮 之间一致：abs₀ 为每条 Δ₀ 见证给出真值的路径。有界全称从内层验证者走向界的任意外层成员时使用传递性；有界存在则在外层见证必须进入内层载体时使用它。在此基础上，σ₁-up 向上保持 Σ₁ 真值，π₁-down 向下保持 Π₁ 真值。反方向一般不能成立：任意外层存在见证未必属于 M，而内层全称验证者也没有说明 M 之外的外层元素。