Absoluteness

Lévy 见证开始挣饭钱。这里的场景正是第四部将要大规模上演的那一幕：一个模型，一个由类裁出的子世界 𝒮 ↾ M，同一批公式两侧各问一遍。驯服这趟通行的唯一条件，M 的传递性 (成员的成员不出 M，恰是上一章那个空集之问所需要的)，已随结构一章铸下；本章将它花出，机械化教科书定理：Δ₀ 公式在传递类与全宇宙之间绝对，Σ₁ 向上、Π₁ 向下两条转移作为廉价延伸。

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

module FOL.Absoluteness where

open import Base.Prelude
open import Base.Truth
open import FOL.ZFStructure using ( ZFStructure; Transitive; _↾_ )
open import FOL.Syntax using ( Term; con; var; Formula; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using
  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-¬; δ-⊤; δ-⊥; δ-∀∈; δ-∃∈
  ; Σ₁; σ-Δ₀; σ-∃; Π₁; π-Δ₀; π-∀ )
import FOL.Semantics
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 中求值，常量即其自身。相对化因此不是句法操作，而是同一泛型语义的两次实例化；满足符号上的上标 ᵛ 与 ᵐ 读作「在哪里求值」。

module Single {ℓ} (𝒮 : ZFStructure (hPropAlgebra ℓ))
              (M : ZFStructure.S 𝒮 → hProp ℓ)
              (trans : Transitive 𝒮 M) where

  open TruthAlgebra (hPropAlgebra ℓ)
  open ZFStructure 𝒮

  SM : Type ℓ
  SM = Σ[ x ∈ S ] (x ∈ᶜ M)

  𝒮M : ZFStructure (hPropAlgebra ℓ)
  𝒮M = 𝒮 ↾ M

  module SemV = FOL.Semantics (hPropAlgebra ℓ) 𝒮
  module SemM = FOL.Semantics (hPropAlgebra ℓ) 𝒮M

  open SemV using ( _^_ ) public

  open module V = SemV.At SM fst public
    renaming ( _⊨_ to _⊨ᵛ_ ; ⟦_⟧ to ⟦_⟧ᵛ )
  open module Mse = SemM.At SM id public
    renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )

内外环境经逐项投影相关；两条私有的字典引理解决词项层：常量在两侧都是自身的值，变量是一次查表。

  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 δ

    ⟦⟧-fst : ∀ {n} (t : Term SM n) (δ : SM ^ n)
           → fst (⟦ t ⟧ᵐ δ) ≡ ⟦ t ⟧ᵛ (map fst δ)
    ⟦⟧-fst (con m) δ = refl
    ⟦⟧-fst (var i) δ = sym (lookup-fst i δ)

定理

对 Δ₀ 见证做一次归纳。联结词情形皆同余；原子走词项引理 (等词两侧都是结构字段 ≈ˢ，连这个情形也归于 cong₂)。传递性前提只在两个有界量词情形被消费，全部数学内容就在那里：往外走时，⟦ t ⟧ 的成员 x 须重新打包为 M 的成员，而 x ∈ ⟦ t ⟧ 加 ⟦ t ⟧ ∈ᶜ M 经传递性恰好给出这一点。教科书证明的承重步被机器定位到字符。

  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 δ)
  abs₀ (δ-∨ d e) δ = cong₂ _⊔_ (abs₀ d δ) (abs₀ e δ)
  abs₀ (δ-⇒ d e) δ = cong₂ _⇒_ (abs₀ d δ) (abs₀ e δ)
  abs₀ (δ-¬ d)   δ = cong ¬_ (abs₀ d δ)
  abs₀ δ-⊤ δ = refl
  abs₀ δ-⊥ δ = refl
  abs₀ (δ-∀∈ {t = t} {φ = φ} d) δ = ⇔toPath fwd bwd
    where
    tm : SM
    tm = ⟦ t ⟧ᵐ δ
    p : fst tm ≡ ⟦ t ⟧ᵛ (map fst δ)
    p = ⟦⟧-fst t δ
    fwd : ⟨ δ ⊨ᵐ (∀̇∈ t φ) ⟩ → ⟨ (map fst δ) ⊨ᵛ (∀̇∈ t φ) ⟩
    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 φ) ⟩
    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
    tm : SM
    tm = ⟦ t ⟧ᵐ δ
    p : fst tm ≡ ⟦ t ⟧ᵛ (map fst δ)
    p = ⟦⟧-fst t δ
    fwd : ⟨ δ ⊨ᵐ (∃̇∈ t φ) ⟩ → ⟨ (map fst δ) ⊨ᵛ (∃̇∈ t φ) ⟩
    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 φ) ⟩
    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 处实例化。只有 Δ₀ 的有界量词才需要那条前提；教科书的小字被机器一字不差地陈述出来。

  σ₁-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)
          → ⟨ (map fst δ) ⊨ᵛ φ ⟩ → ⟨ δ ⊨ᵐ φ ⟩
  π₁-down (π-Δ₀ d) δ = subst ⟨_⟩ (sym (abs₀ d δ))
  π₁-down (π-∀ s)  δ h xm = π₁-down s (xm ∷ δ) (h (fst xm))

小结

传递类得名，其上是定理本体：abs₀ 使 Δ₀ 公式绝对，传递性恰在有界量词处被消费；σ₁-up 与 π₁-down 各以一种量词延伸转移，且不花前提。这些定理是对 Lévy 见证的纯粹算术；将要成批花费它们的那次复合，编在书末的 reification 框架里。