Structures

A formula means nothing by itself; it needs a world to be about. For the language of the previous chapter, a world is a structure in the sense of model theory: a carrier together with interpretations of the two predicate symbols, membership and equality, taking values in a chosen truth algebra. This chapter defines these structures, the ways of cutting them down, and the environments that will feed their elements to formulas.

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

module FOL.ZFStructure where

open import Base.Prelude
open import Base.Truth
open import Cubical.Foundations.HLevels using ( isSetΣSndProp )
open import Cubical.Data.Sigma using ( Σ≡Prop )

The record

The conventions again, book-wide: script 𝒮 stands for a structure, S for its carrier, and x, y, z for carrier elements, the "sets" the language speaks of. The superscript ˢ on the two relation fields is another layer mark: it says a symbol is a field of the structure at hand. The membership family now has three members on the page, one glyph per layer: the library's ∈ (the host), this chapter's ∈ˢ (the structure), and the previous chapter's ∈̇ (the syntax).

record ZFStructure {ℓ ℓ'} (𝕋 : TruthAlgebra ℓ ℓ') : Type (ℓ-max (ℓ-suc ℓ) ℓ') where
  open TruthAlgebra 𝕋
  field
    S         : Type ℓ
    isSetS    : isSet S
    _≈ˢ_ _∈ˢ_ : S → S → Ω

  infix 20 _≈ˢ_ _∈ˢ_

Two remarks on the fields. That the structure equality ≈ˢ is a field, rather than being hard-wired to the host's path equality, is load-bearing: in the forcing part of the book, equality and membership will be a mutually defined pair of graded relations, genuine content of the model that no meta-level equality could supply. On the propositional side nothing is lost: when the hierarchy chapter assembles the book's instance, it simply takes paths for ≈ˢ.

And a remark on what is not here: no axioms. This record is the bare structure; well-foundedness, extensionality, and the rest belong to Part 2, where they become the fields of a model. Everything this part builds consumes only the three projections above, so any two isomorphic structures are, by the host's structure identity principle, simply equal, and the whole development transports across.

The propositional side

On the propositional side one more form of membership is available: extract the underlying type of x ∈ˢ y. The superscript ᵗ marks this Type-valued variant; statements of well-foundedness and proofs by membership induction will quantify over it. It lives in hPropStructure, the propositional side's way of opening a structure: the module re-exports the three projections and adds ∈ᵗ, so one open later a chapter writes y ∈ᵗ x with no structure argument in sight.

module hPropStructure {ℓ} (𝒮 : ZFStructure (hPropAlgebra ℓ)) where
  open ZFStructure 𝒮 public

  _∈ᵗ_ : S → S → Type ℓ
  x ∈ᵗ y = ⟨ x ∈ˢ y ⟩

  infix 20 _∈ᵗ_

Transitive classes

A class M over a carrier is transitive when members of its members stay in it. The absoluteness chapter's theorems consume exactly this hypothesis, and Part 4 builds its world out of transitive stages; the name is minted here, beside the memberships it speaks.

Transitive : ∀ {ℓ} (𝒮 : ZFStructure (hPropAlgebra ℓ))
           → (ZFStructure.S 𝒮 → hProp ℓ) → Type ℓ
Transitive 𝒮 M = ∀ {x y} → y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M
  where open hPropStructure 𝒮

Substructures

↾ reads "restriction": the textbook's passage from a universe to

$(A, \in \restriction A)$. Given a propositional class M, the restricted structure 𝒮 ↾ M takes as carrier the pairs of an element with a proof of membership in M, and inherits both relations along the first projection. The consequence worth savouring: instantiate the whole framework at 𝒮 ↾ M, and the constant domain of the syntax automatically contains only members of M. "The parameters may only come from this class" stops being a side condition to police and becomes the shape of a type; Part 4 builds the constructible universe through exactly this channel.

_↾_ : ∀ {ℓ} (𝒮 : ZFStructure (hPropAlgebra ℓ))
    → (ZFStructure.S 𝒮 → hProp ℓ) → ZFStructure (hPropAlgebra ℓ)
_↾_ {ℓ} 𝒮 M = record
  { S      = Σ[ x ∈ S ] (x ∈ᶜ M)
  ; isSetS = isSetΣSndProp isSetS (λ x → (M x) .snd)
  ; _≈ˢ_   = λ a b → fst a ≈ˢ fst b
  ; _∈ˢ_   = λ a b → fst a ∈ˢ fst b }
  where open ZFStructure 𝒮

infixl 21 _↾_

The restricted equality compares underlying elements; since membership in a propositional class is proof-irrelevant, equality of first projections reflects back to equality of the pairs, so nothing is lost.

↾-reflects : ∀ {ℓ} {𝒮 : ZFStructure (hPropAlgebra ℓ)} {M : ZFStructure.S 𝒮 → hProp ℓ}
             {a b : ZFStructure.S (𝒮 ↾ M)}
           → fst a ≡ fst b → a ≡ b
↾-reflects {M = M} = Σ≡Prop (λ x → (M x) .snd)

Recap

A structure is three projections, carrier, equality, membership, valued in a truth algebra and carrying no axioms; transitive classes name the condition the travelling chapters will keep consuming; ↾ cuts a structure down to a class with nothing lost (↾-reflects). Syntax on one side, structures on the other: the next chapter joins them.