From ambient formulas to formulas over L

Suppose the coding chapters have handed us a formula about the hierarchy, and we want to say the same thing inside L. Two adjustments stand in the way. The formula's constants currently have type V ℓ; to read the formula in L, each constant must become an element of the restricted carrier, that is, a set together with evidence that it is constructible. And the satisfaction of the original formula was computed in the ambient structure, not in the restricted one. This chapter removes both, and it does so one formula at a time: what is transferred is a particular φ, together with the data recording that its constants obey the chosen bound and that its shape is Δ₀.

The removal rests on two facts, each proved in its own chapter. First, the relabelling machinery can replace the constants of a formula of any complexity, provided each constant comes with evidence that it satisfies a chosen bound; here the bound is constructibility rather than membership in a stage, and the evidence is a constructibility proof. Second, Δ₀ absoluteness says that a bounded formula means the same inside a transitive class as outside it. That property is established formula by formula, by induction on the inductive witness certifying the formula is Δ₀; there is no blanket absoluteness for arbitrary formulas, and none should be expected, since unbounded quantifiers already change their truth value when the domain shrinks.

Putting the two together gives the transfer theorem: a Δ₀ formula whose constants are all constructible can be read in the object language of L, and the two readings agree. The agreement is a path of truth values assembled from four steps, and the proof spends no induction of its own; the inductions were already spent, once in each source chapter, on the data this chapter receives.

The whole chapter takes place at a single universe level ℓ. Both structures that interpret the language have equality and membership valued in hProp (ℓ-suc ℓ), so a satisfaction statement is a proposition, and two such statements can be compared by a path. The ambient world is the cumulative hierarchy V at this level; the inner world is L, obtained from it by restricting to the constructible sets.

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

open import Base.Prelude

module L.Absoluteness {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

The formula φ has constants in a type chosen by the surrounding interpretation, and a proof h : BoundedFo InL φ says that each of those constants is constructible. Relabelling sends such a constant to the pair consisting of the ambient set and its constructibility proof, and it does so for formulas of any complexity: unbounded quantifiers move along untouched. The theorem ⊨-map compares satisfaction before and after this change of constant type, while Δ₀ absoluteness compares the outer and restricted structures, and it asks, in addition, that the formula carry its own Δ₀ witness.

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

The two worlds are now named. The ambient structure is 𝒮ᵥ, the ZF-like structure on the hierarchy V ℓ: paths as equality, and the hierarchy's native membership. The inner structure is 𝒮ʟ, the restriction of 𝒮ᵥ to the class isL of constructible sets. This chapter has already chosen isL as the bound its constants must satisfy; the absoluteness instance then asks one more thing of the same class, namely that it be transitive, which isL-trans records.

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 )

Both satisfaction relations take values in the same type hProp (ℓ-suc ℓ). The restricted carrier S consists of an ambient set paired with evidence that it is constructible. Ambient constants denote themselves through id, whereas an inner constant is already such a pair; projecting it with fst recovers the ambient set. These two interpretations are the endpoints compared by the transfer proof.

open hPropStructure 𝒮ʟ using ( S )

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

The absoluteness theorem is instantiated once, over the class isL that the bound already selected, with the additional input isL-trans saying that this class is transitive. Its Δ₀ law abs₀ takes a formula of the inner language together with its Δ₀ witness and returns a path of truth values between inner and outer satisfaction. The witness is an argument, not a formality: the law is available exactly for those formulas whose Δ₀ witness has been written down, and the witness is what tells the induction, performed once in the absoluteness chapter, how this particular formula is built. From here on the inner satisfaction relation is renamed to plain _⊨_, since it is the only one in the foreground.

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

The bound is constructibility

Before any formula can move, the relabelling machinery must be told which constants are allowed and what they become. The whole choice of this section is that bound: a constant of the hierarchy is admissible when it is constructible, and the element of the carrier it becomes is that constant paired with its constructibility evidence. The round-trip condition, which asks that reading the image as a set give back the constant, holds by refl, since the image stores the set as its first component. Nothing else about L enters the instance.

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.

The bound predicate is the whole choice of this section. A constant c of the hierarchy is admissible precisely when the proposition isL c holds, that is, when c lies in some ordinal stage of the constructible hierarchy; InL just unpacks the underlying type of that proposition-valued class. Note where the level lives: isL c is a proposition at level ℓ-suc ℓ, so InL is a predicate valued in types of that level, not a decidable property of sets.

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

The partial constant map is fixed point by point. A source constant is read in the common world V ℓ by id, since it already is a set there; a target constant, an element of the carrier S, is read by fst. The partial assignment sends each admissible c with evidence p : InL c to the pair c , p, and the triangle condition asks that fst (c , p) be c, which holds by refl. So the only correctness obligation is discharged by computation, and the data of L that entered was the evidence p alone.

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

At this instantiation, liftFo applies to a formula of any complexity whose constants satisfy InL, replacing each constant by the pair of the ambient set with its constructibility evidence; and Δ₀-liftFo h dφ turns a Δ₀ witness dφ for the original formula into a Δ₀ witness for the lifted one. The two-sided law abs₀ used by transferFo compares satisfaction only for Δ₀ formulas, so the witness must be carried along, and the relabelling is exactly what makes carrying it possible.

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

The transfer

The question of this section is: when does a Δ₀ statement about the hierarchy, whose constants are constructible, hold in L exactly when it holds outside? The answer is transferFo, proved as one chain of four path-compositions read from the model outward. The first step is the only one that uses the absoluteness induction: performed once, over Δ₀ witnesses, in its own chapter, it is here invoked at the particular lifted formula. The remaining three steps are relabelling bookkeeping, in which the constants are finally looked at and found unchanged.

One step of that bookkeeping deserves a remark. 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.

The statement equates two satisfaction judgments that a priori live in different worlds. On the left, the environment γ consists of elements of S, each a set with a constructibility proof, and γ ⊨ liftFo φ h is satisfaction inside L, of the formula whose constants have been relabelled into L. On the right, the same environment is projected entrywise by map fst, and the original formula φ is evaluated in the ambient hierarchy. Both sides are propositions in the same hProp, so the claimed agreement is a single path, not an implication.

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

The first step changes the interpretation structure and leaves the syntax alone. Absoluteness is applied with the inner Δ₀ witness Δ₀-liftFo h dφ, and it rewrites satisfaction of the lifted formula in L into satisfaction of the same formula in the hierarchy, at the projected environment. The second step is the relabelling theorem ⊨-map at f = fst, which handles the interpretation of the constants of the lifted formula and of the environment variables under the projection: the formula says the same thing when its constants and its environment entries are both read through fst. The two steps agree with how the inner world was built, and sym presents the second in the direction the chain needs.

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

The remaining two steps involve the constants, and together they say that relabelling changed nothing. The correctness law liftFo-correct gives a syntactic path mapFo fst (liftFo φ h) ≡ mapFo id φ: pushing the relabelled formula into the world along fst yields the original pushed along id, because the triangle condition held at each constant. Congruence then moves this path under the fixed environment and satisfaction symbol. Finally ⊨-map with f = id says a formula and its identity image mean the same, closing the chain: inner satisfaction in L equals ambient satisfaction of φ.

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

Recap

liftFo carries a formula about the hierarchy, of any complexity, into the object language of L as soon as its constants are constructible; transferFo adds the requirement of a Δ₀ witness and says that then the two readings agree. The equivalence on this page is therefore Δ₀ only. Beyond Δ₀, the absoluteness chapter proves two one-way laws, Σ₁ truth passing upward and Π₁ truth passing downward, and they apply specifically to those two adjacent classes. Neither result is a restriction on what can be said in L: the separation and replacement schemas there accept formulas of any complexity. They mark, rather, which conclusions can be drawn directly from the hierarchy. A predicate that is easier to write unbounded should be written unbounded, directly over the model, and not through here.