The definable subsets

Part 4 is about to open, and its plan fits in one sentence: build, inside the model just assembled, the sub-universe of sets reachable by first-order definability alone. This chapter forges the single step that the whole construction iterates: from a set A, form Def A, the set of all subsets of A definable in the structure (A, ∈) by a formula with parameters from A. The gap between predicate and formula, which the model chapter called mathematical content, here becomes a machine: Def A collects precisely the first-order shadow of A's power set.

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 makes the essential smallness of the previous chapters bite: every formula evaluates small, so Def A is a set with no resizing spent at all.

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

open import Base.Prelude
open import Base.Truth

module L.Definability {ℓ : Level} where

open import FOL.ZFStructure using ( ZFStructure; Transitive )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; ⊤̇ )
open import FOL.LevyHierarchy using ( Δ₀ )
open import FOL.Manipulation.Relabelling using ( mapFo; mapΔ₀; ⊨-map )
import FOL.Absoluteness
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 )
open import Cubical.Data.Sigma using ( Σ-cong-equiv-snd )
open import Cubical.Data.Unit using ( tt* )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber; presentation
        ; isEmb⟪_⟫↪; _⊆_; extensionality )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open ZFStructure 𝒮ᵥ

The operator

Everything below is relative to one set A, so the chapter 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.

module DefOf (A : S) where

  M : S → hProp (ℓ-suc ℓ)
  M x = x ∈ˢ A

  e : ⟪ A ⟫ ≃ (Σ[ x ∈ S ] (x ∈ᶜ M))
  e = compEquiv (invEquiv (presentation A))
        (Σ-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

  open InnerSmall M ⟪ A ⟫ e {K = ⟪ A ⟫} ι public

With the inner satisfaction ⊨ᵐ and its smallness in scope, the operator writes itself down. smallSat φ m is the truth value of φ at the member m, compressed one universe down; defSet φ is the subset φ carves out of A, a sett over the members φ selects; and Def A is the set of all of them, indexed by the formulas themselves. A formula is a piece of inductive data in Type ℓ, so it is a legitimate small index: syntax as index set is the whole trick.

  smallSat : Formula ⟪ A ⟫  → ⟪ A ⟫ → hProp ℓ
  smallSat φ m = ⊨ᵐ-small φ (ι m ∷ []) .fst

  defSet : Formula ⟪ A ⟫  → S
  defSet φ = sett (Σ[ m ∈ ⟪ A ⟫ ] ⟨ smallSat φ m ⟩) (λ p → ⟪ A ⟫↪ (p .fst))

  Def : S
  Def = sett (Formula ⟪ A ⟫ ) defSet

Membership, specified

Both Def and each defSet φ are setts, 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, two specifications: their members stay inside A, and a member ⟪ A ⟫↪ m belongs to defSet φ exactly when the inner world satisfies φ at m, which is the phrase "definable subset" cashed out literally (the compression smallSat was only an encoding, and the equivalence carries it back).

  Def-spec : (x : S)
           → ⟨ x ∈ˢ Def ⟩ ≡ ∥ Σ[ φ ∈ Formula ⟪ A ⟫  ] (defSet φ ≡ x) ∥₁
  Def-spec x = refl

  defSet⊆A : (φ : Formula ⟪ A ⟫ ) (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
    ⟪⟫↪-inj : {m' m : ⟪ A ⟫} → ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m → m' ≡ m
    ⟪⟫↪-inj {m'} {m} = isEmbedding→Inj isEmb⟪ A ⟫↪ m' m

  defSet-mem : (φ : Formula ⟪ A ⟫ ) (m : ⟪ A ⟫)
             → (⟪ A ⟫↪ m ∈ˢ defSet φ) ≡ ((ι m ∷ []) ⊨ᵐ φ)
  defSet-mem φ m = ⇔toPath fwd bwd
    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) }
    bwd : ⟨ (ι m ∷ []) ⊨ᵐ φ ⟩ → ⟨ ⟪ A ⟫↪ m ∈ˢ defSet φ ⟩
    bwd hφ = ∣ (m , equivFun (decode .snd) hφ) , refl ∣₁

Def refines, never shrinks

A itself is definable: the formula "true" selects everyone, so defSet ⊤̇ ≡ A and hence A ∈ Def A. Dually, every member of Def A is a subset of A. So Def sits between A and the power set: it keeps the whole of A as an element and adds only subsets.

  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₂)
    where
    sub₁ : ⟨ defSet ⊤̇ ⊆ A ⟩
    sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = A} .fst
      (defSet⊆A ⊤̇ y (∈∈ₛ {a = y} {b = defSet ⊤̇} .snd y∈ₛ))
    sub₂ : ⟨ A ⊆ defSet ⊤̇ ⟩
    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)) tt*))

  A∈Def : ⟨ A ∈ˢ Def ⟩
  A∈Def = subst (λ x → ⟨ x ∈ˢ Def ⟩) defSet⊤≡A ∣ ⊤̇ , refl ∣₁

  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 move 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: the step loses no one. Combined with the previous section, iterating Def can only accumulate, which is the shape Part 4's tower needs.

  module Refine (Atrans : Transitive 𝒮ᵥ M) where

    atom : ⟪ A ⟫ → Formula ⟪ A ⟫ 
    atom mₐ = var zero ∈̇ con mₐ

    atom-mem : (mₐ m : ⟪ A ⟫)
             → (⟪ A ⟫↪ m ∈ˢ defSet (atom mₐ)) ≡ (⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ)
    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ₐ ⟩
      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 ∣₁)) })
        (∈∈ₛ {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
            (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)))
        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∈ =
      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 Part 4 leans 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.

    module Abs = FOL.Absoluteness.Single 𝒮ᵥ M Atrans

    abs-defSet : (φ : Formula ⟪ A ⟫ ) → Δ₀ φ → (m : ⟪ A ⟫)
               → (⟪ A ⟫↪ m ∈ˢ defSet φ)
                 ≡ ((⟪ A ⟫↪ m ∷ []) Abs.⊨ᵛ (mapFo ι φ))
    abs-defSet φ d m =
        defSet-mem φ m
      ∙ sym (⊨-map (hPropAlgebra (ℓ-suc ℓ)) 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, essential smallness footing the universe bill. Membership is definitional (Def-spec), the specification defSet-mem says "definable" literally, and the operator only refines: A ∈ Def A always (A∈Def), A ⊆ Def A under transitivity (A⊆Def), and members of Def A never leave A's subsets (Def∋⊆A). The next chapter iterates this step into a universe.