元理论：总结与挑战

摘要

本课结束专门讨论元理论的单元，也随之结束本课程的内容。它重建一条演绎之链：从公理的有效性到系统的可靠性；从关于或非的两条引理到卡尔马引理，再到对有穷前提的完备性；从双见证引理到紧致性定理，并借助它到强完备性；从子句形式到归结法的可靠性与反驳完备性；并在每一环指出它用到哪些结果、在哪一课中证明。它说明课程前面的三个部分，即语言、演绎和语义，如何汇聚于 $\vdash$ 与 $\models$ 的重合，以及每一部分为这一重合贡献了什么；它区分课程证明了的、承认了的和留待解决的东西。它在结业测评中重复入门测评的技能，最后给出六道挑战题，难度高于各课的习题，要求结合其中多课的工具。

学习目标

重建本单元结果的逻辑顺序，指出每个结果所依靠的先前结果以及证明它的那一课，并说明紧致性与强完备性先后顺序的理由。
解释语言、演绎和语义如何汇聚于 $\vdash$ 与 $\models$ 的重合，以及课程每个单元中哪个结果对这一重合不可或缺。
区分课程证明了什么、承认了什么（公理模式、初始规则和归纳法）以及留下了什么未决问题（判定可满足性的代价和带量词的逻辑）。
解答结合标记、卡尔马引理、统一代入、紧致性和归结的问题，在每种情形下利用重合的容易的一面。

本单元的收获

本单元的目标是比较前面各单元在同一语言上建立起来的两种关系，即可推演性 $\Gamma \vdash \varphi$ 和语义后承 $\Gamma \models \varphi$ ，并证明二者重合。这一目标在陈述上已毫无保留地实现了：对任意前提集，无论有穷还是无穷，两种关系都是同一个关系，而归结给出了第三种同样可靠且完备的判定后承的方式。保留之处在于方法，而且每一处都已在相应位置说明：第一课的完备性是构造性的，但不实用，因为它产生的推演和真值表一样长；紧致性保证赋值存在，但不教人如何找到它；归结能够判定，但它在最坏情形下的代价是一个悬而未决的问题。带着这些保留，所走过的路可以读成一条分为四段的演绎之链。

可靠性

关于可靠性与完备性的一课首先确定了术语：如果 $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$ ，系统就是可靠的；如果逆命题成立，系统就是完备的，完备性分三个等级（弱完备、对有穷集完备和强完备）。它拆穿了一个循环论证，这个论证企图“由可靠性”得到完备性，即从 $\nvdash \chi$ 过渡到 $\not\models \chi$ ，而这一步其实是弱完备性的逆否命题；它还说明了这两个性质是相互独立的。接着它证明了 A1、A2、A3 的每个实例都是有效的：假设有一个赋值否证它，借助蕴涵式的假行便得到不可能的值；又通过对行数的强归纳证明了可靠性，其中公理一种情形，前提一种情形，语义分离规则一种情形，而对于双重否定替换规则，则用等价 $\theta \eqsem \neg\neg\theta$ 和语义替换定理。逐行传递的性质不是有效性，而是被一个满足前提的固定赋值所满足，因此可靠性在有前提时也成立，即使前提是无穷的。由它得出每个可满足集的一致性，特别是系统本身的一致性，以及演绎单元所没有的方法：一个反模型证明某个推演不存在。

卡尔马与有穷完备性

同一课分两步证明了逆命题。第一步是卡尔马引理：若 $\varphi$ 的变元都在 $u_{1}, \ldots, u_{n}$ 之中，则 $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ 对一切赋值 $v$ 成立，其中 $\psi^{v}$ 是 $\psi$ （若 $v(\psi) = 1$ ）或 $\neg\psi$ （若不然）；系统从每一行推演出该行关于公式所说的东西。它对复杂度的归纳只有一种复合情形，即 $(\alpha \downarrow \beta)$ ，因为或非是唯一的初始联结词；在这种情形中有三个子情形，需要系统中的两条引理，其中第二条有两种形式： $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ ，借助合取引入、双重否定和两次应用双重否定替换规则推演出来；以及 $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ 和 $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ ，借助析取引入推演出来。第二步消去前提：若 $\varphi$ 是重言式，它就可由全部 $2^{n}$ 行中每一行的前提推演出来，而分情况证明先消去最后一个变元的文字，再消去倒数第二个变元的文字，直到得到 $\vdash \varphi$ ，即弱完备性。借助语义演绎定理和句法演绎定理的逆命题，完备性推广到了有穷前提集；由此，对有穷前提而言，推演与后承重合，可证等价与语义等价重合，而且可推演性是可判定的，因为真值表能回答它。

紧致性与强完备性

关于紧致性定理的一课处理了无穷情形，这是卡尔马引理所达不到的，因为无穷多个前提无法卸入一个蕴涵式。它在完全不提及推演的情况下证明了：一个集合是可满足的，当且仅当它的每个有穷子集都是可满足的。为 $v_{1}, \ldots, v_{n}$ 所取的一个值序列称为好的，如果该集合的每个有穷子集都可以被某个延长它的赋值满足；双见证引理保证一个好序列可以延长为一个好序列，因为如果两种延长都不是好的，两个有穷见证之并就会与该序列是好的相矛盾；而在可能时总是优先取 $1$ 所得到的赋值满足每个公式，这是由一致引理得出的，因为每个公式只有有穷多个变元。这个构造不需要选择公理，因为变元是编了号的，而且每一步都有一条规则。由紧致性得出它的等价形式，即不可满足性形式和后承形式；由后者、对有穷前提的完备性和单调性得出强完备性；再由强完备性和可靠性得出完全的重合： $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ 对一切 $\Gamma$ 成立，并且一个集合是一致的，当且仅当它是可满足的。这一课提醒，这个顺序并非偏好问题：从尚未得到的强完备性推出紧致性将是循环的。这一课最后讲了可数图的着色，它把一个无穷问题翻译为一个其有穷部分都可满足的公式集，并讲了一个公式集所能表达之物的局限。

归结

关于归结法的一课把公式集换成了子句集，每个子句是文字的有穷集合，并有两种表示：子句形式，它具有相同的模型；以及定义式形式，它为每个复合子写法引入一个新变元，只保持可满足性，并且像公式一样增长，而不是像二的幂那样增长。在子句上只作用一条规则：由 $C$ 和 $D$ ，其中 $\ell \in C$ 且 $\ell^{*} \in D$ ，推出 $(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\})$ ；反驳是一个到达 $\Box$ 的推导。可靠性的证明与系统可靠性的证明一样，对推导作归纳，并利用归结式是其前提的后承；反驳完备性则对变元个数作归纳，借助一个变元的消去，这种消去保持可满足性，其证明构造出一个模型；对无穷集合，则再一次借助紧致性。由此得出： $\Gamma \models \varphi$ ，当且仅当 $\Gamma \cup \{\neg\varphi\}$ 的一个子句形式有反驳；并且饱和过程是有穷的，因为有 $n$ 个变元时子句不超过 $4^{n}$ 个，它不用真值表就能判定可满足性。这一课介绍了可满足性问题，其最坏情形下的代价无人知晓，并介绍了两种可以快速判定的情形：霍恩子句和二文字子句。

下图把四段汇成一条链。中间一列的每个节点是一个结果，按逻辑顺序编号，并用弧线连到其证明所用到的前面的环节；四周浮动的是支柱，即这条链一再求助的原理和工具，每个支柱用实线连到依靠它的环节，用虚线连到确立它的环节，而来自前面各单元的支柱则画成圆环。点击一个支柱，会突出显示所有用到它的环节；每个环节都链接到证明它的那一课。请注意，可靠性和紧致性，一个在第一段确立，一个在第三段确立，在其后的各段中再次出现；而本单元最常用到的支柱是赋值与一致引理，其次是归纳法，它有三种形式：对推演的行、对公式的复杂度、对子句集的变元个数。

链的支柱

A归纳法与递归. 对自然数的强归纳，对公式复杂度的归纳（其唯一的复合情形是 $(\alpha \downarrow \beta)$ ），以及递归定义。在第一单元中证明。本单元中不加证明而采用。
B本课程的系统. A1、A2、A3，分离规则和双重否定替换规则；自反性、单调性、推演之间的分离规则、有穷性以及 $\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi)$ 。在第二单元中确定。本单元中不加证明而采用。
C导出技巧. 双重否定，出自关于四种推演技巧的一课；合取引入、析取引入和分情况证明（若 $\Gamma \cup \{\psi\} \vdash \chi$ 且 $\Gamma \cup \{\neg\psi\} \vdash \chi$ ，则 $\Gamma \vdash \chi$ ），出自关于经典逻辑技巧的一课。在第二单元中证明。本单元中不加证明而采用。
D赋值与一致引理. $v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta))$ ；若两个赋值在 $V(\varphi)$ 上一致，则它们给 $\varphi$ 相同的值；有效性用 $2^{n}$ 行来判定。在第三单元中证明。本单元中不加证明而采用。
E语义后承. 蕴涵式的假行、单调性、 $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ 、 $\Gamma \models \varphi$ 当且仅当 $\Gamma \cup \{\neg\varphi\}$ 不可满足，以及语义替换定理。在第三单元中证明。本单元中不加证明而采用。
F合取形式. 值引理；每个公式都等价于一个合取范式，它可能需要 $2^{n}$ 个子句；文字的析取是有效的，当且仅当它含有一个互补对。在第三单元中证明。本单元中不加证明而采用。
G可靠性. 若 $\Gamma \vdash \varphi$ ，则 $\Gamma \models \varphi$ ，对一切集合 $\Gamma$ 成立；一个反模型证明某个推演不存在。确立于: 2. 可靠性.
H紧致性. 一个公式集是可满足的，当且仅当它的每个有穷子集都是可满足的；由此，不可满足的集合在某个有穷部分中就已经不可满足。确立于: 11. 紧致性定理.

第 1 段可靠性
- 不构造真值表而验证模式的每个实例都是有效的。
- 通过对行数的强归纳证明可靠性，包括双重否定替换规则的情形。
- 用一个反模型证明某个公式不可推演，并由可靠性得出一致性。
1. 公理的有效性. A1、A2、A3 的每个实例都是有效的：一个否证它的赋值，借助蕴涵式的假行，将要求不可能的值。
  依据: E (语义后承). 证明于: 可靠性与完备性.
2. 可靠性. 若 $\Gamma \vdash \varphi$ ，则 $\Gamma \models \varphi$ ，对一切 $\Gamma$ 成立：通过对行数的强归纳，公理一种情形，前提一种情形，语义分离规则，以及对双重否定替换规则使用 $\theta \eqsem \neg\neg\theta$ 与语义替换。
  使用: 1. 公理的有效性. 依据: A (归纳法与递归), B (本课程的系统), E (语义后承). 证明于: 可靠性与完备性.
3. 一致性与反模型. 每个可满足集都是一致的；系统是一致的，并且 $\nvdash v_{1}$ ；若一个赋值满足 $\Gamma$ 而否证 $\varphi$ ，则 $\Gamma \nvdash \varphi$ ，真值表证实：不有效的就不是定理。
  依据: G (可靠性), D (赋值与一致引理). 证明于: 可靠性与完备性.
第 2 段卡尔马与有穷完备性
- 在系统中推演出关于或非的两条引理，必要时使用双重否定替换规则。
- 通过对复杂度的归纳证明卡尔马引理，只有一种复合情形。
- 用分情况证明消去各行的前提，并用两个演绎定理卸去有穷前提。
- 用真值表判定有穷前提下的可推演性、可证等价和一致性。
1. 或非引入. $\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta)$ 且 $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ ：否定的合取是 $\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta)$ ；双重否定消去外层的否定，双重否定替换规则消去两个内层的否定。
  依据: B (本课程的系统), C (导出技巧). 证明于: 可靠性与完备性.
2. 或非的否定. $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ 且 $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ ，因为 $\neg(\alpha \downarrow \beta)$ 就是 $(\alpha \vee \beta)$ ，只需析取引入即可。
  依据: B (本课程的系统), C (导出技巧). 证明于: 可靠性与完备性.
3. 卡尔马引理. 若 $V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}$ ，则 $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ 对一切赋值 $v$ 成立；归纳步骤只有一种情形，即 $(\alpha \downarrow \beta)$ ，按 $\alpha$ 和 $\beta$ 的值分为三个子情形。
  使用: 4. 或非引入, 5. 或非的否定. 依据: A (归纳法与递归), D (赋值与一致引理), B (本课程的系统). 证明于: 可靠性与完备性.
4. 弱完备性. 若 $\models \varphi$ ，则 $\vdash \varphi$ ：卡尔马引理从每一行推演出 $\varphi$ ，分情况证明从最后一个变元到第一个变元依次消去文字，共使用引理 $2^{n}$ 次，使用分情况证明 $2^{n} - 1$ 次。
  使用: 6. 卡尔马引理. 依据: C (导出技巧). 证明于: 可靠性与完备性.
5. 对有穷前提的完备性. $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$ ：语义演绎定理导向一个重言式，弱完备性推演出它，演绎定理的逆命题再把前提还回去。
  使用: 7. 弱完备性. 依据: E (语义后承), B (本课程的系统). 证明于: 可靠性与完备性.
6. 有穷重合与判定. 对有穷的 $\Gamma$ ， $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ ，并且 $\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi$ ；由此，从有穷前提出发的可推演性借助真值表是可判定的。
  使用: 8. 对有穷前提的完备性. 依据: G (可靠性), D (赋值与一致引理). 证明于: 可靠性与完备性.
第 3 段紧致性与强完备性
- 通过逐一固定变元的值来证明紧致性，利用好序列的不变量和两个见证的论证。
- 在可满足性形式、不可满足性形式和后承形式之间转换。
- 不循环地由紧致性得到强完备性，再由它得到一致性与可满足性的重合。
- 把关于无穷对象的问题编码为公式集，并用紧致性解决。
1. 双见证引理. 若已固定的值的序列 $s$ 是好的（该集合的每个有穷子集都能被某个延长它的赋值满足），则 $(s, 1)$ 或 $(s, 0)$ 是好的：若两者都不是，两个有穷见证之并就会与 $s$ 是好的相矛盾。
  依据: D (赋值与一致引理). 证明于: 紧致性定理.
2. 紧致性定理. $\Gamma$ 可满足，当且仅当它的每个有穷子集都可满足：把 $v_{n + 1}$ 固定为 $1$ （若 $(s_{n}, 1)$ 是好的），否则固定为 $0$ ，所得的赋值由一致引理满足每个公式。不需要选择公理，因为变元是编了号的。
  使用: 10. 双见证引理. 依据: A (归纳法与递归), D (赋值与一致引理). 证明于: 紧致性定理.
3. 等价形式. $\Gamma$ 不可满足，当且仅当它的某个有穷部分不可满足； $\Gamma \models \varphi$ ，当且仅当 $\Gamma_{0} \models \varphi$ 对某个有穷的 $\Gamma_{0} \subseteq \Gamma$ 成立；而后一种形式反过来蕴涵该定理。
  使用: 11. 紧致性定理. 依据: E (语义后承). 证明于: 紧致性定理.
4. 强完备性. 若 $\Gamma \models \varphi$ ，则 $\Gamma \vdash \varphi$ ，对一切 $\Gamma$ 成立：后承形式给出一个有穷的 $\Gamma_{0}$ ，对有穷前提的完备性给出 $\Gamma_{0} \vdash \varphi$ ，单调性给出 $\Gamma \vdash \varphi$ 。
  使用: 8. 对有穷前提的完备性, 12. 等价形式. 依据: B (本课程的系统). 证明于: 紧致性定理.
5. 推演就是后承. $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ 对一切 $\Gamma$ 成立；定理恰好是重言式，并且一个集合是一致的，当且仅当它是可满足的。
  使用: 13. 强完备性. 依据: G (可靠性). 证明于: 紧致性定理.
6. 可数图的着色. 对每个顶点和每种颜色取一个变元 $x_{i,c}$ ，再取一些公式，表示每个顶点恰有一种颜色、相邻顶点颜色不同，那么一个可数图只要其每个有穷子图都可用 $k$ 种颜色着色，它自身也可以。
  依据: H (紧致性), F (合取形式). 证明于: 紧致性定理.
第 4 段归结
- 用合取形式或定义式形式把公式集表示为子句集。
- 构造反驳，而不在一步中消去两个互补对。
- 证明归结的可靠性和反驳完备性，先对有穷集合，再借助紧致性对任意集合。
- 用饱和来判定后承，并识别可以快速判定的情形。
1. 子句形式. 子句是文字的有穷集合，只要某个文字取值 $1$ 就被满足，而 $\Box$ 不可满足； $\Gamma$ 的一个子句形式与它有相同的模型，并且 $\Gamma \models \varphi$ ，当且仅当 $\Gamma \cup \{\neg\varphi\}$ 的一个子句形式不可满足。
  依据: F (合取形式), E (语义后承). 证明于: 归结法.
2. 定义式子句形式. 对每个子写法取一个新变元并加上它的定义子句，则 $T(\varphi)$ 与 $\varphi$ 等可满足，并且至多有 $4k + 1$ 个子句，每个子句至多三个文字；定义式形式可以判定有穷前提下的后承。
  使用: 16. 子句形式. 依据: A (归纳法与递归), D (赋值与一致引理). 证明于: 归结法.
3. 归结的可靠性. $\{C, D\} \models R_{\ell}(C, D)$ ，对 $\ell$ 的值分情况可证；通过对推导的强归纳， $S \models C$ 对每个子句 $C$ 成立，只要它是由 $S$ 推导出的；若 $S$ 有反驳，则它不可满足。
  使用: 16. 子句形式. 依据: A (归纳法与递归). 证明于: 归结法.
4. 一个变元的消去. $E_{p}(S)$ 保留不含 $p$ 也不含 $\neg p$ 的子句，并加入关于 $p$ 的归结式，它不含 $p$ ，并且与 $S$ 等可满足；由它的一个模型可以得到 $S$ 的一个模型，只需选择 $p$ 的值。
  使用: 18. 归结的可靠性. 依据: D (赋值与一致引理). 证明于: 归结法.
5. 有穷反驳完备性. 每个有穷且不可满足的子句集都有反驳，对变元个数归纳：消去最后一个变元，再插入每个归结式的前提。
  使用: 19. 一个变元的消去. 依据: A (归纳法与递归). 证明于: 归结法.
6. 反驳完备性. 一个子句集，无论有穷还是无穷，不可满足当且仅当它有反驳；由此， $\Gamma \models \varphi$ ，当且仅当 $\Gamma \cup \{\neg\varphi\}$ 的一个子句形式有反驳。
  使用: 16. 子句形式, 18. 归结的可靠性, 20. 有穷反驳完备性. 依据: H (紧致性). 证明于: 归结法.
7. 饱和能判定. 有 $n$ 个变元时，推导出的子句集至多有 $4^{n}$ 个元素；饱和会终止，并且不用真值表就能判定可满足性，尽管并不总是比真值表更快。
  使用: 18. 归结的可靠性, 20. 有穷反驳完备性. 证明于: 归结法.

课程的终点. 这条链终止于这样的地方：课程的两个侧面被认作同一个关系，并且有了判定它的方法。留下来的未决问题已不再是关于命题逻辑的问题，而是关于它的代价以及它向量词的推广的问题。