---
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: [Base.Prelude, FOL.ZFStructure, FOL.Syntax]
routes: [common-foundations]
translations: [https://bedrock.institute/en/FOL.Semantics.md, https://bedrock.institute/ja/FOL.Semantics.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 语义

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

```agda
{-# 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 本身不含集合论公理，定义语义也不需要任何集合论公理。

```agda
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 ∷ γ` 在最前面加入一个分量，原有分量顺次移到后继位置。

```agda
infixl 30 _^_

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

## 求值与满足

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

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

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

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

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

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

  infix 6 _⊨_

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

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

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

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

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

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

## 小结

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