Semantics

Three things turn syntax into meaning: a structure 𝒮 to be talked about, an interpretation of the constants, and an environment giving values to the free variables. The first is a parameter of this whole chapter, along with the truth algebra it is valued in; the generic development speaks through the abstract 𝕋, as the scope discipline prescribes.

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

open import Base.Prelude
open import Base.Truth
open import FOL.ZFStructure using ( ZFStructure )

module FOL.Semantics {ℓ ℓ'} (𝕋 : TruthAlgebra ℓ ℓ') (𝒮 : ZFStructure 𝕋) where

open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

open TruthAlgebra 𝕋
open ZFStructure 𝒮

Environments

One piece of kit first. To evaluate a formula with n free variables, each variable needs a value from the carrier: an assignment, or environment, written γ throughout the book. The book's notation for its type is S ^ n, a vector of length n, matching the traditional superscript $S^n$ (_^_ reads "power"); it is nothing but notation.

infixl  _^_

_^_ : ∀ {ℓ''} → Type ℓ'' → ℕ → Type ℓ''
A ^ n = Vec A n

Evaluation and satisfaction

The remaining ingredient, the constant interpretation ι : K → S, is fixed once by an inner module At: everyday work happens under one fixed ι (the canonical case takes the carrier itself as constant domain, with ι the identity), while the occasional lemma that crosses interpretations, such as those at the end of this chapter, uses qualified names.

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

Two readings, both straight from the textbook: ⟦_⟧ reads "the value of", and _⊨_ reads "satisfies", with the environment on the left, γ ⊨ φ. Evaluation of a term either asks ι (a constant) or looks up the environment (a variable). Satisfaction is a single structural recursion over the twelve constructors.

  ⟦_⟧ : ∀ {n} → Term K n → S ^ n → S
  ⟦ con k ⟧ γ = ι k
  ⟦ var i ⟧ γ = lookup i γ

  infix  _⊨_

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

Look at the right-hand sides: each is exactly the truth algebra's corresponding operation, applied to the meanings of the subformulas. Object conjunction means host conjunction, the object quantifiers mean ⋀ and ⋁ over the carrier; there is no translation layer in between. A formula with n free variables thus means a function S ^ n → Ω, deliberately the same shape as a predicate written directly in the host language; a bridge between the two is catalogued at the book's tail, and this faithfulness is what will make every plank of that bridge a one-line congruence.

The two bounded clauses deserve a second look: their quantification is pinned to the members of ⟦ t ⟧ γ. The syntax chapter promised that formulas whose quantifiers are all bounded behave tamely across structures; that behaviour lives physically in these two lines, and later chapters return to them again and again.

Recap

Meaning is structural recursion: ⟦_⟧ evaluates terms, γ ⊨ φ lands in the truth algebra, and each clause is the corresponding algebra operation, nothing more. Formulas with n free variables mean functions S ^ n → Ω, the same shape as host predicates. The one bridge still missing between formulas and predicates is catalogued at the book's tail, waiting for the day the demand turns industrial.