集合的形式化 #1 公理基础

一、序言

1. 形式化

    形式化的本质是明确规则。我们希望明确表达、定义、证明的规则：表达一个数学对象时，应遵循什么语法规则？如何定义一个数学对象？证明时有哪些推理规则？为了解决这些问题，我们需要从零开始，建立一个形式化的系统。

    与形式化对立的是使用自然语言。我们已经习惯于使用“为定值”“是动点”“取最大值”“的取值范围”等词汇，但事实上它们是不精确的。考虑以下表述：

    (1) 已知 x = -1，求 x 的绝对值

    (2) 已知 x = -1，x² =1，求 x 的绝对值

    (3) 已知 x + 1 < 0，求 x 的取值范围

    (4) 已知 x + 1 < 0, x² < 2，求 x 的取值范围

    同样是“已知 ... ，求 x 的 ...”的形式，“绝对值”和“取值范围”的表现是不同的。对“绝对值”而言，若从已知中的一个条件即可推出绝对值，那么就不需要再看其他条件；对“取值范围”而言，需要综合所有的条件进行判断。而所谓的“综合所有的条件进行判断”具体又遵循什么规则呢？是通过不断地推理限制 x 的范围吗？当条件更复杂时，我们又如何才能确信这个范围已经不能再继续缩小了？总之，我们可能并不能说清楚其中的规则。这样的问题经常困扰着广大学生，而形式化是解决此类问题的方案之一。

    形式化并不意味着像下面这样“强行塞符号，让读者看不懂”：

    事实上，形式化可以实现在严谨性的基础上保证一定的可读性：

    此外，形式化也并不意味着完全抛弃自然语言。在确保可以随时翻译成形式化表述的前提下，我们可以使用自然语言进行描述。在交流证明思路等需要创造性的情境下，也可以使用不太严谨的自然语言。

2. ZFC

    一种经典的形式化方案是 ZFC。ZFC 基于一阶逻辑，在公理体系中初始地声明了以下用于组成公式的符号：  ，并给出了一系列推理规则、公理、公理模式。然而，ZFC 有其局限性：很多操作并不符合 ZFC 给定的这些规则。

    一个很常见的例子是“公式的等价替换”。设公式  中含有公式  ，若在  所在环境下可证  ，那么就有  （将  中的  替换为  ）。例如，根据  ，即可得到  。这种操作不符合 ZFC 给定的规则，也无法对应于一个定理。

    一般对此的解释是：ZFC 所基于的一阶逻辑并不是“元语言”（最底层的形式系统）。ZFC 实际上是元语言中的一个研究对象（形式系统作为数学对象）。在底层的元语言中，我们可以断定：这种操作是合理的。然而，对作者而言，这样的解释并不令人满意。如果 ZFC 之下还有另一个元语言，那么这个元语言究竟是什么？既然有这样一个元语言，为什么不直接在其上建立理论，而非要定义一个形式系统再在其上建立理论？（这里不考虑对数理逻辑的单独研究）

3. Coq

    最终，作者选择的形式化方案是 Coq。Coq 实际上是一个编程语言，但它并不会生成可执行程序，而是会逐行地对输入的代码输出反馈。通过使用 Coq，用户可以在给定的规则内建立数学理论，从而实现形式化。

    这个专栏系列将介绍一种【使用 Coq，从标准库中的 Init 和 ssreflect 出发，形式化与集合相关的基本概念、定理】的方案。由于作者从未系统学习过 Coq，如有错误或不当之处，敬请谅解。

二、Coq 简介

Coq 的官方手册：https://coq.inria.fr/distrib/current/refman/

以下内容是一个简化的、粗略的、可能不准确的、基于作者理解的介绍。

1. 项

    项是 Coq 中的基本概念之一。项可通过以下规则形成：

    (1) Type 是一个项（粗体字表示这里的 Type 不是一个指代词，而是字符串"Type"）

    (2) Prop 是一个项

    (3) 所有的变量（identifier）都是项，其中变量（不精确地说）是不引起混淆的字符串，例如 a，b，c，x，y，z，fxy，pqrs'，x_0 等等

    (4) 对于任意的变量 x，项 T, U，forall x : T, U 是一个项（forall 就是全称量词）

    (5) 对于任意的变量 x，项 T, u，fun x : T => u 是一个项（表示函数建构式）

    (6) 对于任意的项 t, u，t u 是一个项（t 和 u 之间有一个空格，表示函数应用）

    (7) match 表达式也可以用于形成项（较为复杂，这里不介绍）

2. 语境

    每个语境可理解为一个（有限的）集合，可能包含了以下种类的信息：

    (1) 对于任意的项 t, T，t : T 可用于组成语境

    (2) 对于任意的项 c, t, T, c := t : T 可用于组成语境

    (3) 与归纳类型相关的一些信息也可以用于形成语境（较为复杂，这里不介绍）

    对于一个语境，Coq 给定了一些规则来判断这个语境是否是 well-formed 的。在一个 well-formed 的语境中，有规则可以判断项 t, T 是否满足【t 有类型 T】（可写作 t : T），这些用于判断类型关系的规则被称为类型规则（typing rules）。还有一些规则可以判断项 t, T 是否满足【t 可转换为 T】，这些用于判断转换关系的规则被称为转换规则（conversion rules）。例如，设语境中有 P : forall _ : nat, Prop，则 forall x : nat, P x 可转换为 forall y : nat, P y。类型规则和转换规则一起可被视为 Coq 的推理规则。

3. 定义与证明

    在 Coq 中建立理论时，定义新的项可通过使用 Definition 指令、声明归纳类型（较为复杂，这里不介绍）以及其他方式实现。在使用 Definition 指令时，我们需要写出一个项 t，使得在当前语境下 t 有某个类型 T，从而完成指令： Definition c : T := t。 定义完 c 之后，c := t : T 就被加入到语境中。

    如果一个项 P 在某语境下有类型 Prop，那么在这个语境下 P 就被称为命题。如果有项 p 满足 p 在某语境下有类型 P，并且 P 有类型 Prop，那么在这个语境下 P 就被视为被证明了，而 p 则被称为 P 的一个证明。Coq 设计了专门的证明模式方便用户使用策略（tactics）更高效地构造证明。

4. init 标准库

    init 标准库中定义了基本的逻辑对象与数据结构，规定了一些符号记法。

    (1) P -> Q 是 forall _ : P, Q 的记法，当 P, Q 为命题时表示蕴含关系

    (2) True : Prop 表示真命题（通过归纳类型定义）

    (3) False : Prop 表示假命题（通过归纳类型定义）

    (4) not : Prop -> Prop 表示否定，输入一个命题 P，输出一个命题 ~ P （定义为 ~ P := P -> False）

    (5) and : Prop -> Prop -> Prop 表示合取，输入两个命题 P, Q，输出一个命题 P /\ Q（通过归纳类型定义）

    (6) or : Prop -> Prop -> Prop 表示析取，输入两个命题 P, Q, 输出一个命题 P \/ Q（通过归纳类型定义）

    (7) iff : Prop -> Prop -> Prop 表示当且仅当，输入两个命题 P, Q，输出一个命题 P <-> Q（定义为 P <-> Q := (P -> Q) /\ (Q -> P)）

    (8) ex : forall A : Type, (A -> Prop) -> Prop 表示存在量词，ex A P 记作 exists x : A, P x（通过归纳类型定义）

    (9) eq : forall A : Type, A -> A -> Prop 表示相等，eq A x y 记作 x = y（通过归纳类型定义）

    (10) nat : Type 表示自然数，其中 O : nat 表示零，S : nat -> nat 表示后继（通过归纳类型定义）

三、公理

现在我们正式开始建立理论。

    我们添加了四条公理。

    (1) 函数外延。该公理说明：任意两个同类型的函数，若函数值总是相等的，那么这两个函数相等。该命题在原始语境下不可判定（既无法证明该命题，也无法证明该命题的否定）。

    (2) 命题外延。该公理说明：等价的命题相等。由于相等可以进行“替换”（根据相等的归纳类型定义），这条公理部分地解决了序言中提到的“公式的等价替换”问题。该命题在原始语境下不可判定。

    (3) 排中律。该公理允许我们在证明时对 P 和 ~ P 两种情况进行分类讨论。该命题在原始语境下不可判定，但这并不意味着在添加排中律公理之前一个命题可能有“非真非假”的第三种情况。在原始语境下，我们可以证明 forall P : Prop, ~ ~ (P \/ ~ P)，但不能证明 forall P : Prop, ~ ~ P -> P。

    (4) 存在实例化。该公理在效果上允许我们解构一个 exists x : A, P x 的证明，得到一个 a : A 和一个 P a 的证明。这为我们之后的一些操作提供了便利，在后续专栏会提到。事实上，该公理蕴含了选择公理。