语义

对象语言由符号与组合规则构成，而这些符号至今没有任何指称。要让 ∈̇ 或 _≐_ 成为可读的东西，需要供给什么？结构决定变量在什么范围内取值、两条原子谓词在那里指什么；解释为每个常元符号指定其载体元素；环境为每个可用的变量位置指定当前取值。这些数据一经固定，结构递归便为每个词项指定一个载体元素，为每条公式指定一个命题。全章系于一个区分，即符号与指称之分：记号 ∈̇ 属于语法，它最终意味的是结构的关系 ∈ˢ，二者居于不同的层。

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

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

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

固定一个结构 𝒮 : ZFStructure ℓ，即上一章的模型论数据：一个作为 h-集合的载体 S，加上等词 ≈ˢ 与隶属 ∈ˢ，二者都把两个载体元素送到 hProp ℓ 中的一个命题。每条公式的解释都将落在这个命题宇宙之中，于是关于集合的陈述实实在在地成为一个命题，其元素就是证明。除了这些字段之外，不再使用结构的其他内容。ZFStructure 这个 record 本身不含集合论公理，定义语义也不需要任何集合论公理。

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

open ZFStructure 𝒮

record 的字段如今以自己的名字进入作用域：S 是载体，∈ˢ 与 ≈ˢ 是两个关系，于是 x ∈ˢ y 读作结构关于 x、y 的隶属命题。对象语言的构造子也在作用域内，每一类符号在语义一侧都有明确的对应物。常元符号需要一个载体元素，由从常元域到 S 的函数一次固定。变量位置需要一个可随使用变化的取值，由环境供给。原子公式需要两个关系之一。联结词与量词则完全不需要集合论：《基础词汇》中命题上的逻辑运算 ⊓、⊔、⇒、∀[ x ] P x、∃[ x ] P x 在此就位。解释遵循组合原则：词项或公式的意义由它的构造子及其直接组成部分的意义共同确定。

环境

元数为 n 的词项可以引用位置 0 到 n - 1，环境 γ 为其中每个位置指派一个载体元素。S ^ 2 中的环境有两个分量，可供 var zero 与 var (suc zero) 读取；某个具体的词项或公式可以只用其一、两者都用，或都不用。因此长度 n 界定的是可用位置的范围，而不是实际出现的变量的个数。绑定遵循同一原理：量词考虑来自载体的一个候选元素时，环境把该元素加在最前面从而得到扩展，公式体在位置 zero 处读取它。

环境的类型记作 S ^ n，对应传统的上标 $S^n$；_^_ 读作「幂」，纯粹是记号。它定义为 Vec A n，即长度写进类型的有序向量。这里依赖类型真正发挥了作用：公式的元数与环境的长度不可能不一致，不匹配时连合法的组合都构不成。运算 lookup 返回 Fin n 中某位置上的分量，x ∷ γ 在最前面加入一个分量，原有分量顺次移到后继位置。

infixl  _^_

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

求值与满足

两个判断承载语义。以 ⟦ t ⟧ γ 表示词项 t 在环境 γ 下指称的载体元素，以 γ ⊨ φ 表示陈述公式 φ 在 γ 下成立的那个命题。二者都相对于一个固定的常元解释 ι : K → S 而定义：常元从 ι 取值，变量则继续随 γ 变化。量词一出现，这种分离就显出作用：绑定改变变量的取值，而常元符号的指称不动。

解释与环境回答的是两个不同的问题。常元 con k 指称 ι k，与供给哪个环境无关；变量 var i 指称 lookup i γ，与固定哪个解释无关。因此，环境只在变量这一情形参与词项求值，常元符号的含义始终由 ι 固定。这两个情形穷尽了词项求值。

固定常元域 K 与解释 ι : K → S。在这个固定解释下，词项求值把词项和环境送到 S 的元素，满足关系则把公式和环境送到命题。满足关系按公式结构递归定义：原子式使用结构的两个关系，联结词使用《基础词汇》中的命题运算，假使用空命题，量词遍及载体。在有界量词中，界限的指称决定被量化元素须满足的成员条件。

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

两样定义承载本节，其类型说明了它们是什么。求值 ⟦_⟧ 把词项与环境送到一个载体元素。满足 _⊨_ 把环境与公式送到 hProp ℓ 中的一个命题，即任意两个元素都相等的类型；这类类型的元素就是证明。因此满足不是单纯的判定结果，而是一个命题：定义将为每条公式与每个环境算出所指的究竟是哪个命题。元数 n 出现在两个类型之中，所以只有长度相符的环境才能施加于公式：先前关于公式与环境的规矩，如今由类型本身来执行。

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

  infix  _⊨_

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

原子的隶属先对两个词项求值，再把它们交给结构：该断言成为结构关于两个指称的隶属命题。相等原子对 ≈ˢ 如法炮制。在此，带点的符号终于有了含义：∈̇ 被读作 ∈ˢ，比语法低一层。三条命题子句则完全留在宿主一侧：合取由 ⊓ 解释，析取由 ⊔ 解释，蕴涵由 ⇒ 解释，每个都是命题上的运算。合取的证明是一对证明；蕴涵的证明是一个函数，把前件的证明变成后件的证明。这三条子句完全不用集合论，它们是宿主的命题逻辑，施于子公式所指的命题。

  γ ⊨ (t ∈̇ u)  = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ
  γ ⊨ (t ≐ u)  = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ
  γ ⊨ (φ ∧̇ ψ)  = (γ ⊨ φ) ⊓ (γ ⊨ ψ)
  γ ⊨ (φ ∨̇ ψ)  = (γ ⊨ φ) ⊔ (γ ⊨ ψ)
  γ ⊨ (φ ⇒̇ ψ)  = (γ ⊨ φ) ⇒ (γ ⊨ ψ)

假不需要任何环境：⊥̇ 被读作空命题 ⊥。量词是载体最终登场之处。无界的 ∃̇ φ 表达对载体的存在量化：即 S 的某个元素 x 使公式体在扩展环境 x ∷ γ 下成立的那个命题。它的对偶 ∀̇ φ 表达全称量化，其证明是一个函数，为每个 x : S 指派公式体在 x ∷ γ 下的证明。在公式体内部，位置 zero 持有候选元素 x，而 γ 的各分量已移到后继位置；外层公式中自由的变量从尾部读取。由命题截断，存在量化只记录这样的元素存在，并不把该元素作为数据携带。

有界形式增加一个成分：属于界限指称的成员资格。∀̇∈ t φ 要求属于 ⟦ t ⟧ γ 蕴涵公式体，于是 ⟦ t ⟧ γ 的每个成员都满足 φ；∃̇∈ t φ 寻求一个既是成员又满足公式体的元素。注意各环境用在哪里：界限 t 位于新绑定之外，在原有的 γ 中求值；只有公式体面对扩展 x ∷ γ。这两条子句正是「t 的每个成员都满足 φ」与「t 的某个成员满足 φ」这两种读法的语义内容。

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

小结

语义按组成方式给出。词项指称一个载体元素，由常元解释与环境共同确定。元数为 n 的公式确定一个 S ^ n → hProp ℓ 型的函数，无论它是否用尽每个可用位置。原子式查询结构的两个关系；联结词应用宿主的命题运算；量词让一个置于最前的新位置遍及载体，有界形式则在扩展之外检验属于界限指称的成员资格，在扩展之内解释公式体。每条子句都是结构递归的一步。整个构造使用载体 S 以及关系 ∈ˢ、≈ˢ，不使用证明 isSetS，也不使用任何集合论公理。