外围公式到 L 上公式

设编码诸章交给我们一条关于层级的公式，而我们要在 L 内部说出同样的话。这里有两处需要调整。公式的常元当前的类型是 V ℓ；要在 L 中读出这条公式，每个常元都必须换成限制载体中的元素，即一个集合连同它可构造的证据。而且原公式的满足是在外围结构中算出的，不是在限制结构中。本章消去这两处，并且逐条公式地进行：被搬运的是特定的 φ，连同记录其常元守界、形状为 Δ₀ 的数据。

消去依赖两个事实，各自都在自己的章中证得。其一，改名机制可以替换任意复杂度公式的常元，只要每个常元带着满足某个界的证据；此处取的界是可构造性而非「落在某层内」，证据就是可构造性的证明。其二，Δ₀ 绝对性说：有界公式在传递类之内与之外含义相同。这条性质是逐条公式证得的，归纳沿「该公式是 Δ₀」的归纳见证进行；对任意公式并不存在笼统的绝对性，也不该指望有，因为无界量词在论域缩小时本就会改值。

两者合起来便是搬运定理：常元全部可构造的 Δ₀ 公式可以在 L 的对象语言中读出，且两种读法一致。一致是一条真值路径，由四步组装而成，而证明自身不花费任何归纳。归纳早已在两个来源的章中各花一次，花在本章收到的数据上。

本章的全部工作都在同一个宇宙层级 ℓ 上进行。解释语言的两个结构，其等词与隶属关系都取值于 hProp (ℓ-suc ℓ)，因此一条满足陈述是一个命题，两条这样的陈述可以由一条路径来比较。外围世界是该层级上的累积层级 V；内层世界则是 L，即在 V 中限制到可构造集所得。

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

open import Base.Prelude

module L.Absoluteness {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

公式 φ 的常元来自外围解释所选的类型，证明 h : BoundedFo InL φ 说明每个常元都是可构造的。改名把这样的常元送到由外围集合及其可构造性证明组成的对，而且这一替换对任意复杂度的公式都可用：无界量词原样随行。定理 ⊨-map 比较改变常元类型前后的满足关系；Δ₀ 绝对性比较外围结构与限制结构，但额外要求公式带着自己的 Δ₀ 见证。

open import FOL.Syntax using ( Formula )
open import FOL.LevyHierarchy using ( Δ₀ )
open import FOL.Manipulation.ConstantBounding using ( BoundedFo; module Relabel )
open import FOL.Manipulation.Relabelling using ( ⊨-map )
import FOL.Absoluteness

现在给两个世界命名。外围结构是 𝒮ᵥ，即层级 V ℓ 上类似 ZF 的结构：等词取路径，成员关系取层级原生的 ∈。内层结构是 𝒮ʟ，即 𝒮ᵥ 限制到可构造集的类 isL 所得。本章已选定 isL 作为常元须满足的界；绝对性实例随后对同一个类再提一项要求，即它是传递的，isL-trans 记录的正是这一点。

import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )

open import Cubical.Data.Vec using ( map )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V )

两条满足关系都取值于同一个类型 hProp (ℓ-suc ℓ)。限制后的载体 S 由外围集合及其可构造性证据组成。外围常元通过 id 指称自身；内层常元已经是这样的对，用 fst 投影即可取回外围集合。这两个解释正是搬运证明所比较的两端。

open hPropStructure 𝒮ʟ using ( S )

module SemV = FOL.Semantics 𝒮ᵥ
open SemV using ( _^_ )
open SemV.At (V ℓ) id using () renaming ( _⊨_ to _⊨v_ )

绝对性定理只实例化一次：在界已选定的类 isL 上，附加输入 isL-trans 说明该类是传递的。它的 Δ₀ 规律 abs₀ 取内层语言的一条公式及其 Δ₀ 见证，返回内外满足之间的一条真值路径。见证是一个实打实的参数，而非形式：这条规律恰好对那些已写下 Δ₀ 见证的公式可用，而见证正是在绝对性一章中一次性完成的归纳的路线图，它告诉归纳这一条特定公式是如何构造的。此后内层满足关系被改名为朴素的 _⊨_，因为前台从此只有这一个满足关系。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL using ( abs₀ ) renaming ( _⊨ᵐ_ to _⊨_ )

界是可构造性

在公式动身之前，须先告诉改名机制哪些常元合格、它们变成什么。本节的全部选择就是这个界：层级的一个常元合格，指它可构造；它变成的载体元素，就是该常元与它的可构造性证据之对。往返条件要求把像当作集合读回时得到原常元，由于像把集合存在第一个分量，这由 refl 成立。实例中再没有用到关于 L 的别的东西。

完全不含常元的读式白白合格，这值得点名，因为大多数结构性读式正是这一类：它们全靠变元与有界量词说话，压根没有东西需要可构造。

界谓词就是本节的全部选择。层级的一个常元 c 合格，恰指命题 isL c 成立，即 c 落在可构造层级的某个序数层中；InL 只是取出这个命题值类的底层类型。注意层级落在何处：isL c 是层 ℓ-suc ℓ 上的命题，因此 InL 是取值于该层类型的谓词，而不是集合的可判定性质。

InL : V ℓ → Type (ℓ-suc ℓ)
InL c = ⟨ isL c ⟩

部分常元映射被逐点固定。源常元已在共同世界 V ℓ 中是集合，经 id 读取；目标常元是载体 S 的元素，经 fst 读取。部分赋值把每个带证据 p : InL c 的合格常元 c 送到对 c , p，三角条件要求 fst (c , p) 就是 c，由 refl 成立。于是唯一正确性义务由计算消解，而 L 进入的全部数据只是那份证据 p。

module ToL = Relabel {K = V ℓ} {K' = S} {W = V ℓ}
  id fst InL (λ c p → c , p) (λ c p → refl)

在这个实例中，liftFo 适用于常元满足 InL 的任意复杂度的公式，把每个常元换成外围集合与其可构造性证据组成的对；而 Δ₀-liftFo h dφ 把原公式的 Δ₀ 见证 dφ 变成抬升后公式的 Δ₀ 见证。transferFo 所用的双向规律 abs₀ 只对 Δ₀ 公式比较满足，因此见证必须随身携带，而改名正是使携带成为可能的手段。

open ToL public using ( liftFo; Δ₀-liftFo )

搬运

本节的问题是：一条常元可构造的、关于层级的 Δ₀ 陈述，在 L 中成立与在外成立何时恰好一致？答案就是 transferFo，它被证成一条自模型向外读的四步路径串联。第一步是唯一使用绝对性归纳的一步：那次归纳沿 Δ₀ 见证在其自身的章中一次性完成，此处只是在眼前这条抬升后的公式上调用它。其余三步是改名的簿记，常元至此才被检视，并被发现分毫未动。

这份簿记里有一处值得一提。最后一步的恒等改名不是白费。一条公式并不按定义等于它在常元恒等映射下的像，因为那个映射是递归施加的；但它的含义等于，而那正是常元改名定理在 f = id 处所说的话。

陈述等式的是两条先验地处于不同世界中的满足判断。左边，环境 γ 由 S 的元素组成，每个元素是带可构造性证明的集合，γ ⊨ liftFo φ h 是常元已被改名进 L 的公式在 L 内的满足。右边，同一环境被 map fst 逐项投影，原公式 φ 在外围层级中求值。两边都是同一个 hProp 中的命题，因此所断言的一致是一条路径，而非蕴涵。

transferFo : ∀ {n} (φ : Formula (V ℓ) n) (h : BoundedFo InL φ) → Δ₀ φ
           → (γ : S ^ n) → (γ ⊨ liftFo φ h) ≡ ((map fst γ) ⊨v φ)

第一步更换解释结构而语法不动。绝对性以内层 Δ₀ 见证 Δ₀-liftFo h dφ 施用，把抬升后公式在 L 中的满足，改写为同一公式在层级中、于投影后环境下的满足。第二步是取 f = fst 的改名定理 ⊨-map，它处理抬升后公式的常元与环境变量在投影之下的解释：当常元与环境分量都经 fst 读取时，这条公式所说的东西不变。两步都与内层世界的构造方式一致，sym 再把第二步摆成链条所需的方向。

transferFo φ h dφ γ =
    abs₀ (Δ₀-liftFo h dφ) γ
  ∙ sym (⊨-map 𝒮ᵥ fst id (liftFo φ h) (map fst γ))

剩下两步才涉及常元，合起来断言改名什么也没改。正确性规律 liftFo-correct 给出语法层面的路径 mapFo fst (liftFo φ h) ≡ mapFo id φ：把改名后的公式沿 fst 推进世界，与把原公式沿 id 推进去所得相同，因为三角条件在每个常元处都成立。同余再让这条路径在固定环境与满足符号下移动。最后 ⊨-map 取 f = id，断言公式与其恒等像含义相同，链条就此闭合：L 中的内层满足等于 φ 的外围满足。

  ∙ cong (λ ψ → (map fst γ) ⊨v ψ) (ToL.liftFo-correct φ h)
  ∙ ⊨-map 𝒮ᵥ id id φ (map fst γ)

小结

liftFo 把关于层级的、任意复杂度的公式运进 L 的对象语言，只要其常元可构造；transferFo 附加 Δ₀ 见证的要求，并断言此时两种读法一致。因此本页的等价仅限 Δ₀。越出 Δ₀，绝对性一章证明了两条单向规律：Σ₁ 真值向上传递，Π₁ 真值向下传递，并且它们恰好适用于这两个紧邻类别。这两条结果都不是对「在 L 中能说什么」的限制：那边的分离与替换模式接受任意复杂度的公式。它们标出的是「能从层级直接得到哪些结论」。一个用无界形式写起来更简便的谓词，就应当无界地、直接在模型上写出，而不必经过此处。