对象语言

通常，写下关于集合的陈述后，我们会问它是否成立。本章暂且不问真假，先看陈述怎样写成、又怎样组合。为此，我们把陈述的写法本身当作数学对象，构造一门对象语言。

我们先规定怎样指代对象，再用这些写法组成陈述，最后加入「对每个对象」和「存在某个对象」的说法。Agda 代码会逐步划定哪些表达式可以写出。至于它们指什么、陈述是否成立，留待后文再谈。

下面的定义有些取舍乍看可能不太自然：为什么要预先备好对象的名字，又为什么用数字去标记那些可以填入对象的位置？为什么先规定写法、后解释含义？为什么有些逻辑记号作为基本形式，有些则由它们定义出来？这些问题值得带着往下读，不必在本章急于解答。对象语言并没有数学上唯一的标准定义：许多常见方案虽然写法不同，却可以证明在表达能力上大体相当，只是使用起来各有便利。本书采用一种较成熟的方案，并针对后文的集合论研究，在这些便利之间作出我们认为最合适的平衡。随着后文解释和使用这些表达式，具体取舍的理由也会逐渐明朗。

词项

要写「一个对象属于另一个对象」，先得有办法指代这两个对象。可以预先给对象取名，也可以留下带编号的位置，等使用表达式时再指定对象。这样指代单个对象的表达式叫作词项。

先把预定的名字收进类型 K：其中的元素叫作常元名，K 叫作常元域。再用自然数 n 表示当前有多少个带编号的位置；这些位置合起来是语境，每个位置是一个变元位置。《基础词汇》引入的 Fin n 正好给出从 0 起、到 n 的前一个数为止的全部位置。Term K n 可以记录这两种指代方式，但尚未规定名字和位置究竟指什么。

定义 (Term) 给定宇宙层级 ℓ、类型 K : Type ℓ 和自然数 n : ℕ，定义归纳类型 Term K n : Type ℓ。

data Term {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where

每个 k : K 确定一个词项 con k : Term K n；每个 i : Fin n 确定一个词项 var i : Term K n。

  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 表示位置。

公式

有了词项，就能写出关于对象的陈述。这种书面陈述叫作公式，下文用 φ、ψ、θ 表示。最简单的公式由两个词项写成，形如「前者属于后者」或「两者相等」。这类公式叫作原子公式。在此基础上，还能写「并且」「或者」「如果……那么……」，以及下文要介绍的「每个」「某个」。

写公式时常省略括号，因此要先约定各记号如何结合。成员关系和相等结合得最紧，其次是稍后定义的「非」，再是「并且」「或者」，最后是「如果……那么……」。最后一种向右结合，所以 φ ⇒̇ ψ ⇒̇ θ 读作 φ ⇒̇ (ψ ⇒̇ θ)。下面的优先级声明只影响公式的读法，不会增减可写出的公式。

infix   _≐_ _∈̇_
infixr  _∧̇_ _∨̇_
infixr  _⇒̇_
infix   ¬̇_

∈̇、∧̇ 等记号上的小点提醒我们：这里写的是对象语言中的陈述，不是直接在 Agda 中提出的命题。例如，t ∈̇ u 只是写下一条成员关系陈述；t、u 究竟指什么，以及成员关系是否成立，都还没有确定。

定义 (Formula) 给定宇宙层级 ℓ、类型 K : Type ℓ 和自然数 n : ℕ，定义归纳类型 Formula K n : Type ℓ。

data Formula {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where

构造子 _∈̇_ 和 _≐_ 各取两个 Term K n 中的词项，得到一个公式；_∧̇_、_∨̇_ 和 _⇒̇_ 各取两个 Formula K n 中的公式，得到另一个公式；⊥̇ 不取参数。

  _∈̇_ _≐_     : 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 中的词项。

  ∃̇_ ∀̇_       : Formula K (suc n) → Formula K n
  ∀̇∈ ∃̇∈       : Term K n → Formula K (suc n) → Formula K n

⊥̇ 预定用来表达恒假的陈述。目前这些形成规则只规定哪些公式可以写出，还没有判定任何公式的真假。「或者」的 _∨̇_ 与「如果……那么……」的 _⇒̇_ 各有一个构造子，不必先用表示「非」的 ¬̇_ 和表示「并且」的 _∧̇_ 改写。那样改写有时需要尚未假定的逻辑规则。将几种写法分开，后文便能分别解释它们的含义。

∀̇_ 表示「对每个对象」，∃̇_ 表示「存在某个对象」。它们不是把两条现成陈述接起来：后面的陈述还得指向新谈及的对象。为此，量词会在后续公式中添一个位置。下图以原来已有一个位置为例，展示编号如何变化。

新增的 0 号位置对应这个量词的约束变元；原有位置上的变元相对于它仍是自由变元，编号各向后挪一位。因此，量词内部的公式体属于 Formula K (suc n)，整条公式属于 Formula K n。公式体也可以不用新位置。这种只记录位置、不保存名字的方法叫作 de Bruijn 索引：无需为避免重名而更换变元名称，也写不出越过可用范围的引用。

∀̇∈ 和 ∃̇∈ 把量化范围限定在某个集合的元素中，用词项 t 指明这个集合。t 在新位置加入前就已写成，所以仍属于外层的 Term K n；只有量词后面的公式体使用扩展语境。这两种写法称为有界量词，各有独立的构造子，后文便能辨认只使用有界量词的公式。

定义 (¬̇_) 上面的构造子给出了公式的基本形式；否定无须再添一种。我们规定 ¬̇ φ 就是 φ ⇒̇ ⊥̇。因此，递归检查公式时只会遇到蕴涵，无须再处理一种独立的否定情形。后文赋予公式含义时，这个蕴涵便表达对 φ 的否定。

¬̇_ : ∀ {ℓ} {K : Type ℓ} {n} → Formula K n → Formula K n
¬̇ φ = φ ⇒̇ ⊥̇

定义 (⊤̇) 真也不另设构造子，而规定 ⊤̇ 就是 ⊥̇ ⇒̇ ⊥̇。所以，后文只需解释蕴涵和假，就能同时解释否定与真。这两项定义不依赖特定的常元域或语境长度。

⊤̇ : ∀ {ℓ} {K : Type ℓ} {n} → Formula K n
⊤̇ = ⊥̇ ⇒̇ ⊥̇

词项与公式的形成规则适用于不同的常元域 K。若取某个结构的载体作为 K，常元就能指名其中的任意元素；若只为一部分对象预留名字，可用的常元便随之减少；若取空类型 ⊥*，就没有可用的常元。变元位置的数量则由 n 独立决定。

句子与无参公式

我们可以分别禁用两类指代方式。句子没有自由变元：把语境长度设为零，便得到 Formula K 0，但常元仍可出现。无参公式没有常元：把常元域设为空类型 ⊥*，便得到 Formula ⊥* n，但仍可有自由变元。这两类公式都不用另设数据类型或代码名称。

空类型总能映入任意 K，所以后文的常元映射可以把无参公式送入任意常元域。这样，不必先枚举结构的元素，就能枚举无参公式。不过，能编码的并非只有无参公式：后文也会编码带有载体常元的公式。

小结

本章只规定词项和公式怎样写：常元与变元位置提供指代方式，量词决定新位置的作用范围。它们究竟指什么、公式何时成立，还没有规定。下一步先建立一个结构，用来解释这些符号。