Formula expressions for coded recursion

The coded satisfaction recursion must decide, inside L, questions of the form: does the environment γ satisfy the coded formula c? To recognize a compound value such as a Kuratowski pair while keeping the description bounded, its witnesses must themselves be elements of the model. For a pair q with components u and v, a constructible set s is needed with s a member of q and u, v members of s, and the reading formula binds all three at once, evaluating the two component conditions in the assignment v, u, s followed by the old assignment, with the old slots preserved under the shift.

The chapter builds this once, as a structural reader on a small expression language of assignment slots, constructible literals, numerals, and Kuratowski pairs, and proves it adequate in both directions. The outward direction starts from a satisfaction judgment, eliminates its three truncated existentials into a path proposition, and composes the pairing equation with the recursive component paths. The inward direction chooses the explicit internal elements of the two subexpressions and obtains their common constructible container, without extracting any choice from a truncation.

The same reader then specializes in several directions. Membership of an expression's value in the denotation of a term uses transitivity of L: the ambient value's membership in the constructible interpretation of the term proves that value constructible, so it can serve as a model element; this is a genuine construction, distinct from the proposition-valued target restriction that licenses eliminating a truncation. Extensional set descriptions are an ordinary pair of universally quantified implications, with no outer truncation; they characterize a candidate set rather than construct one. The arity-tag recognizers read two nested pairing layers, the arity paired with a tag-and-payload code. Finally the successor and environment-extension formulas are lifted by bounded absoluteness, whose transfer rests on the established transitive-model setup together with the compatibility of lookups under projection. The environment-extension formula closes the chapter.

To keep a first-order description of a compound value in the bounded fragment, fixed pieces are named by constants and each witness is bounded. Everything here takes place at one fixed level ℓ: the ambient hierarchy is V ℓ, and the model whose elements the bounded quantifiers range over is the constructible one sitting inside it. Since a satisfaction judgment compares truth values, the facts the formulas assert are propositions in hProp (ℓ-suc ℓ).

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

open import Base.Prelude

module L.Coding.Expressions {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

Two sides of one distinction run through the chapter. Out in the hierarchy, the structure 𝒮ᵥ interprets the first-order language over V ℓ, and Kuratowski pairing there is the operation pr. Inside the model, the same language is reinterpreted over constructible sets. A clause that recognizes a compound value must therefore be readable in both places at once, and each adequacy statement below says exactly that: the truth value of the internal formula, read in the model, is identified, as a path, with the corresponding ambient statement about pr and the projected assignment.

open import FOL.Syntax
  using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _⇒̇_; ∀̇_; ∃̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )

An element of the constructible model is an ambient set together with a proof that it is constructible. Transitivity of L is what lets bounded witnesses move between the two sides: a member of a constructible set is itself constructible, by isL-trans, and so becomes an element of the model in its own right. Bounded absoluteness does the corresponding work for formulas. A Δ₀ formula about the hierarchy, all of whose constants name constructible sets, means the same inside L; the constant bounding recorded by the BoundedFo data is precisely the hypothesis this transfer needs. The successor and environment-extension formulas are already proved on the hierarchy side, and lifting them into the model is a matter of applying this transfer.

open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import FOL.Manipulation.ConstantBounding using ( BoundedFo )
open import L.Absoluteness {ℓ} using ( InL; liftFo; transferFo )
open import L.Coding.Environment {ℓ}
  using ( sucAt; Δ₀-sucAt; sucAt-adequate; consAt; Δ₀-consAt; consAt-adequate

The numerals need one compatibility fact. The internal numeral numeralL k realizes the von Neumann natural k inside the model, and numeralL-fst identifies its projection with the ambient # k; both directions of the numeral clause lean on this. Because several clauses quantify over finitely many slots at once, environments are shifted along a reindexing of slots. One logical form recurs throughout: an adequacy statement is a path of truth values, obtained from the two implications of an equivalence of propositions, and the bounded quantifiers of the object language are read as truncated existence.

        ; env; cons; shiftPairAt; sgl0At; pair0At; tag0At )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )

open import Cubical.Data.Vec using ( map )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Functions.Logic using ( ⇔toPath; ∃[∶]-syntax )

The ambient hierarchy V ℓ is an h-set, so the equality of two of its sets is a proposition and can sit inside a truth value; this is what makes the packaged equations below legitimate. The natural numbers enter as sets: # k is the von Neumann numeral in the hierarchy and sucV its successor operation, a notion distinct from any universe level and from the arity indices the codes carry. Propositional truncation gives mere existence, and eliminating it is legitimate only into a proposition-valued target, a restriction the pair reader's outward proof honors explicitly.

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )

The truth values at work are the propositions of hProp at level ℓ-suc ℓ, each packaged with its own proof of propositionhood, and the connectives and quantifiers act directly on these propositions. The model's carrier S consists of the pairs of an ambient set and a constructibility certificate. The absoluteness machinery is set up once for this situation: the structure being relativized is the hierarchy 𝒮ᵥ, the class selecting the submodel is isL, transitivity is what keeps Δ₀ formulas absolute, satisfaction is written ⊨, term interpretation ⟦_⟧, and an environment is a vector of model elements.

open hPropStructure 𝒮ʟ using ( S )

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ ; ⟦_⟧ᵐ to ⟦_⟧ )

open import L.Coding.Model {ℓ}

One piece of the model dictionary matters for the main construction: the pair-shaped fact. The model's pairing prʟ projects to the ambient pairing by prʟ-fst, and its bounded reading formula is prAtL; the record Container with container produces, for a value equal to a pair, a constructible set holding both components. Reading a pair by a bounded formula demands exactly such an intermediate set, and lookup-fst and envOverAt, used later, are the projection and environment facts of the same dictionary.

  using ( lookup-fst; prʟ; prʟ-fst; prAtL; prAtL-adequate; envOverAt
        ; Container; container )

A bounded quantifier in the model ranges over elements of S, so any compound value a formula must recognize has to be matched by bounded witnesses that are themselves elements of the model. This section builds the general tool: an inductive language Expr of values assembled from assignment slots, constructible literals, numerals, and Kuratowski pairs, together with one structural reader turning an expression into a formula, and a two-sided adequacy theorem identifying the formula's meaning with the value the expression denotes. Everything else in the chapter is a specialization of this reader.

Two small preparations open the section. PairIs a p packages the statement that the ambient value a equals p as a truth value: since the hierarchy is an h-set, that equality type is a proposition, and the pairing with setIsSet makes it an inhabitant of hProp (ℓ-suc ℓ). Adequacy statements will compare satisfaction judgments with these packaged equalities along paths. The expression language itself is indexed by a natural number n that fixes how many free-variable slots are available; a slot may well go unused.

private
  PairIs : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
  PairIs a p = (a ≡ p) , setIsSet a p

module PairExpression where
  data Expr (n : ℕ) : Type (ℓ-suc ℓ) where

The language of expressions is fixed by four constructors, and each names one way a compound value can present itself to a formula. A slot i refers to the i-th entry of an ambient assignment, the analogue of a variable; a literal a names a whole element of the model, constructibility certificate included, so it behaves like an object-language constant; a numeral k names the von Neumann natural k; and pair composes two subexpressions into a Kuratowski pair. An expression is a finite description of a value, not itself a set, so it admits two independent readings, and the goal is to prove that they agree.

    slot : Fin n → Expr n
    literal : S → Expr n
    numeral : ℕ → Expr n
    pair : Expr n → Expr n → Expr n

  value : ∀ {n} → Expr n → (Fin n → V ℓ) → V ℓ

The first reading is ambient. Given an assignment of hierarchy sets to the slots, value computes the set an expression denotes: a slot is looked up, a literal projects away its certificate with fst, a numeral becomes # k, and a pair is the Kuratowski pair pr of the two denoted sets. This is the reading the adequacy theorem will recover on its right-hand side: the point of a bounded formula is to identify, from inside the model, a value that is naturally described out here.

  value (slot i) γ = γ i
  value (literal a) γ = fst a
  value (numeral k) γ = # k
  value (pair a b) γ = pr (value a γ) (value b γ)

  element : ∀ {n} → Expr n → (Fin n → S) → S

The second reading stays inside the model. Given an assignment of elements of S to the slots, element computes an element of S: literals are already model elements carrying their certificates, numerals use the internal numerals numeralL, and pairs are formed by the model's own pairing prʟ. The two readings are parallel clause by clause, and this parallelism is what makes the bridge between them provable: to compare them one only ever compares corresponding cases.

  element (slot i) γ = γ i
  element (literal a) γ = a
  element (numeral k) γ = numeralL k
  element (pair a b) γ = prʟ (element a γ) (element b γ)

  element-fst : ∀ {n} (e : Expr n) (γ : Fin n → S)

The bridge is element-fst: projecting an internal element yields, as a path, exactly the ambient value at the projected assignment. For slots and literals the two readings coincide on the nose, so the proof is refl. A numeral is the first genuine case: its internal form projects to the ambient one by numeralL-fst, the compatibility fact between internal and ambient numerals that the numeral chapter supplies. Note the direction, since it recurs throughout: the path goes from the projection of the internal value to the ambient value.

              → fst (element e γ) ≡ value e (λ i → fst (γ i))
  element-fst (slot i) γ = refl
  element-fst (literal a) γ = refl
  element-fst (numeral k) γ = numeralL-fst k
  element-fst (pair a b) γ = prʟ-fst (element a γ) (element b γ)

The pair case composes two independent compatibilities: the model's pairing projects to the ambient pairing by prʟ-fst, and each component's projection law is the recursive fact. Congruence under pr assembles the two component paths into one, and the projection law for a nested expression follows by induction. On the syntactic side, lift3 is the reindexing the pair reader will need: it shifts every old slot three places up, lift3 ρ i = suc (suc (suc (ρ i))), preserving which old entry each slot refers to while making room for three fresh variables.

    ∙ cong₂ pr (element-fst a γ) (element-fst b γ)

  lift3 : ∀ {n m} → (Fin n → Fin m) → Fin n → Fin ( + m)
  lift3 ρ i = suc (suc (suc (ρ i)))

  read : ∀ {n m} → Expr n → (Fin n → Fin m) → Fin m → Formula S m
  read (slot i) ρ q = var q ≐ var (ρ i)

The reader read turns an expression at slot q into a bounded formula. A slot demands equality with the corresponding reindexed variable, a literal equality with its constant, a numeral equality with the constant naming its internal numeral. The pair case carries the mathematical content. It binds, by three bounded existentials, a set s in the set at q and elements u, v in s, so that s is a member of the entry at q and u, v are members of s; through the model's pair-reading formula prAtL it asserts that the entry at q equals the pair pr u v. The component conditions are then read recursively at the shifted slots, which is what lift3 provides. Thus a compound value is recognized from inside the model through a constructible intermediate set holding both Kuratowski components.

  read (literal a) ρ q = var q ≐ con a
  read (numeral k) ρ q = var q ≐ con (numeralL k)
  read (pair a b) ρ q = ∃̇∈ (var q) (∃̇∈ (var zero) (∃̇∈ (var (suc zero))
    (prAtL (suc (suc (suc q))) (suc zero) zero
      ∧̇ (read a (lift3 ρ) (suc zero) ∧̇ read b (lift3 ρ) zero))))

Adequacy has two directions, and out is the one a soundness proof consumes: from an inhabitant of the satisfaction judgment it produces the path saying that the entry at q projects to the denoted value. Slots and literals already are such paths by definition, and the numeral case composes the hypothesis with numeralL-fst, the same direction as in element-fst. The interesting work is the pair case, which occupies the next two steps.

  out : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
       → ⟨ γ ⊨ read e ρ q ⟩ → fst (lookup q γ) ≡ value e (λ i → fst (lookup (ρ i) γ))
  out (slot i) ρ q γ h = h
  out (literal a) ρ q γ h = h
  out (numeral k) ρ q γ h = h ∙ numeralL-fst k

The hypothesis of the pair case is a truncated bounded existential with three layers, so the proof eliminates them one at a time, and each elimination needs a proposition-valued target. This is where setIsSet enters: the conclusion is a path in the hierarchy, which is an h-set, hence the target is a proposition and the eliminations are legitimate. What truncation gives and what it does not should be stated plainly. The witnesses s, u, v arrive as elements, so the mathematics can use them, but the hypothesis asserts only their mere existence: no uniqueness, and no chosen representatives.

  out (pair a b) ρ q γ = PT.rec (setIsSet _ _) (λ { (s , s∈ , hs) →
    PT.rec (setIsSet _ _) (λ { (u , u∈ , hu) →
      PT.rec (setIsSet _ _) (λ { (v , v∈ , p , ha , hb) →
        subst ⟨_⟩ (prAtL-adequate (suc (suc (suc q))) (suc zero) zero (v ∷ u ∷ s ∷ γ)) p
        ∙ cong₂ pr (out a (lift3 ρ) (suc zero) (v ∷ u ∷ s ∷ γ) ha)

With the three witnesses in hand, the innermost formula is unfolded by the pair reader's own adequacy: transporting p along prAtL-adequate turns the pairing assertion into the equation fst (lookup q γ) ≡ pr (fst u) (fst v). The two recursive hypotheses then give the components' projections at slots one and zero, fst u ≡ value a and fst v ≡ value b, and congruence under pr rewrites the right-hand side into pr (value a) (value b), which is exactly the value of the pair expression. The inner proof is thus one transport followed by one congruence.

                   (out b (lift3 ρ) zero (v ∷ u ∷ s ∷ γ) hb) }) hu }) hs })

  into : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
        → fst (lookup q γ) ≡ value e (λ i → fst (lookup (ρ i) γ)) → ⟨ γ ⊨ read e ρ q ⟩
  into (slot i) ρ q γ h = h
  into (literal a) ρ q γ h = h

The converse direction into builds an inhabitant of the satisfaction judgment from the bare equation. Slots and literals are immediate; the numeral case composes with the symmetry of numeralL-fst, reversing the direction of the earlier compatibility. In the pair case all three truncated layers must be supplied at once, and here nothing is extracted from a truncation: the witnesses are constructed outright. The internal elements u and v are chosen as element a and element b in the reindexed assignment, and Container and container use the adjusted path e to produce a constructible set s containing both, with all membership certificates. This is a use of transitivity of L in its own right, distinct from the proposition-valuedness that licensed the eliminations above: there truncation was consumed, here concrete elements are produced.

  into (numeral k) ρ q γ h = h ∙ sym (numeralL-fst k)
  into {n} {m} (pair a b) ρ q γ h = ∣ s , c .snd .fst , ∣ u , c .snd .snd .fst ,
    ∣ v , c .snd .snd .snd ,
      subst ⟨_⟩ (sym (prAtL-adequate (suc (suc (suc q))) (suc zero) zero δ)) e
      , into a (lift3 ρ) (suc zero) δ (element-fst a η)

The extended assignment δ is v ∷ u ∷ s ∷ γ, and its layout is the whole bookkeeping of the construction:

The pair formula asserts s ∈ q, u ∈ s, v ∈ s, and q ≡ pr u v; since u sits at slot one and v at slot zero, the recursive reads read a at slot one and read b at slot zero consult exactly the old slots, by lift3. Each subproof is assembled by into itself at the shifted slot, fed the projection path element-fst for the component being read, and the three nested truncated existentials are closed with one explicit ∣_∣₁ per layer.

      , into b (lift3 ρ) zero δ (element-fst b η) ∣₁ ∣₁ ∣₁
    where
    η : Fin n → S
    η i = lookup (ρ i) γ
    u v : S

The remaining local definitions record the arithmetic of the construction. η restricts the old assignment to the reindexed slots, and u and v are the explicit internal elements of the two subexpressions under it; these are chosen outright, not extracted from any truncation. The path e then states that the entry at q equals the ambient pair pr (fst u) (fst v). Its direction matters: the hypothesis h says the entry equals the denoted value of the whole pair, and composing with the symmetry of the components' projection congruence element-fst produces exactly the target the container construction expects.

    u = element a η
    v = element b η
    e : fst (lookup q γ) ≡ pr (fst u) (fst v)
    e = h ∙ sym (cong₂ pr (element-fst a η) (element-fst b η))
    c : Container (lookup q γ) u v

The container is produced from the path e, and its first component is the desired constructible set s, the common intermediate through which both Kuratowski components are reached: s is a member of the entry at q, and u and v are members of s. Prepending v, then u, then s to γ yields the extended assignment δ of arity three more than the original. Every remaining ingredient of the inward construction is now an entry of δ rather than a free-standing element.

    c = container (lookup q γ) u v e
    s : S
    s = c .fst
    δ : S ^ (suc (suc (suc m)))
    δ = v ∷ u ∷ s ∷ γ

The two directions assemble into the advertised form. adequate states that the satisfaction judgment at γ equals, as a truth value, the packaged equation between the projected entry at q and the ambient denotation; ⇔toPath converts the pair of implications out and into into that path. As the first application, member e C says that the value of e belongs to the denotation of the term C: it boundedly quantifies over a member of C's interpretation and demands the expression reader at that member's extended assignment, with the expression shifted into the leading slot.

  adequate : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
            → (γ ⊨ read e ρ q) ≡ PairIs (fst (lookup q γ)) (value e (λ i → fst (lookup (ρ i) γ)))
  adequate e ρ q γ = ⇔toPath (out e ρ q γ) (into e ρ q γ)

  member : ∀ {n} → Expr n → Term S n → Formula S n
  member e C = ∃̇∈ C (read e suc zero)

The outward reader of member eliminates the truncated bounded existential and receives a member x, its membership proof h, and the proof p that x's extended assignment satisfies the expression reader. Applying adequacy outward converts p into the equation fst x ≡ value e ...; transporting h along that equation turns membership of fst x into membership of the denoted value. The target is the membership proposition value e ... ∈ fst (⟦ C ⟧ γ), whose second component supplies exactly the propositionhood required by PT.rec.

  member-out : ∀ {n} (e : Expr n) (C : Term S n) (γ : S ^ n)
              → ⟨ γ ⊨ member e C ⟩ → ⟨ value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ) ⟩
  member-out e C γ = PT.rec (snd (value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ)))
    (λ { (x , h , p) → subst (λ v → ⟨ v ∈ fst (⟦ C ⟧ γ) ⟩) (out e suc zero (x ∷ γ) p) h })

  member-in : ∀ {n} (e : Expr n) (C : Term S n) (γ : S ^ n)

The inward reader must exhibit the member, and the value of e itself serves, once it is made an element of the model. It is a member of fst (⟦ C ⟧ γ) by hypothesis, and the interpretation of the term is constructible, so transitivity of L hands over the constructibility certificate for the value: that is exactly what isL-trans does here. This use of transitivity is different in kind from the proposition-valued target restriction on truncation elimination: no truncation is in play, and what is produced is the explicit data that makes the ambient value a pair of itself and its certificate. With that, x is exactly such a pair, and the entry at the extended assignment projects to the value definitionally, so the recursive into receives the path refl.

             → ⟨ value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ) ⟩ → ⟨ γ ⊨ member e C ⟩
  member-in e C γ h = ∣ x , h , into e suc zero (x ∷ γ) refl ∣₁
    where
    x : S
    x = value e (λ i → fst (lookup i γ)) , isL-trans h (snd (⟦ C ⟧ γ))

The first specialization turns the generic reader into a tag recognizer. tagAtL s k x reads, at slot s, the expression pairing the numeral k with the slot x; it is therefore the bounded formula asserting that the entry at s is the ordered pair of # k and the entry at x. Codes in the recursion carry a numeric tag paired with their payload, and this is exactly that shape.

tagAtL : ∀ {n} → Fin n → ℕ → Fin n → Formula S n
tagAtL s k x = PairExpression.read
  (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot x)) id s

tagAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (x : Fin n) (γ : S ^ n)
  → (γ ⊨ tagAtL s k x)

Its adequacy lemma needs no new proof: instantiating the generic adequacy at this expression with the identity relabelling already computes to the identification of the satisfaction judgment with PairIs of the projected entry and pr (# k) of the projected payload. This is the pattern of the whole section: choose an expression, cite PairExpression.adequate, and the meaning of the clause is read off.

  ≡ PairIs (fst (lookup s γ)) (pr (# k) (fst (lookup x γ)))
tagAtL-adequate s k x γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot x)) id s γ

tagPairAtL : ∀ {n} → Fin n → ℕ → Fin n → Fin n → Formula S n
tagPairAtL s k a b = PairExpression.read

The second specialization handles payloads that are themselves pairs, and the two pairing layers are nested in the expression. tagPairAtL s k a b reads the numeral k paired with the pair of the two slots a and b, so it recognizes entries of the shape pr (# k) (pr (entry a) (entry b)): a tag over a two-component payload.

  (PairExpression.pair (PairExpression.numeral k)
    (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b))) id s

tagPairAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ tagPairAtL s k a b)
  ≡ PairIs (fst (lookup s γ))

The adequacy lemma again computes directly from the generic one, recovering all three components: the tag numeral, and both payload entries after projection. The nesting is handled entirely inside the expression reader; at the level of these clauses nothing but the expression shape is visible.

      (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ))))
tagPairAtL-adequate s k a b γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.numeral k)
    (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b))) id s γ

Sets by extension

The reader of the previous section recognizes a value through its Kuratowski pairing layers; many recursion clauses instead need to say what the members of a set are. Both are statements of the same kind: a first-order formula in the model that, read back in the ambient hierarchy, identifies the value held in a slot. This section builds the extensional shape.

extAt y φ says of the set in slot y that it has exactly the members satisfying a unary condition φ. Its outer structure is two unbounded universal quantifiers joined by an ordinary conjunction: one implication from membership in the set to φ, and one back. extAt itself adds no new propositional truncation, though the parameter φ is an arbitrary formula and may internally contain quantifiers and truncated existentials of its own. Because the outer evidence is a plain conjunction, its two readings are simply the projections of that conjunction, and its introduction is simply their ordered pair. This is the right level of strength for a description: the formula characterizes a candidate set and says nothing about whether one exists, which is a matter for the construction that later supplies the value.

The definition binds one fresh variable for the candidates and is the conjunction of two unbounded universal quantifiers: every member of the set in slot y satisfies φ, and every satisfier is a member. The outer connective is an ordinary conjunction and extAt wraps neither implication in truncation, but the condition φ is passed through as given and may be any formula, with quantifiers or truncated existentials inside. What extAt itself fixes is only the outer shape: a pair of implications under a quantifier, each side being a function on model elements and their satisfaction proofs. That is exactly why the formula can serve as a description: it constrains a value without ever asserting one.

extAt : ∀ {n} → Fin n → Formula S (suc n) → Formula S n
extAt y φ = ∀̇ ((var zero ∈̇ var (suc y)) ⇒̇ φ)
         ∧̇ ∀̇ (φ ⇒̇ (var zero ∈̇ var (suc y)))

module _ {n : ℕ} (y : Fin n) (φ : Formula S (suc n)) (γ : S ^ n) where
  extAt-out : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)

The two readers are the two projections of the outer conjunction. From an inhabitant of extAt y φ, extAt-out takes the first component, which assigns to every model element z the implication from membership of fst z in the set at y to satisfaction of φ in the extended environment; extAt-in takes the second component, which gives that implication in reverse. Neither reader eliminates a truncation, chooses a witness, or transports along a path; whatever φ may contain internally, at this outer level the evidence is an ordered pair and each reader is literally a projection of it.

            → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩
  extAt-out h = h .fst

  extAt-in : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)
           → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩
  extAt-in h = h .snd

Introduction runs the projections in reverse and is the ordered pair of the two implications, each supplied as a function. Hence extAt-in-both: a clause that can establish both directions of its condition satisfies the formula by pairing the two functions, with no further work at the outer level; any quantifier or truncation work happens inside φ and is discharged there. The statement is worth reading as it stands: it produces an inhabitant of a satisfaction judgment from two functions, and asserts nothing about the existence of a set whose members satisfy φ. Whether such a set is ever supplied is decided where the value is constructed, not here.

  extAt-in-both : ((z : S) → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩)
                → ((z : S) → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩)
                → ⟨ γ ⊨ extAt y φ ⟩
  extAt-in-both f g = f , g

Reading a key in two layers

A key of the satisfaction recursion is a set assembled by two nested pairings: an arity paired with a code, and the code itself a tag numeral paired with a payload. Recognizing such a key by a bounded formula therefore means checking both pairing layers, and the structural reader already does this, since it handles expressions of arbitrary nesting. Each formula below is thus the reader applied to a suitable expression, and each adequacy lemma is the corresponding specialization of PairExpression.adequate. The arity is deliberately kept as a variable slot rather than fixed at a numeral, because a clause for a constructor that produces a subformula of different arity needs to speak about the arity value itself.

arityTagPairAtL c ar k a b says that the set in slot c is the ordered pair whose first component is the set in slot ar and whose second component is itself a pairing: the numeral # k paired with the pair of the sets in slots a and b. The defining expression is pair (slot ar) (pair (numeral k) (pair (slot a) (slot b))), read at c under the identity relabelling, and this is the shape of a key whose payload is a two-slot code.

arityTagPairAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Fin n → Formula S n
arityTagPairAtL c ar k a b = PairExpression.read
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k)
      (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b)))) id c

The adequacy statement identifies the truth value of this formula with the proposition PairIs (fst (lookup c γ)) (...), a path in the ambient hierarchy asserting that the set at c equals the nested Kuratowski pair built from the slot projections. The components can then be read off the right-hand side: the tag numeral # k is fixed, while ar, a and b each contribute their looked-up value. Since the statement is a path of truth values rather than a one-way implication, a later proof may rewrite with it in either direction.

arityTagPairAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagPairAtL c ar k a b)
  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ))
        (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ)))))

The proof is a one-line specialization of PairExpression.adequate to the same expression, relabelling, and slot. The bounded witnesses, the elimination and introduction of truncated existentials, and the transport along the adequacy of prAtL were all discharged once in the structural theorem, so no new semantic argument appears here. With the pair-payload case in place, the one-payload variant arityTagAtL c ar k a is defined the same way, except that the innermost expression is the single slot a rather than a pair of two slots.

arityTagPairAtL-adequate c ar k a b γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k)
      (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b)))) id c γ

arityTagAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Formula S n

The body applies the structural reader at c under the identity relabelling, and the adequacy statement again takes the form of a PairIs path: the set at c equals the arity value paired with # k paired with the value at a. This is the shape needed when a code's payload is a single slot rather than two, for instance one variable index or one subformula slot.

arityTagAtL c ar k a = PairExpression.read
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot a))) id c

arityTagAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagAtL c ar k a)

The adequacy proof again cites PairExpression.adequate at the same expression and slot, mirroring the pair case. Both arity-tag formulas and both adequacy lemmas therefore rest on the one structural theorem, which is the return on building the reader generically. What is done with the recovered arity value belongs to the clauses of the satisfaction recursion, which are stated in L.Coding.SatisfactionClauses; this chapter supplies the shapes those clauses read.

  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ)) (pr (# k) (fst (lookup a γ))))
arityTagAtL-adequate c ar k a γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot a))) id c γ

Looking a subcode up in the table

A satisfaction-table entry records, for a key made of an arity and a code, the set of environments satisfying that formula. Reading a subformula's value therefore means forming that key inside the object language: pairing the arity with the subcode and asserting equality with a candidate set. At the subformula's own arity, the table is universally scanned and the key equality guards an implication selecting the matching entry; when the subformula binds a variable, the same lookup is performed at a next arity witnessed internally by the successor formula of the following section.

The shape of a clause

A clause of the recursion binds a code, its arity, its payload components, and the value recorded at the code, then asserts the tagged shape of the code and states one constructor-specific condition between the recorded values. Reading such a clause back is a chain of rewrites along the adequacy lemmas established in this chapter, and assembling one is those rewrites run backwards.

The positive connectives

For conjunction and disjunction the constructor-specific condition is small: the value at the code is the pointwise conjunction, respectively pointwise disjunction, of the two subvalues, all read from the table at the same arity. Everything the clause needs beyond that condition is the lookup machinery above.

The ambient environment set

envSetAt describes, by the extension characterization, the set of environments at the arity held in one slot, relative to the carrier in another. It characterizes that set; it does not construct one.

The definition applies the extension characterization at slot E, with the environment predicate envOverAt as the condition. That predicate classifies a candidate environment relative to a domain and a range, so the freshly bound variable of extAt, at position zero of the extended environment, plays the role of the candidate. The domain and range arguments appear as suc ar and suc B because the condition is evaluated in the extended environment, one arity above the slots the formula itself binds. By the projections extAt-out and extAt-in, an inhabitant of envSetAt E ar B is exactly a pair of implications saying that the set at E contains precisely those candidate environments over the arity recorded at ar that the carrier at B admits. The formula describes the set; its construction happens where the satisfaction table is built.

envSetAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
envSetAt E ar B = extAt E (envOverAt zero (suc ar) (suc B))

Implication and bottom

Among the logical clauses, implication and bottom stand apart from the positive connectives in the shape of their values. Bottom has no subcodes and its condition inside the common extension frame is false, so its value is empty; it still uses the frame's ambient environment set. Implication is interpreted over the set of all environments at the code's arity, so its clause must name that ambient set and constrain it extensionally; this is why the environment set of the previous section exists. A clause stated as an implication, and not as the join of a complement with the consequent, matches the function-space implication on hProp; the direct implication matches the constructive semantics without invoking excluded middle.

The next arity

sucAtL is the internal formula saying that the set in slot j is the sucV of the set in slot i; its adequacy lemma applies to arbitrary sets, without assuming that either is a numeral or an ordinal.

A clause whose subformula sits one arity higher must consult the table at an arity constrained to be the successor of the current one. The hierarchy-side formula sucAt expresses this set equation and names no constants. Lifting it requires the BoundedFo InL argument expected by liftFo; the separate theorem Δ₀-sucAt is used later by transferFo to justify bounded absoluteness.

The definition is sucAtL i j = liftFo (sucAt i j) _. Because sucAt names no constants, its BoundedFo InL argument contains no nontrivial constructibility witnesses. In the adequacy proof, transferFo receives that argument and, separately, Δ₀-sucAt i j, the hierarchy-side Δ₀ certificate. The result identifies satisfaction with PairIs (fst (lookup j γ)) (sucV (fst (lookup i γ))): the proposition that the set at j is the successor set of the set at i.

sucAtL : ∀ {n} → Fin n → Fin n → Formula S n
sucAtL i j = liftFo (sucAt i j) _

sucAtL-adequate : ∀ {n} (i j : Fin n) (γ : S ^ n)
  → (γ ⊨ sucAtL i j) ≡ PairIs (fst (lookup j γ)) (sucV (fst (lookup i γ)))
sucAtL-adequate i j γ =

The proof composes three paths. The transfer lemma first equates satisfaction of the lifted formula in L with ambient satisfaction of sucAt i j at the projected assignment map fst γ, using the boundedness certificate; the transfer rests on the established transitive-model setup. The hierarchy-side adequacy theorem sucAt-adequate then rewrites that satisfaction as the equality of the interpreted values. Finally, the two lookups of the projected assignment are moved to projections of the lookups in γ by lookup-fst, sucV is moved inside by congruence, and the equation is reassembled under PairIs by cong₂. The result is the identification stated.

    transferFo (sucAt i j) _ (Δ₀-sucAt i j) γ
  ∙ sucAt-adequate i j (map fst γ)
  ∙ cong₂ PairIs (lookup-fst j γ) (cong sucV (lookup-fst i γ))

Extending an environment

consAtL describes extending an environment by a new leading value, and its adequacy lemma identifies the resulting coded environment exactly.

A quantified body is evaluated after adjoining a value at the front of the current environment. The hierarchy-side formula consAt already characterizes this operation, while consAtL will express the same characterization inside the constructible model. Its lift requires boundedness certificates for the singleton, pairing, tagging, and key-shifting relations from which the coded extension is assembled. These relations introduce no constant numeral: the distinguished tag is the empty set, and the new head value is read from slot m. The separate lemma numL, defined immediately below, records the constructibility of ambient numerals for later bounded formulas that do name them.

numL k is defined here and proves the ambient numeral # k constructible. The internal numeral numeralL k already carries constructibility of its projection, and numeralL-fst k identifies that projection with # k; transporting the certificate along this path gives ⟨ isL (# k) ⟩. The following private definitions provide BoundedFo InL data for the formulas used to recognize the empty tag, combining bounded shape with constructibility witnesses for any constants they contain. In particular, sgl0At k characterizes the set in slot k as {∅}: it has an empty member and every one of its members is empty. bddSgl0 supplies that combined data; it is not a separate Δ₀ theorem.

numL : (k : ℕ) → InL (# k)
numL k = subst (λ w → ⟨ isL w ⟩) (numeralL-fst k) (numeralL k .snd)

private
  bddSgl0 : ∀ {n} (k : Fin n) → BoundedFo InL (sgl0At k)
  bddSgl0 k = (_ , (_ , _)) , (_ , (_ , _))

pair0At k j characterizes the set in slot k as the unordered pair {∅, W}, where W is the value of the original assignment at slot j; under its inner binder that same value is addressed by suc j. It is not a Kuratowski pair of the two slot values. The formula tag0At s x then combines sgl0At and pair0At: its two distinguished members are {∅} and {∅, W}, so the set at s is the Kuratowski pair pr ∅ W. The certificates bddPair0 and bddTag0 supply BoundedFo InL data for these descriptions, including the required constructibility witnesses for constants.

  bddPair0 : ∀ {n} (k j : Fin n) → BoundedFo InL (pair0At k j)
  bddPair0 k j = (_ , (_ , _)) , ((_ , _) , (_ , ((_ , _) , (_ , _))))

  bddTag0 : ∀ {n} (s x : Fin n) → BoundedFo InL (tag0At s x)
  bddTag0 {n} s x =
      (_ , bddSgl0 {suc n} zero)

The remainder of bddTag0 pairs the singleton certificate, used for the empty-set tag itself, with the pair certificates for the outer and inner pairing layers. After it, bddShift certifies shiftPairAt p' p, which recognizes the entry at p' as obtained from the entry at p by replacing its numeral key with its successor while keeping the paired value unchanged; the certificate is written as a single placeholder because the formula's bounded subformulas are again the leaves and bounded quantifiers already covered.

    , ( (_ , bddPair0 {suc n} zero (suc x))
      , (_ , (bddSgl0 {suc n} zero , bddPair0 {suc n} zero (suc x))) )

  bddShift : ∀ {n} (p' p : Fin n) → BoundedFo InL (shiftPairAt p' p)
  bddShift p' p = _

  bddCons : ∀ {n} (e' m e : Fin n) → BoundedFo InL (consAt e' m e)

bddCons assembles everything the extension formula needs. Reading its three conjuncts: the extended graph holds an entry that is the empty-set tag over the value at m, the new leading entry, certified by bddTag0 at the shifted slot; every entry of the old graph reappears with its key shifted to the successor, certified by bddShift two arities up; and the remaining conjunct repeats the same two certificates for the membership direction that reads back out of the extension. Each conjunct's certificate lives at the depth its quantifiers create, which is why the arities in the annotations grow to suc (suc n).

  bddCons {n} e' m e =
      (_ , bddTag0 {suc n} zero (suc m))
    , ( (_ , (_ , bddShift {suc (suc n)} zero (suc zero)))
      , (_ , ( bddTag0 {suc n} zero (suc m)
             , (_ , bddShift {suc (suc n)} (suc zero) zero) )) )

With the boundedness certificates assembled, consAtL e' m e is the lift of the hierarchy-side formula consAt e' m e through liftFo, supplied with bddCons as its certificate. Its adequacy statement is conditional where the successor's was not: it takes a family g : Fin k → V ℓ together with a proof hE that the set held in slot e is the coded environment env g. Under that hypothesis, satisfaction of consAtL e' m e is identified, as a truth value, with PairIs (fst (lookup e' γ)) (env (cons (fst (lookup m γ)) g)): the set at e' is exactly the coded environment obtained by pushing the value at m onto the front of g. The formula classifies a candidate against an environment that is already coded; it does not construct one, and the hypothesis about the old environment is precisely what makes the classification well-defined.

consAtL : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
consAtL e' m e = liftFo (consAt e' m e) (bddCons e' m e)

consAtL-adequate : ∀ {n} (e' m e : Fin n) (γ : S ^ n)
  {k : ℕ} (g : Fin k → V ℓ)
  → fst (lookup e γ) ≡ env g

The proof opens with the transfer lemma, given all its inputs at once: the formula consAt e' m e, its boundedness certificate bddCons, and the Δ₀ certificate Δ₀-consAt recorded on the hierarchy side. The transfer is bounded absoluteness in action, and it depends on the established transitive-model setup: because L is transitive and every constant the formula names is constructible, satisfaction of the lifted formula in the carrier moves to satisfaction of the original formula at the projected assignment map fst γ, where ambient facts can be stated directly.

  → (γ ⊨ consAtL e' m e)
  ≡ PairIs (fst (lookup e' γ)) (env (cons (fst (lookup m γ)) g))
consAtL-adequate e' m e γ g hE =
    transferFo (consAt e' m e) (bddCons e' m e) (Δ₀-consAt e' m e) γ
  ∙ consAt-adequate e' m e (map fst γ) g

The hierarchy-side adequacy theorem consAt-adequate then rewrites ambient satisfaction as the identification of the new slot with the extended coded environment. It requires the hypothesis in projected form, which is why lookup-fst e γ is composed with hE on the way in: the projection of the entry at e equals env g. Congruence then moves the two remaining lookups, the value at e' by lookup-fst, and the value at m by cong under the function λ w → env (cons w g). The chain of paths ends exactly at the promised PairIs identification, and this closes the chapter's own mathematics: every internal formula needed to recognize syntax shapes, arities, environments, and their extension is in place.

      (lookup-fst e γ ∙ hE)
  ∙ cong₂ PairIs (lookup-fst e' γ)
      (cong (λ w → env (cons w g)) (lookup-fst m γ))

The unbounded quantifiers

The two unbounded-quantifier clauses use the common bounded frame extB, which binds the ambient environment set F and extension data before applying the quantifier-specific body. In quBody q, the parameter q is the outer quantifier over the carrier set w: it is bounded existential for ∃ and bounded universal for ∀. The inner formula ∃̇∈ ya (consAtL ...), which says that the extended environment occurs in the body's recorded value, is unchanged in both cases. Thus the universal case changes only the outer quantifier to implication semantics; it does not replace an innermost conjunction.

Evaluating a term, and the atoms

A term is a variable or a constant, so the clause evaluating a coded term has two cases: a variable's value is what the environment records at its key, while a constant's value is the constant itself, in any environment at all. The two atoms then evaluate both term codes and compare the resulting values, one asserting membership and the other equality; their payload is a pair of term codes, at which the satisfaction table has no entries, which is why the clause builds the lookups itself rather than taking them from a frame.

The bounded quantifiers

A bounded quantifier's payload is a term code paired with a formula code. The bound is evaluated in the environment by the two-case reader, the body's value is read one arity higher, and the pushed values are restricted to elements of the evaluated bound as well as of the carrier. Ranging over the carrier as well as the bound is not redundant: the reference semantics quantifies over the carrier and guards by membership in the bound, and a bound may have members outside the carrier, so quantifying over the bound alone would demand entries the table does not have.

Recap

This chapter built first-order formulas with which a satisfaction clause recognizes compound values inside L. Three kinds of statement carry it. The structural adequacy of the expression reader identifies, in both directions, the satisfaction of a formula about slots, literals, numerals, and Kuratowski pairs with the equality of the projected entry to the denoted ambient value, the pair case passing through a constructible intermediate set. The extensional characterization extAt is an ordinary conjunction of two universally quantified implications, whose readings and introduction are projections and pairing. And the internal successor and environment-extension formulas are lifted by bounded absoluteness over the transitive model, with the adequacy paths composed from the transferred satisfaction, the hierarchy-side theorems, and the compatibility of lookups under projection. On these the clause shapes of the coded satisfaction recursion rest.