---
title: "语义"
module: FOL.Semantics
lang: zh
site: "Bedrock"
description: "语义"
stage: "一阶逻辑"
reading_order: 8
canonical: https://bedrock.institute/zh/FOL.Semantics.html
html: FOL.Semantics.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Semantics.lagda.md
prerequisites: [FOL.ZFStructure, Base.Prelude, Base.Classical, FOL.Syntax]
routes: [common-foundations]
translations: [https://bedrock.institute/en/FOL.Semantics.md, https://bedrock.institute/ja/FOL.Semantics.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---
```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```
# 语义
```agda
open import FOL.ZFStructure using ( ZFStructure; ZFStructureₕ )
```
固定命题值结构 `𝒮 : ZFStructureₕ ℓ`。以它的载体元素为讨论对象，以它的两个关系解释相等和成员关系。
```agda
module FOL.Semantics {ℓ} (𝒮 : ZFStructureₕ ℓ) where
```
```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
open import FOL.Syntax using
( Term; con; var
; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
```
我们已经有了写出陈述的语言，也有了解释这些陈述所需的结构。本章把二者接起来：先指定名字和带编号的位置各自指向什么对象，再把每条公式解释成关于这些对象的命题。赋予陈述含义，与判定它是否成立，是不同的两步；最后一节再说明排中律在判定中起什么作用。
打开已固定的结构，便可直接使用载体 `S`，以及关系 `≈ˢ` 和 `∈ˢ`。这里不假设任何集合论公理。
```agda
open ZFStructure 𝒮
```
## 环境
变元位置只告诉我们从哪里取值，并不指定具体的对象。为语境中的每个可用位置指定一个载体元素，就得到一个**环境**。对于长度为 `n` 的语境，我们用向量 `γ : Vec S n` 记录这份赋值；其中位置 `i : Fin n` 处的分量，就是相应变元的取值。
例如，在环境 `a ∷ b ∷ []` 中，`0` 号位置存放 `a`，`1` 号位置存放 `b`。一条公式可以只使用其中一个位置，也可以多次引用同一个位置，或两个位置都不用。因此，环境记录的是解释公式时可用的取值，并不是为变元的每次出现各存一个值；它的长度与语境长度一致，而不是变元出现的次数。
## 解释词项与公式
常元名也需要指定取值。函数 `ι : K → S` 为每个名字指定一个载体元素，称为**常元解释**。它与变元取值的区别在于：量词扩展环境时，常元的取值保持不变。子模块 `At` 固定 `K : Type ℓc` 和 `ι : K → S`，供下面的定义共同使用。
```agda
module At {ℓc} (K : Type ℓc) (ι : K → S) where
```
### 词项求值
**定义** (`⟦_⟧`) 词项求值将词项 `t : Term K n` 与环境 `γ : Vec S n` 映到载体元素 `⟦ t ⟧ γ : S`，读作「`t` 在 `γ` 下的值」。常元从 `ι` 取值，变元从 `γ` 取值。
```agda
⟦_⟧ : ∀ {n} → Term K n → Vec S n → S
⟦ con k ⟧ γ = ι k
⟦ var i ⟧ γ = lookup i γ
```
共同的下标 `n` 要求环境长度恰好与词项所需的语境长度一致。若常元域就是载体本身，可以取 `ι = id`，让每个元素以自身为名字；若常元域为空，就不可能出现常元情形，但变元仍从环境取值。这两种选择都与语境长度无关。
### 满足关系
**定义** (`_⊨_`) 满足关系将环境 `γ : Vec S n` 与公式 `φ : Formula K n` 映到命题 `γ ⊨ φ : hProp ℓ`，读作「`γ` 满足 `φ`」。`⟨ γ ⊨ φ ⟩` 的元素就是该公式在此取值下成立的证明。按公式的构造方式递归定义这个命题如下。
```agda
infix 4 _⊨_
_⊨_ : ∀ {n} → Vec S n → Formula K n → hProp ℓ
```
对于原子公式，先求出两个词项的值，再应用结构中的相应关系：`∈̇` 对应 `∈ˢ`，`≐` 对应 `≈ˢ`。
```agda
γ ⊨ t ∈̇ u = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ
γ ⊨ t ≐ u = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ
```
对于合取、析取和蕴涵，在同一环境下解释两个子公式，再用《基础词汇》中相应的命题运算组合所得结果。
```agda
γ ⊨ φ ∧̇ ψ = (γ ⊨ φ) ⊓ (γ ⊨ ψ)
γ ⊨ φ ∨̇ ψ = (γ ⊨ φ) ⊔ (γ ⊨ ψ)
γ ⊨ φ ⇒̇ ψ = (γ ⊨ φ) ⇒ (γ ⊨ ψ)
```
假始终解释为 `⊥`。无界量词遍历 `x : S`，把当前的值加到环境最前面，在 `x ∷ γ` 下解释公式体。存在量词断言这样的取值仅仅存在；全称量词要求每个取值都使公式体成立。
```agda
γ ⊨ ⊥̇ = ⊥
γ ⊨ ∃̇ φ = ∃[ x ∶ S ] x ∷ γ ⊨ φ
γ ⊨ ∀̇ φ = ∀[ x ∶ S ] x ∷ γ ⊨ φ
```
对于有界量词，先在原环境下求出界限词项 `t` 的值。全称情形要求：属于该值就蕴含公式体成立；存在情形要求：成员关系与公式体同时成立。只有公式体使用扩展后的环境。
```agda
γ ⊨ ∀̇∈ t φ = ∀[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ (x ∷ γ ⊨ φ)
γ ⊨ ∃̇∈ t φ = ∃[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ (x ∷ γ ⊨ φ)
```
这些子句为每条公式赋予含义，并没有判定它的真假。相等子句采用给定的关系 `≈ˢ`，不一定是 Agda 的路径相等。析取与存在量化使用命题截断，因此一般不能从它们的证明中取出具体的分支或见证作为数据。以上定义都不需要排中律。
### 读懂量化公式
量词在公式体中增加的位置，现在有了取值。以外层环境 `γ = a ∷ []` 为例，在最前面加入 `x` 后，得到 `x ∷ a ∷ []`：原来的值保留不变，只是编号向后挪了一位。下图沿用《对象语言》的位置约定，但这次由环境实际提供各处的值。
$\gamma$
$x\mathbin{∷}\gamma$
$+$
$a$
$x$
$a$
$0$
$0$
$1$
扩展后的环境把量化取值放在 `0` 号位置，把原有取值保留在 `1` 号位置
取一个具体的公式体 `var zero ∈̇ var (suc zero)`，它在扩展环境下表达的就是 `x ∈ˢ a`。在前面加上 `∀̇`，就表示每个载体元素都属于 `a`；加上 `∃̇`，就表示存在一个属于 `a` 的载体元素。这里没有断言其中哪条成立，只是说明每条公式表达了什么命题。
有界量词的界限仍按原环境解释。在 `∀̇∈ (var zero) φ` 中，界限指的是 `a`，而 `φ` 内的首位指的是 `x`。这就是代码用原环境求界限值的原因。至于否定与真，无须另写子句：它们在对象语言中的定义已经展开为蕴涵与假。
## 由公式呈现的谓词
到这里，我们都是从公式出发，得到它所表达的命题。反过来，也可以先给定谓词 `predicate : A → hProp ℓ`，再提供它的一份公式呈现。这里的 `A` 为要讨论的各个情形提供指标，不必就是载体。我们固定同一条公式，为每个 `a : A` 提供相应的环境。
**定义** (`FormulaPredicate`) 给定 `A`、`K`、`ι` 与 `predicate`。它的一份公式呈现由以下数据组成：元数、该元数上的公式、每个指标对应的环境，以及公式的含义逐点等于给定谓词的证明。构造子记作 `presented`。
```agda
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` 所对应环境下的含义。
```agda
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`。把公式与环境保留为实参，就明确记录了判定的对象。
```agda
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`。
```agda
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 路径相等的断言。
```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` 记录给定谓词的一份公式呈现；排中律则进一步提供满足命题的判定。定义含义本身，既不需要排中律，也不需要集合论公理。下一章回到公式的写法，按量词的组成方式给公式分类。