---
title: "外围公式到 L 上公式"
module: L.Absoluteness
lang: zh
site: "Bedrock"
description: "环境公式到 L 上公式"
stage: "可构造层与公理"
reading_order: 37
canonical: https://bedrock.institute/zh/L.Absoluteness.html
html: L.Absoluteness.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Absoluteness.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantBounding, FOL.Manipulation.Relabelling, FOL.Absoluteness, FOL.Semantics, V.Hierarchy, L.Constructible]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Absoluteness.md, https://bedrock.institute/ja/L.Absoluteness.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 外围公式到 L 上公式

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

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

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

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

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

open import Base.Prelude

module L.Absoluteness {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
```

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

```agda
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` 记录的正是这一点。

```agda
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` 投影即可取回外围集合。这两个解释正是搬运证明所比较的两端。

```agda
open hPropStructure 𝒮ʟ using ( S )

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

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

```agda
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` 是取值于该层类型的谓词，而不是集合的可判定性质。

```agda
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`。

```agda
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₀` 只对 Δ₀ 公式比较满足，因此见证必须随身携带，而改名正是使携带成为可能的手段。

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

## 搬运

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

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

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

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

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

```agda
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` 中的内层满足等于 `φ` 的外围满足。

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

## 小结

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