---
title: "Formula expressions for coded recursion"
module: L.Coding.Expressions
lang: en
site: "Bedrock"
description: "Formula expressions for coded recursion"
stage: "Internal coding: expressions and domains"
reading_order: 43
canonical: https://bedrock.institute/en/L.Coding.Expressions.html
html: L.Coding.Expressions.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Expressions.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, FOL.Manipulation.ConstantBounding, L.Absoluteness, L.Coding.Environment, L.Axioms.Numerals, L.Coding.Model]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.Expressions.md, https://bedrock.institute/ja/L.Coding.Expressions.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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 ℓ)`.

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

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

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

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

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

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

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

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

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

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

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

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

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

  lift3 : ∀ {n m} → (Fin n → Fin m) → Fin n → Fin (3 + 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.

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

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

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

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

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

| slot | entry | role |
| --- | --- | --- |
| 0 | `v` | internal element of `b` |
| 1 | `u` | internal element of `a` |
| 2 | `s` | the intermediate set, a member of the entry at `q` |
| `i + 3` | old slot `i` | the original assignment, unchanged |

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
    , ( (_ , 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)`.

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

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

```agda
  → (γ ⊨ 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.

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