BedrockRead this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapThe 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.
{-# 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Δ₀-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.
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.
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.
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.
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.
∙ 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.
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.
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.
(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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
(λ { (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.
, 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.
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.
(λ { (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.
δ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.
(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.
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.
(λ { (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.
(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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
(λ { ((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.
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.
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.
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.
(λ { ((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.
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.
(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.
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.
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.
(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.
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 ψ.
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.
(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.
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.
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.
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.
, ( 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.
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.
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.
, ( 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.
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.
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