---
title: "From ambient formulas to formulas over L"
module: L.Absoluteness
lang: en
site: "Bedrock"
description: "From ambient formulas to formulas over L"
stage: "Constructible stages and the axioms"
reading_order: 37
canonical: https://bedrock.institute/en/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/zh/L.Absoluteness.md, https://bedrock.institute/ja/L.Absoluteness.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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.

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

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.

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

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.

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

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

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

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

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

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

```agda
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 `φ`.

```agda
  ∙ 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.