Bedrock相对化
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图相对化把每个无界量词替换为受选定常元约束的量词。变换后的公式是 Δ₀，并且其通常满足关系与一种语义相符；在该语义中，原公式的无界量词只在选定集合的成员上取值。本章依次构造三件东西：改写算子本身、说明其输出落在 Lévy 层级中 Δ₀ 类的见证 (有界公式的定义见该层级一章)，以及把改写结果的含义同选定集合上的有界量化相认同的正确性定理。论述保持一般性：公式可以带有任意类型 K 的常元，语义也可以通过结构 𝒮 取值于命题宇宙 hProp ℓ。
先看论域：公式可以带有来自任意类型 K 的常元，满足关系可以通过结构 𝒮 取值于命题宇宙 hProp ℓ。设一条公式含无界量词，例如 ∃̇ (x ∈̇ y)，它问的是整个宇宙中是否有元素属于 y。给定常元 c，相对化改写这个量词的方式是为它补上界限 con c：结果为 ∃̇∈ (con c) (x ∈̇ y)，它只问是否有属于 y 的元素同时落在常元 c 所指称者之中。公式的其余部分一概不变。这种改写纯粹是语法的；改写后的公式是否仍表达原意，是另一个语义问题，留待正确性一节处理。
{-# OPTIONS --cubical --safe --guardedness #-} module FOL.Manipulation.Relativization where open import Base.Prelude open import FOL.ZFStructure using ( ZFStructure )
在单个位置把一个无界量词改写成有界量词并不难；这里的任务是在每条公式的任意深度上统一完成改写，并在事后保持记账。本章的三件东西分别回答三个问题。其一，算子 relativize c 执行替换本身，不触动已有的有界量词及其界限。其二，见证 Δ₀-relativize 证明输出落在 Lévy 层级的 Δ₀ 类中，即其中出现的每个量词都有界 (有界公式的定义见该层级一章)。其三，定理 relativize-correct 连接两种读法：在常元的任意解释下，改写后公式的通常满足关系，与原公式的一种读法一致，其中无界量词只在 c 所指称的集合上取值。
open import FOL.Syntax using ( con; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ ) import FOL.Semantics
算子
relativize c 保持原子公式与已有的有界量词不变，同时把 ∃̇ 和 ∀̇ 替换为受 con c 约束的量词。由于界是常元，进入约束子时无须随变量移动而调整。定义是对十个公式构造子的简单递归，读代码之前值得先陈述它的不动点这一语法不变量：相对化之后，结果中的每个量词都有界，而且引入的界限只有 con c 本身的出现。
签名固定了数据：从任意常元符号类型 K 取一个常元 c，以及一条元数为 n 的公式 φ，返回另一条同元数的公式。原子式、三个二元联结词以及伪式的子句根本不做改写，只是递归进入子公式并保持联结词结构。因此相对化保持深度：它唯一可能的结构改动只发生在量词节点。
relativize : ∀ {ℓ} {K : Type ℓ} (c : K) {n} → Formula K n → Formula K n relativize c (t ∈̇ u) = t ∈̇ u relativize c (t ≐ u) = t ≐ u relativize c (φ ∧̇ ψ) = relativize c φ ∧̇ relativize c ψ relativize c (φ ∨̇ ψ) = relativize c φ ∨̇ relativize c ψ
两条无界子句承载了整个要点。∃̇ φ 变为 ∃̇∈ (con c) φ′，∀̇ φ 变为 ∀̇∈ (con c) φ′，其中 φ′ 是主体的相对化：量词现在只在常元 con c 的元素上取值。两条本就有界的子句保持原界限词项 t 不动，正因为它已经约束了量词；只有主体被相对化。注意界限 con c 是词项而非变量，所以用新绑定值扩展环境时它不受任何干扰：整个变换无须任何 de Bruijn 式的重编号。
relativize c (φ ⇒̇ ψ) = relativize c φ ⇒̇ relativize c ψ relativize c ⊥̇ = ⊥̇ relativize c (∃̇ φ) = ∃̇∈ (con c) (relativize c φ) relativize c (∀̇ φ) = ∀̇∈ (con c) (relativize c φ) relativize c (∀̇∈ t φ) = ∀̇∈ t (relativize c φ)
至此分情形完毕：十个构造子全部覆盖，递归对输入公式是结构性的，所以 relativize c φ 对每条公式都有定义。由于两条有界子句只是递归，φ 中原有的有界量词带着自己的界限存活下来，而新界限恰好是无界量词的相对化像。
relativize c (∃̇∈ t φ) = ∃̇∈ t (relativize c φ)
每个无界量词都变为有界量词，其余部分保持不变，因此结果不含任何 ∃̇ 或 ∀̇ 构造子。用 Lévy 层级一章的术语说，这正是 Δ₀ 的含义：归纳族 Δ₀ 对每个获准形状有一个构造子，而对无界量词没有。函数 Δ₀-relativize 对 φ 递归地装配这样的见证，每个构造子一行。
陈述对所有公式 φ 量化，产出的是归纳族中的见证 Δ₀ (relativize c φ)，而非布尔标记。对原子式，见证 δ-∈ 与 δ-≐ 直接给出：原子公式不含任何量词，故属于 Δ₀ 是直接的。联结词子句用 δ-∧、δ-∨ 与 δ-⇒ 组合见证，对应于该类在二元运算下的封闭规则。
Δ₀-relativize : ∀ {ℓ} {K : Type ℓ} (c : K) {n} (φ : Formula K n) → Δ₀ (relativize c φ) Δ₀-relativize c (t ∈̇ u) = δ-∈ Δ₀-relativize c (t ≐ u) = δ-≐ Δ₀-relativize c (φ ∧̇ ψ) = δ-∧ (Δ₀-relativize c φ) (Δ₀-relativize c ψ) Δ₀-relativize c (φ ∨̇ ψ) = δ-∨ (Δ₀-relativize c φ) (Δ₀-relativize c ψ)
伪式不含任何量词，故 δ-⊥ 即可。决定性的行再次是量词：凡 relativize 把无界量词变为有界量词之处，Δ₀-relativize 便对相对化主体的见证应用为有界量化保留的构造子 δ-∃∈ 或 δ-∀∈。原公式中的有界量词也对自己的主体得到同样处理。每种情形里，归纳假设给出子公式的见证，构造子再把它穿过外围的联结词或量词提升上来。
Δ₀-relativize c (φ ⇒̇ ψ) = δ-⇒ (Δ₀-relativize c φ) (Δ₀-relativize c ψ) Δ₀-relativize c ⊥̇ = δ-⊥ Δ₀-relativize c (∃̇ φ) = δ-∃∈ (Δ₀-relativize c φ) Δ₀-relativize c (∀̇ φ) = δ-∀∈ (Δ₀-relativize c φ) Δ₀-relativize c (∀̇∈ t φ) = δ-∀∈ (Δ₀-relativize c φ)
十个情形至此全部覆盖，对 φ 的递归保证每条输入都有见证。这是本章承诺的语法部分：相对化后的公式不只是直观上有界，它们携带显式的 Δ₀ 证书，可供日后的绝对性与可定义性论证直接使用。
Δ₀-relativize c (∃̇∈ t φ) = δ-∃∈ (Δ₀-relativize c φ)
正确性
比较语义解释原公式，但只把其中的无界量词限制到所选界的取值。结构归纳表明，这恰好是相对化公式的通常语义。因此这里同时有两个语义：来自 FOL.Semantics 的标准语义 γ ⊨ _，以及这里定义的辅助关系 γ ⊨ᴬ _；后者在每个联结词、原子式和有界量词处与标准语义一致，只在 ∃̇ 与 ∀̇ 处不同，它附加了约束变元属于选定集合的条件。要证的定理是路径 (γ ⊨ relativize c φ) ≡ (γ ⊨ᴬ φ)，所以两个关系必须落在有同一类型的类型中；这正是模块以命题值结构 𝒮 与常元解释 ι 为参数的原因。
为了比较两种读法，固定一个论域为 S 的命题值 ZF 结构 𝒮、给每个常元符号指派载体元素的解释 ι，以及特选常元 c。标准语义 γ ⊨ _ 与词项求值 ⟦_⟧ 来自 FOL.Semantics，针对给定的 ι。本节在这些数据之上添加一个伴随关系 γ ⊨ᴬ _：它按标准语义解释原公式，只是把其中的无界量词限制到单个载体元素 A，即所选常元的指称 ι c。在原子式、联结词、伪式与有界量词处，伴随关系应与标准语义一致；它只在无界量化被换成 A 内部量化之处不同。论证直接使用 𝒮 的命题值关系。
module Correct {ℓ} (𝒮 : ZFStructure ℓ) {ℓc} {K : Type ℓc} (ι : K → ZFStructure.S 𝒮) (c : K) where open ZFStructure 𝒮 open module Sem = FOL.Semantics 𝒮 using ( module At; _^_ )
界限被一次性命名：A = ι c，即所选常元指称的载体元素。关系 γ ⊨ᴬ φ 取环境 γ : S ^ n 与同元数 n 的公式 φ，返回命题宇宙 hProp ℓ 中的命题，与标准满足关系一样。上标 ᴬ 记录量词被相对化到 A；下面给出各子句，其中只有无界量词子句与标准者不同。
open At K ι using ( _⊨_; ⟦_⟧ ) A : S A = ι c infix 6 _⊨ᴬ_ _⊨ᴬ_ : ∀ {n} → S ^ n → Formula K n → hProp ℓ
前五条子句逐字复制标准语义：原子式成为结构的命题值成员关系与等词，作用于指称 ⟦ t ⟧ γ 与 ⟦ u ⟧ γ；联结词成为逻辑运算 ⊓、⊔、⇒；伪式成为 ⊥。这是有意的：在这些形状上没有可相对化之物，而让这些子句与标准子句定义性地相同，正是相应正确性情形能由 refl 证明的原因。递归同样是结构性的，故 ⊨ᴬ 是全函数。
γ ⊨ᴬ (t ∈̇ u) = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ γ ⊨ᴬ (t ≐ u) = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ γ ⊨ᴬ (φ ∧̇ ψ) = (γ ⊨ᴬ φ) ⊓ (γ ⊨ᴬ ψ) γ ⊨ᴬ (φ ∨̇ ψ) = (γ ⊨ᴬ φ) ⊔ (γ ⊨ᴬ ψ) γ ⊨ᴬ (φ ⇒̇ ψ) = (γ ⊨ᴬ φ) ⇒ (γ ⊨ᴬ ψ)
量词子句是两种语义分岔之处。无界存在量词的 γ ⊨ᴬ (∃̇ φ) 是带下标的并 ∃[ x ] (x ∈ˢ A) ⊓ ((x ∷ γ) ⊨ᴬ φ)：它遍历所有载体元素 x，并合取命题卫式 x ∈ˢ A。对偶地，无界全称量词用 ∀[ x ] P x 配蕴涵卫式 x ∈ˢ A ⇒ _。有界子句本就把量词限制到一个词项，该词项在原环境 γ 中求值；其卫式用的是 ⟦ t ⟧ γ 而非 A，其余与标准读法完全一致。这里仅陈述定义所用的运算；抽象命题运算并未假设使卫式成为二值判定的定律。
γ ⊨ᴬ ⊥̇ = ⊥ γ ⊨ᴬ (∃̇ φ) = ∃[ x ∶ S ] (x ∈ˢ A) ⊓ ((x ∷ γ) ⊨ᴬ φ) γ ⊨ᴬ (∀̇ φ) = ∀[ x ∶ S ] (x ∈ˢ A) ⇒ ((x ∷ γ) ⊨ᴬ φ) γ ⊨ᴬ (∀̇∈ t φ) = ∀[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ ((x ∷ γ) ⊨ᴬ φ) γ ⊨ᴬ (∃̇∈ t φ) = ∃[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ ((x ∷ γ) ⊨ᴬ φ)
正确性由结构归纳证明：relativize c φ 的标准含义等于 φ 的 A-有界含义。原子情形是 refl；算子实际改动的两个量词子句，正是标准语义按计算把 ∃̇∈ (con c) _ 展开为相应子句之处，因为 ⟦ con c ⟧ γ 就是 A；其余情形都是同余。结论是命题宇宙 hProp ℓ 中的路径，而不仅仅是当且仅当，所以两个命题被直接同一，可在日后的论证中沿其传输。
陈述同时对公式 φ 与环境 γ 量化，并断言命题宇宙 hProp ℓ 中的路径。由于 relativize c 未动原子式，左边 γ ⊨ (t ∈̇ u) 计算到恰为 ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ 的命题，而这正是 γ ⊨ᴬ (t ∈̇ u) 的定义；等词与伪式同理，故这些情形由 refl 证明，即定义性等价，无须进一步步骤。联结词情形对相应的逻辑运算使用 cong₂：既然子结果一致，组合后的命题也一致。
relativize-correct : ∀ {n} (φ : Formula K n) (γ : S ^ n) → (γ ⊨ relativize c φ) ≡ (γ ⊨ᴬ φ) relativize-correct (t ∈̇ u) γ = refl relativize-correct (t ≐ u) γ = refl relativize-correct (φ ∧̇ ψ) γ = cong₂ _⊓_ (relativize-correct φ γ) (relativize-correct ψ γ)
存在情形是关键。左边 relativize c (∃̇ φ) 是 ∃̇∈ (con c) φ′，有界存在的标准语义是 ∃[ x ] (x ∈ˢ ⟦ con c ⟧ γ) ⊓ ((x ∷ γ) ⊨ φ′)。但 ⟦ con c ⟧ γ 计算到 A = ι c，于是一旦用扩展环境 x ∷ γ 处的归纳假设把内部的 ⊨ φ′ 换成 ⊨ᴬ φ，该表达式就定义性地成为 ∃̇ φ 的 ᴬ 子句。形式上，funExt 把对每个 x 的逐点一致转为两个下标族的一致，cong 把它穿过卫式 x ∈ˢ A ⊓ _ 传输，外层 cong (λ P → ∃[ x ] P x) 再把族的一致提升为并的一致。全称情形是取 ∀[ x ] P x 与 ⇒ 的对偶版本。
relativize-correct (φ ∨̇ ψ) γ = cong₂ _⊔_ (relativize-correct φ γ) (relativize-correct ψ γ) relativize-correct (φ ⇒̇ ψ) γ = cong₂ _⇒_ (relativize-correct φ γ) (relativize-correct ψ γ) relativize-correct ⊥̇ γ = refl relativize-correct (∃̇ φ) γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x → cong (λ q → (x ∈ˢ A) ⊓ q) (relativize-correct φ (x ∷ γ))))
两条本就有界的子句与上一对互为镜像。这里 relativize c 保留了原界限词项 t，而 ⊨ᴬ 也用 ⟦ t ⟧ γ 为量词加卫，所以卫式从不改变；只需通过 x ∷ γ 处的归纳假设转换主体的满足关系，同样的 funExt、内层 cong 与外层 cong (λ P → ∃[ x ] P x) 或 cong (λ P → ∀[ x ] P x) 模式即可套用。注意界限词项仍在原环境 γ 中求值，与有界量化的标准语义完全一致。
relativize-correct (∀̇ φ) γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x → cong (λ q → (x ∈ˢ A) ⇒ q) (relativize-correct φ (x ∷ γ)))) relativize-correct (∀̇∈ t φ) γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x → cong (λ q → (x ∈ˢ ⟦ t ⟧ γ) ⇒ q) (relativize-correct φ (x ∷ γ)))) relativize-correct (∃̇∈ t φ) γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
十个情形全部处理完毕，递归作用于 φ，故证明对每条公式与每个环境都完成。本章论证至此闭合：相对化是纯语法的变换，其输出是 Δ₀，而它在任何取命题的 ZF 结构中的标准含义是限制到选定集合上的量化。因此，后面的章节可以把一个可定义性条件相对化到集合 A，改用 Δ₀ 公式，并直接从 A 内部的量化读出其满足关系，这一切都由这一条归纳支撑。
cong (λ q → (x ∈ˢ ⟦ t ⟧ γ) ⊓ q) (relativize-correct φ (x ∷ γ))))
小结
relativize 产生 Δ₀ 公式，Δ₀-relativize 记录这一复杂度界，而 relativize-correct 将其含义识别为在选定集合内部量化。三者合起来给出了把任意公式限制到一个集合的标准集合论手法：语法上用指称该集合的常元给量词加界，语义上则由这里证明的那一条归纳完成。往下看，Δ₀ 证书供绝对性论证使用，而正确性路径使人们在分析可定义性时，可以把相对化公式的满足关系换成对 A 的有界量化。