Relabelling

The constant domain is a parameter, and the book keeps swapping it: the working syntax takes a carrier, the parameter-free formulas take the empty type, Part 4 takes a restricted carrier. This chapter is the kit for such swaps, and it works at three altitudes at once: a map between constant domains pushes through syntax functorially, preserves meaning on the nose, and carries the Levy witnesses along unchanged. Like its tail-mates, the kit has no consumer in the trunk yet; its customers arrive with the deeper chapters of Part 4, where formulas migrate between the inner world's constants, the codes' empty domain, and the ambient carrier.

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

module FOL.Manipulation.Relabelling where

open import Base.Prelude
open import Base.Truth
open import FOL.ZFStructure using ( ZFStructure )
open import FOL.Syntax using
  ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using
  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-¬; δ-⊤; δ-⊥; δ-∀∈; δ-∃∈
  ; Σₙ; σ-Δ₀; σ-Π; σ-∃; Πₙ; π-Δ₀; π-Σ; π-∀ )
import FOL.Semantics
import Cubical.Data.Empty as Empty

Syntax level

The syntax is functorial in its constant domain: a map K → K' pushes through a term or formula, relabelling constants and touching nothing else. One clause per constructor, each doing the obvious thing.

mapTm : ∀ {ℓ ℓ'} {K : Type ℓ} {K' : Type ℓ'} {n}
      → (K → K') → Term K n → Term K' n
mapTm f (con k) = con (f k)
mapTm f (var i) = var i

mapFo : ∀ {ℓ ℓ'} {K : Type ℓ} {K' : Type ℓ'} {n}
      → (K → K') → Formula K n → Formula K' n
mapFo f (t ∈̇ u)  = mapTm f t ∈̇ mapTm f u
mapFo f (t ≐ u)  = mapTm f t ≐ mapTm f u
mapFo f (φ ∧̇ ψ)  = mapFo f φ ∧̇ mapFo f ψ
mapFo f (φ ∨̇ ψ)  = mapFo f φ ∨̇ mapFo f ψ
mapFo f (φ ⇒̇ ψ)  = mapFo f φ ⇒̇ mapFo f ψ
mapFo f (¬̇ φ)    = ¬̇ mapFo f φ
mapFo f ⊤̇        = ⊤̇
mapFo f ⊥̇        = ⊥̇
mapFo f (∃̇ φ)    = ∃̇ mapFo f φ
mapFo f (∀̇ φ)    = ∀̇ mapFo f φ
mapFo f (∀̇∈ t φ) = ∀̇∈ (mapTm f t) (mapFo f φ)
mapFo f (∃̇∈ t φ) = ∃̇∈ (mapTm f t) (mapFo f φ)

Two such maps in a row are one map. The composite is the only thing a chapter that migrates a formula through an intermediate domain ever wants, and proving it where the syntax is defined costs twelve congruences and stops every later chapter from writing its own. Both term cases are refl, because a variable carries no constant and a constant is relabelled by application.

mapTm-comp : ∀ {ℓ ℓ' ℓ''} {K : Type ℓ} {K' : Type ℓ'} {K'' : Type ℓ''} {n}
             (f : K → K') (g : K' → K'') (t : Term K n)
           → mapTm g (mapTm f t) ≡ mapTm (λ k → g (f k)) t
mapTm-comp f g (con k) = refl
mapTm-comp f g (var i) = refl

mapFo-comp : ∀ {ℓ ℓ' ℓ''} {K : Type ℓ} {K' : Type ℓ'} {K'' : Type ℓ''} {n}
             (f : K → K') (g : K' → K'') (φ : Formula K n)
           → mapFo g (mapFo f φ) ≡ mapFo (λ k → g (f k)) φ
mapFo-comp f g (t ∈̇ u)  = cong₂ _∈̇_ (mapTm-comp f g t) (mapTm-comp f g u)
mapFo-comp f g (t ≐ u)  = cong₂ _≐_ (mapTm-comp f g t) (mapTm-comp f g u)
mapFo-comp f g (φ ∧̇ ψ)  = cong₂ _∧̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g (φ ∨̇ ψ)  = cong₂ _∨̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g (φ ⇒̇ ψ)  = cong₂ _⇒̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g (¬̇ φ)    = cong ¬̇_ (mapFo-comp f g φ)
mapFo-comp f g ⊤̇        = refl
mapFo-comp f g ⊥̇        = refl
mapFo-comp f g (∃̇ φ)    = cong ∃̇_ (mapFo-comp f g φ)
mapFo-comp f g (∀̇ φ)    = cong ∀̇_ (mapFo-comp f g φ)
mapFo-comp f g (∀̇∈ t φ) = cong₂ ∀̇∈ (mapTm-comp f g t) (mapFo-comp f g φ)
mapFo-comp f g (∃̇∈ t φ) = cong₂ ∃̇∈ (mapTm-comp f g t) (mapFo-comp f g φ)

The most-travelled instance: entering a constant domain from no constants. The syntax chapter introduced the parameter-free formulas, the data axis with the empty type as constant domain; like sentences they bear no separate name, the type Formula (⊥* {ℓ}) n says it whole. From the empty type anything follows, the library's eliminator Empty.rec* says so, and relabelling along it embeds a parameter-free formula into the syntax over any domain whatsoever.

embed : ∀ {ℓ ℓ'} {K : Type ℓ'} {n} → Formula (⊥* {ℓ}) n → Formula K n
embed = mapFo Empty.rec*

Meaning level

Relabelling constants along f : K → K' and then evaluating under ι is the same as evaluating under ι ∘ f directly; the ∘-marked satisfaction and denotation below are the generic semantics opened at that composite. One structural induction, every case a congruence; the two term cases are even

refl.

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

  open TruthAlgebra 𝕋
  open ZFStructure 𝒮
  open FOL.Semantics 𝕋 𝒮 using ( module At; _^_ )

  module _ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K') (ι : K' → S) where

    open At K' ι using ( _⊨_; ⟦_⟧ )
    open At K (λ k → ι (f k)) using () renaming ( _⊨_ to _⊨∘_ ; ⟦_⟧ to ⟦_⟧∘ )

    ⟦⟧-map : ∀ {n} (t : Term K n) (γ : S ^ n)
           → ⟦ mapTm f t ⟧ γ ≡ ⟦ t ⟧∘ γ
    ⟦⟧-map (con k) γ = refl
    ⟦⟧-map (var i) γ = refl

    ⊨-map : ∀ {n} (φ : Formula K n) (γ : S ^ n)
          → (γ ⊨ mapFo f φ) ≡ (γ ⊨∘ φ)
    ⊨-map (t ∈̇ u)  γ = cong₂ _∈ˢ_ (⟦⟧-map t γ) (⟦⟧-map u γ)
    ⊨-map (t ≐ u)  γ = cong₂ _≈ˢ_ (⟦⟧-map t γ) (⟦⟧-map u γ)
    ⊨-map (φ ∧̇ ψ)  γ = cong₂ _⊓_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map (φ ∨̇ ψ)  γ = cong₂ _⊔_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map (φ ⇒̇ ψ)  γ = cong₂ _⇒_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map (¬̇ φ)    γ = cong ¬_ (⊨-map φ γ)
    ⊨-map ⊤̇        γ = refl
    ⊨-map ⊥̇        γ = refl
    ⊨-map (∃̇ φ)    γ = cong (⋁ S) (funExt (λ x → ⊨-map φ (x ∷ γ)))
    ⊨-map (∀̇ φ)    γ = cong (⋀ S) (funExt (λ x → ⊨-map φ (x ∷ γ)))
    ⊨-map (∀̇∈ t φ) γ = cong (⋀ S) (funExt (λ x →
      cong₂ _⇒_ (cong (x ∈ˢ_) (⟦⟧-map t γ)) (⊨-map φ (x ∷ γ))))
    ⊨-map (∃̇∈ t φ) γ = cong (⋁ S) (funExt (λ x →
      cong₂ _⊓_ (cong (x ∈ˢ_) (⟦⟧-map t γ)) (⊨-map φ (x ∷ γ))))

The corollary the parameter-free formulas were waiting for: entering any constant domain through embed keeps their meaning. The data axis and the working syntax share one semantics; nothing needs proving twice. (The ∅-marked satisfaction reads the empty constant domain through

Empty.rec*.)

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

    open At K ι using ( _⊨_ )
    open At (⊥* {ℓe}) (λ b → ι (Empty.rec* b)) using () renaming ( _⊨_ to _⊨∅_ )

    embed-⊨ : ∀ {n} (φ : Formula (⊥* {ℓe}) n) (γ : S ^ n)
            → (γ ⊨ embed φ) ≡ (γ ⊨∅ φ)
    embed-⊨ = ⊨-map Empty.rec* ι

Levy witness level

Relabelling constants preserves the structure of a formula, so a Levy witness follows along, constructor by constructor. This little lemma is what will let an absoluteness argument carry a Δ₀ witness across a change of constant domain.

mapΔ₀ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
        {n} {φ : Formula K n} → Δ₀ φ → Δ₀ (mapFo f φ)
mapΔ₀ f δ-∈ = δ-∈
mapΔ₀ f δ-≐ = δ-≐
mapΔ₀ f (δ-∧ c d) = δ-∧ (mapΔ₀ f c) (mapΔ₀ f d)
mapΔ₀ f (δ-∨ c d) = δ-∨ (mapΔ₀ f c) (mapΔ₀ f d)
mapΔ₀ f (δ-⇒ c d) = δ-⇒ (mapΔ₀ f c) (mapΔ₀ f d)
mapΔ₀ f (δ-¬ c)   = δ-¬ (mapΔ₀ f c)
mapΔ₀ f δ-⊤ = δ-⊤
mapΔ₀ f δ-⊥ = δ-⊥
mapΔ₀ f (δ-∀∈ c) = δ-∀∈ (mapΔ₀ f c)
mapΔ₀ f (δ-∃∈ c) = δ-∃∈ (mapΔ₀ f c)

The lemma extends to the whole alternating tower by mutual induction, reusing

mapΔ₀ at the leaves.

mutual
  mapΣₙ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
          {k n} {φ : Formula K n} → Σₙ k φ → Σₙ k (mapFo f φ)
  mapΣₙ f (σ-Δ₀ d) = σ-Δ₀ (mapΔ₀ f d)
  mapΣₙ f (σ-Π p)  = σ-Π (mapΠₙ f p)
  mapΣₙ f (σ-∃ s)  = σ-∃ (mapΣₙ f s)

  mapΠₙ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
          {k n} {φ : Formula K n} → Πₙ k φ → Πₙ k (mapFo f φ)
  mapΠₙ f (π-Δ₀ d) = π-Δ₀ (mapΔ₀ f d)
  mapΠₙ f (π-Σ s)  = π-Σ (mapΣₙ f s)
  mapΠₙ f (π-∀ p)  = π-∀ (mapΠₙ f p)

Recap

One map of constant domains, three altitudes of transport: mapFo moves the syntax (with embed as the parameter-free entrance), ⊨-map and embed-⊨ certify that meaning does not move at all, and

mapΔ₀ with its tower carries the Levy witnesses. A formula, its meaning, and its grade travel as one; the chapters that migrate formulas between worlds will lean on exactly that.