对象语言

集合论谈论集合，而要证明关于集合论本身的定理，它的语句必须先成为独立的数学对象，即按明确规则构造的表达式，而不是只靠约定形成的记号。本章定义这个对象语言，确定有哪些常元名、可以指涉哪些变量位置，以及词项与公式的形成规则。全章的中心决定关乎作用域：表达式的自由变量语境长度属于其自身类型，超出该语境的引用根本无法写出，而不只是不被允许。

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

每条公式都写在一个有限的自由变量语境上，语境的长度，即自然数 n，属于公式自身的类型。变量是 Fin n 的元素，即位置 0 到 n - 1。形成量词时，这个设计便直接显现出来：量词的公式体比量化所得的公式多一个可用变量位置，指标随之从 n 增到 suc n。词项因此不可能提到语境之外的变量，因为那样的位置并不存在。

module FOL.Syntax where

变量决定公式可以指涉什么，常元决定公式可以指名什么。除语境长度 n 外，公式还建立在任意的常元符号类型 K 上，K 即常元域。K 对整个语言只取定一次，因此一条公式内部可用的名字不会改变。这两个选取彼此独立：K 决定可以指名哪些参数，n 决定可以使用多少个变量位置；扩大其一不会影响另一者。

open import Base.Prelude

词项与公式

词项指称公式所谈论的对象，公式再对这些对象作出断言，所以先讲词项。词项要么是常元，即从 K 中取出的名字；要么是变量，即从 n 个可用位置中取出的一个位置。公式由这样的词项构造而成，起点是词项之间的隶属与相等这两个原子式，再由命题联结词以及有界、无界量词组合。

全书约定：t、u 表示词项，φ、ψ 表示公式，n、m 表示语境长度，i、j 表示变量索引。

这里 Term 是一个类型族：选定类型 K 与数 n，便得到类型 Term K n，词项从不脱离这二者而存在。词项无非是 K 中的一个名字或小于 n 的一个数，因此整个族与 K 同居宇宙层级 ℓ。

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

构造子 con 取 K 的一个元素 c，只把它当作名字。这个名字暂时没有含义，要等解释给出以后才知道它指称什么。构造子 var i 从 Fin n 中选出位置 i。取 n = 2 时，var 0、var 1 与 con c 都是 Term K 2 中的词项，而 var 2 无法写出：Fin 2 中没有名为 2 的元素，所以它不是会被事后检查退回的词项，而是根本无法形成的表达式。

自然数 n 决定哪些位置可以被指名，而不是它们被使用的次数。con c 与 var 0 的类型都是 Term K 2，尽管二者都没有提到两个变量；一条公式也可以多次使用同一个位置。公式正是由这样的词项构造而成。

  con : K → Term K n
  var : Fin n → Term K n

词项是名字，公式则是断言。最小的断言是原子式 _∈̇_ 与 _≐_：一个词项属于另一个词项，或者两个词项相等。联结词 ∧̇ ∨̇ ⇒̇ ¬̇ ⊤̇ ⊥̇ 由原子式构成复合的陈述，量词 ∃̇ ∀̇ 则遍及一切对象。与之并列，∀̇∈ 与 ∃̇∈ 是有界量词，读作「对……的每个成员」与「对……的某个成员」。这些符号都带一个小小的上点。点是层标记：∈̇ 说的是对象语言所述的隶属，与周围理论的隶属关系相隔一层；带点的符号永远是语法，而不是含义。

量词约束变量，语法把这个事实记进指标。其公式体比量化后的公式多一个可用变量位置，公式体中的位置 0 就是刚被约束的那个变量。哪些出现落在量词的管辖之下，由此仅凭位置确定，这就是 de Bruijn 方式；公式内部不存放名字，因此这些形成规则无需约定 α 改名，也无需区分同名变量。公式本身并不标记那个多出的位置是否真的被使用。

复合公式写成一行时，需要商定阅读的次序，这四行把它一次定下，对整个对象层有效。原子式与否定结合得最紧，层级 18 与 13。合取与析取居中，层级 12；蕴涵最弱，层级 10；两对都右结合，于是 φ ⇒̇ ψ ⇒̇ θ 读作 φ ⇒̇ (ψ ⇒̇ θ)，正是迭代蕴涵的通常分组。这些是解析上的约定，不给语言增添任何东西；有了它们，嵌套公式按普通数学行文的样子即可读清，只有想要的分组不同时才需要括号。这是全书对对象层读取层级的唯一一次宣告。

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

Formula 族与 Term 的索引方式完全相同：常元域 K 与可用变量位置的个数 n。原子式 _∈̇_ 与 _≐_ 取 Term K n 中的两个词项，断言它们之间的隶属或相等。命题构造子由公式得到公式：_∧̇_、_∨̇_、_⇒̇_ 构成合取、析取与蕴涵，⊥̇ 就是假本身。它们都不约束也不释放变量，所以指标始终停在 n；只有量词在约束变量时才会改变它。

联结词取作构造子而非缩写，是带有语义理由的决定。公式最终要在宿主的命题类型 hProp 中被解读，每个联结词都由那里相应的直接运算解释，而不化归为别的符号。经典教科书可以省事，把 φ ∨̇ ψ 拼成 ¬̇ (¬̇ φ ∧̇ ¬̇ ψ)、把 ∀̇ 拼成 ¬̇ ∃̇ ¬̇、把 φ ⇒̇ ψ 拼成 ¬̇ φ ∨̇ ψ，因为经典逻辑里双重否定会消去。构造性地看，这种消去并非一般可得，替换后的写法给不出想要的含义。因此本书将 ∨̇、⇒̇ 与量词直接取为构造子。

data Formula {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where
  _∈̇_ _≐_     : 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) 的公式体，返回 n 个位置上的公式：公式体多出一个可支配的位置，即位置 0，这正是量词约束的变量。多出的位置只是可用，并非必须；从不提及它的公式体也是合法的公式。有界形式 ∀̇∈ 与 ∃̇∈ 读作「对……的每个成员」与「对……的某个成员」。它们的界限 t 是外层语境中的词项，即 Term K n 的词项，量化遍及 t 的成员；公式体同样是 Formula K (suc n)。

有界量词本可用普通量词拼出，仍将其保留为构造子是第二个刻意的决定，这次的理由关乎语法本身。倘若 ∀̇∈ t φ 只是缩写，「φ 的每个量词都有界」就成了关于 φ 恰巧如何拼写的事实，任何按 φ 形状进行计算的过程都看不见它。作为构造子，有界性属于形状。后续章节将用一个对每个构造子恰设一个情形的数据类型给公式分类，并以一个对 ∃̇ 与 ∀̇ 全然不设情形的数据类型证明所有量词皆有界；这样的证书之所以可能，正因为有界形式是独立给出的。这种形状的公式在不同结构之间表现良好，模型诸章将接手这条线索，可构造宇宙诸章会把它继续下去。

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

否定不是构造子，而是定义出来的符号：¬̇ φ 按定义就是 φ ⇒̇ ⊥̇。这个定义有一个可见的计算后果。对公式做匹配的函数遇到的并非否定本身，而是后件为 ⊥̇ 的蕴涵，为 _⇒̇_ 准备的子句已经覆盖了它。因此永远不必为否定单写子句，语义也不例外。

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

真以同样方式定义：⊤̇ 即 ⊥̇ ⇒̇ ⊥̇，从荒谬到荒谬的蕴涵。语法之外别无假设，本章也不为这些符号日后的解读施加任何定律。既然定义会展开为构造子，解释只需用它处理 _⇒̇_ 的既有子句来对待它们，无须任何特别安排。与构造子一样，¬̇_ 与 ⊤̇ 把宇宙层级与 K 作为隐式参数，同一对符号因此在每个常元域、每个变量个数下都可用。

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

一套语法服务全书的每一种用途；自由度在于常元域 K 的取法：

句子与无参公式

句子没有自由变量，无参公式没有常元。两项限制彼此独立；一旦公式要在模型内部被编码和求值，这个区分就变得关键。

句子是没有自由变量的公式。作用域既然内蕴，这就是一个类型 Formula K 0，而非附加条件，本书不为它另设名字。无参公式则沿另一条轴限制：常元域取空类型 ⊥*，任何参数都无从指名，而自由变量照旧。它同样只是一个类型 Formula ⊥* n，没有单独的名字。从空类型出发的函数对任何 K 都存在，所以无参公式可以在任何常元域上被解读，常元改名工具组给出的正是这个映射。当语法需要在不先枚举周围集合的前提下被枚举时，无参公式尤其有用，参数可以改由环境提供。但可编码的并不只有无参公式；后面的编码也直接处理 Formula S n，其中包括取自载体 S 的常元。

小结

词项与公式共同把作用域纳入形成规则本身。常元域 K 决定可以指名哪些参数，n 决定可以使用哪些自由变量位置；二者都不表示名字实际出现的次数。量词只改变公式体的语境长度，de Bruijn 位置则无需变量名便能确定被约束的变量。分别令 n 或 K 取空的情形，就得到句子或无参公式，两项限制因而始终清楚地彼此独立。