Satisfaction by recursion on formulas

Read this chapter directly, or use the reading guide and dependency map to choose another route.

Reading guide · Dependency map

Given a set B in L and a formula, we construct the set of environments over B that satisfy that formula. The construction proceeds by recursion on the formula: for a compound formula the set is determined by the sets of its immediate subformulas, while the atoms and falsity are handled directly. In every case the set is obtained by separation, from the set of all length-n environments over B, of those whose entries meet a describing condition. The membership equations of the resulting sets describe the ten formula constructors.

The recursion being on a meta-language formula shapes every step. Agda can inspect the formula, so each step may name the sets produced at the subformulas as constants of the describing condition, and the object language never has to quantify over a code. The atoms are correspondingly short: a meta-language term is visibly a variable or a constant, so reading its value has one case rather than the two that a coded clause must distinguish.

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

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

module L.Coding.Satisfaction {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

The construction is carried out under excluded middle at the successor of the model level. Its formulas belong to the language of set theory, with equality, membership, the three binary connectives, falsity, and bounded and unbounded quantifiers.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Term; con; var; Formula
        ; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Absoluteness

Satisfaction will be read in the constructible substructure of the cumulative hierarchy. Formula absoluteness supplies that restricted reading, while ordered pairs encode the graphs used as environments.

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )

For each formula, separation cuts its satisfaction set out of the set of coded environments. The formulas appAt and consAtL describe lookup in an environment graph and extension by one value; envSet supplies all environments of the required length.

open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate )
open import L.Coding.Expressions {ℓ} using ( consAtL; numL )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )

Existential clauses produce propositionally truncated witnesses. Finite indices are converted to natural numbers and then represented by von Neumann numerals inside the hierarchy.

open import Cubical.Data.FinData using ( toℕ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )

The hierarchy's numeral construction names those indices as sets. Opening the constructible truth-valued structure fixes the meaning of membership and satisfaction throughout the chapter.

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_ )

The notation _⊨_ below is satisfaction in the restricted constructible structure, evaluated under a finite environment vector.

open hPropStructure 𝒮ʟ

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

Evaluating variables and constants

A variable obtains its value from the environment at its index; a constant already names its value. Both facts are said inside the object language, because the describing conditions are formulas. The term reader tmIs says, of a value slot and an environment slot, that the environment assigns to the term the value at the value slot. For a constant this is the bare equation between the value slot and the constant. For a variable it is an existence statement: some carrier element equals the numeral of the index, and the application clause says that the pair of that index and the recorded value belongs to the graph of the environment recorded at the environment slot. Satisfaction judgments throughout are read in L.

private
  nn : ℕ → S
  nn k = # k , numL k

The internal numerals pair the ambient von Neumann numerals with their constructibility proofs, so an index can be named inside L wherever it is needed.

tmIs : ∀ {n m} → Term S n → Fin m → Fin m → Formula S m

The reader takes a term, the slot holding the value of the term, and the slot holding the environment in which the term is read, and it returns a formula over environments of that length.

tmIs (var i) v e =
  ∃̇ ((var zero ≐ con (nn (toℕ i))) ∧̇ appAt (suc e) zero (suc v))

For a variable, the clause says that some carrier element x equals the numeral of the index, and that the pair of that index and the value at the value slot belongs to the graph of the environment recorded at the environment slot. The equation only pins the index witness; the application clause carries the content.

tmIs (con c) v e = var v ≐ con c

For a constant, no environment is consulted: the value slot is simply identified with the constant.

tmIs-var-in : ∀ {n m} (i : Fin n) (γ : S ^ m) (v e : Fin m)
            → ⟨ pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩
            → ⟨ γ ⊨ tmIs {n} (var i) v e ⟩

The adequacy lemmas connect the formula with the ambient membership it encodes. Inward: if the environment at slot e contains the pair of the numeral i and the value at slot v, then γ satisfies the reader.

tmIs-var-in i γ v e h = ∣ nn (toℕ i)
  , ( refl
    , subst ⟨_⟩ (sym (appAt-adequate (suc e) zero (suc v) (nn (toℕ i) ∷ γ))) h ) ∣₁

The witness is the numeral itself; its defining equation is definitional, and the membership travels along the adequacy path, read in reverse, from the ambient statement to the internal clause over the extended environment.

tmIs-var-out : ∀ {n m} (i : Fin n) (γ : S ^ m) (v e : Fin m)
             → ⟨ γ ⊨ tmIs {n} (var i) v e ⟩
             → ⟨ pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩

Outward, satisfaction of the reader yields the ambient membership. Here a general principle of the chapter appears for the first time: a truncated witness may be consumed whenever the goal is a proposition or a truncation, and nothing below violates this.

tmIs-var-out i γ v e = PT.rec
  (snd (pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ)))

The truncated witness pairs an entry x with the proof that x is the numeral of the index and that the clause over the extended environment holds.

  (λ { (x , (qx , m)) →
    subst (λ w → ⟨ pr w (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩) qx
      (subst ⟨_⟩ (appAt-adequate (suc e) zero (suc v) (x ∷ γ)) m) })

The adequacy path identifies the clause with the membership of the pair of x and the value; rewriting x back to the numeral along its equation leaves exactly the membership that the outward direction owes.

The set of satisfying environments

For each constructor, a formula describes which environments to retain by separation, and every describing condition is a one-variable formula over environments of the formula's own arity. The connectives refer to the sets already built for the subformulas, naming them as constants. An unbounded quantifier conses a member of the carrier onto the environment and asks whether the extension belongs to the set one arity up; the bounded quantifiers add the second guard that the new entry lies in the bounding term's value. Every step of the construction is thus one separation.

private
  opaque
    sep : (a : S) → Formula S 1 → S
    sep a φ = hasSeparationL a φ .fst .fst

Separation is recorded once, in its opaque wrapper: from a set and a one-variable formula it produces the subset.

    sep-mem : (a : S) (φ : Formula S 1) (x : S)
            → (x ∈ˢ sep a φ) ≡ ((x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ))
    sep-mem a φ = hasSeparationL a φ .fst .snd

The membership specification is the whole content of separation: membership in the subset is membership in the ambient set together with satisfaction of the condition.

module _ (B : S) where
  cond : ∀ {n} → Formula S n → Formula S 1

Fix a base set B. Every formula will determine a unary condition on a coded environment over B; separating the environments that satisfy this condition produces its satisfaction set.

  Sat : ∀ {n} → Formula S n → S
  Sat {n} φ = sep (envSet B n) (cond φ)

The set of satisfying environments is the separation, from the full environment set at the formula's arity, of the environments meeting the condition.

  Sat-mem : ∀ {n} (φ : Formula S n) (x : S)
          → (x ∈ˢ Sat φ) ≡ ((x ∈ˢ envSet B n) ⊓ ((x ∷ []) ⊨ cond φ))
  Sat-mem {n} φ = sep-mem (envSet B n) (cond φ)

Its membership equation records exactly the two requirements: the environment has the right arity and values, and it meets the condition specific to the formula.

  cond (t ∈̇ u) =
    (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero))
          ∧̇ ( tmIs u zero (suc (suc zero))
          ∧̇ (var (suc zero) ∈̇ var zero) ))))

The membership atom binds two entries and asserts the object-language membership of the value of t, read at slot suc zero, in the value of u, read at slot zero. Both values are read against the environment slot.

  cond (t ≐ u) =
    (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero))
          ∧̇ ( tmIs u zero (suc (suc zero))
          ∧̇ (var (suc zero) ≐ var zero) ))))

The equality atom has the same shape with equality in place of membership.

  cond (a ∧̇ b) =
    ((var zero ∈̇ con (Sat a)) ∧̇ (var zero ∈̇ con (Sat b)))

A conjunction's condition asks of the environment that it belong to both subformula sets, each named as a constant.

  cond (a ∨̇ b) =
    ((var zero ∈̇ con (Sat a)) ∨̇ (var zero ∈̇ con (Sat b)))

A disjunction's condition asks for membership in at least one of the two.

  cond (a ⇒̇ b) =
    ((var zero ∈̇ con (Sat a)) ⇒̇ (var zero ∈̇ con (Sat b)))

An implication's condition says that membership in the antecedent's set implies membership in the consequent's set.

  cond ⊥̇ = ⊥̇

Falsity is its own condition: no environment satisfies it.

  cond (∃̇ a) =
    (∃̇∈ (con B) (∃̇ ( consAtL zero (suc zero) (suc (suc zero))
                  ∧̇ (var zero ∈̇ con (Sat a)) )))

An unbounded existential ranges over the carrier: some member x of B extends the environment, the extension clause certifies that the new list is an environment, and the extended environment belongs to the subformula's set.

  cond (∀̇ a) =
    (∀̇∈ (con B) (∀̇ ( consAtL zero (suc zero) (suc (suc zero))
                  ⇒̇ (var zero ∈̇ con (Sat a)) )))

The unbounded universal is its dual: every member of the carrier, once consed, lands the extended environment in the subformula's set.

  cond (∀̇∈ t a) =
    (∀̇ ( tmIs t zero (suc zero)
      ⇒̇ ∀̇∈ (con B) ( (var zero ∈̇ var (suc zero))
                   ⇒̇ ∀̇ ( consAtL zero (suc zero) (suc (suc (suc zero)))
                       ⇒̇ (var zero ∈̇ con (Sat a)) ) ) ))

A bounded universal runs in three quantified layers. The outermost reads the value w of the bounding term from its slot; over each such w, the carrier member x is quantified with the two guards x ∈ B and x ∈ w; and for each x, the extension e' of the environment by x, certified by the extension clause, is required to belong to the subformula's set. Here w is only the auxiliary slot of the bound; the environment of the subformula a is e', which adds exactly one entry to the environment.

  cond (∃̇∈ t a) =
    (∃̇ ( tmIs t zero (suc zero)
      ∧̇ ∃̇∈ (con B) ( (var zero ∈̇ var (suc zero))
                   ∧̇ ∃̇ ( consAtL zero (suc zero) (suc (suc (suc zero)))
                       ∧̇ (var zero ∈̇ con (Sat a)) ) ) ))

The bounded existential composes the same three layers as an existence statement: the bounding term's value is read first, and the witness is a member of the carrier lying in that value, whose extension belongs to the subformula's set. Both guards, the base and the bound, are kept.

Reading the conditions

The general equation Sat-mem separates membership in the environment set from satisfaction of the condition. Conjunction, disjunction, implication, and falsity reduce directly by the definition of cond; no auxiliary equivalence is needed for them. The remaining helpers expose the witnesses hidden by the two atomic existentials and by the existential quantifiers, or read the functions supplied by universal quantifiers. They concern only satisfaction of cond φ; the environment-set conjunct remains in Sat-mem.

  CondAtom : ∀ {n} → Term S n → Term S n
           → (S → S → Type (ℓ-suc ℓ)) → S → Type (ℓ-suc ℓ)
  CondAtom t u R z = Σ[ v ∈ S ] (Σ[ w ∈ S ]
    (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs t (suc zero) (suc (suc zero)) ⟩
     × (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs u zero (suc (suc zero)) ⟩ × R v w)))

For the two atoms, the condition is an existence statement, and its unpacked shape is the Σ-type CondAtom: a value v for t and a value w for u, each read through the term reader against the environment at z, together with the relation R between the two underlying sets. The type itself carries no truncation; the truncated form appears at the helpers below.

  cond∈-in : ∀ {n} (t u : Term S n) (z : S)
           → ∥ CondAtom t u (λ v w → ⟨ fst v ∈ fst w ⟩) z ∥₁
           → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩
  cond∈-in t u z = PT.map (λ { (v , (w , r)) → v , ∣ w , r ∣₁ })

The inward mapping for membership repackages the truncated triple as the nested witnesses the two quantifiers expect. The elimination is legitimate because the goal, an outer truncation, is itself a proposition, not because of any property of the relation inside.

  cond∈-out : ∀ {n} (t u : Term S n) (z : S)
            → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩
            → ∥ CondAtom t u (λ v w → ⟨ fst v ∈ fst w ⟩) z ∥₁
  cond∈-out t u z = PT.rec squash₁
    (λ { (v , hv) → PT.map (λ { (w , r) → v , (w , r) }) hv })

The outward mapping flattens the nested witnesses back into the triple, the whole argument remaining inside truncation.

  cond≐-in : ∀ {n} (t u : Term S n) (z : S)
           → ∥ CondAtom t u (λ v w → fst v ≡ fst w) z ∥₁
           → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩
  cond≐-in t u z = PT.map (λ { (v , (w , r)) → v , ∣ w , r ∣₁ })

The equality atom carries the relation fst v ≡ fst w, equality of underlying sets, and its inward mapping is word for word the membership one.

  cond≐-out : ∀ {n} (t u : Term S n) (z : S)
            → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩
            → ∥ CondAtom t u (λ v w → fst v ≡ fst w) z ∥₁
  cond≐-out t u z = PT.rec squash₁
    (λ { (v , hv) → PT.map (λ { (w , r) → v , (w , r) }) hv })

Its outward mapping is likewise the membership one with the relation exchanged.

  CondQuant : ∀ {n} → Formula S (suc n) → S → Type (ℓ-suc ℓ)
  CondQuant a z = Σ[ x ∈ S ] (⟨ fst x ∈ fst B ⟩
    × (Σ[ e' ∈ S ] (⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩
                    × ⟨ fst e' ∈ fst (Sat a) ⟩)))

For the unbounded existential, the unpacked condition is the Σ-type CondQuant: a member x of the base, an entry e' certified by the extension clause to be the environment z extended by x, and membership of e' in the subformula's set. Again the type is untruncated, and the truncation is added at the helpers.

  cond∃-in : ∀ {n} (a : Formula S (suc n)) (z : S)
           → ∥ CondQuant a z ∥₁ → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩
  cond∃-in a z = PT.map (λ { (x , (x∈ , (e' , r))) → x , (x∈ , ∣ e' , r ∣₁) })

Inward folds the extension data into the single truncated witness that the existential's own quantifier provides.

  cond∃-out : ∀ {n} (a : Formula S (suc n)) (z : S)
            → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩ → ∥ CondQuant a z ∥₁
  cond∃-out a z = PT.rec squash₁
    (λ { (x , (x∈ , hv)) → PT.map (λ { (e' , r) → x , (x∈ , (e' , r)) }) hv })

Outward unfolds the two nested truncated witnesses in turn; both goals are truncations and therefore propositions, so the unfolding is legitimate.

  cond∀-in : ∀ {n} (a : Formula S (suc n)) (z : S)
           → ((x e' : S) → ⟨ fst x ∈ fst B ⟩
              → ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩

For every permitted value and its certified extension, the premise supplies membership in the subformula's satisfaction set.

              → ⟨ fst e' ∈ fst (Sat a) ⟩)
           → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩
  cond∀-in a z k x x∈ e' hc = k x e' x∈ hc

For the unbounded universal, the unpacked condition is a function assigning to every base member and its extension the subformula's truth at that extension. Inward and outward are that one function read in the two directions of the quantifier.

  cond∀-out : ∀ {n} (a : Formula S (suc n)) (z : S)
            → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩
            → ((x e' : S) → ⟨ fst x ∈ fst B ⟩

Reading the condition outward retains the value from B and the environment obtained by adjoining it.

               → ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩
               → ⟨ fst e' ∈ fst (Sat a) ⟩)
  cond∀-out a z h x e' x∈ hc = h x x∈ e' hc

No truncation appears, because satisfaction of a universal is verified by supplying its verifier, which is exactly what both directions do.

  CondBnd : ∀ {n} → Formula S (suc n) → S → S → Type (ℓ-suc ℓ)
  CondBnd a z w = Σ[ x ∈ S ] ((⟨ fst x ∈ fst B ⟩ × ⟨ fst x ∈ fst w ⟩)
    × (Σ[ e' ∈ S ]
        (⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩
         × ⟨ fst e' ∈ fst (Sat a) ⟩)))

The bounded quantifiers add one layer. The condition quantifies, in order, the value w of the bounding term, a member x of the base lying in w, and the extension e' of the environment z by x, certified by the extension clause and required to belong to the subformula's set. The role of w is auxiliary: it carries the bound's value, while the environment of the subformula is e', which adds exactly one entry, the member x, to the environment z.

  cond∃∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
            → ∥ (Σ[ w ∈ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
                             × ∥ CondBnd a z w ∥₁)) ∥₁
            → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩

The bounded existential stacks its witnesses: the outer truncation is over the value w of the bounding term, and inside it sits the inner truncation of CondBnd a z w, holding the carrier member and its extension.

  cond∃∈-in t a z = PT.map
    (λ { (w , (hw , hx)) → w , (hw , PT.map
      (λ { (x , ((x∈B , x∈w) , (e' , r))) → x , (x∈B , (x∈w , ∣ e' , r ∣₁)) })
      hx) })

The first PT.map eliminates the outer truncation over w, and the nested PT.map eliminates the inner truncation of CondBnd, folding the member and the extension into the existential's own quantifier. Both goals are truncations and hence propositions, so the two eliminations are legitimate for the same reason.

  cond∃∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
             → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩
             → ∥ (Σ[ w ∈ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
                              × ∥ CondBnd a z w ∥₁)) ∥₁

The outward statement exposes the same two-layer shape: the value of the bound on the outside, and within it the truncated record of the carrier member and its extension.

  cond∃∈-out t a z = PT.map
    (λ { (w , (hw , hx)) → w , (hw , PT.rec squash₁
      (λ { (x , (x∈B , (x∈w , hv))) → PT.map
        (λ { (e' , r) → x , ((x∈B , x∈w) , (e' , r)) }) hv })
      hx) })

Its proof unfolds the two layers in turn, the whole journey remaining inside truncation.

  cond∀∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
            → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
               → (x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ fst x ∈ fst w ⟩

The two guards require x to belong both to the base B and to the value w of the bounding term.

               → ⟨ (e' ∷ x ∷ w ∷ z ∷ [])
                    ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩
               → ⟨ fst e' ∈ fst (Sat a) ⟩)
            → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩
  cond∀∈-in t a z k w hw x x∈B x∈w e' hc = k w hw x e' x∈B x∈w hc

The bounded universal's condition is a function over the three quantified layers: to every value w of the bounding term it assigns, for every base member x inside w and every extension e' certified as the environment z extended by x, the subformula's truth at e'. The inward mapping is that function, applied.

  cond∀∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
             → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩
             → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩

The result ranges over the same bound value, base member, and certified one-entry extension.

                → (x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ fst x ∈ fst w ⟩
                → ⟨ (e' ∷ x ∷ w ∷ z ∷ [])
                     ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩
                → ⟨ fst e' ∈ fst (Sat a) ⟩)
  cond∀∈-out t a z h w hw x e' x∈B x∈w hc = h w hw x x∈B x∈w e' hc

The outward mapping is the same function, read back through the three quantifiers. No truncation appears in either direction, since a universal is verified by supplying its verifier, and here the verifier is supplied layer by layer, for the value, for the member, and for the extension.