Absoluteness

The Levy witnesses earn their keep. The scene is the one Part 4 will play out at scale: a model, a sub-world 𝒮 ↾ M carved out by a class, and formulas asked on both sides. The one condition that tames the passage, transitivity of M (members of members stay in M, exactly what the empty question of the previous chapter needed), was minted with the structures; this chapter spends it, mechanizing the textbook theorem: Δ₀ formulas are absolute between a transitive class and the universe, with the Σ₁-upward and Π₁-downward transfers as cheap extensions, and, as the capstone, the one-line composition that turns an inner graded representation into outer satisfaction.

{-# 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

The setting: one syntax, two semantics

Fix an ambient structure 𝒮 and a transitive class M; the inner world is the restriction 𝒮 ↾ M, whose carrier SM consists of M's members. The syntax takes K := SM: constants in a formula can only be members of M, the parameter discipline enforced by the type. The same formula family then receives two semantics: evaluated outside, in 𝒮, with constants interpreted through

fst; and evaluated inside, in 𝒮 ↾ M, with constants standing for themselves. Relativization is thus not a syntactic operation but two instantiations of one generic semantics; the superscripts ᵛ and ᵐ on the satisfaction symbols read "evaluated where".

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 ⟦_⟧ᵐ )

Inner and outer environments are related by projecting every entry; two private dictionary lemmas settle the term level, where a constant is its own value on both sides and a variable is a lookup.

  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 δ)

The theorem

One induction over the Δ₀ witness. The connective cases are congruences; the atoms go through the term lemmas (equality is the structure field ≈ˢ on both sides, so even that case is a cong₂). The transitivity hypothesis is consumed only in the two bounded-quantifier cases, and there lies the whole mathematical content: outward, a member x of ⟦ t ⟧ must be re-packed as a member of M, and x ∈ ⟦ t ⟧ together with ⟦ t ⟧ ∈ᶜ M yields exactly that by transitivity. The machine locates the textbook proof's load-bearing step to the character.

  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φ }

Σ₁ upward, Π₁ downward

The extensions are one constructor each, and note the asymmetry: neither consumes transitivity. An inner existential witness travels outward through

fst; an outer universal is instantiated at fst. Only Δ₀'s bounded quantifiers ever needed the hypothesis; the machine states the textbook's fine print exactly.

  σ₁-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))

Recap

Transitive classes named, and over them the theorem: abs₀ makes Δ₀ formulas absolute, with transitivity consumed exactly at the bounded quantifiers;

σ₁-up and π₁-down extend the transfer one quantifier kind each, free of the hypothesis. These theorems are pure arithmetic on the Levy witnesses; the composition that will spend them wholesale is catalogued with the reification framework at the book's tail.