命题演算
词与符号
前面的对话使人回想起刘易斯·卡罗尔的二部创意曲。在两个场合，乌龟都不肯以规范正常的方式去用规范正常的词------或者说，至少当那么做对他不利时，他就不肯那么做。上一章，我们给出了用来思考卡罗尔悖论的一种方式。在这一章里，我们要让一些符号去做阿基里斯没能让乌龟用词去做的事。这就是说，我们将要构造一个形式系统，其符号集中有一个符号要做的，正是阿基里斯希望”并且”这个词被乌龟说到时会去做的事。符号集中还有一个符号，将起到”若…则…”这个词组所应该起的作用。另外，还有两个词是我们想要处理的：“或”和”非”。只依赖于正确使用这四个词的那种推理，叫作命题推理。
字母表及命题演算的第一条规则
我将要介绍的这个新的形式系统称为命题演算。它有点像一个谜题：并不马上把每一件事都解释清楚，而是让你自己多多少少把这些事情想出来。我们从符号表开始：
我要披露的这个系统的头一条规则是：
联结规则：如果x和y都是系统的定理，那么串＜xy＞也是该系统的定理。
这条规则取来两个定理并且把它们组合成一个。这会使你回想起刚才的对话。
良构串
还有一些其它的推理规则，我们都将简要地加以介绍------但是首先，有一点是很重要的：我们要定义所有串的一个子集，即”良构串”的集合。它们是用递归的方式来定义的。我们先从这里开始：
原子：P、Q、R都称作原子。新的原子是在老的原子的右上角加撇构成的------比如，R、Q”、P”等等。这便使我们可以源源不断地提供原子。所有的原子都是良构的。
然后我们有四条递归的规则：
形成规则：如果x和y都是良构的，那么以下的四种串也都是良构的：
(1) ～x
(2) ＜xy＞
(3) ＜xy＞
(4) ＜xy＞
举例来说，下列所有的串都是良构的：
P 原子
～P 根据(1)
～～P 根据(1)
Q 原子
～Q 根据(1)
＜P～Q＞ 根据(2)
～＜P～Q＞ 根据(1)
＜～～PQ＞ 根据(4)
＜～＜P～Q＞＜～～PQ＞＞ 根据(3)
最后的一个看起来似乎有点庞大，但它是直接由两个组份构造起来的------这两个组分就是刚好在它上面的那两行。而它们之中的每一个本身又都是由再前面的行构造起来的…如此等等。每一个串都可以用这种方法追溯到它的基本成分------这就是原子。你可以简单地往回运用形成规则，直到你不能再往下用为止。这个过程保证会终止，因为每一条形成规则（当向前运用时）都是一条加长规则，所以往回运用它总能把你带到原子那里去。
这种把串进行分解的方法于是就可以用来核对任何一个串是否良构。这是一个对良构的自顶向下的判定过程。为了考察一下你对这种判定过程的理解，你不妨来核对一下，下面的这些串当中哪些是良构的：
(1) ＜P＞
(2) ＜～P＞
(3) ＜PQR＞
(4) ＜PQ＞
(5) ＜＜PQ＞＜Q～P＞＞
(6) ＜P～P＞
(7) ＜＜P＜QR＞＞＜～P～R＞＞
(8) ＜PQ＞＜QP＞
（答案：那些编号为斐波那契数的串不是良构的，其余的都是。）
再给几条推理规则
现在我们来看其余的规则，这些规则可用来构造这个系统的定理。下面是几条推理规则。在所有这些规则里，符号”x”和”y”总是理解为只限于良构的串。
分隔规则：如果＜xy＞是一个定理，那么x和y都是定理。
附带说一下""这个符号代表什么概念，你现在该有一个相当不错的猜测（提示：它就是前面的对话中那个引起麻烦的词）。而从下面的规则里，你将能够想象出弯号（”～“）相当于什么概念：
双重弯号规则：像”～～“这样的串可以从任何定理中删去。它也可以嵌入到任何定理之中，条件是所得的结果是良构串。
幻想规则
我们看到，这个系统的一个特别之处在于它没有公理------只有规则。如果你回过头想一下先前我们看到过的形式系统，你可能就会奇怪：怎么才能有定理呢？事情怎么才能开始呢？回答是有那么一条规则，它无中生有地制造定理------它不需要一个”老定理”作为输入（其他的规则都是要求输入的）。这个特别的规则被称为幻想规则。我这样称呼它，理由很简单。
在使用这条幻想规则时，你做的第一件事是写下一个随你喜欢的任何良构串X，然后用提问的方式来将其”幻想一下”：“假如这个串x是一个公理，或者是一个定理，将会怎么样？“。然后，你就让系统自己来给出回答。也就是说，你继续往下做，把x当作起始行造一个推导，并让我们假设y是结束行（当然，这个推导必须严格地遵循该系统的规则）。从x到y所得的每一样东西（包括x和y在内）都是幻想，x是幻想的前提，而y是幻想的结果。下一步是从幻想中跳出来，这时，我们可以肯定的是
假如x是一个定理，那么y就会是一个定理。
到此，你也许会奇怪：真正的定理在哪里呢？真正的定理是这个串
＜xy＞
注意这个串与印在上面的那个句子是一回事。
为了标识进入一个幻想的入口和离开一个幻想的出口，我们分别用方括号”[“和”]“。于是，只要你看到一个左方括号，你就知道你正在”推”入一个幻想中，而下一行将会包含该幻想的前提。每当你看到一个右方括号，你就知道你正在”弹”出来，并且上一行正是结果。把在幻想中产生的推导的那些行凹进去写，是会有所帮助的（但这并不是必须的）。
这里有一个关于幻想规则的例示，其中串P作为前提。（当然，P碰巧不是一个定理，但是这并不要紧。我们只是在寻问：“假如它是，会怎么样？”）。我们制造如下的幻想：
[ 推入幻想
P 前提
～～P 结果（根据双弯号规则）
弹出幻想
这个幻想说明：
假如P是一个定理，那么～～P也就是一个定理。
我们现在把这个中文（这是元语言）句子”压挤”成形式化的记号（这是对象语言）：＜P～～P＞。这个东西------我们的第一条命题演算的定理------会向你显示""这个符号的预期解释。
这里是另一个运用幻想规则的推导：
[ 推入
＜PQ＞ 前提
P 分隔
Q 分隔
＜QP＞ 联结
弹出
＜＜PQ＞＜QP＞＞ 幻想规则
有一点很重要：必须理解只有最后一行才是一条真正的定理------剩下的都是在幻想之中的。
递归和幻想规则
正如你从”推入”和”弹出”这两个递归术语可以猜测到的，幻想规则是能够递归地使用的------于是，幻想中可以有幻想，然后再次套进幻想，如此等等。这意味着存在有各种各样的”有关现实的层次”，正像在嵌套的故事里或电影中一样。当你从一个电影中的电影里弹出来时，有那么一会儿你感到你好像已经到达了现实世界，但事实上你离开顶层还差一个层次。同样，当你从一个幻想中的幻想里弹出来时，你是在一个比你刚才所在的要”更现实一些”的世界里，但是你离顶层还差一个层次。
我们来看：在电影院里”请勿吸烟”的牌子，对电影里的人物是不适用的------在演电影时，是不会把它从现实世界搬入到幻想世界里去的。但是在命题演算的情形，却可以有从现实世界到幻想里去的搬入，甚至还有从一个幻想到它所含的幻想里去的搬入。这可以由下面的规则来形式化：
搬入规则：在一个幻想里边，任何来自于”现实性”高一个层次的定理都可以拿进并使用。
这就像电影院里的一块”请勿吸烟”牌子不仅适用于所有的电影观众，还适用于电影里的所有演员，而且，只要重复这同样的想法，对于在多层嵌套电影里的任何人也就都适用了！（提醒：不能有相反方向的搬动：在幻想里面的定理不可以搬到外头来！如果不是这样，你就可以写任何东西作为一个幻想的第一行，然后把它拎出到现实世界中当成一个定理了。）
为了说明搬入是怎样起作用的，并且说明幻想规则是怎样能够递归地使用的，我们给出如下的推导：
[ 推入
P 外层幻想的前提
[ 再次推入
Q 内层幻想的前提
P 把P搬入到内层幻想
＜PQ＞ 联结
] 弹出内层幻想，回到外层幻想
＜Q＜PQ＞＞ 幻想规则
弹出外层幻想，到达现实世界！
＜P＜Q＜PQ＞＞＞ 幻想规则
注意，我把外层幻想凹进去一次，而把内层幻想再次凹进去，以强调这些嵌套着的”现实性层次”的特性。可以从这样一种角度去看幻想规则，就是说，一个对于系统的观察被嵌入到这个系统中。也即，被产生出来的定理可以看成是”如果x是一个定理，那么y也是”这样一个关于系统的句子在系统内的一个表示。更精确一点，对＜PQ＞来说，它的预期解释就是”若P，则Q”，或者等价地说，“P蕴涵Q”。
幻想规则的逆规则
现在我们看到，刘易斯·卡罗尔的对话都是关于”若-则”语句的。特别是，阿基里斯在劝导乌龟接受一个”若-则”语句的第二个子句时遇到了极大的麻烦，尽管这是在这个”若-则”语句的第一个子句以及这个”若-则”语句本身都已经被接受的时候。下一个规则是让你去推断一个""串的第二个”子句”，前提是该""串本身是一个定理，并且它的第一个”子句”也是一个定理。
分离规则：如果x和＜xy＞二者都是定理，那么y是一个定理。
附带说一下，这条规则常常被称作”Modus Ponens”，而幻想规则常常被称为”演绎定理”。
符号的预期解释
这时候我们应该来戳穿戏法了，即披露出我们的这个新系统中其他符号的”意义”。现在该点明了，我们是打算让符号""与普通的日常用词”并且”起的作用相同。符号”～“表示”非”这个词------是否定的一种形式化变种。尖括号”＜“和”＞“是用来分组的------它们的功能非常类似于普通代数中的括弧。其主要的不同在于：在代数里，你可以任意写进一对括弧或省略它们，全凭趣味和风格，而在一个形式系统里，这种无政府主义的自由是不被容忍的。符号""代表”或”这个词（“或”的拉丁文是”vel”）。我们所指的”或”是所谓的”相容或”，它意味着＜xy＞的解释是”或者是x或者是y------或者二者都是”。
唯一我们还没有解释的符号就是原子了。一个原子没有唯一的解释------它可以用任何中文句子来解释（如果这个原子是在一个串或一个推导中多次出现的，则必须在处处都用同样的句子来解释）。因此，举例来说，＜P～P＞这个良构串就可以解释成复合句
心是佛，并且心不是佛。
现在让我们来看看迄今所推得的每一条定理，并且来解释它们。第一个是＜P～～P＞。如果我们保持对P作同样的解释，我们就有如下的解释：
若心是佛，
则并非心不是佛。
注意我是怎样来转述双重否定的。在任何自然语言里，将一个否定重复两次总是很别扭的，所以为了避免这样，我们就用两种不同的方式来表示否定。我们推得的第二个定理是＜＜PQ＞＜QP＞＞。如果我们把Q用句子”麻三斤”来解释，那么我们的定理读起来就会像下面这样：
若心是佛且这块麻重三斤，
则这块麻重三斤且心是佛。
第三个定理是＜P＜Q＜PQ＞＞＞。它变成了如下的嵌套的”若-则”句子：
若心是佛，
则：若这块麻重三斤，
则心是佛且这块麻重三斤。
你可能已经注意到了，每个定理被解释时说了些完全不足道的、自明的事情。（有时它们是如此自明，以至于它们听起来让人觉得空洞，而且------特别奇怪地------是混乱的或者甚至是错的！）这一点可能不会给人们深刻的印象，但只须记住，客观上存在着很多可能会产生出来的假命题------虽然它们并没有被产生出来。这个系统------命题演算------是一步步很干净地从真走到真，仔细地回避所有的假。正像一个人一心要不弄湿脚，他就会在小河里小心地一步步从一块蹬石走到下一块，完全遵照蹬石的布局，而不管它可能是如何地曲来拐去和难走。给人印象深刻的东西是------在命题演算中------所有的事情是纯粹”符号地”做出来的。没有谁置身其中成为”里边的人”，去考虑这些串的意义。它做起来完全是机械的，不经思考的，硬性规定的，甚至是傻乎乎的。
把规则的清单列全
我们还没有说完命题演算的所有规则。完整的一组规则开列在下面，其中包括三条新的。
联结规则：如果x和y是定理，那么＜xy＞是个定理。
分隔规则：如果＜xy＞是个定理，那么x和y二者都是定理。
双弯号规则：”～～“这个串可以从任何定理中删除。它也可以嵌入到任何定理中去，只要所得的结果本身是良构串。
幻想规则：如果假定x是一个定理时能推导出y来，那么＜xy＞是个定理。
搬入规则：在一个幻想里边，任何来自于”现实性”高一个层次的定理都可以拿进并使用。
分离规则：如果x和＜xy＞二者都是定理，那么y是个定理。
易位规则：＜xy＞与＜～y～x＞是可互换的。
德·摩根规则：＜～x～y＞与～＜xy＞是可互换的。
思维陀螺规则：＜xy＞与＜～xy＞是可互换的。
（思维陀螺规则是根据一个名叫斯维彻罗的人命名的，这人对陀螺极有兴趣，专门研究陀螺味道的逻辑学。）前述规则中的”可互换的”这个词的意思如下：如果一种形式的表达式作为一个定理或者一个定理的部分出现，就可以用另一种形式来替换，而且替换后得到的串依然还是个定理。必须把这个牢记在心里：符号”x”和”y”总是代表该系统的良构串。
对规则的论证
在我们看到这些规则被用在推导里边之前，让我们先来看看对它们的一些非常简短的论证。你也许能自己去论证它们，比用我的例子要更好------这就是为什么我仅仅只给出少数几个例子。
易位规则把一种我们不自觉地做出的，用来倒转条件语句的方式明确地表达了出来，例如，下面这个”禅述”
如果你正在学习”道”，
那么你就远离了它。
意味着下述同一件事
如果你接近了”道”，
那么你就不是正在学习它。
德·摩根规则可以用我们熟悉的句子”幡不在动，并且风也不在动”来说明。如果用P来将”幡在动”符号化，用Q来将”风在动”符号化，那么这个复合句就可以用＜～P～Q＞来符号化。依照德·摩根律，这可以与～＜PQ＞互换，后者的解释是”或者幡在动或者风在动，这不真”。没有人能否认这是一个可以得出的合禅理的结论。
对于思维陀螺规则，考虑一下句子”或者一朵云正挂在山上，或者月光正在穿透湖水的波纹”，我假设这是一位冥想着的禅宗法师说的，他记得一个熟悉的湖，他能在心里摹想它，却不能看到它。现在请你留神：思维陀螺规则告诉我们的是，这与下述想法可以互换：“如果一朵云不挂在山上，那么月光正在穿透湖的水波。“这大概不能给你什么启发，但这是命题演算所能提供的最好的东西了。
摆弄这个系统
现在让我们把这些规则应用到一个先前的定理上去，并且看看我们能得到什么。例如，取定理＜P～～P＞：
＜P～～P＞ 老定理
＜～～～P～P＞ 易位
＜～P～P＞ 双弯号
＜P～P＞ 思维陀螺
这个新的定理，当它被解释时，是说：
或者心是佛，或者心不是佛。
我们再一次看到，被解释了的定理虽然也许不那么惊人，但至少是真的。
半解释
当一个人把命题演算的定理大声念出来时，解释每样东西，但不解释原子，这是很自然的。我称之为半解释。例如，＜P～P＞的半解释就是
P或者非P。
即便事实上P不是一个句子，上面的”半句子”听起来仍然是真的，因为你能够很容易地想象在P处插入任何一个句子------这个被半解释了的定理的形式向你保证了，不管你如何作出你的选择，结果所得的句子都将是真的。而这正是命题演算的关键思想：它产生一些定理，当它们被半解释时，它们被看成是”普遍为真的半句子”，由此就意味着：不管我们怎样去把解释做完全，最后的结果总是一个真语句。
岩头之斧
现在我们可以来做一个更高级的练习，它基于一个称之为”岩头之斧”的禅宗公案。我们看看它是怎样开始的：
德山一日谓师（即岩头------译注）曰：“我这里有两僧入山，住庵多时，汝去看他怎生。“师遂将一斧去，见两人在庵内坐。师乃拈起斧曰：“道得也一下斧，道不得也一下斧。”1
如果你们说点什么，我就砍掉这个公案；如果你们不说什么，我也要砍掉这个公案------因为我想把它的某些东西翻译成我们的记法。让我们用P来将”道得（你们说点什么）“符号化，而”一下斧（我要砍掉你们的脑袋）“则用Q来符号化。于是岩头之斧的威吓就可用这样的串来符号化：＜＜PQ＞＜～PQ＞＞。假如这个斧子威吓是个公理的话，会怎么样呢？这里有一个幻想是来回答这个问题的。
(1) [ 推入
(2) ＜＜PQ＞＜～PQ＞＞ 岩头公理
(2) ＜PQ＞ 分隔
(4) ＜～Q～P＞ 易位
(5) ＜～PQ＞ 分隔
(6) ＜～Q～～P＞ 易位
(7) [ 再一次推入
(8) ～Q 前提
(9) ＜～Q～P＞ 把第4行搬入
(10) ～P 分离
(11) ＜～Q～～P＞ 把第6行搬入
(12) ～～P 分离（8和11行）
(13) ＜～P～～P＞ 联结
(14) ～＜P～P＞ 德·摩根
(15) ] 弹出一次
(16) ＜～Q～＜P～P＞＞ 幻想规则
(17) ＜＜P～P＞Q＞ 易位
(18) [ 推入
(19) ～P 前提（也是结果！）
(20) ] 弹出
(21) ＜～P～P＞ 幻想规则
(22) ＜P～P＞ 思维陀螺
(23) Q 分离（22和17行）
(24) ] 弹出
命题演算的能力在这个例子中显示了出来。嘿，不过是用了二十四步，我们推出了Q：两颗脑袋都要被砍掉！（不祥的是，我们最后祈求来帮忙的规则正是”分离”…）现在再继续这个公案看起来似乎是多余的了，因为我们知道会发生什么…然而，我还是放弃我要砍掉这个公案的决心。毕竟，它是一个真的禅宗公案。这里我们来讲述剩下的故事：
二人殊不顾。师掷下斧曰：“作家！作家！“归，举似德山，山曰：“汝道他如何？“师曰：“洞山门下不道全无，若是德山门下，未梦见在。”2
你看清楚我如何了吗？禅宗又是如何呢？
存在一个对定理的判定过程吗？
命题演算给我们一组规则来产生语句，这些语句在任何可想象的世界中都是真的。这就是它的所有定理听起来如此简单的原因：它们似乎完全没有内容！从这种角度去看，命题演算可以看成是浪费时间，因为它告诉我们的东西完全是不足道的。从另一方面来说，它是通过详细说明那些普遍真的语句的形式来做这件事的，而这使得宇宙里核心的真理看得更清楚了：它们不仅是基本的，而且是有规律的：它们能用一组印符规则产生出来。换句话说，它们全是”用同样的布裁出来的”。你可以考虑一下，对于禅宗公案能否说这同样的话。它们全能用一组印符规则产生出来吗？
提出判定过程这一问题，在这里正是时候。也就是说，有什么机械的方法来区别定理和非定理吗？如果有，就说明命题演算的定理的集合不仅是递归可枚举的，而且也是递归的。结果是，的确存在一个有趣的判定过程------真值表方法。在这里介绍这种方法多少有点离题。你可以在几乎任何一本标准的逻辑书中找到它。而关于禅宗公案怎么样呢？能想象有一个机械的判定过程把正宗的禅宗公案与其他的东西区分开来吗？
我们知道系统是一致的吗？
到现在为止，我们仅仅是假设了：所有的定理，当它们解释为表示什么时，都是真语句。但是我们确实知道是这么回事吗？我们能证明是这么回事吗？这正是换一种方式来问那些预期的解释（对""来说是”并且”，等等）是否有资格被称为符号的”被动意义”。一个人可以从两种非常不同的观点来看这个问题，我称它们为”严谨”观点和”马虎”观点。我现在根据自己的理解来介绍一下它们，并拟人化为”严谨”的观点和”马虎”的观点。
严谨：只有我们设法证明了它，我们才会知道所有的定理在预期的解释之下结果为真。这才是慎密的、考虑周到的行为方式。
马虎：正好相反。显而易见，所有的定理结果都将是真的。如果你不相信我，那么重新再看一下系统的规则。你将发现，每条规则都是使一个符号精确地按照它表示的那个词所应起的作用去起作用。举例来说，联结规则是使""这个符号去起到”并且”应该起的作用；而分离规则是使""去起到它应该起的作用，如果它是代表了”蕴涵”或者”若-则”的话；如此等等。只要你不是像乌龟先生那样，你将在每条规则里识别出一种规范化的模式，它是用于你自己的思维中的。所以，如果你信赖你自己的思维模式，那么你就必须相信，所有的定理到最后都为真！这就是我的看法。我不需要什么进一步的证明。如果你认为某个定理会是假的，那么可想而知，你大概是认为某条规则错了。是哪一条？指给我看看吧。
严谨：我不能断定有什么规则出了错，所以我不能为你指出来。但是，我还是能想象出下面这种场景。你根据这些规则往下推，遇到了一个定理------比如说是x。同时我也根据这些规则往下推，遇到了另外一个定理------它碰巧是～x。你能不能硬让自己设想一种这样的情景？
马虎：好，让我们假定这已经发生了。为什么这会使你烦恼呢？或者让我换一种方式来说。假定这是用WJU系统来摆弄的，我遇上了一个定理x，而你遇上了xU。你能不能硬让自己去设想一下这个？
严谨：当然------事实上WJ和WJU都是定理。
马虎：这不使你忧虑吗？
严谨：当然不。你的例子是荒谬的，因为WJ与WJU并不是矛盾的，而在命题演算中，两个串x和～x却是矛盾的。
马虎：那好，就算是的------但前提是你希望把”～“解释成”非”。但是你凭什么认为”～“一定就解释为”非”呢？
严谨：凭规则本身。当你考察它们的时候，你领悟到，对于”～“，唯一可以设想的解释是”非”------并且同样地，对""的唯一可以设想的解释是”并且”，等等。
马虎：换句话说，你相信规则抓住了这些词的意义了？
严谨：一点不错。
马虎：那么你还仍然乐意去接受x和～x都能是定理这样的想法吗？为什么不同样接受这样的观念：刺猬是青蛙，1等于2，月亮是由生奶酪做成的？对我来说，我不准备哪怕是考虑一下我思维过程的如此基本的成分是不是错了------因为一旦我接受了这种观念，那我也就必须考虑我分析整个问题的模式是不是也错了，从而我将卷入完全的混乱之中。
严谨：你的论证很有力…然而我还是希望能看到一个证明，所有的定理都为真，或者x和～x任何时候都不能同是定理。
马虎：你想要一个证明。我推测，这意味着比起你确信你自己的慎密来，你是想更确信命题演算是一致的。任何我能够想到的证明，都将包含比起命题演算中任何东西本身都更复杂的智力工作。因此，它能证明什么？你希望有一个关于命题演算一致性的证明的这种愿望，使我想到这么一个人------他正在学汉语------非要求给他一本这样的字典，里面对所有的简单的词都用复杂的东西来定义…
再谈卡罗尔对话
这场小小的辩论展示了，试图用逻辑和推理来维护它们自身是很困难的。到某一时刻，你就无路可退了：除了大声嚷嚷”我知道我是对的！“之外，并不存在这种维护。我们又遇到了刘易斯·卡罗尔在他的对话中尖锐地提出的论点：你无法永远维护你的推理模式。到了一定的地步，就只有靠信仰了。
一个推理系统可以比作一个蛋。蛋有一个壳来保护它里边的东西。当你想把一个蛋用船运到什么地方去，你当然不只信赖它的壳。你会把蛋装进某种形状的容器里，这是根据你所能设想的蛋的航程会多么艰难而选择的。你可能由于分外小心，而把蛋放在一些一层套一层的箱子里边。然而，不管你把你的蛋装进去的箱子层数有多少，你还是能想象会有某种灾难打破这个蛋。但是这并不意味着你永远也不冒险去运输你的蛋了。与此相仿，一个人永远也不能给出一个最终的、绝对的证明，去阐明在某个系统中的一个证明是正确的。当然，一个人可以给出一个关于一个证明的证明，或者关于一个证明的证明的证明------但是，最外层的系统的有效性总还是一个未经证明的假设，是凭我们的信仰来接受的。一个人总是能想象某种未曾料到的微妙之处，它使证明的每一个层次最终彻底完蛋，从而那个”已证”的结果也最终将被看作是不正确的。但是这并不意味着，数学家和逻辑学家总是持续地在担心，数学的整个大厦可能是错的。相反，一旦非正统的证明被提出来------有时是极为冗长的证明，有时是由计算机生成的证明------人们就停下来开始去想一想根据那个半神圣的词”已证”：它们究竟是个什么意思？
在这一点上，回到卡罗尔对话去，也许对你来说是一个极好的练习。我们把那个辩论的每个阶段译成我们的记法，而把争论的起因作为开始：
阿基里斯：如果你有了＜＜AB＞Z＞，并且你也有＜AB＞，那么你当然有Z。
乌龟：哦！你意思是：＜＜＜＜AB＞Z＞＜AB＞＞Z＞，是不是？
（提示：尽管阿基里斯考虑的是一条推理规则，乌龟却马上又把它降格成该系统的一个平凡的串。如果你只使用字母A、B和Z，你将得到一个产生越来越长的串的递归模式。）
捷径与导出规则
当在命题演算中进行推导时，人们很快就会发明各式各样的捷径，它们严格来说并不是该系统的组成部分。例如，如果在某个场合需要＜Q～Q＞这样的串，而＜P～P＞在早先已经被推导出来了，许多人会如同＜Q～Q＞已经被推导出来了那样而进行下去，因为他们知道，它的推导与＜P～P＞的推导是完全平行的。推导出的定理被当作一个”定理图式”------作为其他定理的模子。结果这变成了一个完美有效的过程，引导你去得到新的定理，但正如我们介绍它时指出的，它不是命题演算的一条规则。它是------说得更恰当一点------一条导出规则。它是我们所具有的关于该系统的那些知识的一部分。这条规则是否总是保证你从定理到定理，这一点当然需要证明------但这样的一个证明并不像在系统中的一个推导一样。它是一个普通的直观的意义上的证明------一个以W方式进行的一连串推理。这种关于命题演算的理论是一个”元理论”，而它里边的结果可以称作”元定理”------关于定理的定理（附带说一下，请注意在短语”关于定理的定理”中特别用了黑体字。这是我们的约定：元定理是有关定理（可导出的串）的定理（被证明了的结果））。
在命题演算中，一个人能够发现许多其他的元定理，或者说导出的推理规则。例如，这里有一个第二德·摩根规则：
＜～x～y＞与～＜xy＞是可互换的。
如果这是系统的一条规则，它就可以大大加快许多的推导。那么，如果我们证明了它是正确的，这就够了吗？从那以后我们就可以像一条推理规则一样地来用它了吗？
并没有理由去怀疑这种特殊的导出规则的正确性。但是一旦你开始承认导出规则是命题演算中你的那些操作过程的一部分，你就丢掉了系统的形式性，因为导出规则是非形式地导出的------它是在系统之外的。形式系统是被当作这样一种东西提出来的：它明确地展示出一个证明的每一个步骤，而且这一切都在一个唯一的、严密的构架中进行，因此任何数学家都可以机械地来检验另一个人的工作。但是如果你乐意从一开始就走到那个构架之外去，那么你干脆还不如压根不创造这个构架。所以，走这样的捷径是有缺点的。
将更高的层次形式化
不过，这里有一个替代的办法。为什么不把元理论也形式化呢？用这种办法，导出规则（元定理）就会是一个更大的形式系统的定理，同时，去寻找捷径，并且把它们当作定理来推导，也就会被认为是合法的了------就是说，把它们当作形式化了的元理论的定理------它们随后就可以被用来加快命题演算中定理的推导过程。这是一个令人感兴趣的主意，但是当它一被提出来，就会又有人跳到前面去考虑元元理论，如此等等。这一点是很清楚的：不管你形式化了多少层次，最后总有人还想在顶层去造捷径。
甚至还可能有人提出：一个推理理论可以与它自己的元理论是同样的，只要它是仔细地做出来的。这似乎是说，所有的层次都将压缩成为一个层次，从而，关于系统的思考就将成为在系统里边的一种工作方式！但是这并不那么简单。即使一个系统能够”对自身进行思考”，它也仍然不是在它自身之外。你站在系统之外去观察它，与它观察它自身的方式是不同的。所以仍然还有一个元理论------站在外边所作的观察------即使是对一个这样能够在它里边”对自身进行思考”的理论也是如此。我们将发现，存在一些能够”对自身进行思考”的理论。事实上，我们马上将要看到一个系统，在它里边这一点完全出人意料地发生了，甚至我们都没有想让它这样！并且我们将看到这一点所产生的种种后果。但是对于我们研究命题演算来说，我们将把牢这个最简单的思想------不把各种层次混同在一起。如果你没有仔细地将在系统里边的工作（J方式）与对于系统的思考（W方式）区分开，就会产生出谬误来。举例来说，似乎完全有理由去假设，由于＜P～P＞（它的半解释是”或者P或者非P”）是一个定理，于是或者P，或者～P一定是一个定理。但这就错到家了：后面的那一对中没有一个是定理。通常，下面这样做是一种危险的做法，即，去假设符号能够在不同的层次之间随便滑来滑去------这里，这不同的层次就是形式系统的语言与它的元语言（汉语）。
对系统的长处和短处的思考
现在，你已经看到了带有如下目的的系统的一个例子------描述逻辑思想体系的一部分。这个系统所处理的概念是为数很少的，它们都是非常简单、非常精确的概念。但是命题演算的这种简单性和精确性恰恰正合数学家们的心意。这样说有两个理由。（1）可以对它本身的一些性质进行研究，正像几何学研究简单的、固定的图形一样。在它上面还能够造一些变种，采用不同的符号、不同的推理规则、不同的公理或者公理图式，等等（顺带说一下，这里所介绍的命题演算版本与甘岑在三十年代早期所发明的一个命题演算有关联。还存在其它的一些版本，里边只用一条推理规则------通常是分离规则------并且有一些公理或者公理图式）。关于在精美的形式系统中进行命题推理的各种方式的研究，是纯数学的一个吸引人的分支。（2）命题演算能够很容易地扩充，把推理的其它一些主要的方面包括进来。这一点将部分地在下一章中展示出来，在那里，命题演算加进了枪机、枪柄、枪筒，从而充实成为一个更强有力的武器，用它可以完成复杂的数论推理。
证明之别于推导
命题演算非常像以某些方式进行的推理，但是人们是不应该把它的规则与人的思维的规则同等看待的。一个证明是某种非形式的东西，或者换句话说，是日常思维的产物，用人的语言写的，说给人听的。思维的各种各样复杂的特点都可能用在证明里面，虽然它们可能”感觉是对的”，人们却还是不知道它们是否在逻辑上能有保证。这正是形式化真正的目的所在。一个推导是证明的人造对应物，它的用意也是要去达到同样的目标，但却是通过一种逻辑结构去达到，这个逻辑结构的那些方法不仅是全然明确的，而且也是非常简单的。
如果说------而且通常是这样的情况------发生了这样的事：一个形式的推导与相应的”自然的”证明相比要长得多得多，这似乎是很糟糕的。这是人们为了使每一步都如此简单而付出的代价。在一般情况下，说一个推导和一个证明是”简单的”，这是在这个词的补偿意义上来说的。说证明是简单的，是指每一步”看上去是对的”，虽然一个人可能还不知道为什么是这样；而说推导是简单的，是指它的无数步骤中的每一步都被认为是如此不足道，以至于无从加以责难，而且由于整个的推导都恰好是由这样的不足道的步骤所组成，它可以被认为是没有错的。可是，任何一种简单性都会带来一种特殊类型的复杂性。对于证明，是它们赖以依靠的背景系统------即，人的语言------的复杂性；对推导来说，这是它们的天文规模，这使得它们几乎是不可能把握得住的。
于是，命题演算应被当作是综合人工证明之类的结构的一般方法的一部分。然而，它并没有很大的灵活性或一般性。我们仅仅是想把它用在一些数学的概念方面------而数学概念自身就是相当不灵活的。作为这方面的一个比较有意思的例子，让我们来做一个推导，在它里边一个非常奇特的串被拿来作为在一个幻想之中的前提：＜P～P＞。起码它的半解释是很怪的。可是命题演算并不去考虑半解释，它只是印符地摆弄那些串------并且，印符地看，关于这个串并不存在任何真正奇怪的东西。这里就是把这个串当作前提的一个幻想：
(1) [ 推入
(2) ＜P～P＞ 前提
(3) P 分隔
(4) ～P 分隔
(5) [ 推入
(6) ～Q 前提
(7) P 把第3行搬入
(8) ～～P 双弯号
(9) ] 弹出
(10) ＜～Q～～P＞ 幻想
⑾ ＜～PQ＞ 易位
⑿ Q 分离（4，11行）
⒀ ] 弹出
⒁ ＜＜P～P＞Q＞ 幻想
这个定理有一个非常古怪的半解释：
P和非P合在一起蕴涵Q。
由于Q可以解释为任何语句，我们就能无拘束地拿这条定理去说，“从一个矛盾出发，结果可以是任何东西”！所以，在以命题演算为基础的系统里，是不能包含有矛盾的。它们对整个系统的影响，就像是一个瞬时会扩散开的癌。
对付矛盾
这听上去不太像人的思维。如果你在你自己的思维中找到了一个矛盾，不太可能你整个的心智都被摧毁了。相反，你也许会开始对你觉得是导致了矛盾思维的那些信仰或推理方式产生疑问。换句话说，就你所能做到的程度，你会走出你所在的那些你觉得是对矛盾负有责任的系统，并试图去修理它们。对你来说，一件最不可能去做的事情是举起你的双手并且喊道：“好了，我猜想这表明我现在相信任何一件事情了！“作为一句笑话是可以这样说的------但是不能认真。
事实上，矛盾是在生活的各个领域中取得澄清和进步的一个主要源泉------数学也不例外。在过去的年代里，发现了数学里的一个矛盾，数学家们会立即致力于认定系统对此负有责任，跳出它之外，去探究它，并且去修正它。对矛盾的发现和修正是加强了而不是削弱了数学。这必须花时间和大量无结果的初步尝试，但最终它还是结出了成果。例如，在中世纪，无穷级数
1-1+1-1+1-…
的值引起了热烈的争论。它被”证明了”等于0，1，1/2，并且可能还有其他的值。从这样的有争议的发现之中，产生了一个较充实、较深刻的关于无穷级数的理论。
一个更有关联的例子，是我们现在正面对面碰到的矛盾------即在我们真正进行思考的方式与命题演算模仿我们的方式二者之间的矛盾。这曾经是许多逻辑学家烦恼的一个根源，大量创造性的努力被用来从事于尝试修补命题演算，以使得它不会如此犯傻和顽固地行动。有一种尝试是安德森和贝尔纳普在《衍推》3一书中提出的，它涉及了”相关蕴涵”，即试图使对应”若-则”的符号能反映真实的因果关系，或者至少反映意义的联系。考虑下列命题演算的定理：
(1)．＜P＜QP＞＞
(2)．＜P＜Q～Q＞＞
(3)．＜＜P～P＞Q＞
(4)．＜＜PQ＞＜QP＞＞
它们------以及许多像它们一样的其它定理------都表明了，仅只为一个若-则语句在命题演算里是可证的，在这个若-则语句的第一个和第二个子句之间并不需要有任何的关联。为了反对这个，“相关蕴涵”对是否在某一情况下应用推理规则这一点加了某种限制。直观地讲，它是说”某种东西可以从另外的某种东西推出，仅当它们彼此有关联。“举例来说，上面给出的那个推导中的第10行在这样的一个系统中是不被允许的，而这就中断了对串＜＜P～P＞Q＞的推导。
一些更为过激的尝试完全抛弃了对完全性或一致性的寻求，而试图去模仿人的带有不一致性的推理。这样的研究不再以提供给数学一个坚实的支持为目标，而是纯粹去研究人的思维过程。
且不去管它的古怪，命题演算是有着某些值得注意的特色的。如果有人把它嵌进到一个更大的系统里去（正如我们将在下一章里做的），并且如果他确信较大的系统不包含矛盾（我们将这样确信），那么命题演算能做这个人所能希望的一切：它提供有效的命题推理------所有那些能够造出来的命题推理。因此，如果任何时候不完全性或不一致性被暴露出来，人们就能确信，这一定是那个较大的系统的毛病，而不是它的子系统命题演算的过错。
艾舍尔作
