The object language

第一部开篇。宿主语言从头到尾都在说话；本部要构造的是被谈论的语言：以成员与等词为仅有谓词的集合论一阶语言，作为归纳数据类型深嵌入。宿主的表达力严格更强，所以嵌入的 Formula 从不用来说什么；它存在，是因为后面各部要把公式当作数学对象来研究：数它们、编码它们、追问它们能定义什么。本章是纯语法，不欠真值与结构任何东西。

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

module FOL.Syntax where

open import Base.Prelude

词项与公式

先立几个贯穿全书的变量约定：t、u 代表词项，φ、ψ 代表公式，n、m 代表自由变量个数，i、j 代表变量本身。词项要么是常量，要么是变量。允许哪些常量是一个类型参数 K，称为常量域；变量是 Fin n 的元素，于是带 n 个自由变量的词项只能提及变量 0 到 n - 1。作用域由此内蕴：越界的词项不是被禁止，而是不可表示。

data Term {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where
  con : K → Term K n         -- a constant, drawn from the domain K
  var : Fin n → Term K n     -- a de Bruijn variable

公式随后，以同样的方式索引。对象语言的每个构造子都带一个上点：这是一枚层标记，见点即知这个符号是语法而非含义。读法：∈̇ 是对象成员，≐ 是对象等词，∧̇ ∨̇ ⇒̇ ¬̇ ⊤̇ ⊥̇ 是联结词，∃̇ ∀̇ 是量词，∀̇∈、∃̇∈ 是有界量词，读作「对……的每个成员」与「对……的某个成员」。约束采用 de Bruijn 方式：量词所取的公式体多出一个自由变量，变量 0 即刚被约束的那个。

构造子清单里可以看出两个设计决定。其一，联结词全部是原语，理由在这门语言即将奔赴的语义：每个构造子将恰好意指一个真值代数运算，而该代数是构造性的。经典教科书可以省笔墨，把 φ ∨ ψ 拼作 ¬ (¬ φ ∧ ¬ ψ)、∀ 拼作 ¬ ∃ ¬、φ ⇒ ψ 拼作 ¬ φ ∨ ψ，因为经典地看双重否定会互相抵消。构造性地看它们不抵消：¬ ¬ P 严格弱于 P，上述每一种拼写都会给联结词指派错误的含义。所以 ∨、∀、⇒ 必须是构造子。剩下三个 (⊤̇、⊥̇、¬̇) 本来可以诚实地拼出，例如 ¬̇ φ 拼作 φ ⇒̇ ⊥̇；仍将它们原语化，是为了让后续每一次结构递归对所有联结词一视同仁，一子句一条，不留任何需要特判的编码。

其二，有界量词虽然可用 ∀̇ 拼写，仍占有原语席位。倘若它们只是缩写，「φ 的每个量词都有界」就成了关于 φ 恰巧如何拼写的事实，任何在 φ 的形状上计算的东西都看不见它。作为构造子，有界性就是形状：后面的章节按构造子给公式分类，用一个对 ∃̇ 与 ∀̇ 不设情形的归纳数据来证明「量词皆有界」，而这种缺席要能开口说话，有界形式必须自立门户。这种形状的公式在不同结构之间表现格外驯良，这条线索将在第二部的模型落定后重新拾起并延伸进第四部。此处的 fixity 表是对象层在全书的唯一一次集中声明，各级刻意与它将被解释成的真值代数运算对齐。

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

data Formula {ℓ} (K : Type ℓ) (n : ℕ) : Type ℓ where
  _∈̇_ _≐_     : Term K n → Term K n → Formula K n        -- atoms: membership, equality
  _∧̇_ _∨̇_ _⇒̇_ : Formula K n → Formula K n → Formula K n  -- binary connectives
  ¬̇_          : Formula K n → Formula K n                -- negation
  ⊤̇ ⊥̇         : Formula K n                              -- truth, falsity
  ∃̇_ ∀̇_       : Formula K (suc n) → Formula K n          -- quantifiers
  ∀̇∈ ∃̇∈       : Term K n → Formula K (suc n) → Formula K n  -- bounded quantifiers

参数 K 让一族语法覆盖全书的所有用途：

句子与无参公式

句子是没有自由变量的公式；作用域既然内蕴，这是一个类型 Formula K 0，而非附加条件，本书不为它另设名字。无参公式限制的是另一条正交的轴。常量是外部集合以参数身份进入公式的通道；这里常量域取空类型 ⊥*，参数于是全然没有，而自由变量照旧；与句子一样，这只是一个类型 Formula ⊥* n，本书不为它另设名字。从空类型可以推出一切，所以无参公式可以进入任意常量域上的语法；执行这次进入的映射编在书末的常量变换章里。无参公式不是工作语法的对手，而是它的同伴：常量囊括一切集合的语法太大，数不得也编不得码，因此后面各部凡需要把公式当数据用，理论作为公式的集合、模型内部的公式码，收集的都是无参公式，参数改经环境喂入。

小结

对象语言是归纳族 Formula K n：常量域作参数，作用域经 Fin 内蕴，构造子全原语、全带点。围绕它的：无参公式，这条数据轴的进入映射随书末的常量变换工具组到来。留意缺席者：全篇没有替换算子、没有弱化算子。这个设计将一直保持下去，本书仅需的那一点变量机件在本书稍后登场。眼下，公式先得有可谈论的对象。