语义

固定命题值结构 𝒮 : ZFStructureₕ ℓ。以它的载体元素为讨论对象，以它的两个关系解释相等和成员关系。

module FOL.Semantics {ℓ} (𝒮 : ZFStructureₕ ℓ) where

我们已经有了写出陈述的语言，也有了解释这些陈述所需的结构。本章把二者接起来：先指定名字和带编号的位置各自指向什么对象，再把每条公式解释成关于这些对象的命题。赋予陈述含义，与判定它是否成立，是不同的两步；最后一节再说明排中律在判定中起什么作用。

打开已固定的结构，便可直接使用载体 S，以及关系 ≈ˢ 和 ∈ˢ。这里不假设任何集合论公理。

open ZFStructure 𝒮

环境

变元位置只告诉我们从哪里取值，并不指定具体的对象。为语境中的每个可用位置指定一个载体元素，就得到一个环境。对于长度为 n 的语境，我们用向量 γ : Vec S n 记录这份赋值；其中位置 i : Fin n 处的分量，就是相应变元的取值。

例如，在环境 a ∷ b ∷ [] 中，0 号位置存放 a，1 号位置存放 b。一条公式可以只使用其中一个位置，也可以多次引用同一个位置，或两个位置都不用。因此，环境记录的是解释公式时可用的取值，并不是为变元的每次出现各存一个值；它的长度与语境长度一致，而不是变元出现的次数。

解释词项与公式

常元名也需要指定取值。函数 ι : K → S 为每个名字指定一个载体元素，称为常元解释。它与变元取值的区别在于：量词扩展环境时，常元的取值保持不变。子模块 At 固定 K : Type ℓc 和 ι : K → S，供下面的定义共同使用。

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

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

infix  _⊨_
_⊨_ : ∀ {n} → Vec S n → Formula K n → hProp ℓ

γ ⊨ t ∈̇ u = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ
γ ⊨ t ≐ u = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ

γ ⊨ φ ∧̇ ψ = (γ ⊨ φ) ⊓ (γ ⊨ ψ)
γ ⊨ φ ∨̇ ψ = (γ ⊨ φ) ⊔ (γ ⊨ ψ)
γ ⊨ φ ⇒̇ ψ = (γ ⊨ φ) ⇒ (γ ⊨ ψ)

γ ⊨ ⊥̇   = ⊥
γ ⊨ ∃̇ φ = ∃[ x ∶ S ] x ∷ γ ⊨ φ
γ ⊨ ∀̇ φ = ∀[ x ∶ S ] x ∷ γ ⊨ φ

γ ⊨ ∀̇∈ t φ = ∀[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ (x ∷ γ ⊨ φ)
γ ⊨ ∃̇∈ t φ = ∃[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ (x ∷ γ ⊨ φ)

这些子句为每条公式赋予含义，并没有判定它的真假。相等子句采用给定的关系 ≈ˢ，不一定是 Agda 的路径相等。析取与存在量化使用命题截断，因此一般不能从它们的证明中取出具体的分支或见证作为数据。以上定义都不需要排中律。

读懂量化公式

量词在公式体中增加的位置，现在有了取值。以外层环境 γ = a ∷ [] 为例，在最前面加入 x 后，得到 x ∷ a ∷ []：原来的值保留不变，只是编号向后挪了一位。下图沿用《对象语言》的位置约定，但这次由环境实际提供各处的值。

取一个具体的公式体 var zero ∈̇ var (suc zero)，它在扩展环境下表达的就是 x ∈ˢ a。在前面加上 ∀̇，就表示每个载体元素都属于 a；加上 ∃̇，就表示存在一个属于 a 的载体元素。这里没有断言其中哪条成立，只是说明每条公式表达了什么命题。

有界量词的界限仍按原环境解释。在 ∀̇∈ (var zero) φ 中，界限指的是 a，而 φ 内的首位指的是 x。这就是代码用原环境求界限值的原因。至于否定与真，无须另写子句：它们在对象语言中的定义已经展开为蕴涵与假。

由公式呈现的谓词

到这里，我们都是从公式出发，得到它所表达的命题。反过来，也可以先给定谓词 predicate : A → hProp ℓ，再提供它的一份公式呈现。这里的 A 为要讨论的各个情形提供指标，不必就是载体。我们固定同一条公式，为每个 a : A 提供相应的环境。

定义 (FormulaPredicate) 给定 A、K、ι 与 predicate。它的一份公式呈现由以下数据组成：元数、该元数上的公式、每个指标对应的环境，以及公式的含义逐点等于给定谓词的证明。构造子记作 presented。

record FormulaPredicate {ℓa ℓc} (A : Type ℓa) (K : Type ℓc)
                        (ι : K → S) (predicate : A → hProp ℓ)
    : Type (ℓ-max ℓa (ℓ-max ℓc (ℓ-suc ℓ))) where
  constructor presented

下面四个字段依次记录这些数据。元数 arity 与前面的下标 n 一样，表示可用变元位置的数量。reading 中的局部模块名 I 指定解释 At K ι；因此，environment a I.⊨ formula 就是公式在 a 所对应环境下的含义。

  field
    arity       : ℕ
    formula     : Formula K arity
    environment : A → Vec S arity
    reading     : (a : A) → let module I = At K ι in predicate a ≡ (environment a I.⊨ formula)

例如，固定 a : S，考虑谓词 λ x → x ∈ˢ a。可以用公式 var zero ∈̇ var (suc zero) 呈现它，并为每个 x 配上环境 x ∷ a ∷ []。谓词只有一个实参，公式的元数却是二：环境同时提供变化的实参与固定的对象。公式求值后直接得到原谓词，因此 reading 可用 refl 证明。

待呈现的谓词与常元解释是参数，不是额外的字段。字段 reading 给出两个 hProp ℓ 值之间的路径；沿这条路径，可以把给定谓词的证明转换为满足关系的证明，也可以反向转换。公式与环境都不要求唯一。

排中律下的判定

解释一条公式，得到的是命题，并不会自动得到它的证明或反驳。不过，若给定 lem : LEM ℓ，就能对这个命题应用排中律。这项假设用在此处，而不是前面的语义定义中。

引理 (decideSatisfaction) 给定常元解释、环境与公式，LEM ℓ 给出相应满足命题的判定。

证明 用 At 得到该命题，再应用 lem。把公式与环境保留为实参，就明确记录了判定的对象。

decideSatisfaction : ∀ {ℓc n} {K : Type ℓc} (ι : K → S)
                   → LEM ℓ → (γ : Vec S n) → (φ : Formula K n)
                   → let module I = At K ι in Dec ⟨ γ I.⊨ φ ⟩
decideSatisfaction ι lem γ φ = lem (γ I.⊨ φ)
  where module I = At _ ι

两个原子情形让这种对应更具体。它们都不用常元名，因此取空常元域 ⊥* {ℓ}，用空类型的消去函数作为解释。环境 x ∷ y ∷ [] 将两个对象放在各自的位置。

推论 (decideMembership) LEM ℓ 可判定任意两个载体元素之间的成员关系。

证明 将引理应用于成员关系原子公式。两个变元分别求值得到 x 和 y，所以公式的含义恰好是 x ∈ˢ y。

decideMembership : LEM ℓ → (x y : S) → Dec ⟨ x ∈ˢ y ⟩
decideMembership lem x y =
  decideSatisfaction {K = ⊥* {ℓ}} (⊥*-rec {A = S}) lem
    (x ∷ y ∷ []) (var zero ∈̇ var (suc zero))

推论 (decideEquality) LEM ℓ 可判定任意两个载体元素之间由结构指定的相等关系。

证明 沿用相同的常元域与环境，改用相等原子公式。其含义是 x ≈ˢ y，而不是关于 Agda 路径相等的断言。

decideEquality : LEM ℓ → (x y : S) → Dec ⟨ x ≈ˢ y ⟩
decideEquality lem x y =
  decideSatisfaction {K = ⊥* {ℓ}} (⊥*-rec {A = S}) lem
    (x ∷ y ∷ []) (var zero ≐ var (suc zero))

小结

常元解释与环境确定词项的取值，结构中的关系与命题运算再确定公式的含义。量词改变新加入的首位取值，同时保留外层已有的取值。FormulaPredicate 记录给定谓词的一份公式呈现；排中律则进一步提供满足命题的判定。定义含义本身，既不需要排中律，也不需要集合论公理。下一章回到公式的写法，按量词的组成方式给公式分类。