Relativization

The textbook's other classic move: relativize a formula to a bound, tightening every unbounded quantifier ∃̇, ∀̇ into its bounded counterpart. Two facts make the operation valuable here. The result is always Δ₀, the Δ₀ witness included, so the absoluteness chapter's theorem applies to it; and when the bound denotes a transitive set, satisfaction of the relativized formula in the big world coincides with satisfaction of the original in the small one. Between them, "truth inside a set" becomes a Δ₀ matter of the ambient world.

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

module FOL.Manipulation.Relativize where

open import Base.Prelude
open import Base.Truth
open import FOL.ZFStructure using ( ZFStructure )
open import FOL.Syntax using
  ( con; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using
  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-¬; δ-⊤; δ-⊥; δ-∀∈; δ-∃∈ )
import FOL.Semantics

The operator

The bound enters as a constant c of the domain: con c is a term at every arity, so pushing the operator under binders needs no variable bookkeeping whatsoever. Atoms and bounded quantifiers pass through untouched; only the two unbounded constructors change clothes. A bound that is a proper class has no constant to stand on, and lies beyond this operator's range; Part 4 meets that wall head-on.

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

Every unbounded quantifier became bounded and nothing else changed, so the result has no ∃̇/∀̇ constructors at all: the Δ₀ witness assembles constructor by constructor.

Δ₀-relativize : ∀ {ℓ} {K : Type ℓ} (c : K) {n} (φ : Formula K n) → Δ₀ (relativize c φ)
Δ₀-relativize c (t ∈̇ u)  = δ-∈
Δ₀-relativize c (t ≐ u)  = δ-≐
Δ₀-relativize c (φ ∧̇ ψ)  = δ-∧ (Δ₀-relativize c φ) (Δ₀-relativize c ψ)
Δ₀-relativize c (φ ∨̇ ψ)  = δ-∨ (Δ₀-relativize c φ) (Δ₀-relativize c ψ)
Δ₀-relativize c (φ ⇒̇ ψ)  = δ-⇒ (Δ₀-relativize c φ) (Δ₀-relativize c ψ)
Δ₀-relativize c (¬̇ φ)    = δ-¬ (Δ₀-relativize c φ)
Δ₀-relativize c ⊤̇        = δ-⊤
Δ₀-relativize c ⊥̇        = δ-⊥
Δ₀-relativize c (∃̇ φ)    = δ-∃∈ (Δ₀-relativize c φ)
Δ₀-relativize c (∀̇ φ)    = δ-∀∈ (Δ₀-relativize c φ)
Δ₀-relativize c (∀̇∈ t φ) = δ-∀∈ (Δ₀-relativize c φ)
Δ₀-relativize c (∃̇∈ t φ) = δ-∃∈ (Δ₀-relativize c φ)

Correctness

What should relativization mean? Fix a structure, an interpretation, and let A be the bound's value. The intended reading of "φ relativized" is: evaluate φ as usual, except that both unbounded quantifiers range over members of A only. That reading is itself a semantics, a companion to the standard one differing in exactly two clauses.

module Correct {ℓ ℓ'} (𝕋 : TruthAlgebra ℓ ℓ') (𝒮 : ZFStructure 𝕋)
               {ℓc} {K : Type ℓc} (ι : K → ZFStructure.S 𝒮) (c : K) where

  open TruthAlgebra 𝕋
  open ZFStructure 𝒮
  open module Sem = FOL.Semantics 𝕋 𝒮 using ( module At; _^_ )
  open At K ι using ( _⊨_; ⟦_⟧ )

  A : S
  A = ι c

  infix  _⊨ᴬ_
  _⊨ᴬ_ : ∀ {n} → S ^ n → Formula K n → Ω
  γ ⊨ᴬ (t ∈̇ u)  = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ
  γ ⊨ᴬ (t ≐ u)  = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ
  γ ⊨ᴬ (φ ∧̇ ψ)  = (γ ⊨ᴬ φ) ⊓ (γ ⊨ᴬ ψ)
  γ ⊨ᴬ (φ ∨̇ ψ)  = (γ ⊨ᴬ φ) ⊔ (γ ⊨ᴬ ψ)
  γ ⊨ᴬ (φ ⇒̇ ψ)  = (γ ⊨ᴬ φ) ⇒ (γ ⊨ᴬ ψ)
  γ ⊨ᴬ (¬̇ φ)    = ¬ (γ ⊨ᴬ φ)
  γ ⊨ᴬ ⊤̇        = ⊤
  γ ⊨ᴬ ⊥̇        = ⊥
  γ ⊨ᴬ (∃̇ φ)    = ⋁ S (λ x → (x ∈ˢ A) ⊓ ((x ∷ γ) ⊨ᴬ φ))
  γ ⊨ᴬ (∀̇ φ)    = ⋀ S (λ x → (x ∈ˢ A) ⇒ ((x ∷ γ) ⊨ᴬ φ))
  γ ⊨ᴬ (∀̇∈ t φ) = ⋀ S (λ x → (x ∈ˢ ⟦ t ⟧ γ) ⇒ ((x ∷ γ) ⊨ᴬ φ))
  γ ⊨ᴬ (∃̇∈ t φ) = ⋁ S (λ x → (x ∈ˢ ⟦ t ⟧ γ) ⊓ ((x ∷ γ) ⊨ᴬ φ))

Correctness is then one structural induction: the standard meaning of relativize c φ equals the A-bounded meaning of φ. The atoms are

refl; the two clauses where the operator actually works are where the standard semantics of ∃̇∈ (con c) _ unfolds, by computation, to exactly the companion's clause, since ⟦ con c ⟧ γ is A; everything else is congruence.

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

Recap

relativize tightens the unbounded quantifiers to a constant bound,

Δ₀-relativize certifies the result, and relativize-correct pins its meaning to the bounded reading. With this, Part 1 closes: the object language, its structures and semantics, the variable calculus, representations with their certificate algebra, the Levy hierarchy, absoluteness, and relativization. Every later part of the book speaks through this toolkit; next, the axioms of set theory.