Abstracting the parameters

A constant is how an ambient set enters a formula, and the role it plays there is that of a parameter. Every use the book makes of formulas as data has had to work around them: constants are as many as there are sets, so a syntax with constants can be neither counted nor coded, and the parameter-free formulas were introduced for exactly that reason. This chapter builds the trade that turns one into the other. A formula with parameters becomes a parameter-free formula of higher arity together with a vector of the constants it mentioned, and satisfaction is preserved when those constants are supplied in the environment instead of in the syntax. Nothing is lost and nothing is added: the two formulas say the same thing at the same points, and all that changes is where the parameters sit.

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

module FOL.Manipulation.Parameters where

open import Base.Prelude
open import Base.Truth
open import FOL.ZFStructure using ( ZFStructure )
open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Semantics
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Vec using ( _++_; map )
import Cubical.Data.Empty as Empty

Counting by occurrence

The design point of the chapter is decided here, before any syntax moves. A formula's constants are counted by occurrence, not by value: a formula with k constant-occurrences yields a vector of length k, and two occurrences of the same constant are two entries of that vector, holding the same set twice.

A reader who expects the set of constants a formula mentions will look for the decidable equality that would let two occurrences of one constant be recognized as one, and will not find it. There is none to find: the constant domain is an arbitrary type, nothing obliges its equality to be decidable, and on a carrier of sets it demonstrably is not. Counting by occurrence is what frees the whole chapter from that demand. The price is an abstraction of higher arity than strictly necessary, paid in variables that receive a value twice over, and nothing downstream can tell the difference: a vector of parameters is a vector of parameters.

The count is a structural recursion over the twelve constructors, with a term's count feeding it: a constant is one occurrence, a variable is none. Where a constructor has two parts, the counts add, left part first.

countTm : ∀ {ℓc} {K : Type ℓc} {n} → Term K n → ℕ
countTm (con c) = suc zero
countTm (var i) = zero

countFo : ∀ {ℓc} {K : Type ℓc} {n} → Formula K n → ℕ
countFo (t ∈̇ u)  = countTm t + countTm u
countFo (t ≐ u)  = countTm t + countTm u
countFo (φ ∧̇ ψ)  = countFo φ + countFo ψ
countFo (φ ∨̇ ψ)  = countFo φ + countFo ψ
countFo (φ ⇒̇ ψ)  = countFo φ + countFo ψ
countFo (¬̇ φ)    = countFo φ
countFo ⊤̇        = zero
countFo ⊥̇        = zero
countFo (∃̇ φ)    = countFo φ
countFo (∀̇ φ)    = countFo φ
countFo (∀̇∈ t φ) = countTm t + countFo φ
countFo (∃̇∈ t φ) = countTm t + countFo φ

Collecting is the same recursion written a second time, and it has to be a second recursion rather than one returning both: the length of the vector it returns is precisely what the first computes, so the count must already exist for the collection to be typeable at all. Every clause mirrors its counterpart above, with ++ where the count had +, so the constants come out in the order the formula mentions them, left to right.

constantsTm : ∀ {ℓc} {K : Type ℓc} {n} (t : Term K n) → Vec K (countTm t)
constantsTm (con c) = c ∷ []
constantsTm (var i) = []

constantsFo : ∀ {ℓc} {K : Type ℓc} {n} (φ : Formula K n) → Vec K (countFo φ)
constantsFo (t ∈̇ u)  = constantsTm t ++ constantsTm u
constantsFo (t ≐ u)  = constantsTm t ++ constantsTm u
constantsFo (φ ∧̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo (φ ∨̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo (φ ⇒̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo (¬̇ φ)    = constantsFo φ
constantsFo ⊤̇        = []
constantsFo ⊥̇        = []
constantsFo (∃̇ φ)    = constantsFo φ
constantsFo (∀̇ φ)    = constantsFo φ
constantsFo (∀̇∈ t φ) = constantsTm t ++ constantsFo φ
constantsFo (∃̇∈ t φ) = constantsTm t ++ constantsFo φ

Where the new variables go

The abstraction raises the arity from n to n + k: the original n variables keep their de Bruijn indices, and the k constant-occurrences are read off the k slots that follow. That layout is not a preference, it is what the binders allow. A quantifier's body lives in a context with one more variable, index 0 being the one just bound, so a parameter block placed before the variables would have to be renumbered at every binder. Placed after them, suc n + k is suc (n + k) on the nose: the block simply rides one index higher inside the body, and four binding constructors cost nothing at all. This is also the whole of what "the abstracted variables must not be captured" comes to here. The block sits above every binder, and no binder ever reaches it.

Two placements do the index arithmetic, and each is three lines. padRight b reads an index of the first a slots of a + b; padLeft a reads an index of the last b. They are one another's mirror, and the asymmetry in their arguments is the asymmetry of the recursion: padRight recurses on the index, padLeft on the number of slots it steps over.

padRight : ∀ {a} b → Fin a → Fin (a + b)
padRight b zero    = zero
padRight b (suc i) = suc (padRight b i)

padLeft : ∀ a {b} → Fin b → Fin (a + b)
padLeft zero    j = j
padLeft (suc a) j = suc (padLeft a j)

Each placement has one law, and it is the law an environment obeys: looking up a padded index in a concatenated vector is looking up the original index in the corresponding half. Both are proved by hand, clause by clause, over the vector and the index together; a proof routed through some library round trip between an index of a sum and a pair of indices would only invite a conversion problem where there is none. A third law of the same kind reads a mapped vector, and it is the one that lets the interpretation of the constants pass through the collection.

lookup-padRight : ∀ {ℓa} {A : Type ℓa} {a b} (p : Vec A a) (q : Vec A b) (i : Fin a)
                → lookup (padRight b i) (p ++ q) ≡ lookup i p
lookup-padRight []      q ()
lookup-padRight (x ∷ p) q zero    = refl
lookup-padRight (x ∷ p) q (suc i) = lookup-padRight p q i

lookup-padLeft : ∀ {ℓa} {A : Type ℓa} a {b} (p : Vec A a) (q : Vec A b) (j : Fin b)
               → lookup (padLeft a j) (p ++ q) ≡ lookup j q
lookup-padLeft zero    []      q j = refl
lookup-padLeft (suc a) (x ∷ p) q j = lookup-padLeft a p q j

lookup-map : ∀ {ℓa ℓb} {A : Type ℓa} {B : Type ℓb} {n}
             (f : A → B) (v : Vec A n) (j : Fin n)
           → lookup j (map f v) ≡ f (lookup j v)
lookup-map f []      ()
lookup-map f (x ∷ v) zero    = refl
lookup-map f (x ∷ v) (suc j) = lookup-map f v j

The abstraction

The abstraction is written once in a generic form and instantiated once. The generic form takes a placement: a function θ assigning to each constant-occurrence of the formula a variable of the target context, and it returns the formula with every constant replaced by the variable θ names for it. The target's arity is n + k for a k the placement is free to choose, so the generic form abstracts into a context with room to spare.

Genericity here is not decoration; it is what keeps the two-part constructors from needing a second pass. A conjunction's occurrences are its left operand's followed by its right operand's, so the two operands are abstracted under the placements θ ∘ padRight and θ ∘ padLeft, composed before the traversal rather than recovered afterwards by renaming the two halves into the joined context. One pass over the formula, no weakening lemma, and each of the twelve clauses is the shape the corresponding clause of every other structural recursion in this part has. Under a binder the placement gains a suc, which is the parameter block riding one index higher, and nothing else happens at all.

placeTm : ∀ {ℓz ℓc} {K : Type ℓc} {n k} (t : Term K n)
        → (Fin (countTm t) → Fin (n + k)) → Term (⊥* {ℓz}) (n + k)
placeTm         (con c) θ = var (θ zero)
placeTm {k = k} (var i) θ = var (padRight k i)

placeFo : ∀ {ℓz ℓc} {K : Type ℓc} {n k} (φ : Formula K n)
        → (Fin (countFo φ) → Fin (n + k)) → Formula (⊥* {ℓz}) (n + k)
placeFo (t ∈̇ u)  θ = placeTm t (λ i → θ (padRight (countTm u) i))
                   ∈̇ placeTm u (λ j → θ (padLeft (countTm t) j))
placeFo (t ≐ u)  θ = placeTm t (λ i → θ (padRight (countTm u) i))
                   ≐ placeTm u (λ j → θ (padLeft (countTm t) j))
placeFo (φ ∧̇ ψ)  θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
                   ∧̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo (φ ∨̇ ψ)  θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
                   ∨̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo (φ ⇒̇ ψ)  θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
                   ⇒̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo (¬̇ φ)    θ = ¬̇ placeFo φ θ
placeFo ⊤̇        θ = ⊤̇
placeFo ⊥̇        θ = ⊥̇
placeFo (∃̇ φ)    θ = ∃̇ placeFo φ (λ j → suc (θ j))
placeFo (∀̇ φ)    θ = ∀̇ placeFo φ (λ j → suc (θ j))
placeFo (∀̇∈ t φ) θ = ∀̇∈ (placeTm t (λ i → θ (padRight (countFo φ) i)))
                        (placeFo φ (λ j → suc (θ (padLeft (countTm t) j))))
placeFo (∃̇∈ t φ) θ = ∃̇∈ (placeTm t (λ i → θ (padRight (countFo φ) i)))
                        (placeFo φ (λ j → suc (θ (padLeft (countTm t) j))))

The instance is the one the rest of the book will name: take the budget to be exactly the occurrence count and the placement to be the block that follows the variables. This is the abstraction proper, and its type is the chapter's headline: a formula over K with n free variables becomes a parameter-free formula with n + countFo φ of them.

absFo : ∀ {ℓz ℓc} {K : Type ℓc} {n} (φ : Formula K n) → Formula (⊥* {ℓz}) (n + countFo φ)
absFo {n = n} φ = placeFo φ (padLeft n)

Adequacy

Meaning is checked against the generic semantics, at an arbitrary truth algebra, an arbitrary structure, and an arbitrary constant interpretation. Two satisfactions are in scope at once and are told apart by a mark: ⊨ is the original's, read at the interpretation ι, and ⊨₀ is the abstraction's, read at the empty constant domain, where the interpretation has nothing to do and the library's eliminator says so.

module _ {ℓ ℓ'} (𝕋 : TruthAlgebra ℓ ℓ') (𝒮 : ZFStructure 𝕋) where

  open TruthAlgebra 𝕋
  open ZFStructure 𝒮

  private module Sem = FOL.Semantics 𝕋 𝒮
  open Sem using ( _^_ )

  module _ {ℓz ℓc} {K : Type ℓc} (ι : K → S) where

    open Sem.At K ι using ( _⊨_; ⟦_⟧ )
    open Sem.At (⊥* {ℓz}) Empty.rec* using ()
      renaming ( _⊨_ to _⊨₀_ ; ⟦_⟧ to ⟦_⟧₀ )

The statement is generic in the placement, and it has to be, because the recursion's placements are built at the recursive calls. It is stated at a variable environment γ and a variable parameter environment σ, constrained by one hypothesis: at every occurrence, the slot the placement names holds the interpretation of the constant the collection recorded there. That hypothesis is the whole content of "the constants are supplied in the environment", and stating it as a hypothesis rather than substituting a concrete environment is what keeps every clause from normalizing a vector.

Splitting the hypothesis is the only bookkeeping the two-part constructors need, and each half is one composition with a pad law.

    private
      leftHalf : ∀ {n k a b} (θ : Fin (a + b) → Fin (n + k))
                 (γ : S ^ n) (σ : S ^ k) (p : Vec K a) (q : Vec K b)
               → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (p ++ q)))
               → (∀ i → lookup (θ (padRight b i)) (γ ++ σ) ≡ ι (lookup i p))
      leftHalf θ γ σ p q h i = h (padRight _ i) ∙ cong ι (lookup-padRight p q i)

      rightHalf : ∀ {n k} a {b} (θ : Fin (a + b) → Fin (n + k))
                  (γ : S ^ n) (σ : S ^ k) (p : Vec K a) (q : Vec K b)
                → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (p ++ q)))
                → (∀ j → lookup (θ (padLeft a j)) (γ ++ σ) ≡ ι (lookup j q))
      rightHalf a θ γ σ p q h j = h (padLeft a j) ∙ cong ι (lookup-padLeft a p q j)

Terms first, two cases and both immediate. A constant's value is what the hypothesis says the slot holds; a variable's value is untouched, and the pad law finds it again in the extended environment.

    ⟦⟧-place : ∀ {n k} (t : Term K n) (θ : Fin (countTm t) → Fin (n + k))
               (γ : S ^ n) (σ : S ^ k)
             → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsTm t)))
             → ⟦ t ⟧ γ ≡ ⟦ placeTm t θ ⟧₀ (γ ++ σ)
    ⟦⟧-place (con c) θ γ σ h = sym (h zero)
    ⟦⟧-place (var i) θ γ σ h = sym (lookup-padRight γ σ i)

Then the fourteen cases of the formula induction, twelve of them here and the two term cases just discharged. Every propositional clause is a congruence, because the semantics assigns each object connective exactly the truth algebra's operation and there is no translation layer to cross. The four binding clauses push a value onto the environment and appeal to the induction hypothesis at the extended one, and the hypothesis about the parameter slots travels unchanged: consing on the left and shifting the placement by suc cancel each other by computation, so the binders need no lemma of their own. The two bounded clauses split, term on the left and body on the right, exactly as their constructors do.

    ⊨-place : ∀ {n k} (φ : Formula K n) (θ : Fin (countFo φ) → Fin (n + k))
              (γ : S ^ n) (σ : S ^ k)
            → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsFo φ)))
            → (γ ⊨ φ) ≡ ((γ ++ σ) ⊨₀ placeFo φ θ)
    ⊨-place (t ∈̇ u) θ γ σ h = cong₂ _∈ˢ_
      (⟦⟧-place t (λ i → θ (padRight (countTm u) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsTm u) h))
      (⟦⟧-place u (λ j → θ (padLeft (countTm t) j)) γ σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsTm u) h))
    ⊨-place (t ≐ u) θ γ σ h = cong₂ _≈ˢ_
      (⟦⟧-place t (λ i → θ (padRight (countTm u) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsTm u) h))
      (⟦⟧-place u (λ j → θ (padLeft (countTm t) j)) γ σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsTm u) h))
    ⊨-place (φ ∧̇ ψ) θ γ σ h = cong₂ _⊓_
      (⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
        (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
      (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
        (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
    ⊨-place (φ ∨̇ ψ) θ γ σ h = cong₂ _⊔_
      (⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
        (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
      (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
        (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
    ⊨-place (φ ⇒̇ ψ) θ γ σ h = cong₂ _⇒_
      (⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
        (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
      (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
        (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
    ⊨-place (¬̇ φ)   θ γ σ h = cong ¬_ (⊨-place φ θ γ σ h)
    ⊨-place ⊤̇       θ γ σ h = refl
    ⊨-place ⊥̇       θ γ σ h = refl
    ⊨-place (∃̇ φ)   θ γ σ h = cong (⋁ S) (funExt (λ x →
      ⊨-place φ (λ j → suc (θ j)) (x ∷ γ) σ h))
    ⊨-place (∀̇ φ)   θ γ σ h = cong (⋀ S) (funExt (λ x →
      ⊨-place φ (λ j → suc (θ j)) (x ∷ γ) σ h))
    ⊨-place (∀̇∈ t φ) θ γ σ h = cong (⋀ S) (funExt (λ x → cong₂ _⇒_
      (cong (x ∈ˢ_) (⟦⟧-place t (λ i → θ (padRight (countFo φ) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsFo φ) h)))
      (⊨-place φ (λ j → suc (θ (padLeft (countTm t) j))) (x ∷ γ) σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsFo φ) h))))
    ⊨-place (∃̇∈ t φ) θ γ σ h = cong (⋁ S) (funExt (λ x → cong₂ _⊓_
      (cong (x ∈ˢ_) (⟦⟧-place t (λ i → θ (padRight (countFo φ) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsFo φ) h)))
      (⊨-place φ (λ j → suc (θ (padLeft (countTm t) j))) (x ∷ γ) σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsFo φ) h))))

The adequacy proper follows by choosing the placement the abstraction chose and the parameter environment the collection prescribes: the constants themselves, interpreted. Its hypothesis is then the two pad laws in sequence, and the theorem reads exactly as promised. Satisfaction of the original at γ is satisfaction of the abstraction at γ extended by the collected constants.

    ⊨-abs : ∀ {n} (φ : Formula K n) (γ : S ^ n)
          → (γ ⊨ φ) ≡ ((γ ++ map ι (constantsFo φ)) ⊨₀ absFo φ)
    ⊨-abs {n} φ γ = ⊨-place φ (padLeft n) γ (map ι (constantsFo φ)) hyp
      where
      hyp : ∀ j → lookup (padLeft n j) (γ ++ map ι (constantsFo φ))
                ≡ ι (lookup j (constantsFo φ))
      hyp j = lookup-padLeft n γ (map ι (constantsFo φ)) j
            ∙ lookup-map ι (constantsFo φ) j

What a definable subset is

The corollary the next chapter consumes lives at arity one, because that is the arity a subset is carved by. A definable subset of a set A is carved by a formula of one free variable with constants from A, and membership in it is satisfaction of that formula in the world (A, ∈). That world is a structure like any other, and the development above was stated at an arbitrary one, so instantiating it there is the entire argument: at the restricted structure and the definable powerset's own constant interpretation, ⊨-abs₁ says the subset carved by φ is the subset carved by the parameter-free absFo φ at the parameters constantsFo φ supplied in the environment. The satisfaction on both sides is the inner one, the notion the definable powerset is defined by, and not the ambient reading of a relativized formula; the two differ, and it is the inner one that is owed.

One point of shape, and the reason the arity-one case is worth writing down: at arity one the extended environment is x ∷ map ι p, a single member followed by the parameters, which is the very shape a one-entry environment has everywhere else in the book.

    ⊨-abs₁ : (φ : Formula K ) (x : S)
           → ((x ∷ []) ⊨ φ) ≡ ((x ∷ map ι (constantsFo φ)) ⊨₀ absFo φ)
    ⊨-abs₁ φ x = ⊨-abs φ (x ∷ [])

Packaged as an existential, the same fact is the sentence the next chapter will quote: every formula of one free variable is a parameter-free formula of arity 1 + k at a vector of k parameters, agreeing with it at every point.

    asPure₁ : (φ : Formula K )
            → Σ[ k ∈ ℕ ] Σ[ χ ∈ Formula (⊥* {ℓz}) (suc k) ] Σ[ p ∈ Vec K k ]
                ((x : S) → ((x ∷ []) ⊨ φ) ≡ ((x ∷ map ι p) ⊨₀ χ))
    asPure₁ φ = countFo φ , absFo φ , constantsFo φ , ⊨-abs₁ φ

Recap

Constants counted by occurrence (countFo) and collected in that order (constantsFo); one generic traversal placeFo that puts each occurrence wherever a placement says, instantiated as the abstraction

absFo, which raises the arity by the occurrence count and returns a parameter-free formula; and ⊨-abs, which certifies that the trade costs no meaning, with ⊨-abs₁ and asPure₁ spending it at the arity a subset is carved by. Parameters can now leave the syntax and live in the environment, which is the one thing standing between a definable subset and a formula that can be counted.