第14章：形式系统——给推理一个地基

在你能证明一件事之前，你得先说清楚"证明"是什么意思。

---

上卷的十三章是一次旅行。我们从熵增出发，穿过符号系统的废墟，绕过向量空间的陷阱，在复杂度理论的边界上停了很久。整个过程，我们一直在谈"推理"——但从未真正定义它。

这是故意的。直觉需要先行，定义跟在后面。

但现在是时候付账了。下卷要做的事情只有一件：把推理这件事说清楚。不是用比喻，不是用历史，而是用精确的语言，把推理的结构挖出来，放在灯光下看清楚。

这需要一个起点。这个起点叫做形式系统。

---

14.1 语言的歧义性问题

考虑这句话："如果天下雨，地就湿。天下雨了。所以地湿了。"

这个推理看起来完全正确。但问题是，它为什么正确？

你可能会说：因为这符合常识。但常识不是数学。或者你会说：因为逻辑上必然如此。但"逻辑上必然"是什么意思？如果我们要严肃对待这个问题，就必须找到某种不依赖"常识"和"显然"的解释。

自然语言是有歧义的。"或"在不同语境下可能是"至少一个"也可能是"恰好一个"。"如果……那么……"在日常用法里千变万化——"如果你考上了就请你吃饭"和"如果这个算法正确那么复杂度是 $O(n\log n)$"，这两个"如果"的逻辑结构完全不同。

形式化的目的不是让语言变得难看，而是消除歧义。我们需要一套符号，每个符号只有一个含义，由定义给出，不依赖语境，不依赖常识。

兔狲教授评

常识不是数学，这句话说得很好。但别以为形式化就是把常识翻译成符号。形式化是在强迫你承认：你那些"显然"里藏着多少从没想清楚的东西。符号只是逼你原形毕露的工具，不是答案本身。就这样。

---

14.2 命题：推理的原材料

最小的推理单元是命题——一个可以被断言为真或假的陈述。"今天下雨"是命题。"下雨"不是，因为它没有断言任何事情。"这句话是假的"看起来是命题，但它制造了自指悖论——我们先把它放在一边，第15章会正面处理它。

命题用大写字母 $P,Q,R,\dots$ 表示。复杂的命题由简单命题通过逻辑连接词组合而成：

符号	读法	含义
$\mathrm{\neg }P$	非 $P$	$P$ 的否定
$P\wedge Q$	$P$ 且 $Q$	两者都成立
$P\vee Q$	$P$ 或 $Q$	至少一个成立
$P\to Q$	若 $P$ 则 $Q$	$P$ 成立时 $Q$ 必定成立
$P\leftrightarrow Q$	$P$ 当且仅当 $Q$	两者同真同假

这些符号的含义由精确的规则给出，不是约定俗成的。$P\to Q$ 的意思不是"$P$ 导致 $Q$"，不是"$P$ 在时间上先于 $Q$"，而只是：不存在 $P$ 为真而 $Q$ 为假的情况。这个定义可能比你的直觉更冷酷——"如果月亮是方的，那么 2 + 2 = 5"在这个定义下是真命题——但正是这种冷酷让数学推理成为可能。

为什么接受这个反直觉的定义？

逻辑连接词不是在描述因果，而是在约束推断的合法性。$P\to Q$ 的问题是：如果你接受了 $P$，你是否被迫也要接受 $Q$？只有在 $P$ 为真、$Q$ 为假时，答案才是否定的——所以那是唯一要排除的情况。前件为假时，蕴含式不构成任何约束，整体视为真。代价是"真命题"不再等于"有意义的命题"。这个代价，数学家认为值得付。

---

14.3 形式系统：给推理划定游戏规则

有了命题的语言，下一步是说清楚什么样的推断是合法的。这就是形式系统的工作。

一个形式系统 $\mathcal{F}$ 由四个部分组成：

语言 $\mathcal{L}$：规定哪些符号串是合法的命题。就像中文的语法规定哪些字符串是合法的句子，形式语言的语法规定哪些符号串是合法的公式。

公理 $\mathcal{A}$：一批被直接接受为真的命题，无需证明。比如命题逻辑里的 $P\to (Q\to P)$——不管 $P$ 和 $Q$ 是什么，这个式子总是成立的。公理是整个系统的起点。

推断规则 $\mathcal{R}$：从已有命题推出新命题的合法步骤。最基本的一条叫做假言推理（Modus Ponens）：如果你知道 $P\to Q$，也知道 $P$，那么你可以得出 $Q$。写成横线形式就是：

$$\frac{P\to QP}{Q}$$

横线上是前提，横线下是结论。这不是在描述什么是"真"的，而是在规定什么样的推断步骤是允许的。

证明：把公理和推断规则连接起来的有限序列。一个证明是一列命题 $A_1,A_2,\dots ,A_n$，其中每个 $A_i$ 要么是公理，要么是对前面某些命题应用了某条推断规则的结果。最后一个命题 $A_n$ 就是这个证明所证的定理。

当我们说 $\mathcal{F}⊢A$——读作"$A$ 在 $\mathcal{F}$ 中可证"——意思是存在这样一个证明序列，以 $A$ 结尾。

---

14.4 证明是句法对象

这里有一个关键的哲学立场值得停下来想一想。

在形式系统里，证明是一个句法对象——一个符号串的序列，可以被机械地检验。验证一个证明不需要理解它在"说什么"，只需要检查每一步是否合法应用了某条推断规则。

这意味着什么？它意味着一台机器——不理解数学，不知道"真"是什么意思，只会做符号匹配——可以验证任何形式证明的正确性。现代定理证明助手（Lean、Coq、Isabelle）正是这样工作的：你写证明，机器检查符号。

验证 vs. 发现

注意这里的非对称性。验证一个证明是机械的，多项式时间可完成——只需逐步检查每条推断规则是否合法。发现一个证明是另一回事：没有通用算法能在任意情形下保证找到证明（第15章会说明这是不可能的）。这个不对称性贯穿整个可计算性理论，也是"NP问题"令人困惑的根源之一。

这不是数学的终结，而是数学的一个深刻特性：数学真理是可以被机械验证的。我们不必依赖权威，不必信任直觉，只需要检查符号串。

当然，想出证明的过程——发现正确的推断路径——不是机械的，也许永远不会是。但验证是机械的，这一点已经足够深刻。

兔狲教授评

这里容易飘。"机器可以验证证明"不等于"机器理解了证明"。验证是对符号串做模式匹配，和"理解"没有关系。把"可机械验证"当成数学的荣耀来讲，你得先想清楚你在夸的到底是什么。验证的是形式，不是意义。

---

14.5 上下文：假设的簿记

现实的推理很少从零开始。通常我们说："假设 $P$ 成立，那么可以推出……"。这种带假设的推理需要一个记录假设的地方，叫做上下文，用 $\mathrm{\Gamma }$ 表示。

$\mathrm{\Gamma }⊢A$ 读作：在假设集 $\mathrm{\Gamma }$ 下，$A$ 可被推导出来。

比如 $\{P\to Q,P\}⊢Q$ 说的是：假设"若 $P$ 则 $Q$"和"$P$"，可以推出 $Q$。

上下文看起来是个簿记工具，但它的行为方式决定了整个逻辑系统的性质。有三条关于上下文的基本规则，通常在后台默默运行，以至于大多数人从未意识到它们的存在：

弱化：如果在假设 $\mathrm{\Gamma }$ 下能推出 $A$，那么有了更多假设也能推出 $A$——多余的假设不会造成伤害。这很直觉，但它说的是：假设集里可以有永远用不到的东西。

收缩：同一个假设可以被使用任意多次。你知道 $P$，可以用它一次，也可以用它一百次，不会有任何损耗。

交换：假设的顺序无关紧要。$\{P,Q\}$ 和 $\{Q,P\}$ 是一样的。

这三条规则在经典逻辑里是理所当然的——资源无限，顺序无关。但第16章会拿走收缩规则，这一改动会让整个逻辑的性质发生根本变化：每个假设恰好只能用一次，推理变成了资源管理。

兔狲教授评

大多数人学了十年逻辑，从来不知道自己一直在默默使用这三条规则。这不是额外知识，这是你推理的地基。你连地基是什么都不知道，就在上面盖楼——盖出来的东西你自己都不知道为什么能站。名字的缺席，不等于它们不存在。

这三条规则为什么值得命名？

因为它们并不是"逻辑本身"，而是关于逻辑的元选择——选择了它们，你得到经典逻辑；拒绝它们中的某一条，你得到不同的逻辑体系。大多数数学课完全不提这三条规则，因为在经典语境下它们从不违反。但正是这种"不言而喻"掩盖了逻辑的可选择性。形式系统能做的事情之一，就是让这些隐藏的选择变得可见。

---

14.6 语义：符号背后的含义

形式系统在句法层面操作符号。但我们通常希望这些符号"有含义"——对应某个真实的世界或数学结构。

给命题赋予含义的方式叫做赋值：把每个命题变元映射到真或假。在给定赋值下，复合命题的真值由连接词的规则递归确定——$P\wedge Q$ 在 $P$ 和 $Q$ 都为真时才为真，$P\to Q$ 在 $P$ 为假或 $Q$ 为真时为真，等等。

如果一个命题在所有赋值下都为真，称它为重言式，记 $\models A$。这是语义层面的概念——$A$ 不管命题变元取什么值都成立。

现在有两个层面需要区分：

• $\mathcal{F}⊢A$：在句法层面，$A$ 有一个形式证明
• $\models A$：在语义层面，$A$ 是重言式

这两个层面之间的关系是形式逻辑的核心问题：

可靠性：若 $\mathcal{F}⊢A$，则 $\models A$。系统只证明真的东西，不说谎。

完备性：若 $\models A$，则 $\mathcal{F}⊢A$。所有真的东西系统都能证明，没有遗漏。

命题逻辑的标准形式系统同时满足这两个性质。一阶谓词逻辑也是——哥德尔 1930 年证明了这一点，那是他最后一次带来好消息。一年之后，他带来的是完全不同的东西。

---

14.7 系统越强，代价越大

不同的形式系统有不同的表达能力，从弱到强大致排列如下：

命题逻辑：只处理命题和连接词，无法谈论"所有"和"存在"。足够简单，可以被机械判定——存在算法，对任意命题，在有限步内判断它是否是重言式。

一阶谓词逻辑：加入量词 $\mathrm{\forall }$（对所有）和 $\mathrm{\exists }$（存在），可以表达"所有自然数都有后继"这类陈述。完备，但不可判定——不存在通用算法判定一个一阶命题是否可证。

皮亚诺算术（PA）：在一阶逻辑上加入自然数的公理，强大到可以表达初等数论中几乎所有陈述。正是在这个层级，哥德尔的噩耗到来。

集合论（ZFC）：现代数学的通用语言，几乎所有数学对象都可以在其中编码和研究。

这个层级有一个规律：越强的系统，表达能力越大，但自我验证的能力越小。命题逻辑简单到可以穷举检查自身；皮亚诺算术强大到连自身的一致性都无法证明。强大有强大的代价。这个代价，正是下一章要算清楚的账。

为什么"更强"会带来自我验证的失能？

直觉上：一个足够强的系统能谈论自己，而一旦能谈论自己，就能构造关于自身的悖论性陈述。弱的系统无法表达"我自己的命题"，所以不会遇到这个问题。这就像语言一样——越表达能力丰富的语言，越容易产生自指悖论；简单的形式语言，恰恰因为无法自我指涉而安全。哥德尔发现的不是数学的缺陷，而是表达能力的内在代价。

---

14.8 实战：写出第一个形式证明

在继续之前，停下来做一件事：写一个真实的形式证明序列。不是"理解它在说什么"，是真的写出来，每行注明它从哪里来。

这会让接下来的一切变得不同。

---

我们用命题逻辑的一个极简系统，公理只有两条（这是 Łukasiewicz 的简化版本，足够我们练习）：

公理模式 L1：$P\to (Q\to P)$

公理模式 L2：$(P\to (Q\to R))\to ((P\to Q)\to (P\to R))$

唯一推断规则：假言推理（Modus Ponens）：从 $P$ 和 $P\to Q$ 推出 $Q$。

公理模式的意思是：用任意命题变元替换 $P,Q,R$，得到的结果都是公理。比如 $A\to (B\to A)$、$A\to ((A\to B)\to A)$、$(C\to C)\to (C\to C)$，全部都是 L1 的实例。

---

目标：证明 $P\to P$（一个命题蕴含它自身）。

这看起来显然——但在这个系统里，它不是公理，必须从公理推出来。

给你一个脚手架，试着填写每行的来源（公理实例，还是对哪两行应用 MP）：

行号	命题	来源
1	$P\to ((P\to P)\to P)$	L1，其中 $Q$ 取 $P\to P$
2	$(P\to ((P\to P)\to P))\to ((P\to (P\to P))\to (P\to P))$	？
3	$(P\to (P\to P))\to (P\to P)$	？（对第1、2行用 MP）
4	$P\to (P\to P)$	？
5	$P\to P$	？（对第3、4行用 MP）

第2行是 L2 的一个实例——找出 $P,Q,R$ 各取什么值才能得到这一行。第4行是 L1 的一个实例——同样找出对应的 $P,Q$。

填完之后，你就完成了一个完整的形式证明：五行，每行有明确来源，不依赖任何直觉，只靠符号操作。

这个证明的意义不在于 $P\to P$ 这个结论，而在于你亲身体验了"证明是句法对象"的含义——每一步都是机械的符号检查，没有任何"显然"。

---

悬而未决

形式化能捕捉所有推理吗？ 数学家在实际工作中依赖大量非形式的直觉——某个构造"应该"有效，某个证明"显然"可以推广。这些直觉能被形式化吗？还是说形式系统本质上遗漏了推理的某个不可言说的维度？

公理的选择是客观的吗？ 不同的公理集合给出不同的数学宇宙。选择公理——ZFC 里最有争议的公理——并非"显然"正确，数学家们为此争论了一个世纪。形式化把这个争论变得更清晰了，但并没有解决它。

这台机器可靠吗？完备吗？ 我们建造了形式系统，描述了它的语言、公理、推断规则，也区分了句法和语义。但有一个问题我们一直没有正面回答：它证明出来的东西，都是真的吗？所有真的东西，它都能证明吗？这两个问题的答案，一个令人欣慰，另一个令人震惊。第15章正面处理它们。

---

思考题

★ 热身

以下符号串，哪些是合法的命题公式？哪些不是？不需要给理由，只需要判断。

1. $P\to Q\wedge R$
2. $\mathrm{\neg }\mathrm{\neg }P$
3. $\wedge PQ$
4. $(P\to Q)\to (\mathrm{\neg }Q\to \mathrm{\neg }P)$
5. $P\to$

（提示：合法的命题公式由命题变元、连接词、括号按语法规则组合而成。连接词是二元或一元的运算符，不能单独出现在末尾。）

---

★★ 推导

以下三个断言，哪些成立？用自然语言说清楚理由，并指出每条断言依赖了本章哪个概念（推断规则、弱化、收缩、还是演绎定理）。

1. 若 $\mathrm{\Gamma }⊢P\wedge Q$，则 $\mathrm{\Gamma }⊢P$。
2. 若 $\mathrm{\Gamma }⊢P$ 且 $\mathrm{\Gamma }⊢Q$，则 $\mathrm{\Gamma }⊢P\wedge Q$。
3. 若 $\mathrm{\Gamma },P⊢Q$，则 $\mathrm{\Gamma }⊢P\to Q$。

第三条叫做演绎定理。它说的是：在假设 $P$ 的条件下能推出 $Q$，等价于不用这个假设就能推出"$P$ 蕴含 $Q$"。这条规则的意义是：假设可以被"吸收"进蕴含连接词里。想清楚这个吸收是在句法层面还是语义层面发生的。

---

★★★ 挑战

演绎定理是一个关于形式系统的元定理，不是系统内部的一条公理或推断规则。试着用本章引入的语言（$⊢$、上下文 $\mathrm{\Gamma }$、推断规则），精确写出"元定理"和"系统内定理"的区别是什么。

进一步：演绎定理本身能在某个形式系统内被证明吗？还是它必须在系统之外，用数学归纳法对证明长度做归纳来建立？这个问题的答案，和第15章里"系统无法证明自身一致性"之间有什么关联？不需要解决，只需要用本章的语言把这个问题陈述清楚。