--- title: "对象语言" module: FOL.Syntax lang: zh site: "Bedrock" description: "对象语言" stage: "一阶逻辑" reading_order: 6 canonical: https://bedrock.institute/zh/FOL.Syntax.html html: FOL.Syntax.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Syntax.lagda.md prerequisites: [Base.Prelude] routes: [common-foundations] translations: [https://bedrock.institute/en/FOL.Syntax.md, https://bedrock.institute/ja/FOL.Syntax.md] agent_guide: https://bedrock.institute/llms.txt license: "CC-BY-NC-SA-4.0" --- ```agda {-# OPTIONS --cubical --safe --guardedness #-} module FOL.Syntax where ``` # 对象语言 ```agda open import Base.Prelude ``` 通常，写下关于集合的陈述后，我们会问它是否成立。本章暂且不问真假，先看陈述怎样写成、又怎样组合。为此，我们把陈述的写法本身当作数学对象，构造一门**对象语言**。 我们先规定怎样指代对象，再用这些写法组成陈述，最后加入「对每个对象」和「存在某个对象」的说法。Agda 代码会逐步划定哪些表达式可以写出。至于它们指什么、陈述是否成立，留待后文再谈。 下面的定义有些取舍乍看可能不太自然：为什么要预先备好对象的名字，又为什么用数字去标记那些可以填入对象的位置？为什么先规定写法、后解释含义？为什么有些逻辑记号作为基本形式，有些则由它们定义出来？这些问题值得带着往下读，不必在本章急于解答。对象语言并没有数学上唯一的标准定义：许多常见方案虽然写法不同，却可以证明在表达能力上大体相当，只是使用起来各有便利。本书采用一种较成熟的方案，并针对后文的集合论研究，在这些便利之间作出我们认为最合适的平衡。随着后文解释和使用这些表达式，具体取舍的理由也会逐渐明朗。 ## 词项 要写「一个对象属于另一个对象」，先得有办法指代这两个对象。可以预先给对象取名，也可以留下带编号的位置，等使用表达式时再指定对象。这样指代单个对象的表达式叫作**词项**。 先把预定的名字收进类型 `K`：其中的元素叫作**常元名**，`K` 叫作**常元域**。再用自然数 `n` 表示当前有多少个带编号的位置；这些位置合起来是**语境**，每个位置是一个**变元位置**。《基础词汇》引入的 `Fin n` 正好给出从 `0` 起、到 `n` 的前一个数为止的全部位置。`Term K n` 可以记录这两种指代方式，但尚未规定名字和位置究竟指什么。 **定义** (`Term`) 给定宇宙层级 `ℓ`、类型 `K : Type ℓ` 和自然数 `n : ℕ`，定义归纳类型 `Term K n : Type ℓ`。 ```agda data Term {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where ``` 每个 `k : K` 确定一个词项 `con k : Term K n`；每个 `i : Fin n` 确定一个词项 `var i : Term K n`。 ```agda con : K → Term K n var : Fin n → Term K n ``` 这两个构造子形成的是指代对象的写法，而不是对象本身。给定名字 `k : K`，可以写出词项 `con k`；给定位置 `i : Fin n`，可以写出词项 `var i`。若语境长度为二，可用位置只有 `0` 和 `1`，没有 `2`。不过，`con` 形成的词项不占用任何位置，仍可属于 `Term K 2`。下文用 `t`、`u` 表示词项，用 `i`、`j` 表示位置。 ## 公式 有了词项，就能写出关于对象的陈述。这种书面陈述叫作**公式**，下文用 `φ`、`ψ`、`θ` 表示。最简单的公式由两个词项写成，形如「前者属于后者」或「两者相等」。这类公式叫作**原子公式**。在此基础上，还能写「并且」「或者」「如果……那么……」，以及下文要介绍的「每个」「某个」。 写公式时常省略括号，因此要先约定各记号如何结合。成员关系和相等结合得最紧，其次是稍后定义的「非」，再是「并且」「或者」，最后是「如果……那么……」。最后一种向右结合，所以 `φ ⇒̇ ψ ⇒̇ θ` 读作 `φ ⇒̇ (ψ ⇒̇ θ)`。下面的**优先级**声明只影响公式的读法，不会增减可写出的公式。 ```agda infix 18 _≐_ _∈̇_ infixr 12 _∧̇_ _∨̇_ infixr 10 _⇒̇_ infix 13 ¬̇_ ``` `∈̇`、`∧̇` 等记号上的小点提醒我们：这里写的是对象语言中的陈述，不是直接在 Agda 中提出的命题。例如，`t ∈̇ u` 只是写下一条成员关系陈述；`t`、`u` 究竟指什么，以及成员关系是否成立，都还没有确定。 **定义** (`Formula`) 给定宇宙层级 `ℓ`、类型 `K : Type ℓ` 和自然数 `n : ℕ`，定义归纳类型 `Formula K n : Type ℓ`。 ```agda data Formula {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where ``` 构造子 `_∈̇_` 和 `_≐_` 各取两个 `Term K n` 中的词项，得到一个公式；`_∧̇_`、`_∨̇_` 和 `_⇒̇_` 各取两个 `Formula K n` 中的公式，得到另一个公式；`⊥̇` 不取参数。 ```agda _∈̇_ _≐_ : Term K n → Term K n → Formula K n _∧̇_ _∨̇_ _⇒̇_ : Formula K n → Formula K n → Formula K n ⊥̇ : Formula K n ``` 构造子 `∃̇_` 和 `∀̇_` 各取一个 `Formula K (suc n)` 中的公式，得到 `Formula K n` 中的公式；`∀̇∈` 和 `∃̇∈` 还各取一个 `Term K n` 中的词项。 ```agda ∃̇_ ∀̇_ : Formula K (suc n) → Formula K n ∀̇∈ ∃̇∈ : Term K n → Formula K (suc n) → Formula K n ``` `⊥̇` 预定用来表达恒假的陈述。目前这些形成规则只规定哪些公式可以写出，还没有判定任何公式的真假。「或者」的 `_∨̇_` 与「如果……那么……」的 `_⇒̇_` 各有一个构造子，不必先用表示「非」的 `¬̇_` 和表示「并且」的 `_∧̇_` 改写。那样改写有时需要尚未假定的逻辑规则。将几种写法分开，后文便能分别解释它们的含义。 `∀̇_` 表示「对每个对象」，`∃̇_` 表示「存在某个对象」。它们不是把两条现成陈述接起来：后面的陈述还得指向新谈及的对象。为此，**量词**会在后续公式中添一个位置。下图以原来已有一个位置为例，展示编号如何变化。
下方箭头表示旧位置 `0` 顺移为 `1`，仍指向 $a$；上方箭头表示量词为 $x$ 新开位置 `0`
新增的 `0` 号位置对应这个量词的**约束变元**；原有位置上的变元相对于它仍是**自由变元**，编号各向后挪一位。因此，量词内部的公式体属于 `Formula K (suc n)`，整条公式属于 `Formula K n`。公式体也可以不用新位置。这种只记录位置、不保存名字的方法叫作 **de Bruijn 索引**：无需为避免重名而更换变元名称，也写不出越过可用范围的引用。 `∀̇∈` 和 `∃̇∈` 把量化范围限定在某个集合的元素中，用词项 `t` 指明这个集合。`t` 在新位置加入前就已写成，所以仍属于外层的 `Term K n`；只有量词后面的公式体使用扩展语境。这两种写法称为**有界量词**，各有独立的构造子，后文便能辨认只使用有界量词的公式。 **定义** (`¬̇_`) 上面的构造子给出了公式的基本形式；否定无须再添一种。我们规定 `¬̇ φ` 就是 `φ ⇒̇ ⊥̇`。因此，递归检查公式时只会遇到蕴涵，无须再处理一种独立的否定情形。后文赋予公式含义时，这个蕴涵便表达对 `φ` 的否定。 ```agda ¬̇_ : ∀ {ℓ} {K : Type ℓ} {n} → Formula K n → Formula K n ¬̇ φ = φ ⇒̇ ⊥̇ ``` **定义** (`⊤̇`) 真也不另设构造子，而规定 `⊤̇` 就是 `⊥̇ ⇒̇ ⊥̇`。所以，后文只需解释蕴涵和假，就能同时解释否定与真。这两项定义不依赖特定的常元域或语境长度。 ```agda ⊤̇ : ∀ {ℓ} {K : Type ℓ} {n} → Formula K n ⊤̇ = ⊥̇ ⇒̇ ⊥̇ ``` 词项与公式的形成规则适用于不同的常元域 `K`。若取某个结构的载体作为 `K`，常元就能指名其中的任意元素；若只为一部分对象预留名字，可用的常元便随之减少；若取空类型 `⊥*`，就没有可用的常元。变元位置的数量则由 `n` 独立决定。 ## 句子与无参公式 我们可以分别禁用两类指代方式。**句子**没有自由变元：把语境长度设为零，便得到 `Formula K 0`，但常元仍可出现。**无参公式**没有常元：把常元域设为空类型 `⊥*`，便得到 `Formula ⊥* n`，但仍可有自由变元。这两类公式都不用另设数据类型或代码名称。 | 可用的指代方式 | 公式类型 | |---|---| | 两者皆可 | `Formula K n` | | 仅常元 | `Formula K 0` | | 仅变元位置 | `Formula ⊥* n` | | 两者均无 | `Formula ⊥* 0` | : 自由变元与常元名可以分别禁用 空类型总能映入任意 `K`，所以后文的常元映射可以把无参公式送入任意常元域。这样，不必先枚举结构的元素，就能枚举无参公式。不过，能编码的并非只有无参公式：后文也会编码带有载体常元的公式。 ## 小结 本章只规定词项和公式怎样写：常元与变元位置提供指代方式，量词决定新位置的作用范围。它们究竟指什么、公式何时成立，还没有规定。下一步先建立一个结构，用来解释这些符号。