Reading a hierarchy formula inside L

The coding chapters wrote their readers about the hierarchy: a formula whose constants are sets of V, evaluated where the quantifiers range over all of V. The chapters that consume them from here on speak about L instead: formulas whose constants are elements of the model, evaluated where the quantifiers range over L only. The two are different languages, and something has to carry a reader from one to the other.

Two facts do it, and both are already proved. Relabelling replaces each constant of a formula by an element of the model, provided each constant is one; that is the bounded-formula machinery, used here with the bound "constructible" rather than "inside a stage". And Δ₀ absoluteness says that a bounded formula means the same thing inside a transitive class as outside it, which is what makes the replacement harmless.

So a Δ₀ reader whose constants are constructible transfers, and the transfer is one chain of four steps with no induction of its own. Every later chapter that wants to say, in the object language of L, that one set is the pair of two others, or that a code has such-and-such a shape, gets to say it by quoting a reader and applying this.

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

open import Base.Prelude
open import Base.Truth

module L.Absoluteness {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
open import FOL.LevyHierarchy using ( Δ₀ )
open import FOL.Manipulation.Bounding using ( BoundedFo; module Relabel )
open import FOL.Manipulation.Relabelling using ( ⊨-map )
import FOL.Absoluteness
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 )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ using ( S )

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

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

The bound is constructibility

The relabelling is instantiated once. A constant of the hierarchy is admissible when it is constructible; the element of the model it becomes is that constant paired with its certificate; and the round trip is refl, since taking the underlying set of that pair gives the constant back. Nothing else about L is used.

A reader with no constants at all is admissible for free, which is worth naming, because most of the structural readers are of that kind: they speak entirely through variables and bounded quantifiers, so there is nothing to be constructible.

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

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

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

The transfer

Four steps, read from the model outward. Absoluteness moves the lifted formula from satisfaction in L to satisfaction in the hierarchy at the projected environment. Then relabelling along the projection is undone, twice: once to recognize the lifted formula as the original with its constants replaced, and once, in the opposite direction, to see the original as itself. The middle step is where the relabelling's own correctness enters, and it is the only place the constants are looked at.

The identity relabelling in the last step is not idle. A formula is not definitionally its own image under the identity map on constants, since the map is applied by recursion; but its meaning is, and that is exactly what the relabelling theorem says at f = id.

transferFo : ∀ {n} (φ : Formula (V ℓ) n) (h : BoundedFo InL φ) → Δ₀ φ
           → (γ : S ^ n) → (γ ⊨ liftFo φ h) ≡ ((map fst γ) ⊨v φ)
transferFo φ h dφ γ =
    abs₀ (Δ₀-liftFo h dφ) γ
  ∙ sym (⊨-map (hPropAlgebra (ℓ-suc ℓ)) 𝒮ᵥ fst id (liftFo φ h) (map fst γ))
  ∙ cong (λ ψ → (map fst γ) ⊨v ψ) (ToL.liftFo-correct φ h)
  ∙ ⊨-map (hPropAlgebra (ℓ-suc ℓ)) 𝒮ᵥ id id φ (map fst γ)

Recap

liftFo carries a Δ₀ formula about the hierarchy into the object language of L, provided its constants are constructible, and transferFo says the two say the same thing. The coding chapters were written on the hierarchy side and stay there; this is how their readers are quoted from the L side, and it costs a chain of four steps rather than a re-statement.

One thing this does not do, and should not be asked to. It is Δ₀ only, because absoluteness is. That is no longer a restriction on what can be said in L, since the comprehension fields there take formulas of any complexity; it is a restriction on what can be imported from the hierarchy for free. A predicate that is easier to write unbounded should be written unbounded, directly over the model, and never routed through here.