---
title: "A Δ₀ description of the definable power set"
module: L.GCH.DefinablePowerSetDescription
lang: en
site: "Bedrock"
description: "A Δ₀ description of the definable power set"
stage: "Proving GCH"
reading_order: 101
canonical: https://bedrock.institute/en/L.GCH.DefinablePowerSetDescription.html
html: L.GCH.DefinablePowerSetDescription.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/DefinablePowerSetDescription.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Definability, L.Coding.Model, L.Coding.SatisfactionBridge, L.Coding.DefinablePowerSet, L.Coding.CodeSet, L.Coding.UniformSatisfaction, L.Coding.Satisfaction, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.CodeAlphabet, L.GCH.SatisfactionDescription]
routes: [gch-descriptions]
translations: [https://bedrock.institute/zh/L.GCH.DefinablePowerSetDescription.md, https://bedrock.institute/ja/L.GCH.DefinablePowerSetDescription.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
The problem of this chapter is to recognize, by a bounded formula, the collection of subsets of a constructible carrier that are first-order definable over that carrier with parameters from it. This collection is the definable power set `𝒟ₒ`, not the full internal power set. Its internal description is correct only when the numeral tags, code domain, and satisfaction table have their intended meanings.

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

The construction uses excluded middle as the book's single explicit classical hypothesis. Propositional truncation will nevertheless remain visible throughout: an existence proof may establish that a formula or table value exists without selecting one globally.

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

Fix a universe level `ℓ` and an instance `lem : LEM (ℓ-suc ℓ)`. Every result in the module, including the final soundness and completeness statements, is understood under precisely this hypothesis.

```agda
module L.GCH.DefinablePowerSetDescription {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

The object-language description is deliberately bounded. It is assembled from membership atoms, conjunction, implication, and bounded existential and universal quantifiers; `checkΔ₀` will later verify this syntactic shape. Constant mapping is needed when an externally given formula is compared with its interpretation in the coded satisfaction construction.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; _⇒̇_; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
import FOL.Absoluteness
```

The intended output is `𝒟ₒ W`: the set of subsets of `W` definable in the restricted structure over `W`, with parameters from `W`. Extensionality will identify a candidate output with this set once both membership directions have been proved, while ordered-pair codes represent environments, formula keys, and table entries.

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ; 𝒟ₒ-intro; 𝒟ₒ-inv )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Coding.Model {ℓ} using ( prAtL; container )
```

For a formula `ψ`, the satisfaction construction records which one-entry environments satisfy `ψ`. The bridge theorem identifies the resulting slice of `W` with the subset defined by `ψ`. The genuine code set contains the key built from `ψ`, and functionality of the genuine satisfaction table fixes the value at that key. These facts become available only after `satAt` has certified the proposed code set and table; they do not make decoding unique or select a defining formula for a subset.

```agda
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst; defSet-Sat )
open import L.Coding.DefinablePowerSet {ℓ} lem using ( envOne )
open import L.Coding.CodeSet {ℓ} lem using ( keyS; key∈AllCodes )
open import L.Coding.UniformSatisfaction {ℓ} lem using ( module Table; val-at )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
```

Every quantifier in the description must remain bounded by a set already present in the environment. The auxiliary quantifiers below express the two components of an ordered-pair code within those bounds, and their two directions let us pass between object-language satisfaction and the corresponding semantic witnesses.

```agda
open import L.Coding.Quantification {ℓ} using
  ( sh; i0; i1; i3; i6; f0; f1; down
  ; sndEx; sndAll; sndEx-out; sndAll-in; fillSnd; useSnd
  ; pr-out; pr-in; sndS )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
```

The ten distinguished slots are interpreted as the numerals zero through nine by `Tags`. In particular, the clauses below use the tags zero and one to recognize a one-entry environment and a key of arity one. The separate predicate `satAt` supplies the stronger semantic fact that the proposed code domain and table implement the alphabet and recursive satisfaction construction over the carrier.

```agda
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )
open import L.GCH.SatisfactionDescription {ℓ} lem using ( satAt; module SatRead; module Match )
```

An environment is represented by a finite vector of constructible sets. Products combine the two membership conditions that define a slice, and their propositionhood ensures that truncated witnesses may be eliminated into these conditions without introducing a choice.

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Unit using ( tt )
open import Cubical.Data.Vec using ( _∷_; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Foundations.HLevels using ( isProp× )
```

The proofs repeatedly turn pointwise equivalences of membership into equalities of sets. Membership is proposition-valued, so a merely existing code, formula, or presentation can be eliminated while proving either membership direction; `∈-asFiber` then recovers a presentation index when an ambient member must be read as an element of a carrier.

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈-asFiber )
```

The von Neumann numerals used as tags live in the cumulative hierarchy. In particular, zero marks the only entry of a one-variable environment, while one marks the arity of the formulas considered here.

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_ )
```

Write `S` for the carrier of constructible sets. An element of `S` consists of an underlying set together with its constructibility certificate, so bounded witnesses in the formulas remain inside the intended model.

```agda
open hPropStructure 𝒮ʟ using ( S )
```

We write `γ ⊨ φ` for satisfaction of an object-language formula at a finite environment of constructible sets. The absoluteness result behind this notation lets the later semantic argument compare that internal reading with ordinary membership in the surrounding cumulative hierarchy.

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

A singleton environment is described by two bounded clauses over one slot: every member of the coded set `e` is the ordered pair of the tag zero and the value `z`, and some member of `e` is that pair. The universal clause excludes all other members, and the existential clause excludes the empty set.

```agda
singleOf : ∀ {j} → Fin j → Fin j → Fin j → Formula S j
singleOf e N0 z = ∀̇∈ (var e) (prAtL i0 (sh 1 N0) (sh 1 z)) ∧̇ ∃̇∈ (var e) (prAtL i0 (sh 1 N0) (sh 1 z))
```

The definable-subset clause has two conjuncts. The first says every member of the coded set `x` lies in `w` and has its one-entry environment inside the value `y`. The second says every member `z` of `w` whose one-entry environment lies in `y` belongs to `x`. Together they say exactly that `x` is cut out of `w` by the value `y`.

```agda
definesB : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Formula S j
definesB x w y N0 =
    ∀̇∈ (var x) ((var i0 ∈̇ var (sh 1 w)) ∧̇ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1))
  ∧̇ ∀̇∈ (var w) (∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⇒̇ (var i0 ∈̇ var (sh 1 x)))
```

The membership clause ranges over members of the proposed value. For each member it merely asks for an element `c` of the proposed domain `C` shaped as a pair with tag one, together with a table entry pairing `c` with a value `y` that cuts the member out of `w`. At this stage `c` is only key-shaped: only the later hypothesis `satAt` permits it to be decoded as the key of an actual formula.

```agda
memAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
memAt v w T C N =
  ∀̇∈ (var v) (∃̇∈ (var (sh 1 C)) (sndEx i0 (sh 2 (N f1))
    (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0)))))))
```

The covering clause runs in the converse direction. Whenever an element `c` of `C` has the shape of a tag-one key, it requires merely a table value `y` at `c` and a member `x` of the proposed output cut out by `y`. Thus it covers every key-shaped element of the proposed domain; identifying these with all actual arity-one formula keys again depends on `satAt`.

```agda
allAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
allAt v w T C N =
  ∀̇∈ (var C) (sndAll i0 (sh 1 (N f1))
    (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))))))
```

The formula `defAt` conjoins the membership and covering clauses. By itself it only relates the proposed output to the proposed code domain and table; combined with correct `Tags` and `satAt` data, the two clauses become the two inclusions proving that the output is `𝒟ₒ W`.

```agda
opaque
  defAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
  defAt v w T C N = memAt v w T C N ∧̇ allAt v w T C N
```

The definition remains opaque in ordinary reasoning so that later arguments use its mathematical interface, the two inclusions, rather than its long syntactic expansion. It is unfolded locally only to verify boundedness and to prove the two reading directions.

```agda
opaque
  unfolding defAt
```

The Δ₀ certificate is produced by the structural checker: the formula uses only variables, membership, conjunction, implication, and bounded quantifiers. It certifies the shape of the formula, not the correctness of the description.

```agda
  Δ₀-defAt : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) → Δ₀ (defAt v w T C N)
  Δ₀-defAt v w T C N = checkΔ₀ (defAt v w T C N) tt
```

Reading the description splits it into its two conjuncts.

```agda
  defAt-out : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m)
            → ⟨ γ ⊨ defAt v w T C N ⟩ → ⟨ γ ⊨ memAt v w T C N ⟩ × ⟨ γ ⊨ allAt v w T C N ⟩
  defAt-out v w T C N γ h = h
```

Filling the description pairs the two conjuncts back together.

```agda
  defAt-in : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m)
           → ⟨ γ ⊨ memAt v w T C N ⟩ → ⟨ γ ⊨ allAt v w T C N ⟩ → ⟨ γ ⊨ defAt v w T C N ⟩
  defAt-in v w T C N γ h1 h2 = h1 , h2
```

The first semantic calculation concerns `singleOf`. Fix the coded set `E` and value `Z`, and assume that the distinguished tag really denotes zero. Under this assumption the two bounded clauses will be shown equivalent to the set equality `E = envOne Z`.

```agda
module _ {j : ℕ} (e N0 z : Fin j) (δ : S ^ j) (q0 : fst (lookup N0 δ) ≡ # 0) where
  private
    E = fst (lookup e δ)
    Z = fst (lookup z δ)
```

Reading the singleton clause yields the equality of the coded set with the standard singleton environment of the value. Forward: every member of the coded set is the ordered pair of the numeral zero and the value, transported through the adequacy of the pairing atom.

```agda
  singleOf-out : ⟨ δ ⊨ singleOf e N0 z ⟩ → E ≡ envOne Z
  singleOf-out (hall , hex) = extensionalV (λ y → ⇔toPath (fwd y) (bwd y))
    where
    fwd : (y : V ℓ) → ⟨ y ∈ E ⟩ → ⟨ y ∈ envOne Z ⟩
    fwd y hy = ∣ lift zero , sym (pr-out i0 (sh 1 N0) (sh 1 z) (down (lookup e δ) y hy ∷ δ) (hall (down (lookup e δ) y hy) hy)
```

For the reverse inclusion, begin with a member of the standard one-entry environment. The existential conjunct supplies some member of the coded set, and its pairing equation, together with the known zero tag, identifies that member with the one already given. Transporting its membership along this equality puts the original member in the coded set.

```agda
                                 ∙ cong (λ a → pr a Z) q0) ∣₁
    bwd : (y : V ℓ) → ⟨ y ∈ envOne Z ⟩ → ⟨ y ∈ E ⟩
    bwd y = PT.rec (snd (y ∈ E))
      (λ { (lift zero , qy) → PT.rec (snd (y ∈ E))
        (λ { (y' , (y'∈ , hy')) →
```

A member of `envOne Z` is the ordered pair `pr (# 0) Z`. Rewriting the tag slot as the numeral zero therefore identifies this member with the ordered pair required by `singleOf`; it does not identify the member with `Z` itself.

```agda
          subst (λ u → ⟨ u ∈ E ⟩)
            (pr-out i0 (sh 1 N0) (sh 1 z) (y' ∷ δ) hy' ∙ cong (λ a → pr a Z) q0 ∙ qy) y'∈ })
        hex
         ; (lift (suc ()) , _) })
```

Conversely, assume the coded set equals the standard one-entry environment. Its unique index is zero, so every member has the required ordered-pair form; impossible successor indices close the remaining cases. The canonical zero entry supplies the bounded existential witness, and transport along the assumed equality supplies its membership.

```agda
  singleOf-in : E ≡ envOne Z → ⟨ δ ⊨ singleOf e N0 z ⟩
  singleOf-in q =
      (λ y hy → pr-in i0 (sh 1 N0) (sh 1 z) (y ∷ δ)
         (PT.rec (setIsSet (fst y) (pr (fst (lookup N0 δ)) Z))
           (λ { (lift zero , qy) → sym qy ∙ cong (λ a → pr a Z) (sym q0) ; (lift (suc ()) , _) })
```

The member is named, its membership is transported, and the existential witness pairs the zero numeral with the value, transported against the tag equation.

```agda
           (subst (λ u → ⟨ fst y ∈ u ⟩) q hy)))
    , ∣ yS , ( subst (λ u → ⟨ pr (# 0) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁
             , pr-in i0 (sh 1 N0) (sh 1 z) (yS ∷ δ) (cong (λ a → pr a Z) (sym q0)) ) ∣₁
    where
    yS : S
```

The named member is the presentation, inside the coded set, of the pair of the zero numeral and the value.

```agda
    yS = down (lookup e δ) (pr (# 0) Z) (subst (λ u → ⟨ pr (# 0) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁)
```

The cut relation between a set `X`, a carrier `Wv`, and a value `Y` is a pair of pointwise directions: every member of `X` lies in `Wv` with its singleton environment in `Y`, and every member of `Wv` whose singleton environment lies in `Y` belongs to `X`. The quantification is over constructible sets, so the relation is stated on the constructible carrier.

```agda
Cuts : (X Wv Y : V ℓ) → Type (ℓ-suc ℓ)
Cuts X Wv Y = ((z : S) → ⟨ fst z ∈ X ⟩ → ⟨ fst z ∈ Wv ⟩ × ⟨ envOne (fst z) ∈ Y ⟩)
            × ((z : S) → ⟨ fst z ∈ Wv ⟩ → ⟨ envOne (fst z) ∈ Y ⟩ → ⟨ fst z ∈ X ⟩)
```

To compare the object-language clause with the mathematical cut relation, fix the slots for `x`, `w`, `y`, and the zero tag. Their interpretations are named `X`, `Wv`, and `Y`; the tag equation is exactly what lets `singleOf` denote the standard one-entry environment.

```agda
module _ {j : ℕ} (x w y N0 : Fin j) (δ : S ^ j) (q0 : fst (lookup N0 δ) ≡ # 0) where
  private
    X = fst (lookup x δ)
    Wv = fst (lookup w δ)
    Y = fst (lookup y δ)
```

Because `Y` is a constructible set, any proof that a one-entry environment belongs to `Y` can be converted into a carrier representative of that environment. This presentation is what permits the bounded existential in `definesB` to range over an actual member of `Y`.

```agda
    YS = lookup y δ
```

Reading the existential of the singleton clause converts it into membership of the standard singleton environment in the value: the witness is a member of the value, and the singleton clause identifies the coded entry with the standard environment of the index.

```agda
    one-out : (z : S) → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⟩ → ⟨ envOne (fst z) ∈ Y ⟩
    one-out z = PT.rec (snd (envOne (fst z) ∈ Y))
      (λ { (e , (e∈ , he)) → subst (λ u → ⟨ u ∈ Y ⟩) (singleOf-out i0 (sh 2 N0) i1 (e ∷ z ∷ δ) q0 he) e∈ })
```

Filling the existential is the converse: the standard singleton environment is presented inside the value, and the singleton clause is filled at the extended environment.

```agda
    one-in : (z : S) → ⟨ envOne (fst z) ∈ Y ⟩ → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⟩
    one-in z h = ∣ down YS (envOne (fst z)) h , (h , singleOf-in i0 (sh 2 N0) i1 (down YS (envOne (fst z)) h ∷ z ∷ δ) q0 refl) ∣₁
```

Reading the definable-subset clause produces the two directions of the cut relation. The first conjunct gives, for each member of `X`, its membership in `Wv` and membership of its one-entry environment in `Y`; the second converts these two facts back into membership in `X`.

```agda
  definesB-out : ⟨ δ ⊨ definesB x w y N0 ⟩ → Cuts X Wv Y
  definesB-out (h1 , h2) = (λ z hz → h1 z hz .fst , one-out z (h1 z hz .snd)) , (λ z hw he → h2 z hw (one-in z he))
```

Conversely, the two pointwise directions in `Cuts X Wv Y` fill the two conjuncts of the object-language definable-subset clause. The private conversions above translate precisely between the bounded singleton witness and membership of the standard one-entry environment in `Y`.

```agda
  definesB-in : Cuts X Wv Y → ⟨ δ ⊨ definesB x w y N0 ⟩
  definesB-in (o , i) = (λ z hz → o z hz .fst , one-in z (o z hz .snd)) , (λ z hw he → i z hw (one-out z he))
```

## Reading the bounded subset clauses

The full reading module names the four sets: the proposed value, the carrier, the table, and the code domain.

```agda
module Read {m : ℕ} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Vv = fst (lookup v γ)
    Wv = fst (lookup w γ)
    Tv = fst (lookup T γ)
```

The code domain's underlying set and the numeral behind the tag one are named, since the membership clause selects codes shaped as the pair of the tag one and a second component.

```agda
    Cv = fst (lookup C γ)
    N1v = fst (lookup (N f1) γ)
```

Reading the membership clause yields, for each member of the proposed value, a truncated record: a code in the domain, split as the pair of the tag one and a component, a table entry pairing that code with a value, and the cut relation between the member and that value. The record exists under truncation; no code or value is chosen.

```agda
  mem-out : ⟨ γ ⊨ memAt v w T C N ⟩ → (x : S) → ⟨ fst x ∈ Vv ⟩
          → ∥ Σ[ c ∈ S ] Σ[ p ∈ S ] Σ[ y ∈ S ]
              (⟨ fst c ∈ Cv ⟩ × ((fst c ≡ pr (# 1) (fst p)) × (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × Cuts (fst x) Wv (fst y)))) ∥₁
  mem-out h x x∈ = PT.rec squash₁
    (λ { (c , (c∈ , hc)) → PT.rec squash₁
```

To read the membership clause, first expose the key-shaped member `c` of the proposed code domain and then the table entry pairing `c` with a value `y`. The pairing specifications turn the encoded second components into the semantic equations displayed in the result, while the tag equation changes the formal tag into the actual numeral one.

```agda
      (λ { (p , s , (ec , he)) → PT.rec squash₁
        (λ { (e , (e∈ , hy)) → PT.map
          (λ { (y , s' , (ee , hd)) →
            c , p , y , ( c∈ , ( ec ∙ cong (λ a → pr a (fst p)) (tg f1)
                        , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈
```

The innermost existential is read through `definesB-out`, which produces the cut relation between the member and the value `y` of the table entry.

```agda
                          , definesB-out i6 (sh 7 w) i0 (sh 7 (N f0)) (y ∷ s' ∷ e ∷ p ∷ s ∷ c ∷ x ∷ γ) (tg f0) hd ) ) ) })
          (sndEx-out i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0))) (e ∷ p ∷ s ∷ c ∷ x ∷ γ) hy) })
        he })
      (sndEx-out i0 (sh 2 (N f1)) (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0))))) (c ∷ x ∷ γ) hc) })
    (h x x∈)
```

Filling the membership clause is the converse construction: it takes the function producing truncated records for each member and assembles the satisfaction of the clause.

```agda
  mem-in : ((x : S) → ⟨ fst x ∈ Vv ⟩
            → ∥ Σ[ c ∈ S ] Σ[ p ∈ S ] Σ[ y ∈ S ]
                (⟨ fst c ∈ Cv ⟩ × ((fst c ≡ pr (# 1) (fst p)) × (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × Cuts (fst x) Wv (fst y)))) ∥₁)
         → ⟨ γ ⊨ memAt v w T C N ⟩
  mem-in g x x∈ = PT.map
```

Conversely, suppose such a truncated semantic record is given for each member of the proposed output. The equation `c = pr (# 1) p` supplies the arity-one shape required by the bounded formula, and membership of `pr(c,y)` in the table supplies a bounded representative for the table entry.

```agda
    (λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) →
      let ec' : fst c ≡ pr N1v (fst p)
          ec' = ec ∙ cong (λ a → pr a (fst p)) (sym (tg f1))
          δ4 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ x ∷ γ
          eS = down (lookup T γ) (pr (fst c) (fst y)) e∈
```

The seven-slot environment is then assembled, and the cut relation is translated back into the definable-subset clause by `definesB-in`.

```agda
          δ7 = y ∷ container eS c y refl .fst ∷ eS ∷ δ4
      in c , ( c∈ , fillSnd i0 (c ∷ x ∷ γ) (lookup (N f1) γ) p ec'
                 (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0)))))
                 ∣ eS , ( e∈ , fillSnd i0 (eS ∷ δ4) c y refl (definesB i6 (sh 7 w) i0 (sh 7 (N f0)))
                              (definesB-in i6 (sh 7 w) i0 (sh 7 (N f0)) δ7 (tg f0) cuts) i3 refl ) ∣₁
```

After the key shape, table entry, and cut condition have been encoded, the outer bounded quantifier applies this truncated package to the original member of the proposed output. Hence the semantic record is sufficient to reconstruct satisfaction of the whole membership clause.

```agda
                 (sh 2 (N f1)) refl ) })
    (g x x∈)
```

Reading the covering clause takes a code `c` that splits as the pair of the tag one and `p`, and yields, merely, a table value `y` at `c` together with a set `x` cut by `y`.

```agda
  all-out : ⟨ γ ⊨ allAt v w T C N ⟩ → (c p : S) → ⟨ fst c ∈ Cv ⟩ → fst c ≡ pr (# 1) (fst p)
          → ∥ Σ[ y ∈ S ] Σ[ x ∈ S ] (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × (⟨ fst x ∈ Vv ⟩ × Cuts (fst x) Wv (fst y))) ∥₁
  all-out h c p c∈ ec = PT.rec squash₁
    (λ { (e , (e∈ , hy)) → PT.rec squash₁
      (λ { (y , s' , (ee , hx)) → PT.map
```

The proof eliminates the table entry and the three-slot existential, and the definable-subset reading produces the cut relation between the member and the table value.

```agda
        (λ { (x , (x∈ , hd)) →
          y , x , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈
                  , ( x∈ , definesB-out i0 (sh 7 w) i1 (sh 7 (N f0)) (x ∷ y ∷ s' ∷ e ∷ δ3) (tg f0) hd ) ) })
        hx })
      (sndEx-out i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))) (e ∷ δ3) hy) })
```

For the converse construction, fix a member `c` of the code domain and inspect any presentation of it as `pr (# 1) p`. The semantic coverage hypothesis then provides, under propositional truncation, a table value and the subset that this value cuts out; these witnesses fill the bounded conclusion for that presentation.

```agda
    (useSnd i0 (c ∷ γ) (lookup (N f1) γ) p ec'
      (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0))))))
      (sh 1 (N f1)) refl (h c c∈))
    where
    ec' : fst c ≡ pr N1v (fst p)
```

The equation using the formal tag is converted to the required arity-one equation by `Tags`. The auxiliary containers merely keep the component and code within bounded quantifiers; they add no mathematical choice or uniqueness to the semantic witness.

```agda
    ec' = ec ∙ cong (λ a → pr a (fst p)) (sym (tg f1))
    δ3 : S ^ (3 + m)
    δ3 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ γ
```

Filling the coverage clause therefore ranges over every member of the proposed code domain that is presented with arity-one key shape. For each such presentation, the semantic hypothesis supplies a table value, a cut-out member of the proposed output, and their memberships, all under propositional truncation. No claim that these are genuine formula keys is made until `satAt` is added later.

```agda
  all-in : ((c p : S) → ⟨ fst c ∈ Cv ⟩ → fst c ≡ pr (# 1) (fst p)
            → ∥ Σ[ y ∈ S ] Σ[ x ∈ S ] (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × (⟨ fst x ∈ Vv ⟩ × Cuts (fst x) Wv (fst y))) ∥₁)
         → ⟨ γ ⊨ allAt v w T C N ⟩
  all-in g c c∈ = sndAll-in' (λ p s s∈ p∈ ec →
    PT.map (λ { (y , x , (e∈ , (x∈ , cuts))) →
```

The innermost bounded existential now receives the sliced set `x` together with its membership in the value set and the `Cuts` evidence just encoded by `definesB`. This completes the converse translation: semantic witnesses for a table entry and its slice yield satisfaction of the membership clause, while all existential data remain propositionally truncated.

```agda
      let eS = down (lookup T γ) (pr (fst c) (fst y)) e∈
          δ6 = y ∷ container eS c y refl .fst ∷ eS ∷ p ∷ s ∷ c ∷ γ
      in eS , ( e∈ , fillSnd i0 (eS ∷ p ∷ s ∷ c ∷ γ) c y refl (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0))))
                       ∣ x , (x∈ , definesB-in i0 (sh 7 w) i1 (sh 7 (N f0)) (x ∷ δ6) (tg f0) cuts) ∣₁ i3 refl ) })
      (g c p c∈ (ec ∙ cong (λ a → pr a (fst p)) (tg f1))))
```

The coverage clause contains the same two nested existential choices: a value of the satisfaction table and the subset that this value cuts out of the working set. Naming their combined outward reading lets the next argument treat this pair of merely existing witnesses as one proposition-valued package.

```agda
    where
    sndAll-in' = sndAll-in i0 (sh 1 (N f1))
      (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))))) (c ∷ γ)
```

## Correctness of the bounded description

We can now compare the bounded description with the actual definability operation. This comparison requires more than satisfaction of `defAt`: the numeral tags must have their intended values, the working-set slot must denote `W`, and `satAt` must certify that the code set and table have their genuine satisfaction semantics.

```agda
module DefRead {m : ℕ} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N) (hs : ⟨ γ ⊨ satAt T w C E N ⟩) where
  open Alphabet W
  open Match W
  private
```

Two earlier readers supply the needed bridge. `SatRead` identifies the advertised code domain and table with the real codes and satisfaction values over `W`; `Read` turns `defAt` into its two semantic slice conditions. `DefOf (fst W)` then interprets each decoded arity-one formula as one subset of `W`.

```agda
    module SR = SatRead T w C E N γ W qw tg hs
    module RD = Read v w T C N γ tg
    module DA = DefOf (fst W)
    Vv = fst (lookup v γ)
    Wv = fst (lookup w γ)
```

Write `Tv` and `Cv` for the underlying sets occupying the table and code slots. The point of `satAt` is precisely that membership in these advertised sets can now be converted to, and reconstructed from, membership in the genuine satisfaction table and code domain.

```agda
    Tv = fst (lookup T γ)
    Cv = fst (lookup C γ)
```

The map `toS` relabels every constant of a formula over the alphabet into the corresponding constant of `S`, producing a formula that the ambient satisfaction judges.

```agda
    toS : Formula Ab 1 → Formula S 1
    toS = mapFo (asConst W)
```

The table-value lemma says that the value recorded at the key of a formula equals the explicit satisfaction set of the relabeled formula. The proof composes the table's outward projection with the uniform satisfaction's value identification.

```agda
    valOf : (ψ : Formula Ab 1) (c y : S) → fst c ≡ fst (keyS W ψ) → ⟨ pr (fst c) (fst y) ∈ Tv ⟩
          → fst y ≡ fst (Sat W (toS ψ))
    valOf ψ c y qc h = SR.T-out c y h .snd ∙ cong fst (val-at W W ψ c (SR.T-out c y h .fst) qc)
```

The central bridge concerns one formula at a time. If `Cuts` says that `x` consists exactly of those members of `W` whose one-variable environments lie in the satisfaction set of `ψ`, then `x` is equal to the particular definable subset `DA.defSet ψ`. Extensionality proves this equality in both membership directions.

```agda
    cut≡ : (ψ : Formula Ab 1) (x : S) → Cuts (fst x) Wv (fst (Sat W (toS ψ))) → DA.defSet ψ ≡ fst x
    cut≡ ψ x (o , i) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z))
      where
      fwd : (z : V ℓ) → ⟨ z ∈ DA.defSet ψ ⟩ → ⟨ z ∈ fst x ⟩
      fwd z = PT.rec (snd (z ∈ fst x))
```

For the first direction, membership in `DA.defSet ψ` supplies, under propositional truncation, a representative of an element of `W`. The satisfaction bridge places that representative's one-variable environment in the satisfaction set of `ψ`, so the inward half of `Cuts` places the represented set in `x`.

```agda
        (λ { ((q , hq) , e) →
          i (down W z (subst (λ u → ⟨ u ∈ fst W ⟩) e (ι∈ q)))
            (subst (λ u → ⟨ z ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ fst W ⟩) e (ι∈ q)))
            (subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) e
              (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁)) })
```

For the other direction, begin with `z ∈ x`. The outward half of `Cuts` gives both `z ∈ W` and membership of its one-variable environment in the satisfaction set. The first fact is converted by `∈-asFiber` into an actual index of the presentation of `W`, together with a path back to `z`.

```agda
      bwd : (z : V ℓ) → ⟨ z ∈ fst x ⟩ → ⟨ z ∈ DA.defSet ψ ⟩
      bwd z hz =
        let zS = down x z hz
            zW = subst (λ u → ⟨ z ∈ u ⟩) qw (o zS hz .fst)
            fib = ∈-asFiber {a = z} {b = fst W} zW
```

Transport the environment membership along that presentation path and apply `defSet-Sat` in reverse. This proves that the representative belongs to `DA.defSet ψ`; transporting back along the same path proves `z ∈ DA.defSet ψ` and completes the extensional equality.

```agda
        in subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
             (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst)))
               (subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) (sym (fib .snd)) (o zS hz .snd)))
```

Conversely, suppose `DA.defSet ψ` is already known to equal `x`. To reconstruct `Cuts`, take a member of `x`, rewrite it as a member of `DA.defSet ψ`, and unpack definable-set membership. This yields both its presentation as an element of `W` and the corresponding one-variable environment's membership in the satisfaction set.

```agda
    cuts-of : (ψ : Formula Ab 1) (x : S) → DA.defSet ψ ≡ fst x → Cuts (fst x) Wv (fst (Sat W (toS ψ)))
    cuts-of ψ x e = o , i
      where
      o : (z : S) → ⟨ fst z ∈ fst x ⟩ → ⟨ fst z ∈ Wv ⟩ × ⟨ envOne (fst z) ∈ fst (Sat W (toS ψ)) ⟩
      o z hz = PT.rec (isProp× (snd (fst z ∈ Wv)) (snd (envOne (fst z) ∈ fst (Sat W (toS ψ)))))
```

Unpacking that membership gives a representative in `W` and, through `defSet-Sat`, the required satisfaction-set membership of its one-variable environment. The equality between the representative and the original member transports both conclusions back to the member of `x`.

```agda
        (λ { ((q , hq) , eq) →
            subst (λ u → ⟨ fst z ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ fst W ⟩) eq (ι∈ q))
          , subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) eq (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁) })
        (subst (λ u → ⟨ fst z ∈ u ⟩) (sym e) hz)
      i : (z : S) → ⟨ fst z ∈ Wv ⟩ → ⟨ envOne (fst z) ∈ fst (Sat W (toS ψ)) ⟩ → ⟨ fst z ∈ fst x ⟩
```

For the inward half of `Cuts`, start with a presented member of `W` whose one-variable environment satisfies `ψ`. The satisfaction bridge turns this into membership in `DA.defSet ψ`; the assumed equality `DA.defSet ψ = fst x` then places the member in `x`.

```agda
      i z hw he =
        let fib = ∈-asFiber {a = fst z} {b = fst W} (subst (λ u → ⟨ fst z ∈ u ⟩) qw hw)
        in subst (λ u → ⟨ fst z ∈ u ⟩) e
             (subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
               (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst)))
```

The final transports only reconcile the chosen presentation of the member with its underlying set. Thus `cut≡` and `cuts-of` together identify the `Cuts` predicate for `ψ` with equality to the single definable subset `DA.defSet ψ`; neither direction asserts uniqueness of a defining formula.

```agda
                 (subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) (sym (fib .snd)) he)))
```

Soundness can now be stated accurately. Under the standing identification of the working-set slot with `W`, the correct numeral tags, and the `satAt` certification of the code set and satisfaction table, satisfaction of `defAt` forces the value slot to be exactly `𝒟ₒ (fst W)`. Here `𝒟ₒ` collects the subsets of `W` definable by first-order formulas with parameters from `W`; it is not the full internal power set.

```agda
  def-sound : ⟨ γ ⊨ defAt v w T C N ⟩ → Vv ≡ 𝒟ₒ (fst W)
  def-sound hd = extensionalV (λ x → ⇔toPath (fwd x) (bwd x))
    where
    hm = defAt-out v w T C N γ hd .fst
    ha = defAt-out v w T C N γ hd .snd
```

For the forward inclusion, the membership clause supplies, under propositional truncation, a key-shaped code, a satisfaction-table entry, and the condition describing the subset cut out by that entry. After `satAt` identifies the proposed code domain with the genuine one, `decodeAll` yields merely an arity-one formula whose code has the required second component. The table-value lemma then identifies the entry's value with that formula's satisfaction set.

```agda
    fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ 𝒟ₒ (fst W) ⟩
    fwd x hx = PT.rec (snd (x ∈ 𝒟ₒ (fst W)))
      (λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) → PT.rec (snd (x ∈ 𝒟ₒ (fst W)))
        (λ { (ψ , qp) →
          𝒟ₒ-intro (fst W) x ∣ ψ , cut≡ ψ xS
```

The `Cuts` fact is transported along the table-value identification to the satisfaction set of the decoded formula, and the definable-power-set introduction places the sliced set inside `𝒟ₒ`. The truncated formula decoding is consumed into the proposition-valued introduction.

```agda
            (subst (λ u → Cuts x Wv u) (valOf ψ c y (ec ∙ cong (pr (# 1)) qp) e∈) cuts) ∣₁ })
        (decodeAll c (SR.C-out c c∈) 1 (fst p) ec) })
      (RD.mem-out hm xS hx)
      where
      xS : S
```

The value slot is presented as a carrier element for reading the outward direction of the membership clause.

```agda
      xS = down (lookup v γ) x hx
```

For the reverse inclusion, membership in `𝒟ₒ (fst W)` yields only a propositionally truncated formula `ψ` together with an equality `DA.defSet ψ = x`. Inside elimination into the membership proposition, the coverage half of `defAt` provides a table value and a set `x'` in the value slot for the key built from this temporary witness `ψ`.

```agda
    bwd : (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (fst W) ⟩ → ⟨ x ∈ Vv ⟩
    bwd x hx = PT.rec (snd (x ∈ Vv))
      (λ { (ψ , e) → PT.rec (snd (x ∈ Vv))
        (λ { (y , x' , (e∈ , (x'∈ , cuts))) →
          subst (λ u → ⟨ u ∈ Vv ⟩)
```

The slice equality is transported along the table-value identification to recover the underlying set of the sliced set, and the transport places it inside the value slot.

```agda
            (sym (cut≡ ψ x' (subst (λ u → Cuts (fst x') Wv u) (valOf ψ (keyS W ψ) y refl e∈) cuts)) ∙ e)
            x'∈ })
        (RD.all-out ha (keyS W ψ) (sndS (keyS W ψ) (# 1) (cd ψ) refl) (SR.C-in (keyS W ψ) (key∈AllCodes W ψ)) refl) })
      (𝒟ₒ-inv (fst W) x hx)
```

Completeness runs the same equivalence backwards. Still assuming the working-set identification, correct tags, and `satAt`, an equality between the value slot and `𝒟ₒ (fst W)` suffices to satisfy `defAt`. The two conjuncts respectively show that every listed set has a defining formula and that every arity-one formula contributes its definable subset.

```agda
  def-complete : Vv ≡ 𝒟ₒ (fst W) → ⟨ γ ⊨ defAt v w T C N ⟩
  def-complete qv = defAt-in v w T C N γ mem all
    where
```

Each formula's table entry is selected from the already-defined recursion table, which guarantees both the membership in the table and the identification with the explicit satisfaction set.

```agda
    entry : (ψ : Formula Ab 1) → Σ[ y ∈ S ] (⟨ pr (fst (keyS W ψ)) (fst y) ∈ Tv ⟩ × (fst y ≡ fst (Sat W (toS ψ))))
    entry ψ = Table.val W W (keyS W ψ) (key∈AllCodes W ψ)
            , ( SR.T-in (keyS W ψ) (key∈AllCodes W ψ)
              , cong fst (val-at W W ψ (keyS W ψ) (key∈AllCodes W ψ) refl) )
```

For the membership conjunct, a member of the value slot is transported into `𝒟ₒ (fst W)` and then unpacked by `𝒟ₒ-inv`. The defining formula exists only under propositional truncation. Within that truncation, its formula key, the corresponding table entry, and the required `Cuts` evidence are assembled; no defining formula is selected globally or retained as canonical data.

```agda
    mem : ⟨ γ ⊨ memAt v w T C N ⟩
    mem = RD.mem-in (λ x x∈ → PT.map
      (λ { (ψ , e) →
        keyS W ψ , sndS (keyS W ψ) (# 1) (cd ψ) refl , entry ψ .fst
        , ( SR.C-in (keyS W ψ) (key∈AllCodes W ψ)
```

The chosen table value is the value already determined by the recursive satisfaction table for this formula key. Transporting `cuts-of` along its equality with the explicit satisfaction set supplies the slice evidence. This use of a temporary formula witness stays inside `PT.map`, so the resulting membership witness remains propositionally truncated.

```agda
          , ( refl
            , ( entry ψ .snd .fst
              , subst (λ u → Cuts (fst x) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ x e) ) ) ) })
      (𝒟ₒ-inv (fst W) (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qv x∈)))
```

The coverage conjunct is proved for every arity-one key in the code domain, with the pair decomposition named explicitly.

```agda
    all : ⟨ γ ⊨ allAt v w T C N ⟩
    all = RD.all-in (λ c p c∈ ec → PT.map
      (λ { (ψ , qp) →
        let qc : fst c ≡ fst (keyS W ψ)
            qc = ec ∙ cong (pr (# 1)) qp
```

For a given arity-one key, decoding supplies merely a formula `ψ` whose code is the key's second component. Its definable subset `DA.defSet ψ` belongs to `𝒟ₒ (fst W)` by introduction, and the assumed equality transports this membership into the value slot. Decoding does not choose a unique or canonical formula.

```agda
            xS : S
            xS = down (lookup v γ) (DA.defSet ψ)
                   (subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (fst W) (DA.defSet ψ) ∣ ψ , refl ∣₁))
        in entry ψ .fst , xS
         , ( subst (λ u → ⟨ pr u (fst (entry ψ .fst)) ∈ Tv ⟩) (sym qc) (entry ψ .snd .fst)
```

The satisfaction table supplies the value attached to the decoded formula key, while `cuts-of` proves that this value cuts out exactly `DA.defSet ψ`. Together with the membership just obtained, these data satisfy the coverage clause. Because `decodeAll` is propositionally truncated and is eliminated only into that proposition-valued clause, the construction records existence without retaining a decoded formula.

```agda
           , ( subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (fst W) (DA.defSet ψ) ∣ ψ , refl ∣₁)
             , subst (λ u → Cuts (DA.defSet ψ) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ xS refl) ) ) })
      (decodeAll c (SR.C-out c c∈) 1 (fst p) ec))
```

The exported soundness direction exposes the exact interface used later: once the working-set slot denotes `W`, `Tags` fixes the numeral slots, and `satAt` validates the code and satisfaction data, `defAt` implies equality with `𝒟ₒ (fst W)`. Thus the bounded formula receives its intended meaning only in this calibrated background.

```agda
def-sound : ∀ {m} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
          → fst (lookup w γ) ≡ fst W → Tags γ N → ⟨ γ ⊨ satAt T w C E N ⟩
          → ⟨ γ ⊨ defAt v w T C N ⟩ → fst (lookup v γ) ≡ 𝒟ₒ (fst W)
def-sound v w T C E N γ W qw tg hs = DefRead.def-sound v w T C E N γ W qw tg hs
```

The exported completeness direction has the same hypotheses and reverses the implication: equality with `𝒟ₒ (fst W)` reconstructs satisfaction of `defAt`. Together the two theorems characterize the definable-subset collection without choosing a representative formula for each member and without identifying it with the full internal power set.

```agda
def-complete : ∀ {m} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
             → fst (lookup w γ) ≡ fst W → Tags γ N → ⟨ γ ⊨ satAt T w C E N ⟩
             → fst (lookup v γ) ≡ 𝒟ₒ (fst W) → ⟨ γ ⊨ defAt v w T C N ⟩
def-complete v w T C E N γ W qw tg hs = DefRead.def-complete v w T C E N γ W qw tg hs
```