--- title: "Definable subsets of a set" module: L.Definability lang: en site: "Bedrock" description: "Definable subsets of a set" stage: "Constructible stages and the axioms" reading_order: 24 canonical: https://bedrock.institute/en/L.Definability.html html: L.Definability.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Definability.lagda.md prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Absoluteness, V.Hierarchy, V.Smallness] routes: [constructible-axioms] translations: [https://bedrock.institute/zh/L.Definability.md, https://bedrock.institute/ja/L.Definability.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Definable subsets of a set For a set `A`, the operator `Def A` collects exactly the subsets of `A` defined by a first-order formula over the restricted structure on `A`, with finitely many parameters from `A`. Its membership theorem exposes the formula, environment, and satisfaction relation used by later constructibility arguments. Two design points carry the chapter. The formulas take `A`'s small member type `⟪ A ⟫` as their constant domain, so "parameters from `A`" is enforced by the type. And satisfaction is the **inner** semantics, on the restricted structure `𝒮ᵥ ↾ (∈ A)`: quantifiers range over members of `A` only, which is what "definable *in* `(A, ∈)`" means in the textbook, and which lets the essential smallness of the previous chapters apply here: every formula evaluates small, so `Def A` is a set, with no resizing needed at all. The question of this chapter: for a set `A`, which subsets of `A` can be singled out by a first-order formula interpreted inside `(A, ∈)`? The answer will be collected into a single operator `Def A`, itself a set of the ambient hierarchy. Everything takes place at one fixed universe level ℓ, so that `Def A` is small enough to exist as a set at the same level as `A`. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module L.Definability {ℓ : Level} where open import FOL.ZFStructure using ( ZFStructure; Transitive ) ``` The formulas come from an inductive object language: `Formula K n` has constants indexed by a type `K` and `n` slots indexing free variables, with atoms built from a structure's membership and equality relations. Choosing `K = ⟪ A ⟫`, the small member type of `A`, makes "parameters from `A`" true by construction: every constant names a member of `A`. The bounded fragment `Δ₀` will matter later, when the inner and outer readings of satisfaction are compared; constant mapping and relabelling are the operations that move a formula between constant domains and transport satisfaction along such a move. ```agda open import FOL.Syntax using ( Formula; var; con; _∈̇_; ⊤̇ ) open import FOL.LevyHierarchy using ( Δ₀ ) open import FOL.Manipulation.ConstantMapping using ( mapFo ) open import FOL.Manipulation.Relabelling using ( mapΔ₀; ⊨-map ) import FOL.Absoluteness ``` "Definable *in* `(A, ∈)`" means quantifiers may only range over members of `A`. So satisfaction must be taken in the structure restricted to the class `x ↦ x ∈ˢ A`, not in the ambient hierarchy. The chapter works over the ambient structure `𝒮ᵥ` carried by the level-ℓ hierarchy, with carrier `S` and membership `∈ₛ`; the restriction to `A` and the smallness of the restricted world come from the smallness chapter: given a class, a small type with an equivalence to the restricted carrier, and a constant interpretation, it rebuilds the restricted structure and proves every formula evaluates to a small proposition there. The restriction class here is simply membership in `A`. ```agda open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Smallness {ℓ} using ( module InnerSmall ) open import Cubical.Foundations.Equiv using ( _≃_; equivFun; invEq; invEquiv; compEquiv; propBiimpl→Equiv ) open import Cubical.Functions.Embedding using ( isEmbedding→Inj ) ``` Essential smallness is what lets satisfaction become an index for a set. Since each formula evaluates to a *small* proposition inside `(A, ∈)`, the members of `A` satisfying a formula can be indexed by a small type, and the hierarchy constructor `sett` turns a small index type and an indexing map into a set. Both the subset defined by one formula and `Def` itself will be built this way. Membership in a `sett` is then only a truncated existence statement, and propositions-valued targets force truncation to be eliminated into propositions rather than yielding chosen witnesses. The shape of the constructions produces the chapter's path-based specifications. ```agda open import Cubical.Data.Sigma using ( Σ-cong-equiv-snd ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( sett ) ``` Finally, the vocabulary of truth values. The connectives and quantifiers act directly on propositions in `hProp (ℓ-suc ℓ)`, so satisfaction takes values in `hProp (ℓ-suc ℓ)`, with `⟨ p ⟩` projecting the underlying proposition of an `hProp`. Equality of such propositions is a path, so specifications about membership will be stated as paths of propositions and proved by chains of them. With this setup, the next section fixes one set `A` and defines its definable subsets. ```agda open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber; presentation ; isEmb⟪_⟫↪; _⊆_; extensionality ) open ZFStructure 𝒮ᵥ ``` ## The operator Everything below is relative to one set `A`, so the section works in a module `DefOf A`. The restriction class is membership in `A`, and the essential smallness witness `e` is the library's `presentation`: the small member type `⟪ A ⟫` *is* the restricted carrier, up to equivalence (with the small membership converted pointwise to the large one). The constant interpretation `ι` sends a constant, an index in `⟪ A ⟫`, to the corresponding member of the restricted carrier; its first component is the member itself, definitionally. The class `M` assigns to each set `x` the proposition `x ∈ˢ A`, so the restricted carrier `Σ[ x ∈ S ] (x ∈ᶜ M)` is, elementwise, a member of `A` together with the proof that it is one. The equivalence `e` exhibits this carrier as essentially small. Its first factor is the inverse of `presentation A`, which identifies a member of `A` merely lying in the fiber of the indexing map with an index in `⟪ A ⟫`; its second factor converts, for each `v`, the small membership statement `v ∈ₛ A` into the large one `v ∈ˢ A` and back. These are propositions, so the pointwise conversion is legitimate. ```agda module DefOf (A : S) where M : S → hProp (ℓ-suc ℓ) M x = x ∈ˢ A e : ⟪ A ⟫ ≃ (Σ[ x ∈ S ] (x ∈ᶜ M)) e = compEquiv (invEquiv (presentation A)) ``` The constant interpretation `ι` is then just the equivalence `e` read as a function. Because the domain type of formulas will be `⟪ A ⟫` itself, a constant of the language is an index for a member of `A`, and `ι` decodes it into the restricted carrier. The first projection of `ι m` is definitionally the underlying set `⟪ A ⟫↪ m`, a fact the membership proofs will use without ceremony. ```agda (Σ-cong-equiv-snd (λ v → propBiimpl→Equiv (snd (v ∈ₛ A)) (snd (v ∈ˢ A)) (∈∈ₛ {a = v} {b = A} .snd) (∈∈ₛ {a = v} {b = A} .fst))) ι : ⟪ A ⟫ → Σ[ x ∈ S ] (x ∈ᶜ M) ι = equivFun e ``` Opening `InnerSmall` at this data rebuilds the world: the structure `𝒮M` restricted to membership in `A`, its satisfaction relation `⊨ᵐ`, and the theorem `⊨ᵐ-small` that every formula over `⟪ A ⟫` evaluates to a small proposition. Making the opening public means later chapters read inner satisfaction under exactly these names. From here on, "satisfies" always means this inner relation, with quantifiers confined to members of `A`. ```agda open InnerSmall M ⟪ A ⟫ e {K = ⟪ A ⟫} ι public ``` With the inner satisfaction `⊨ᵐ` and its smallness in scope, the operator can be defined directly. `smallSat φ m` is the truth value of `φ` at the member `m`, living one universe down; `defSet φ` is the subset `φ` defines out of `A`, a `sett` over the members `φ` selects; and `Def A` is the collection of all of them, indexed by the formulas themselves. A formula is a piece of inductive data in `Type ℓ`, hence a legitimate small index: this is precisely **syntax as index set**. The compression `smallSat` packages the two-step evaluation: `⊨ᵐ-small φ (ι m ∷ [])` is a pair whose first component is a small proposition equivalent to the inner satisfaction statement, and whose second component is that equivalence. The environment `ι m ∷ []` has a single entry because `φ` has one free-variable slot, filled by the member `m` through `ι`. Independently of this, any constants occurring in `φ` are interpreted through the constant interpretation `ι`, so they may name arbitrary members of `A`: parameters enter through constants, and the variable entry only fixes where the single free slot is evaluated. The underlying proposition `⟨ smallSat φ m ⟩` says that `φ` holds at `m` inside `(A, ∈)`, in the small form suitable for indexing a `sett`. ```agda smallSat : Formula ⟪ A ⟫ 1 → ⟪ A ⟫ → hProp ℓ smallSat φ m = ⊨ᵐ-small φ (ι m ∷ []) .fst defSet : Formula ⟪ A ⟫ 1 → S defSet φ = sett (Σ[ m ∈ ⟪ A ⟫ ] ⟨ smallSat φ m ⟩) (λ p → ⟪ A ⟫↪ (p .fst)) Def : S ``` The definable subset `defSet φ` is presented by the index type `Σ[ m ∈ ⟪ A ⟫ ] ⟨ smallSat φ m ⟩`: an index is a member `m` together with a proof that `φ` holds at it, and the indexing map sends such a pair to the set `⟪ A ⟫↪ m`. Note the truncation discipline: the proof component is a proof, not chosen data, and membership in `defSet φ` only asks for a proof to *merely* exist. Finally `Def` applies the same construction one level up, with the formulas themselves as the index family: each formula merely hits some `defSet φ`. Because formulas live in `Type ℓ`, the index type is small and the result is again a set of the hierarchy. ```agda Def = sett (Formula ⟪ A ⟫ 1) defSet ``` ## Membership, specified Both `Def` and each `defSet φ` are `sett`s, so their membership is *definitionally* "merely hit by the index family". For `Def` this needs no proof at all: a member of `Def` is merely a `defSet φ`. For the definable subsets there are two specifications: their members stay inside `A`, and a member `⟪ A ⟫↪ m` belongs to `defSet φ` **exactly when the inner world satisfies `φ` at `m`**; this is literally what "definable subset" means (the compression `smallSat` was only an encoding, and the equivalence preserves it). The first specification says each `defSet φ` is contained in `A`. A member of `defSet φ` merely comes from an index `(m , _)` with some proof, together with a path `q` identifying the indexed set with `y`. Since membership in `A` is a proposition, truncation can be eliminated into it: the proof transports the known fact `⟪ A ⟫↪ m ∈ˢ A` along `q` to obtain `y ∈ˢ A`. The known fact itself is exactly the small membership `⟪ A ⟫↪ m ∈ₛ A`, converted through `∈∈ₛ`. ```agda defSet⊆A : (φ : Formula ⟪ A ⟫ 1) (y : S) → ⟨ y ∈ˢ defSet φ ⟩ → ⟨ y ∈ˢ A ⟩ defSet⊆A φ y = PT.rec (snd (y ∈ˢ A)) λ { ((m , _) , q) → subst (λ v → ⟨ v ∈ˢ A ⟩) q (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)) } private ``` The second specification is the heart of the chapter, and it is stated as a path of propositions, not a pair of implications: membership of `⟪ A ⟫↪ m` in `defSet φ` equals the inner satisfaction statement `(ι m ∷ []) ⊨ᵐ φ`. The auxiliary `decode` re-expands `smallSat` into the full pair, so the equivalence in its second component is available to both directions. Note also the private injectivity lemma: `⟪ A ⟫↪` is an embedding of `⟪ A ⟫` into the carrier, so paths between its values come from paths between indices; this will recover `m' ≡ m` from a path of sets. ```agda ⟪⟫↪-inj : {m' m : ⟪ A ⟫} → ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m → m' ≡ m ⟪⟫↪-inj {m'} {m} = isEmbedding→Inj isEmb⟪ A ⟫↪ m' m defSet-mem : (φ : Formula ⟪ A ⟫ 1) (m : ⟪ A ⟫) → (⟪ A ⟫↪ m ∈ˢ defSet φ) ≡ ((ι m ∷ []) ⊨ᵐ φ) defSet-mem φ m = ⇔toPath fwd bwd ``` The forward direction unpacks what membership merely gives: an index `(m' , h)`, where `h` proves `smallSat φ m'`, and a path `q` with `⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m`. Injectivity turns `q` into `m' ≡ m`, and transporting `h` along it yields a proof of `smallSat φ m`. The second component of `decode`, the equivalence between the small proposition and inner satisfaction, then converts this proof into the target statement. Every ingredient is used: truncation gives the index, embedding gives the path between indices, transport moves the proof, equivalence decodes it. ```agda where decode = ⊨ᵐ-small φ (ι m ∷ []) fwd : ⟨ ⟪ A ⟫↪ m ∈ˢ defSet φ ⟩ → ⟨ (ι m ∷ []) ⊨ᵐ φ ⟩ fwd = PT.rec (snd ((ι m ∷ []) ⊨ᵐ φ)) λ { ((m' , h) , q) → invEq (decode .snd) (subst (λ k → ⟨ smallSat φ k ⟩) (⟪⟫↪-inj q) h) } ``` The reverse direction is short because the equivalence also runs that way: given `hφ : (ι m ∷ []) ⊨ᵐ φ`, apply the equivalence to get a proof of `smallSat φ m`, and take the index `(m , proof)` with the trivial path `refl`. The result is truncated with `∣_∣₁`, which is all that membership demands. Together the two directions give the promised exact correspondence between inner satisfaction and membership in the definable subset. ```agda bwd : ⟨ (ι m ∷ []) ⊨ᵐ φ ⟩ → ⟨ ⟪ A ⟫↪ m ∈ˢ defSet φ ⟩ bwd hφ = ∣ (m , equivFun (decode .snd) hφ) , refl ∣₁ ``` ## Def refines, never shrinks Two facts locate `Def A` before any transitivity assumption is made. The always-true formula defines all of `A`, so `A` itself is an element of `Def A`; and every element of `Def A` is a subset of `A`. This does not yet assert `A ⊆ Def A`. That stronger inclusion is proved in the next section from transitivity, by defining each member of `A` separately. The private helper `A-mem` converts a large membership proof into its fiber form: a member `y` of `A` merely comes from some index `m` with `⟪ A ⟫↪ m ≡ y`, and since `∈-asFiber` returns the fiber as data (the truncation lives inside the membership proof it consumes), the pair can be taken apart with `let`. Equality of the two sets is then proved by `extensionality`, so it suffices to establish inclusion in both directions. ```agda private A-mem : (y : S) → ⟨ y ∈ˢ A ⟩ → Σ[ m ∈ ⟪ A ⟫ ] (⟪ A ⟫↪ m ≡ y) A-mem y y∈ = ∈-asFiber {a = y} {b = A} y∈ defSet⊤≡A : defSet ⊤̇ ≡ A defSet⊤≡A = extensionality (defSet ⊤̇) A (sub₁ , sub₂) ``` The easy direction reuses the containment just proved. A set-theoretic member `y` of `defSet ⊤̇` gives, via the definition of `sett` membership, a truncated index; `defSet⊆A` then places `y` inside `A`, and the conversion `∈∈ₛ` repackages the statement in the form the inclusion `⊆` expects. Nothing here uses what `⊤̇` means: this half holds for every `defSet φ`. ```agda where sub₁ : ⟨ defSet ⊤̇ ⊆ A ⟩ sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = A} .fst (defSet⊆A ⊤̇ y (∈∈ₛ {a = y} {b = defSet ⊤̇} .snd y∈ₛ)) sub₂ : ⟨ A ⊆ defSet ⊤̇ ⟩ ``` The converse uses what "true" means: since `⊤̇` holds at every member, `defSet-mem ⊤̇ m` identifies `⟪ A ⟫↪ m ∈ˢ defSet ⊤̇` with a proposition that any inhabitant proves, here supplied as the identity function. So each member `y` of `A`, being merely `⟪ A ⟫↪ m`, is transported along the fiber path into `defSet ⊤̇`. Note the use of `sym (defSet-mem ⊤̇ m)` inside `subst ⟨_⟩`: the theorem is a path of propositions, so it transports proofs in whichever direction the goal needs. ```agda sub₂ y y∈ₛ = let (m , q) = A-mem y (∈∈ₛ {a = y} {b = A} .snd y∈ₛ) in subst (λ v → ⟨ v ∈ₛ defSet ⊤̇ ⟩) q (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = defSet ⊤̇} .fst (subst ⟨_⟩ (sym (defSet-mem ⊤̇ m)) (λ z → z))) ``` The dual containment `Def∋⊆A` says every element of `Def A` is a subset of `A`. Its hypothesis is itself a truncation: `x` merely is some `defSet φ`. The target is a proposition, being built from propositions by products, so `PT.rec` may eliminate the truncation; the case then transports `y ∈ˢ x` backwards along the path identifying `x` with `defSet φ` and applies the containment of `defSet φ`. Combined with `defSet⊤≡A`, which yields `A ∈ Def`, the picture is complete: `Def` contains `A` as an element and contains only subsets of `A`. ```agda Def∋⊆A : (x : S) → ⟨ x ∈ˢ Def ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ A ⟩ Def∋⊆A x = PT.rec (isPropΠ λ y → isPropΠ λ _ → snd (y ∈ˢ A)) (λ { (φ , q) y y∈x → defSet⊆A φ y (subst (λ s → ⟨ y ∈ˢ s ⟩) (sym q) y∈x) }) ``` ## Under transitivity, A ⊆ Def A When `A` is transitive, each **member** `a` of `A` is itself definable, by the same two-symbol construction that built intersection in the model chapter: the atomic formula "the variable is a member of `a`". Separation's implicit "∈ A" clause is what transitivity discharges: members of `a` are already members of `A`, so the atom carves out exactly `a`. Hence `A ⊆ Def A`: no element is omitted. Combined with the previous section, iterating `Def` can only accumulate, which is exactly what the constructible tower requires. The submodule takes transitivity of `A` as an explicit hypothesis. The atomic formula `atom mₐ` is `var zero ∈̇ con mₐ`: one free-variable slot, and a single constant naming the element `mₐ`. This is where the design choice of using `⟪ A ⟫` as the constant domain pays off again: every member of `A` is available as a constant, with `ι` decoding it into the restricted carrier. ```agda module Refine (Atrans : Transitive 𝒮ᵥ M) where atom : ⟪ A ⟫ → Formula ⟪ A ⟫ 1 atom mₐ = var zero ∈̇ con mₐ atom-mem : (mₐ m : ⟪ A ⟫) → (⟪ A ⟫↪ m ∈ˢ defSet (atom mₐ)) ≡ (⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ) ``` The specialization of the membership theorem to this atom is immediate, because the environment is fixed to the single parameter `m` and the inner truth of `var zero ∈̇ con mₐ` is, by the semantics of atoms, precisely membership `⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ` inside the restricted world. Since restricted membership is defined by the ambient membership of the underlying sets, the atom really selects the elements of `⟪ A ⟫↪ mₐ`; the remaining work is only to show the presented set `defSet (atom mₐ)` equals that element. ```agda atom-mem mₐ m = defSet-mem (atom mₐ) m defSet-atom≡ : (mₐ : ⟪ A ⟫) → defSet (atom mₐ) ≡ ⟪ A ⟫↪ mₐ defSet-atom≡ mₐ = extensionality (defSet (atom mₐ)) (⟪ A ⟫↪ mₐ) (sub₁ , sub₂) where sub₁ : ⟨ defSet (atom mₐ) ⊆ ⟪ A ⟫↪ mₐ ⟩ ``` The forward inclusion eliminates the truncated index of `y ∈ˢ defSet (atom mₐ)`: an index is a pair `(m , h)` of a member and a proof that the atom holds at it, plus the path `q` from the indexing map. By `atom-mem`, the proof `h` becomes membership `⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ` in the ambient sense, and `∈∈ₛ` converts it to a set-theoretic member of `⟪ A ⟫↪ mₐ`; transporting along `q` finishes. This mirrors the proof of `defSet⊆A` with the atom's meaning in place of the trivial containment in `A`. ```agda sub₁ y y∈ₛ = PT.rec (snd (y ∈ₛ ⟪ A ⟫↪ mₐ)) (λ { ((m , h) , q) → subst (λ v → ⟨ v ∈ₛ ⟪ A ⟫↪ mₐ ⟩) q (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = ⟪ A ⟫↪ mₐ} .fst (subst ⟨_⟩ (atom-mem mₐ m) ∣ (m , h) , refl ∣₁)) }) ``` The reverse inclusion is where transitivity enters. Given `y ∈ˢ ⟪ A ⟫↪ mₐ`, unfold it to the ambient membership `y∈a`; transitivity of `A` states that a member of a member of `A` is again a member of `A`, applied here with the witness `mₐ-as` that `⟪ A ⟫↪ mₐ ∈ˢ A`. So `y ∈ˢ A`, and the fiber decomposition hands over an index `m` with `⟪ A ⟫↪ m ≡ y`, ready to be presented as an inhabitant of `defSet (atom mₐ)`. ```agda (∈∈ₛ {a = y} {b = defSet (atom mₐ)} .snd y∈ₛ) sub₂ : ⟨ ⟪ A ⟫↪ mₐ ⊆ defSet (atom mₐ) ⟩ sub₂ y y∈ₛ = let y∈a = ∈∈ₛ {a = y} {b = ⟪ A ⟫↪ mₐ} .snd y∈ₛ y∈A = Atrans {x = ⟪ A ⟫↪ mₐ} {y = y} y∈a mₐ-as ``` To conclude, the index `m` just obtained must actually satisfy the atom at itself. Transporting `y∈a` backwards along the fiber path puts membership inside `⟪ A ⟫↪ mₐ`, and `atom-mem`, read in the reverse direction via `sym`, converts that into a proof of `smallSat (atom mₐ) m`. The final transport along `q` lands in `defSet (atom mₐ)`. Both inclusions together give the equality of sets. Note how every transport here moves a *proof* along a path of sets or of propositions, never building new data. ```agda (m , q) = ∈-asFiber {a = y} {b = A} y∈A in subst (λ v → ⟨ v ∈ₛ defSet (atom mₐ) ⟩) q (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = defSet (atom mₐ)} .fst (subst ⟨_⟩ (sym (atom-mem mₐ m)) (subst (λ v → ⟨ v ∈ˢ ⟪ A ⟫↪ mₐ ⟩) (sym q) y∈a))) ``` With the equality in hand, membership in `Def` is one truncation away. Given `a ∈ˢ A`, the fiber decomposition of that membership provides an index `mₐ` with `⟪ A ⟫↪ mₐ ≡ a`; since the fiber is data here, the pair can be opened with `let` and `mₐ` named. ```agda where mₐ-as : ⟨ ⟪ A ⟫↪ mₐ ∈ˢ A ⟩ mₐ-as = ∈∈ₛ {a = ⟪ A ⟫↪ mₐ} {b = A} .snd (∈ₛ⟪ A ⟫↪ mₐ) A⊆Def : (a : S) → ⟨ a ∈ˢ A ⟩ → ⟨ a ∈ˢ Def ⟩ A⊆Def a a∈ = ``` The element `defSet (atom mₐ)` of `Def` equals `⟪ A ⟫↪ mₐ`, and composing that equality with the fiber path `q` gives `defSet (atom mₐ) ≡ a`. Wrapping the pair of a formula and this equality in the truncation `∣_∣₁` produces exactly what membership in `Def` demands: a formula whose defined subset is `a`, merely. Thus every element of `A` survives into `Def`, and with the previous section the operator only refines. ```agda let (mₐ , q) = ∈-asFiber {a = a} {b = A} a∈ in ∣ atom mₐ , defSet-atom≡ mₐ ∙ q ∣₁ ``` ### Definability read from outside One consequence deserves its own name, because the constructible-stage proofs lean on it repeatedly. Membership in `defSet φ` is a statement of the *inner* world `(A, ∈)`, and the arguments to come are conducted in the ambient hierarchy. For a Δ₀ formula the two readings agree, which is the absoluteness theorem; what remains is bookkeeping, since absoluteness is stated over the members of the class while `defSet` is stated over the small index type. Relabelling closes that gap, and the whole proof is a three-step path: the specification of `defSet`, then the relabelling of the formula, then absoluteness. `A` must be transitive for this, which is why the lemma lives in this submodule; every stage of the tower is. The absoluteness module is instantiated at the ambient structure, the class `M`, and the transitivity hypothesis, yielding the restricted structure `Abs.𝒮M`, the outer satisfaction `Abs.⊨ᵛ`, and the Δ₀ absoluteness `Abs.abs₀`. The statement takes a witness `d` certifying that `φ` is Δ₀, and asserts a path of propositions: membership of `⟪ A ⟫↪ m` in `defSet φ` equals the satisfaction of `mapFo ι φ` in the *ambient* structure at the environment `⟪ A ⟫↪ m ∷ []`. The formula on the right has its constants mapped through `ι`, so it is a formula over the ambient carrier naming members of `A`. ```agda module Abs = FOL.Absoluteness.Single 𝒮ᵥ M Atrans abs-defSet : (φ : Formula ⟪ A ⟫ 1) → Δ₀ φ → (m : ⟪ A ⟫) → (⟪ A ⟫↪ m ∈ˢ defSet φ) ≡ ((⟪ A ⟫↪ m ∷ []) Abs.⊨ᵛ (mapFo ι φ)) abs-defSet φ d m = ``` The proof concatenates three paths. First, `defSet-mem` reads membership in the definable subset as inner satisfaction of `φ` at `ι m`. Second, `⊨-map` (in the symmetric direction, hence `sym`) says that relabelling the constants through `ι` does not change the truth value, because `ι` is precisely the constant interpretation of the inner world; what remains is inner satisfaction of the relabelled formula `mapFo ι φ`. Third, `abs₀` transports inner satisfaction of that Δ₀ formula to outer satisfaction in the ambient structure, this being the only step that uses transitivity. The result lets later chapters treat membership in a definable subset as an ambient, not merely inner, statement. ```agda defSet-mem φ m ∙ sym (⊨-map Abs.𝒮M ι id φ (ι m ∷ [])) ∙ Abs.abs₀ (mapΔ₀ ι d) (ι m ∷ []) ``` ## Recap `Def A` is the set of subsets of `A` definable in the inner world `(A, ∈)` with parameters from `A`: syntax as index set, inner satisfaction for meaning, and essential smallness supplying the required universe level. The specification `defSet-mem` states directly what "definable" means, and the operator only refines: `A ⊆ Def A` under transitivity (`A⊆Def`), and members of `Def A` are subsets of `A` (`Def∋⊆A`). The next chapter iterates this step into a universe.