证明与语义表

1. 什么是证明

论证是这样一种主张：某个结论可以从若干前提推出。证明则是了断这一主张的东西：一个有限的、可核验的对象，任何人都能逐行读下来并且认可，不必听信你的一面之词。证明的意义不在于它令人信服——一场好的演讲同样令人信服——而在于其中的每一步都不可能是别的样子。

这个要求比听上去更严格。「下雨了，所以地面是湿的」说得很在理，但它倚仗你关于雨和地面的知识。形式逻辑把这些剥去，转而提出一个更窄的问题：仅就句子的形式而言，前提为真而结论为假，究竟有没有哪怕一种可能？如果一种也没有，论证就是有效的，而证明就是这种可能不存在的记录。

本指南讲的是产生这份记录的一种方法——语义表法，也叫真值树。你在计算器里输入一个论证时，本站用的正是这个方法；只要跟着走过一遍，你就能只凭一支笔在纸上核验一个论证。

2. 有效，以及你怎么知道

用推断符号写下一个论证：前提在左，结论在右。p → q, ¬q ⊨ ¬p 这一主张是说，从一个条件句和它后件的否定，可以推出它前件的否定。推断符号不是又一个联结词。它是关于两侧公式的一个主张，非对即错。

有效性的定义直接指出了检验的办法：把变元的每一种真假指派都过一遍，看看有没有哪一种能让所有前提为真而结论为假。真值表做的就是这件事，变元只有两三个时它完全够用。麻烦在于表的规模按 2ⁿ 增长。十个变元要一千行，二十个要一百万行，而且表并不告诉你哪几行才是关键。

表列则从另一头攻这同一个问题。它不去罗列所有可能再从中找出坏的那一种，而是先假定存在一种坏的，然后试着把它造出来。如果这一尝试在它可能走的每条路上都坍缩为矛盾，那么这样的指派并不存在，论证有效。如果尝试成功了，造出来的东西就是一个可以直接读出的反例。

3. 表列法

表列是一棵由带号公式构成的树。每一行都是一个前面标着 T 或 F 的公式，这个符号说明该枝对这个公式作了什么假定——不是它的真值是什么，而是要让论证垮掉，它得是什么。整套方法只有四步：

1. 把每个前提写成带 T 的。你在假定论证的所有前提都成立。
2. 把结论写成带 F 的。你在假定它偏偏不成立——这就是你要驳倒的那个假设。
3. 取任意一行还不是原子的公式，按它的主联结词和符号套用相应规则，把规则产出的内容加到经过该行的每一条枝的末端。
4. 一旦某条枝上同时出现同一公式 A 的 T A 与 F A，就把它关闭。当所有枝都关闭，或者再没有可分解的行时停止。

这个循环里既不需要机巧，也不需要选择策略。每一行恰好对应一条规则，按任何次序套用都会得到同样的裁断——这正是机器能够胜任的原因，也是机器给出结果时你可以信赖它的原因。

4. 规则

每个联结词在每个符号下各有一条规则，共十条。它们分成两类，而两类之间的差别正是表列之所以是树而不是清单的全部理由。α 规则说的是若干件事必须同时成立，于是把结果沿着枝一路堆叠下去。β 规则说的是两件事必居其一，于是把枝一分为二，让每种情形各走各的路。

每条规则不过是它那个联结词的真值条件倒过来读。合取只有两边都真才真，所以 T (A ∧ B) 把 T A 和 T B 堆叠起来。合取只要有一边为假就假，可公式并不说是哪一边，所以 F (A ∧ B) 不得不两边都试：它分枝。析取那里同样的不对称反过来起作用；而条件句为假意味着前件成立、后件落空——这是蕴涵唯一会破的情形。

请留意规则从不做的事：它们从不凭空造出公式。规则产出的一切，都是它所来自那一行的一个片段。这个性质，即子公式性质，正是使该方法有限的原因，下面我们还会回到它。

5. 关闭一条枝

一条枝就是一条完整的推理线索：从根读到叶，你就得到一整套假定。当这些假定彼此正面矛盾时，也就是同一个公式的 T A 与 F A 同时出现在这条枝上时，这条枝就关闭了。A 有多复杂、两行相隔多远都无关紧要——只要一条枝要求某个公式既真又假，就没有任何东西能满足它。

给关闭的枝标上 ×，写明是哪两行让它关闭的，然后不再在这条枝上花工夫。一个本就不可能的假定，再没有什么可学的了。

当每一条枝都关闭时，表列就是封闭的，这便是证明。它表明你出发时的那个设想——所有前提为真、结论为假——在它可能走的每一条路上都通向矛盾。既然没有路剩下，这样的指派就不存在，论证有效。这是一个反证法，只不过摊开成了不会漏掉任何情形的样子。

6. 逐行看一个证明

以否定后件式为例：p → q, ¬q ⊨ ¬p。第 1、2 行是假定为真的前提。第 3 行是假定为假的结论——而结论既然是 ¬p，假定它为假就是假定 p 为真，这一点由第 5 行记下。第 4 行来自把否定规则用在第 2 行上：¬q 为真，则 q 为假。第 1 行的条件句是唯一还带联结词的行，而它属于 β 规则，于是树就分叉了：

左枝假定条件句之所以成立是因为它的前件落空——可第 5 行已经有 p 为真，于是这条枝自相矛盾而关闭。右枝假定它之所以成立是因为它的后件为真——可第 4 行已经有 q 为假，于是它也关闭。

两条枝都关闭了，所以无从让 p → q 与 ¬q 为真而 ¬p 为假。论证有效，而这棵树就是理由。请注意，这个证明自始至终没有提到雨、地面，也没有提到 p 和 q 代表什么。它不需要。

7. 当一条枝始终敞着

并非每个论证都有效，而这正是该方法见真章的地方。如果你把一条枝做到再没有什么可分解——只剩下原子和被否定的原子——它却仍未关闭，那么这条枝就是饱和且敞开的。它没有关闭并不是因为你收手太早，而是确实无可再试。

一条敞开的枝不止是一句「无效」的裁断。读出它那些原子上的符号，你就得到一个指派：凡标 T 的原子为真，凡标 F 的原子为假。这个指派让每个前提为真、让结论为假，而这正是反例的定义。逻辑学家称之为反模型；它是对「为什么不行」的一个具体回答，而不是一句拒绝。

肯定后件式，p → q, q ⊨ p，就是教科书上的例子。它的表列留下一条敞开的枝，其中 p 为假、q 为真——条件句成立，它的后件也成立，前件却不成立。仅这一个指派就足以驳倒该论证。

8. 为什么它总会结束

每条规则都把一个公式换成它自己的子公式，而任何子公式都严格短于它所来自的公式。因此没有哪条枝能无止境地长下去：每一步都沿着一架由原论证的碎片搭成的有限梯子往下走，而梯子是有底的。到最后，一条枝上的每一行都是原子或原子的否定，再没有什么可做。

这是一个实实在在的保证，而不是一种指望。它意味着该方法是命题逻辑的一个判定程序：拿任何论证去跑，它都会停下来，给出一棵封闭的树或者一条敞开的枝，而绝不会耸耸肩了事。本站的证明器在此之上还设了节点上限，但那只是防止某个病态公式耗尽浏览器标签页——数学本身并不需要这样的限制。

9. 其他证明系统

表列只是若干证明系统之一，而且是反驳形态的那一种：它靠排除失败来工作。自然演绎则反其道而行，用否定前件式、条件证明之类的规则，从前提出发向前搭出结论，读起来更像数学家用散文论证的样子。自然演绎的证明通常更短；找到它通常更需要巧思。

相继式演算把推断符号本身形式化，把推断主张当作对象来处理，因而是想要证明关于证明的命题时的首选工具。归结法把一切归约为子句和唯一一条规则，读起来乏味，跑起来却极快——多数自动定理证明器和 SAT 求解器都建立在它之上。

对于哪些命题论证有效，它们的答案完全一致；它们的分别在于证明长什么样，以及什么容易找到。就学习而言，表列最为友善，因为一个失败的证明并非死路——它顺手把反例交到你手上。

10. 练习

学会这个方法最快的办法就是动手跑一遍。用 ⊨、⊢ 或 |= 在计算器里输入一个论证，表列会画在真值表旁边，你可以拿树去对照各行。然后先在纸上做几个证明，再去看答案。