常元改名

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

一阶公式携带着来自某个常元域 K 的常元符号，但符号本身是惰性的：决定它们所指的只有解释函数。本章研究当一个函数 f : K → K' 改写每个常元符号时会发生什么，这一作用记作 mapFo f。这里回答两个问题。其一，含义是否在改名后幸存，精确地说：改名后在 ι 下的满足，是否等同于改名前在复合解释 ι ∘ f 下的满足？其二，公式在 Lévy 层级中的语法分类是否幸存，即 Δ₀ 见证以及更一般的 Σₙ/Πₙ 见证能否沿 f 搬运？两个答案都是肯定的，而且两个证明都是结构性的，与语法的构造子一一对应。

取一个定义在常元域 K 上的公式，沿函数 f : K → K' 改名它的常元。这个公式说什么，取决于哪个解释来读它：是目标解释 ι : K' → S 作用于改名后的公式，还是复合解释 ι ∘ f 作用于原公式。本章的语义一半问这两种读法是否总是一致，语法一半问公式在 Lévy 层级中的分类是否在改名下幸存。两个答案都由结构归纳给出，与语法的构造子一一对应。

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

module FOL.Manipulation.Relabelling where

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure )

被研究的作用在词项上记作 mapTm f，在公式上记作 mapFo f：函数 f : K → K' 把每个常元 con k 改名为 con (f k)，并让每个变量原样不动。由于它只作用于常元，每个联结词与每个量词 (无论有界与否) 都保持原位，这正是 Lévy 分类应当幸存的原因。分类本身以归纳见证给出：Δ₀ φ 的一个元素是显式数据，证明 φ 中每个量词都有界，每个获准的形状对应一个构造子；Σₙ k φ 与 Πₙ k φ 则记录交替的无界块。

open import FOL.Syntax using
  ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo; embed )
open import FOL.LevyHierarchy using
  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈

在语义一侧，带载体 S 的结构 𝒮 经解释 ι : K → S 来读 K 上的公式，得到满足关系 _⊨_ 与词项求值 ⟦_⟧。因此待比较的两种读法共享同一语法，差别只在解释；下面的证明让二者并排出现，以保持区分。

  ; Σₙ; σ-Δ₀; σ-Π; σ-∃; Πₙ; π-Δ₀; π-Σ; π-∀ )
import FOL.Semantics
import Cubical.Data.Empty as Empty

含义层

常元改名是纯语法操作，因此必须检查它不扰动含义。精确的陈述是一条交换律：对任意常元域映射 f : K → K' 与目标域的任意解释 ι : K' → S，改名后的公式在 ι 下的求值，与原公式在复合解释 ι ∘ f 下的求值给出相同的命题。证明按结构归纳进行：基底情形由词项求值提供，其余由逻辑运算的同余性完成。

固定一个论域为 S 的命题值 ZF 结构 𝒮、一个改名 f : K → K'，以及目标域的解释 ι : K' → S。复合 ι ∘ f 同样是源域的一个合格解释，于是同一批公式有了两种读法：改名后的公式在 ι 下，原公式在 ι ∘ f 下。交换问题就是问这两种读法是否给出相等的命题。

module _ {ℓ} (𝒮 : ZFStructure ℓ) where

  open ZFStructure 𝒮
  open FOL.Semantics 𝒮 using ( module At; _^_ )

  module _ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K') (ι : K' → S) where

原子情形已经显示了两种读法为何必须一致。考虑公式 t ∈̇ u：第一种读法把它求值为 ⟦ mapTm f t ⟧ γ ∈ˢ ⟦ mapTm f u ⟧ γ，第二种读法求值为 ⟦ t ⟧∘ γ ∈ˢ ⟦ u ⟧∘ γ。词项引理 ⟦⟧-map 对每个词项给出 ⟦ mapTm f t ⟧ γ ≡ ⟦ t ⟧∘ γ，其两种情形都由 refl 成立：改名后的常元 con (f k) 求值为 ι (f k)，这正是复合读法所计算的；而变量完全不涉及常元。

    open At K' ι using ( _⊨_; ⟦_⟧ )
    open At K (λ k → ι (f k)) using () renaming ( _⊨_ to _⊨∘_ ; ⟦_⟧ to ⟦_⟧∘ )

    ⟦⟧-map : ∀ {n} (t : Term K n) (γ : S ^ n)
           → ⟦ mapTm f t ⟧ γ ≡ ⟦ t ⟧∘ γ
    ⟦⟧-map (con k) γ = refl

满足引理 ⊨-map 把这一一致从词项提升到公式，得到命题之间的路径：(γ ⊨ mapFo f φ) ≡ (γ ⊨∘ φ)。对原子情形 t ∈̇ u，来自 ⟦⟧-map 的两条词项路径经 cong₂ _∈ˢ_ 送入属于关系，产生该命题两种读法之间的路径。等号原子经 ≈ˢ 完全同样地处理。

    ⟦⟧-map (var i) γ = refl

    ⊨-map : ∀ {n} (φ : Formula K n) (γ : S ^ n)
          → (γ ⊨ mapFo f φ) ≡ (γ ⊨∘ φ)
    ⊨-map (t ∈̇ u)  γ = cong₂ _∈ˢ_ (⟦⟧-map t γ) (⟦⟧-map u γ)
    ⊨-map (t ≐ u)  γ = cong₂ _≈ˢ_ (⟦⟧-map t γ) (⟦⟧-map u γ)

命题联结词同样由同余处理，因为结构用相应的逻辑运算来解释它们：φ 的两种读法之间的一条路径与 ψ 的两条读法之间的一条路径，经 ⊓ 合成 φ ∧̇ ψ 的一条路径；析取与蕴涵同理。假 ⊥̇ 完全不含常元，其两种读法是同一个值，路径即 refl。

    ⊨-map (φ ∧̇ ψ)  γ = cong₂ _⊓_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map (φ ∨̇ ψ)  γ = cong₂ _⊔_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map (φ ⇒̇ ψ)  γ = cong₂ _⇒_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map ⊥̇        γ = refl

量词会把一个元素 x 加到环境的最前端。对无界量词，归纳假设对每个 x : S 给出一条路径；函数外延性把这些逐点路径合成一条函数路径，cong 再将存在量化或全称量化沿它搬运。

    ⊨-map (∃̇ φ)    γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x → ⊨-map φ (x ∷ γ)))
    ⊨-map (∀̇ φ)    γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x → ⊨-map φ (x ∷ γ)))

有界量词还多一个成分：⟦⟧-map 识别界定词项的两种解释，归纳假设识别量词作用域的两种解释。对蕴含或合取使用同余后，再搬运最外层的量化。

    ⊨-map (∀̇∈ t φ) γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
      cong₂ _⇒_ (cong (x ∈ˢ_) (⟦⟧-map t γ)) (⊨-map φ (x ∷ γ))))
    ⊨-map (∃̇∈ t φ) γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
      cong₂ _⊓_ (cong (x ∈ˢ_) (⟦⟧-map t γ)) (⊨-map φ (x ∷ γ))))

交换引理本身已经包含无参情形，下面的推论只是把它读出来。无参公式是常元域为空类型 ⊥* 的公式：没有需要解释的常元符号，因此经 embed 可以嵌入为任意域 K 上的公式，而其含义的两种读法无论 K 与 ι 如何都必须一致。

内层模块固定任意目标域 K 与解释 ι : K → S，然后打开两次满足关系：一次通常地用于 K 上的公式，一次以名字 _⊨∅_ 用于空常元域上的公式，其解释为函数 λ b → ι (Empty.rec* b)。这个函数是合法的，因为 Empty.rec* 是空类型的消去子：⊥* 的一个元素本可产生任何类型 (包括 S) 的元素，所以该解释实际上永远不需要具体的值。

  module _ {ℓe ℓc} {K : Type ℓc} (ι : K → S) where

    open At K ι using ( _⊨_ )
    open At (⊥* {ℓe}) (λ b → ι (Empty.rec* b)) using () renaming ( _⊨_ to _⊨∅_ )

    embed-⊨ : ∀ {n} (φ : Formula (⊥* {ℓe}) n) (γ : S ^ n)
            → (γ ⊨ embed φ) ≡ (γ ⊨∅ φ)

于是推论 embed-⊨ 就是 ⊨-map 的直接实例，其中 f 取为视为函数 ⊥* → K 的空消去子 Empty.rec*：对每个无参公式 φ 与环境 γ，embed φ 在 ι 下的满足与 φ 在带 ∅ 标记读法下的满足之间有一条路径。换言之，把无参公式嵌入更丰富的常元域不会改变它所说的话。

    embed-⊨ = ⊨-map Empty.rec* ι

Lévy 见证层

含义只是故事的一半。Lévy 层级按量词结构给公式分类，这一分类用归纳见证表示：Δ₀ φ 是显式数据，证明 φ 中每个量词都有界；Σₙ k φ 与 Πₙ k φ 记录交替的无界块。由于常元改名只替换常元符号，而让每个联结词与量词 (无论有界与否) 原位不动，见证理应幸存。mapΔ₀ 先在 Δ₀ 层面展示这一点，随后互归纳把它向上扩展。

常元改名只替换常元符号，而让每个量词 (无论有界与否) 原位不动，因此公式的量词形状在 mapFo f 下不变。Lévy 见证记录的正是这一形状，所以它应当能沿任意 f 搬运。mapΔ₀ 的类型在基底层面陈述了这一点：从 φ 的一个 Δ₀ 见证产生 mapFo f φ 的一个 Δ₀ 见证。原子情形是直接的：t ∈̇ u 的见证 δ-∈ 不带参数，因为原子公式没有需要约束的量词，而 mapFo f 把该公式变为同一形状的另一个原子公式，所以 δ-∈ 再次证明它；≐ 同理。

mapΔ₀ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
        {n} {φ : Formula K n} → Δ₀ φ → Δ₀ (mapFo f φ)
mapΔ₀ f δ-∈ = δ-∈
mapΔ₀ f δ-≐ = δ-≐
mapΔ₀ f (δ-∧ c d) = δ-∧ (mapΔ₀ f c) (mapΔ₀ f d)

Δ₀ 的其余构造子是联结词、假与有界量词。每一个都打包其子公式的见证，每次递归调用搬运一个结构上更小的见证，再由该构造子在改名后的公式上重建打包。关键在于，Δ₀ 对无界量词 ∃̇ 与 ∀̇ 没有构造子，只有对有界的 ∀̇∈ 与 ∃̇∈ 的构造子，而这两个情形的递归与联结词完全一样。由于 mapFo f 从不把有界量词变成无界量词，每个见证输入都有对应的情形，这正是定义成为全函数的原因。

mapΔ₀ f (δ-∨ c d) = δ-∨ (mapΔ₀ f c) (mapΔ₀ f d)
mapΔ₀ f (δ-⇒ c d) = δ-⇒ (mapΔ₀ f c) (mapΔ₀ f d)
mapΔ₀ f δ-⊥ = δ-⊥
mapΔ₀ f (δ-∀∈ c) = δ-∀∈ (mapΔ₀ f c)
mapΔ₀ f (δ-∃∈ c) = δ-∃∈ (mapΔ₀ f c)

Δ₀ 层是一个归纳定义的层级的基底：Σₙ 见证要么是 Δ₀ 见证，要么是低一层的 Π 见证，要么是一段无界存在量词的见证；Πₙ 对偶。由于 Σₙ 与 Πₙ 相互定义，二者的改名引理必须在同一个 mutual 块中同时证明。

在 Δ₀ 之上，Σₙ 见证要么是 Δ₀ 见证，要么是低一层的 Π 见证，要么是一段无界存在量词的见证；Πₙ 对偶。两种形式相互定义，因此二者的搬运引理在同一个 mutual 块中同时证明，其形状与 mapΔ₀ 相同：从 φ 的一个 Σₙ (相应地 Πₙ) 见证，产生同一层级 k 上 mapFo f φ 的一个见证。见证 σ-Δ₀ d 包装一个 Δ₀ 见证，由 mapΔ₀ f d 在叶端搬运；见证 σ-Π p 记录层级交替中的一次转向，由调用 Π 引理来处理，这正是两个证明必须互递归的原因。

mutual
  mapΣₙ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
          {k n} {φ : Formula K n} → Σₙ k φ → Σₙ k (mapFo f φ)
  mapΣₙ f (σ-Δ₀ d) = σ-Δ₀ (mapΔ₀ f d)
  mapΣₙ f (σ-Π p)  = σ-Π (mapΠₙ f p)

Σ 的其余情形 σ-∃ s 处理一段无界存在量词：该块在 mapFo f 下仍是块，因此子见证 s 由对 mapΣₙ 自身的递归调用搬运。Π 一侧是完全的对偶，π-Δ₀ 委托给 mapΔ₀，π-Σ 为层级交替调用 mapΣₙ。

  mapΣₙ f (σ-∃ s)  = σ-∃ (mapΣₙ f s)

  mapΠₙ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
          {k n} {φ : Formula K n} → Πₙ k φ → Πₙ k (mapFo f φ)
  mapΠₙ f (π-Δ₀ d) = π-Δ₀ (mapΔ₀ f d)
  mapΠₙ f (π-Σ s)  = π-Σ (mapΣₙ f s)

最后的情形 π-∀ p 与 σ-Π 成镜像，在 Π 一侧搬运层级交替。终止性在这里不是额外的论证而是结构性事实：每次递归调用都作用于见证的结构上更小的分支，而 mapΔ₀ 位于两个递归的叶端。其结果是对整个有限 Lévy 层级的单一搬运原理：由归纳见证记录的公式级别在常元改名下不变。

  mapΠₙ f (π-∀ p)  = π-∀ (mapΠₙ f p)

小结

本章确立了常元改名作用 mapFo f 的两条不变性。语义上，⊨-map 断言常元改名与满足关系可交换，精确地说：改名后在 ι 下求值等于改名前在 ι ∘ f 下求值；无参嵌入 embed-⊨ 作为源域为空的特例随之而来。语法上，mapΔ₀、mapΣₙ 与 mapΠₙ 断言证明公式量词结构的 Lévy 见证可沿任意改名搬运。合起来，公式可以在常元域之间移动，其含义与复杂度见证一同移动；这正是后面章节在空域与可构造层级的各域之间转换时所依赖的事实。