Semantics

把语法变成含义需要三样东西：被谈论的结构 𝒮、常量的解释，以及给自由变量赋值的环境。第一样连同它取值的真值代数是本章整体的参数；泛型开发按作用域纪律的安排，经抽象的 𝕋 说话。

{-# 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 𝒮

环境

先备一件行头。要对带 n 个自由变量的公式求值，每个变量都需要一个来自载体的取值：一份赋值表，即环境，全书写作 γ。其类型记为 S ^ n，长度为 n 的向量，对齐传统上标记号 $S^n$ (_^_ 读作「幂」)；它只是记号。

infixl 30 _^_

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

求值与满足

剩下那样原料，常量解释 ι : K → S，由内部模块 At 一次固定：日常工作在一个固定的 ι 下进行 (典范情形以载体自身为常量域，ι 取恒等)，偶尔需要跨解释的引理，如本章末那几条，则以限定名访问。

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

两个记号都直接来自教科书：⟦_⟧ 读作「取值」，_⊨_ 读作「满足」，环境在左，写 γ ⊨ φ。词项求值要么问 ι (常量)，要么查环境 (变量)。满足关系是对十二个构造子的一次结构递归。

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

  infix 6 _⊨_

  _⊨_ : ∀ {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 ∷ γ) ⊨ φ))

看各子句的右端：每一条都恰好是真值代数的对应运算，作用在子公式的含义上。对象合取的含义就是宿主合取，对象量词的含义就是载体上的 ⋀ 与 ⋁，中间没有任何翻译层。于是带 n 个自由变量的公式，含义是一个 S ^ n → Ω 型的函数，与宿主语言直接写出的谓词刻意同形；两者之间的桥编在书末，而这份忠实性将让那座桥的每一块板都归于一行同余。

两条有界子句值得再看一眼：它们的量化被钉在 ⟦ t ⟧ γ 的成员上。语法章许诺过，全部量词皆有界的公式在结构之间表现驯良；那份驯良物理上就住在这两行里，后面的章节将一次次回到这里。

小结

含义就是结构递归：⟦_⟧ 给词项取值，γ ⊨ φ 落进真值代数，每条子句恰是对应的代数运算，分毫不多。带 n 个自由变量的公式，含义是 S ^ n → Ω 型函数，与宿主谓词同形。公式与谓词之间尚缺一座桥；它编在书末，静候需求转入量产的那一天。