数理逻辑 I：最终回顾

课程的宗旨

所有数学课程都要求证明，所有哲学课程都要求论证；然而，没有一门课程把推理本身作为研究对象。因此，本课程诞生时就有一个总目标：构建第一个以推理为对象的完整数学理论，并让它的四个组成部分一目了然：一种语言，其公式可以无歧义地识别；一种演算，它产生推演而不考虑符号的意义；一种意义，它在每个赋值下给每个公式指派其值；以及演算与意义相一致的证明，也就是证明 $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ 对任意公式集 $\Gamma$ 和任意公式 $\varphi$ 成立。关于学习计划的一课把这一总目标展开为七项总体学习目标，最好按图引用它们时所用的编号把它们列在眼前：

1. 区分对象语言与元语言，并用形成规则判定一个符号串是否是公式。
2. 把自然语言中的陈述句和论证形式化，指出形式化保留了什么、丢失了什么。
3. 在本课程的系统（卢卡西维茨公理、分离规则和双重否定替换）中构造推演，综合运用公理、初始规则和派生规则。
4. 用对自然数的归纳、对公式复杂度的归纳和对推演长度的归纳证明元定理。
5. 用真值表和等价式判定有效性、可满足性、语义后承和语义等价。
6. 把公式变换为范式，并用范式表示真值函数和电路。
7. 解释并运用可靠性、完备性和紧致性，并用归结判定不可满足性。

此外，课程的每一课都说明了自己的具体目标。各课并不说明每个具体目标服务于哪项总体目标；这种对应是从外部所做的解读，采用与本站其他课程相同的方法。每个具体目标被分配给一项主要的总体目标，如果它还涉及其他目标，再分配给若干次要目标；每个具体目标在其主要目标中计一整份，在每个次要目标中计半份；一节课以权重最大的那项总体目标为主要目标，以其他获得权重的目标为次要目标。如果两项目标权重相同，则由本单元的目标决定；如果两者都不是本单元的目标，则取编号较小者。因此，关于归纳法的一课虽然属于语言单元，但它的四个具体目标都是归纳证明，所以它连到目标 4。导言课遵循同样的规则。总结课则遵循自己的标准：其主要目标是所在单元的目标，因为它的演绎之链、结业测评和大部分挑战汇集了该单元所教的内容；其次要目标是它的具体目标和六个挑战所训练的其他目标。若是如此，整门课程就呈现为一条脊柱的形状：头部是总目标；脊柱是各单元的顺序，每个单元占一段；每节课是该段上的一个节点，与其主要目标相连；七项目标环绕脊柱浮动，由滋养它们的各课支撑。