实用逻辑和自动推理手册

前言

本书是关于可以执行自动推理的计算机程序的. 我对推理的理解相当狭义: 重点在于形式演绎推理, 而非诸如扑克博弈或医学诊断之类的问题. 另一方面, 我对自动的理解则相当宽泛, 包括人与机器协同推理的交互式方案, 并且我始终关注演绎推理在现实世界问题中的应用. 事实上, 除了其本身固有的魅力之外, 这一学科因其工业应用而日益重要.

本书旨在作为该领域以及逻辑推理本身的入门导引. 读者无需具备数理逻辑的先修知识, 但不可避免地, 拥有一定的数学背景和计算机编程经验 (尤其是函数式语言, 如 OCaml, F#, Standard ML, Haskell或LISP) 将大有裨益. 与该领域众多专题性著作不同, 本书力求提供一个广泛而均衡的综合性导论, 并具有两个显著特点.

• 纯逻辑与自动定理证明以紧密交织的方式加以阐述. 逻辑学的成果在发展过程中始终着眼于其在自动定理证明中的作用, 并尽可能以显式计算的方式加以展开.
• 自动定理证明方法的阐述均参照实际的具体实现, 读者若能方便地使用计算机, 即可亲自进行实验. 所有代码均采用高层次函数式语言OCaml编写.

尽管这种编排方式有待商榷, 但我是在审慎考虑并广泛尝试了各种替代方案之后才采用的. 更详细的自我辩护将在后文给出, 但大多数读者可能希望直接跳到正文部分, 从第 xvi 页的如何阅读本书开始.

意识形态面向

本节将更详细地阐述本书背后的写作理念, 并尝试为之辩护. 我还将描述本书的关注重点以及未涵盖的主要主题. 要充分理解讨论中提出的某些观点, 需要具备相关学科知识. 读者可以选择跳过或略读此部分内容.

我的首要目标是对自动定理证明领域的众多核心成果进行广泛而均衡的讨论. 此外, 主要对纯数理逻辑感兴趣的读者应当发现, 本书涵盖了数理逻辑主流基础教材中的大部分传统成果: 紧致性, Löwenheim-Skolem定理, 证明系统的完备性, 插值, Gödel定理, 等等. 但我始终力求以具体的, 显式的和算法化的方式来呈现这些结果, 即使这并非自动证明器代码的直接需要, 其通常都会涉及可以实际进行实验和使用的真实代码, 至少在原则上如此. 例如:

• 第5.13节中插值定理的证明包含了一个构造插值公式的算法, 该算法利用了先前的定理证明代码;
• 第5.5节通过显式地交替运行证明与反驳代码来演示基于有限模型性质的可判定性, 而非笼统地援引定理7.13.

我希望许多读者能和我一样欣赏这种具体的, 亲身实践的风格. 形式逻辑通常需要对繁琐的句法细节给予相当程度的关注. 这对初学者而言可能颇为痛苦, 因此教师和作者往往不得不在两种令人不快的选择之间权衡: (i) 以令人煎熬的详尽程度将一切和盘托出, 或 (ii) 大量含糊其辞以掩盖粗疏的解释. 尽管教师有充分的理由对方式(i)望而却步, 但我的教学经验表明, 许多学生仍然不满于从未被告知事情全貌的感觉. 通过在计算机上实现这些内容, 我认为我们可以两全其美: 细节以精确的形式呈现, 但我们大体上可以让计算机去应对那些令人不快的后果.

诚然, 过去150年来数学变得更加抽象化, 更倾向集合论, 而远离了构造性方法. 这在当代模型论中尤为明显, 一些处于学科历史根基的传统主题正被逐渐淡化. 但逆流而行的并非只有我一人, 因为计算机的兴起正在帮助恢复显式算法方法在数学多个领域中的地位. 这在代数几何及相关领域中尤为显著 (Cox, Little和O'Shea 1992; Schenk 2003), 其中计算机代数, 特别是Gröbner基 (见第5.11节), 已经产生了相当大的影响. 但类似的思想也正在其他领域被探索, 甚至包括范畴论 (Rydeheard和Burstall 1988), 后者通常被视为抽象非构造性数学的精髓. 关于算法化视角在一般数学中的价值, 我无法比Knuth (1974) 的这段话说得更好:

有三年时间, 我在加州理工学院为数学专业的二年级学生讲授抽象代数课程, 其中最困难的主题总是矩阵的Jordan标准型. 到第三年, 我尝试了一种新方法, 从算法的角度来审视这一课题, 一切突然变得清晰明了. 同样的事情也发生在关于由生成元和关系定义的有限群的讨论中, 以及另一门课程中的二次型约化理论上. 通过以算法的方式呈现这些主题, 数学定理的目的和意义变得一目了然.
后来, 在撰写一本关于计算机算术的书 [Knuth (1969)] 时, 我发现初等数论中几乎每一个定理都以自然的, 有充分动机的方式出现在使计算机进行高速数值计算的问题中. 因此我认为, 传统的数论课程完全可以改用这种视角, 为已然优美的理论增添一层实用的动机.

就逻辑而言, 这种方法似乎尤为自然. 从最早期开始, 逻辑学的发展就受到将推理归结为计算这一愿望的驱动: logos一词, 即logic的词根, 不仅意味着逻辑思维, 还意味着计算或算账. 更近一些, 正是逻辑中的可判定性问题促使Turing等人精确定义了可计算函数的概念, 并建立了界定算法方法范围的抽象模型. 逻辑与计算之间的这种关系可以追溯到中世纪之前, 并一直延续至今. 例如, 计算机系统设计与验证中的问题正在激发更多的逻辑学研究, 而逻辑原理在程序设计语言的设计中也发挥着日益重要的作用. 因此, 逻辑推理不仅可以被视为现代计算机时代的众多受益者之一, 更可以被视为其最重要的思想源泉.

本书的另一个可能令某些读者感到意外的特点, 是其系统性的模型论取向; 相比之下, 许多其他教材如Goubault-Larrecq和Mackie (1997) 将证明论置于核心地位. 我在较晚的章节 (第6章) 才引入传统的证明系统, 而且几乎不提及, 更不利用自然演绎或相继式演算证明的结构性质. 尽管这些主题引人入胜, 但我认为经典逻辑的所有传统计算机证明方法完全可以在不借助它们的情况下很好地呈现. 事实上, 用于自动定理证明的特殊反驳完备演算 (二元归结, 超归结, 等等) 同样提供了关于证明范式 (canonical form) 的强有力的结果. 在某些情况下, 这些结果甚至比Gentzen式证明论的结果更便于推导理论性成果 (Matiyasevich 1975), 正如我们在第5.10节中仿照Lifschitz (1980) 对零点定理 (Nullstellensatz) 的证明所示. 无论如何, 对于自动推理而言, 特定证明系统的细节远不如对相应搜索空间的探查方式那样重要. 例如, 请注意tableau方法和逆方法之间的巨大差异, 尽管二者都可以被理解为对无切相继式证明的搜索.

我希望为所描述的所有方法提供完整的, 经过仔细解释的代码. (根据我的经验, 人们很容易低估从一个看似简明的算法到具体实现之间的难度.) 为了呈现几乎与通常用于描述算法的伪代码一样可读的真实可执行代码, 使用一种非常高层次的语言似乎是必要的, 这样就可以忽略数据表示和内存分配等具体问题. 为此我选择了函数式编程语言Objective CAML (OCaml). OCaml是Edinburgh ML的后裔, 后者是一种专门为编写定理证明器而设计的编程语言, 已有多个主要系统用它编写.

使用OCaml (而非诸如C或Java) 的一个缺点是许多读者对它并不熟悉. 然而, 我只使用了一个简单的子集, 在附录2中有简要说明; 代码风格是纯函数式的, 没有赋值或顺序执行 (除了产生诊断输出). 在少数情况下 (例如在二元决策图的代码中传递状态), 命令式代码可能更为简洁, 但坚持使用尽可能简单的子集似乎是值得的. 纯函数式编程对于我所希望鼓励的那种探索式修改尤为方便, 因为人们不必担心一个计算对其他计算产生意外的副作用.

最后, 我以来源于McCarthy (1963) 的一段引文作为结尾, 它精妙地概括了本书所蕴含的理念, 暗示了逻辑作为一门真正应用科学的潜在新角色.

我们有理由期望, 计算与数理逻辑之间的关系在下一个世纪将像上一个世纪分析学与物理学之间的关系那样富有成果.

本书没有涵盖的内容

尽管我力求涵盖广泛的主题, 但有所取舍是必要的, 以防止本书变得庞大到难以驾驭. 我聚焦于经典单类 (one-sorted) 一阶逻辑中的理论, 因为在这一连贯的框架下, 自动推理的许多核心方法都可以得到展示. 因此, 我不无遗憾地将一些重要领域排除在深入讨论之外, 包括模型检查, 归纳定理证明, 多类 (many-sorted) 逻辑, 模态逻辑, 描述逻辑, 直觉主义逻辑, lambda演算, 高阶逻辑和类型论. 然而, 我相信本书将为读者深入研究上述任何领域做好充分的准备, 其中许多领域恰恰最适合通过与经典一阶逻辑的对比来加以理解.

另一个指导原则是, 只有在我认为自己能够以较为初等的水平来呈现某一主题, 而无需过多技术细节或艰深理论的情况下, 才会将其纳入. 这意味着我忽略了例如有序paramodulation, 圆柱代数分解以及Gödel第二不完备性定理等内容. 但在这些情况下, 我尽量提供了充足的参考文献, 以便有兴趣的读者能够自行深入探究.

致谢

本书经过多年以随性的方式逐步演变为目前的形态. 在此期间, 我先后在剑桥大学计算机实验室, Åbo Akademi大学/TUCS以及Intel公司工作, 并曾短期访问其他机构; 我最要感谢的是Tania和Yestin, 感谢他们陪伴我辗转各地, 并容忍我在这个项目上投入的过多时间. 要在此公正地描述多年来结识的朋友和同事们对我思想的塑造程度, 是不可能的. 但我要特别感谢Mike Gordon, 是他最初给了我进入这一迷人领域的机会.

我撰写本书的部分原因在于, 据我所知, 尚无现有教材能够涵盖我所希望覆盖的逻辑学与自动推理领域的广泛主题. 因此, 本书的总体风格和方法是我自己的, 任何现有教材都无需为其不良影响承担责任. 但在纯逻辑方面, 我主要遵循了Kreisel和Krivine (1971) 对基本元定理的阐述方式. 他们优雅的发展路径恰好契合我的目的, 纯粹以模型论为基础, 并使用自动定理证明的常用工具, 如Skolem化和(所谓的)Herbrand定理. 例如, 第5.13节中那个极具算法美感的插值定理证明, 本质上就是他们的成果.

尽管我从事自动推理研究已近 20 年, 但我仍时常在文献中发现先前不曾注意到的旧成果, 或通过与同事的私人交流而得知它们. 在这方面, 我感谢Grigori Mints向我指出了Lifschitz利用归结证明对零点定理的证明 (第5.10节), 感谢Loïc Pottier告知我Hörmander的实数量词消去算法 (第5.9节), 也感谢Lars Hörmander本人回答了我关于这一过程起源的问题.

我非常幸运地拥有众多朋友和同事, 他们评阅了本书的草稿, 给予了令人振奋的鼓励, 采用并改进了相关代码, 甚至据此进行教学. 他们的影响往往使我的思路更加清晰, 有时还使我免于严重的错误, 但不消说, 他们无需为文中任何残留的缺陷负责. 在此衷心感谢Rob Arthan, Jeremy Avigad, Clark Barrett, Robert Bauer, Bruno Buchberger, Amine Chaieb, Michael Champigny, Ed Clarke, Byron Cook, Nancy Day, Torkel Franzén (令人惋惜的是, 他未能看到本书的最终完成), Dan Friedman, Mike Gordon, Alexey Gotsman, Jim Grundy, Tom Hales, Tony Hoare, Peter Homeier, Joe Hurd, Robert Jones, Shuvendu Lahiri, Arthur van Leeuwen, Sean McLaughlin, Wojtek Moczydlowski, Magnus Myreen, Tobias Nipkow, Michael Norrish, John O'Leary, Cagdas Ozgenc, Heath Putnam, Tom Ridge, Konrad Slind, Jørgen Villadsen, Norbert Voelker, Ed Westbrook, Freek Wiedijk, Carl Witty, Burkhart Wolff, 以及无疑还有许多其他通信者, 他们的贡献随着时间的流逝而被我疏忽地遗忘了, 感谢他们无价的帮助.

即使在网络时代, 能够使用优质的图书馆仍然至关重要. 我要感谢剑桥大学图书馆, 计算机实验室和DPMMS图书馆, Åbo Akademi的数学和计算机科学图书馆, 以及近年来波特兰州立大学图书馆和Intel图书馆的工作人员, 他们经常帮助我查找晦涩的参考文献. 我还要感谢无与伦比的Powell's书店 (www.powells.com), 它已被证明是经典逻辑学和计算机科学文献的宝库.

最后, 我要感谢Frances Nex极其细致入微的文字编辑工作, 以及剑桥大学出版社的Catherine Appleton, Charlotte Broom, Clare Dennison和David Tranah, 他们不顾我的一再拖延, 将本书引领至出版, 并提供了宝贵的建议, 出版社匿名审稿人的有益评论也为此提供了有力的支持.

如何阅读本书

本书的设计是按顺序从头到尾阅读的. 然而, 在学习了第1章以及第2章和第3章各自的大部分内容之后, 读者便可根据自己的兴趣选读其他部分. 为此, 我尽量将一些重要的交叉引用明确标出, 并尽可能避免使用过于繁复或非标准的记号.

每章末尾都附有若干练习题. 这些练习几乎从不是常规性的, 有些还非常困难. 这反映了我的信念: 解决一个真正具有挑战性的问题, 比费力做完大量琐碎的操练题更为有趣, 也更富有教益. 如果大多数题目看起来太难, 读者不必灰心. 它们全部是可选的, 也就是说, 不做任何练习也可以理解正文的内容.

本书所使用的数学

数学在本书中扮演着双重角色: 主题本身以数学方式处理, 同时自动推理也被应用于数学中的一些问题. 但在大多数情况下, 所需的数学知识并不十分高深: 基础代数, 集合与函数, 归纳法, 以及也许最根本的, 对证明这一概念的理解. 在少数地方会用到更高深的分析和代数知识, 不过我已尽量在行文中加以解释. 附录1是相关数学背景的摘要, 读者可在需要时查阅, 或者甚至在一开始就浏览一遍.

本书中的软件

本书的一个重要组成部分是配套软件, 其中包含用OCaml编程语言编写的各种定理证明技术的简单实现. 尽管不详细研究代码一般也能理解本书, 但解释往往围绕代码展开, 代码被用作替代冗长而形式化的语法过程描述的手段. (例如, 第6.4-6.8节中一阶逻辑的完备性证明, 以及第7.6节中Robinson算术的${\mathrm{\Sigma }}_1$-完备性证明, 本质上都是关于某些特定OCaml函数总能正确运行的详细非形式论证.) 因此, 如果至少没有对代码如何工作的一个粗略印象, 你可能会觉得本书某些部分相当吃力.

由于我预计许多读者几乎没有或完全没有编程经验, 至少在OCaml这样的函数式语言方面是如此, 我在附录2中概述了一些关键概念. 我并不自欺欺人地以为阅读这份简短的附录就能将一个新手变成熟练的函数式程序员, 但我希望它至少能提供一些方向指引, 其中也包含了读者在需要时可以进一步查阅的参考文献. 事实上, 整本书都可以被视为函数式编程的一个大型案例研究, 展示了许多重要的概念, 如结构化数据类型, 递归, 高阶函数, 延续和抽象数据类型.

我希望许多读者不仅会阅读代码, 还会实际运行它, 将其应用于新的问题, 甚至尝试修改或扩展它. 但要做到这些, 你需要一个OCaml解释器 (再次参见附录2). 定理证明代码本身几乎全部以分散的方式列在正文中. 由于读者实际手动输入代码大概收益甚微, 所有代码均可从本书的网站 (www.cambridge.org/9780521899574) 下载, 然后只需几次按键即可加载到OCaml解释器中, 或者一次一个片段地复制粘贴.

将来, 我希望在同一网址提供代码的更新, 也许还有其他语言的移植版本. 关于如何运行代码的更多细节可以在那里找到, 从而可以一边跟随书中的解释一边并行地试验代码, 但我在这里只提几个重要的要点. 最简单的方式大概是加载与本书相关的全部代码, 例如在包含代码的目录 (文件夹) 中启动OCaml解释器ocaml, 然后输入:

#use "init.ml";;

默认环境被设置为自动将法式≪引用≫中的内容解析为一阶公式. 若要使用第1章中的某些代码, 你需要将其改为解析算术表达式:

let default_parser = make_parser parse_expression;;

let default_parser = parse_prop_formula;;

除此之外, 你基本上可以随意选取你感兴趣的任何部分的代码来使用. 在极少数情况下, 作为讲解流程的一部分, 某个函数会先给出一个基础版本, 随后再替换为同名的更完善或更高效的版本. 在这种情况下, 默认环境始终会提供最新的版本; 如果你希望严格跟随讲解的顺序, 可能需要从源文件中复制粘贴较早的版本.

这些代码主要是为教学目的而编写的, 我始终将清晰性和/或简洁性置于效率之上. 尽管如此, 它们有时在实际应用中也可能确实有用. 无论如何, 在使用之前, 请仔细阅读网站上列出的(极少的)法律限制条款. 另外请注意, Stålmarck算法 (第2.10节) 受专利保护, 因此stal.ml文件中的代码不应用于商业用途.

第1章 引论

本章我们引入了逻辑推理和机械化它的想法, 简要触及了重要的历史性发展. 我们通过讨论逻辑学中的一些最为基础的想法以及刻画符号方法是如何在计算机上实现的来为后续内容奠定基础.

第1.1节 什么是逻辑推理?

存在许多理由相信某个东西为真. 它或许似乎是显而易见的, 或许至少第一眼看上去是令人信服的, 可能我们的父母之前告诉过我们, 也可能是其与相关科学实现的结果达成了惊人的一致性. 尽管往往是可靠的, 但是这些判断的方法也并非万无一失, 其也曾被用于说服人们地球是平的, 圣诞老人是存在的, 原子不可被进一步划分为更小的粒子.

逻辑推理相较于其他推理的不同之处在于其会避免任何未经澄清的假设, 并将自身限制于不会出错且超越理性置辩的推理. 为了避免作出任何无法保证的假设, 逻辑推理不能依赖于要被推理的对象或者概念的任何特殊性质. 这意味着逻辑推理必须从所有这样的特殊特征之中抽象出来, 并在应用于其他领域时同等有效 (valid). 论证之所以被接受为逻辑性的(论证), 在于其与某种一般形式的相合, 而非因为其所处理的特定内容. 例如, 将以下的传统例子:

所有人都是要死的
Socrates是一个人
因此Socrates是要死的

所有正整数都是四个整数的平方之和
$15$是一个正整数
因此$15$是四个整数的平方之和

所有的$X$都是$Y$
$a$是$X$
因此$a$是$Y$

这个推理模式是逻辑有效的, 因为其有效性并不依赖于内容: 正整数和要死的的含义是无关紧要的. 我们可以将$X$, $Y$, $a$替换为任何我们喜欢的东西, 只要尊重语法范畴即可, 而语句仍然保持有效. 与之相对的是, 考虑以下推理:

所有的雅典人都是希腊人
Socrates是一个雅典人
因此Socrates是要死的

尽管这个结论是全然正确的, 但是这个论证并非逻辑有效的, 因为其依赖于所牵涉的项的内容. 其他的具有同样的似是而非形式的论证当然也可能是假的, 例如

所有的雅典人都是希腊人
Socrates是一个雅典人
因此Socrates没有胡须

然而, 第一个论证可以转变为一个逻辑有效的论证, 通过将隐式的假设所有的希腊人都是要死的显式化. 现在这个论证是以下一般的逻辑有效的形式的一个实例:

所有的$G$都是$M$
所有的$A$都是$G$
$s$是$A$
因此$s$是$M$

第一眼看上去, 这种对于推理的法医鉴识式分析似乎并不令人印象非常深刻. 逻辑有效的推理从未告诉过我们任何关于世界的本质上新颖的东西——正如Wittgenstein (1922) 所言, 当我知道天气要么下雨要么不下雨时, 我对于天气一无所知. 换言之, 如果我们的确从推理的链条之中学到了关于世界的什么新东西, 那么它必然包含并非纯粹逻辑的步骤. Schilpp (1944) 中引用Russell所言:

Hegel从纯粹逻辑之中推导出了世界的全部本质, 包括小行星的不存在性, 其之所以能够做到这点, 只是因为他逻辑无能.

但是逻辑分析可以清晰地揭示关于真实世界的事实之间的必要关系, 直接地表明何处掺入了或许不能保证的假设. 例如, 根据如果刚刚下过雨, 那么地面是潮湿的可以逻辑推出如果地面并非超市, 那么刚刚就不可能下过雨. 这是被称为逆否的一般原理的一个实例: 从如果$P$那么$Q$可以推出如果非$Q$那么非$P$. 然而, 从如果$P$那么$Q$到如果$Q$那么$P$一般并非有效, 在这种情况下就是我们发现我们不能推出如果地面是潮湿的, 那么刚刚下过雨, 因为也可能是由于爆裂的水管或者灌溉设施什么的才导致了潮湿.

或许正如Locke (1689) 所言, 这样的例子可能是琐碎的, 不过这种初等的逻辑谬误我们也经常会遇到. 更为重要的是, 数学之中的演绎远非琐碎所能概括, 而是一直使人类历史之中的一些伟大智者深深着迷, 经常也使得他们感到挫败. 从简单而不可辩驳的假设出发, 经过漫长而复杂的逻辑演绎链条, 可以通往复杂且违反直觉的定理, 正如Hobbes所发现的 (Aubrey 1898):

在一位绅士的私人书房里, Euclid的原本摊开着, 翻到的是第1卷第47命题 [Pythagoras定理]. 他读了这个命题. 天哪, 他说道 (他时不时会用一句有力的誓语来加强语气), 这不可能! 于是他读了该命题的证明, 证明将他引回到某个前置命题; 他读了那个命题. 那个命题又将他引回到另一个命题, 他也读了. 如此层层回溯 [et sic deinceps], 最终他被严格地说服了那个真理. 这使他爱上了几何学.

的确, Euclid的开创性作品几何原本建立了一种特定的推理风格, 其经完善之后构成了如今数学的脊骨. 这种风格在于先断言少量公理——这些公理被认为具有数学内容——然后运用纯粹的逻辑推理从中推导出结论. Euclid本人并未完全实现逻辑与非逻辑的彻底分离, 但他的工作最终由Hilbert (1899) 和Tarski (1959) 加以完善, 他们使得一些假设显式化, 例如Pasch公理.

{原注: 可以说, 这种方法在Socrates的论辩术中已有预兆, Plato对此有所记述. 苏格拉底会引导他那些不幸的对话者, 从他们自己的观点出发, 经过一连串看似不可避免的推论, 从而赢得辩论. 当荒谬的结论被推导出来时, 最初的立场便站不住脚了. 要使这种方法具有其令人叹服的力量, 每一步推理都必须毫无疑义, 且不能暗中引入任何隐含的假设.}

第1.2节 Calculemus!

推理就是算账 (reckoning). 在本书的卷首语中我们引用了Hobbes关于逻辑推理和数值计算之间的相似性的阐述. 尽管Hobbes应该因为使得这个想法更为广为人知而受到嘉奖, 这个想法本身即便在1651年也不是全新的. 的确由Plato和Aristotle所使用以代表推理或者逻辑思维的希腊词汇logos在其他上下文中也可能表示计算或者算账. 当古希腊哲学家的作品在中世纪的欧洲广为人知的时候, logos一般被翻译为ratio, 这是代表算账的拉丁词汇 (因而有了英语词汇rational, ratiocination, 等等). 即便在如今的英语里, 我们有时也能听到I reckon that ..., 这里的reckon指的是某种推理而并非字面意义上的要去计算.

然而, 推理和算账之间的联系在Gottfried Wilhelm von Leibniz (1646–1716) 的作品之前几乎只是一种暗示性的口号. Leibniz相信一个根据计算进行推理的系统必须包含两个基本组件:

• 一种通用语言 (characteristica universalis), 由此可以表达任意的东西;
• 一种推理演算 (calculus ratiocinator), 用于判定以characteristica表达的断言的真假.

Leibniz梦想着有朝一日不能达成一致意见的双方不会陷入徒劳的争辩, 而是将他们的不一致转换为characteristica, 然后彼此言称calculemus (让我们计算吧). 他甚至可能设想过让机器来完成这些计算. 那时候, 各种机械计算装置已被设计和建造出来, Leibniz本人也在1671年设计了一台能够进行乘法运算的机器, 并说道:

杰出之人不应像奴隶一样, 将大量时间耗费在计算的苦役上, 如果使用机器的话, 这些工作完全可以放心地交给任何人去做.

因此, Leibniz预见了使自动推理成为可能的基本要素: 一种精确表达思想的语言, 在该语言中操纵思想的计算规则, 以及这种计算的机械化. 莱布尼茨在实现这些构想方面的具体成就是有限的, 且直到近年来才为人所知. 但尽管他的工作对技术发展的直接影响有限, 他的梦想在今天仍然引起共鸣.

第1.3节 符号化

Leibniz将注意力放在建立合适的语言这一基本的首要步骤上是正确的. 然而, 他太过雄心壮志以至于想要表达人类思维的所有方面. 最终的进步来自于扩展已经在数学中所使用的符号记号的应用范围. 例如, 如今我们会说$x^2\le y+z$而非$x$乘上自身小于等于$y$与$z$之和. 随着时间推移, 越来越多的数学开始以形式符号记号表达, 取代了自然语言渲染. 对此我们可以找到几个坚实的理由.

首先, 一套精心选择的符号形式通常更加简短, 减少了无关信息的干扰, 有助于更简洁更直观地表达思想 (至少对于内行人而言是如此). 例如, 莱布尼茨本人发明的微分记号$dy/dx$, 巧妙地传达了小差分之比的思想, 并使得像链式法则$dy/dx=dy/du\cdot du/dx$这样的定理, 凭借与普通代数的类比, 看起来就显得合情合理.

其次, 使用更加规范化的表达形式可以避免日常语言中的一些歧义, 从而更精确地传达含义. 对词语确切含义的疑虑在许多领域都很常见, 尤其是在法律领域. 数学也无法免于类似的根本分歧, 即对一个定理究竟在说什么, 或其成立条件究竟是什么的争论, 而且对这些问题的共识会随时间而改变 (Lakatos 1976; Lakatos 1980).

最后, 也许也是最重要的一点, 一套精心选择的符号记法能够使数学推理本身变得更加容易. 一个简单但极为出色的例子是数的位值 (positional)表示法, 其中一个数由一串数字符号表示, 每个符号隐含地乘以基数 (base)的某个幂次. 在十进制中, 基数为$10$, 我们将数码序列$179$理解为:$$179=1\times {10}^2+7\times {10}^1+9\times {10}^0\text{.}$$

第1.4节 Boole的逻辑代数

词汇algebra来源于阿拉伯语的al-jabr, 最早在九世纪由Mohammed al-Khwarizmi (约780-850) 使用, 而他的名字正是算法 (algorithm)一词的词源. al-jabr一词的字面意思是重新结合, 但花拉子密用它来特指他通过合并 (重新结合) 同类项来解方程的方法, 例如从$x+4=6-x$变换到$2x=6-4$, 进而得到解$x=1$. 在此后的几个世纪里, 历经欧洲文艺复兴时期, 代数的含义本质上一直是用于解方程的运算规则.

在十九世纪, 传统意义上的代数达到了它的极限. 此前的核心关注点之一是求解越来越高次的方程, 但Niels Henrik Abel (1802-1829) 在1824年证明, 对于五次及五次以上的多项式方程, 不存在利用此前对低次方程有效的根式表达式来求解的一般方法. 然而与此同时, 代数的范围也在扩展并走向一般化. 传统上, 变量代表的是实数, 通常是有待确定的未知数. 但很快, 将所有常规的代数运算规则应用于虚量$i$并假定其具有形式性质$i^2=-1$, 成为了标准做法. 尽管这一做法在很长一段时间内缺乏严格的证明, 但它确实行之有效.

代数方法甚至被应用于通常意义上并非数的对象, 如矩阵和Hamilton的 四元数, 即使代价是放弃通常的乘法交换律$xy=yx$. 人们逐渐认识到, 符号的潜在解释可以被忽略, 只要一劳永逸地确立了所使用的运算规则在该解释下都是有效的. George Boole (1815-1864) 对这一状况做了颇具远见的描述:

凡熟悉符号代数理论现状者皆知, 分析过程的有效性并不取决于所使用符号的解释, 而仅仅取决于它们的组合法则. 凡不影响所假定关系之真实性的解释体系, 都同样可以被接受; 事实上, 同一过程在一种解释方案下可以代表一个关于数的性质的问题的解, 在另一种解释方案下可以代表一个几何问题的解, 在第三种解释方案下则可以代表一个动力学或光学问题的解. (Boole 1847)

Boole进而指出, 尽管如此, 由于历史或文化的偶然因素, 当时所有的代数所涉及的对象在某种意义上都是量化的 (quantitative). 转而他引入了一种代数, 其对象要被解释为真或假的真值, 而其中的变量则表示命题. 使用命题这个词汇, 我们指的是一个断言, 其作出了对于事实的声明, 因而可以有意义地被认为要么为真要么为假. {译注: 这里说的断言, 和类型论里的判断, 在技术意义上不同, 作者只是生活化地使用这个名词.} 例如, $1<2$, 所有人都是要死的, 月球由奶酪构成, 存在无限多个素数$p$使得$p+2$也是素数都是命题的例子. 根据我们现有的知识水平, 前两个命题为真, 第三个为假, 第四个的真值则是未知的 (此即所谓的孪生素数猜想, 数学界的著名开放问题).

{原注: 实际上Boole给出了两种不同但有关联的解释: 一种是类的代数, 另一种是命题的代数; 我们将会专注于后者.} {译注: 这里说的类, 应该指的是某个固定集合的子集.}

我们熟悉对数施加各种算术运算, 如一元的负 (minus) (取相反数) 以及二元的乘 (乘法) 和加 (加法). 以完全类似的方式, 我们可以使用所谓的逻辑联结词来组合真值, 例如一元的非 (逻辑否定或补) 以及二元的与 (合取) 和或 (析取). 而且, 在书写表达式时, 我们可以用字母来代表任意命题, 正如代数中用字母代表数一样. Boole在对于他的系统的精确表述中, 以及对于许多逻辑常量和联结词使用熟悉的代数符号时, 强调了其与普通算术之间的联系:

$0$	假
$1$	真
$pq$	$p$且$q$
$p+q$	$p$或$q$

在这种解释之下, 许多令人熟悉的代数定律仍然成立. 例如, $p$且$q$总是和$q$且$p$具有相同的真值, 所以我们可以认为交换律$pq=qp$成立. 类似地, 既然$0$是假, 那么$0$且$p$不论$p$是什么总是为假, 即$0p=0$. 但是, 命题的布尔代数满足额外的定律, 其没有算术的对应物, 特别是$p^2=p$, 其中$p^2$是$pp$的缩写.

在日常英语里, 词汇或是有歧义的. 复合命题$p$或$q$可以解释为可兼的或 ($p$或$q$或两者都成立), 也可以解释为不可兼的 ($p$或$q$但是不能两者都成立). 日常使用里经常隐含了两种情况是互斥的 (例如我会明天做或者后天做). Boole原本的系统限制了这种代数, 以使得$p+q$只有在$pq=0$时才有意义, 就像在普通代数里$x/y$只有在$y\models 0$时才有意义. 然而, 遵循Boole的继任者William Stanley Jevons (1835–1882), 习惯上我们允许不加限制的或, 并以可兼的方式解释它. 我们总是会按照如今标准的含义理解或, $p$或$q$的意思是$p$或$q$或两者都成立.

第1.4.1小节 机械化

甚至在Boole之前, 用于逻辑推演的机器就已经被开发出来了, 其中最著名的是由Charles Stanhope (第三代Stanhope伯爵, 1753–1816) 发明的Stanhope演示器. 受此启发, Jevons (1870) 随后设计并建造了他的逻辑机器, 这是一种类似钢琴的装置, 能够在Boole的类代数中执行某些运算. 然而, 由于机械工程的局限性以及逻辑学本身发展的缓慢, 推理的机械化真正开始蓬勃发展是在稍晚的时期, 即现代计算机时代的开端. 我们将在本书后续章节中结合技术发展进一步介绍这段历史. Jevons的原始机器现陈列于Oxford科学史博物馆.

第1.4.2小节 逻辑形式

在1.1节中, 我们谈到了论证具有相同的形式, 但并未对此给出精确的定义. 事实上, 对于用英语或其他自然语言表达的论证而言, 要做到这一点是很困难的, 因为自然语言往往无法清楚地呈现句子的逻辑结构: 表面上的相似性可能掩盖根本性的结构差异, 反之亦然. 例如, 英语中的is既可以表示具有...的性质 ($4$ is even), 也可以表示和...相同 ($2+2$ is $4$). 这个例子以及类似的情况常常引发哲学上的混淆.

一旦我们拥有了逻辑概念的精确符号体系 (如Boole的逻辑代数), 我们就可以简单地说: 两个论证具有相同的形式, 如果它们都是相同的形式表达式的实例, 实例化是通过一致地将变量替换为其他命题得到的. 并且我们可以利用形式语言对逻辑上有效的论证给出数学上精确的定义. 这并不意味着逻辑形式和纯逻辑论证的定义在哲学上是一个无足轻重的问题; 恰恰相反. 但我们满足于不去解决这个问题, 而是通过采纳一个精确的数学定义来巧妙地绕过它, 正如Hertz (1894) 回避了力学中力的含义这一问题一样. 在积累了足够的具体经验之后, 我们将简要探讨 (第7.8节) 我们对逻辑论证的界定如何与一些传统的哲学区分相对应.

第1.5节 句法和语义

逻辑学的一个独特之处在于它严格区分符号表达式与其所代表的对象. 这一点值得特别强调, 因为在日常数学中, 我们常常不自觉地从符号直接过渡到符号所指称的数学对象. 例如, 当我们读写$12$时, 我们将其视为一个数, 即集合$\mathbb{N}$的一个元素, 而非用来表示该数的两个数码符号的序列. 然而, 当我们想要精确地进行形式化操作时, 无论是逐位相加十进制数, 还是运用代数法则重排符号表达式, 我们都需要维持这种区分. 毕竟, 当推导出诸如$x+y=y+x$这样的等式时, 整个的要义在于两边所指称的数学对象是相同的; 如果我们只考虑潜在意义 (underlying meaning), 那么我们就不能直接讨论这样的形式操作.

因此, 通常我们关注的是: (i) 某个特定的合法形式表达式集合, 以及 (ii) 它们对应的意义. 这两者被严格区分开来, 但通过一种解释联系在一起, 解释将表达式映射至它们的意义:$$\text{[表达式]}\stackrel{\text{解释}}{\to }\text{[意义]}$$

形式化表达式与其意义之间的区分在语言学中同样重要, 我们将借用该学科的一些术语. 语言学有两个传统的子领域: 句法学, 关注句子的语法构成; 语义学, 关注句子的意义. 类似地, 在逻辑学中, 我们通常将那些如同代数运算般脱离意义而独立考察的方法称为句法的, 而将意义起重要作用的方法称为语义的. 句法和语义这两个词在语言学中还有更具体的含义, 这些含义同样被逻辑学所采纳.

• 一种语言的句法是一套语法规则体系, 规定了如何生成或识别合乎语法的短语和句子. 例如, 我们会认为I went to the shop是合乎语法的英语, 而I shop to the went则不是, 因为名词和动词的位置被交换了. 在逻辑系统中同样如此, 我们通常也会有规则告诉我们如何生成或识别合式表达式, 例如允许$x+1$但不允许$+1\times$.
• 一个特定单词, 符号, 记号或短语的语义就是它的意义. 更广泛地说, 一种语言的语义是一种系统性地为该语言中所有 (合乎语法的) 表达式赋予意义的方式. 用语言学术语来说, 选择一种解释恰好就等同于为该语言给出一套语义.

第1.5.1小节 对象语言和元语言

我们将要描述执行逻辑推理的形式规则, 然而又要用...逻辑来对这些规则进行推理, 这可能会令人困惑! 在这方面, 将我们所谈论的(形式)逻辑与我们用来对其进行推理的(日常直觉)逻辑之间的区别牢记在心是有益的. 为了强调这一对比, 我们有时会使用以下语言学术语. 元语言是用来谈论另一种不同的对象语言的语言, 类似地, 元逻辑是用来对于对象逻辑进行推理的. 因此, 我们通常将关于形式逻辑和自动推理系统所推导出的定理称为元定理, 而不仅仅是定理. 这样做不(只)是为了听起来更宏大, 而是为了强调它们与在那些形式系统内部表达的定理之间的区别. 同样, 应用于形式化数学证明的元逻辑推理通常被称为元数学 (参见第7.1节). 顺便提一下, 我们所选用的编程语言OCaml源自Edinburgh ML, 后者是专门为编写定理证明程序而设计的 (Gordon, Milner和Wadsworth 1979), 其名称代表元语言 (Meta Language). 这种对象-元的区分 (Tarski 1936; Carnap 1937) 并不局限于逻辑语言. 例如, 在一堂用英语讲授的俄语课上, 我们可以将俄语视为对象语言, 而将英语视为元语言.

第1.5.2小节 抽象和具体句法

句法的细节并无根本性的重要意义. 数学有时是打印的, 有时是手写的, 人们做出各种本质上任意的选择, 这些选择并不改变符号组合使用的结构方式. 在计算机上实现逻辑的机械化时, 为简便起见, 我们将限制自己只使用标准的ASCII字符集, 其中包括无重音的拉丁字母, 数字以及一些常见的标点符号和空格. 对于许多逻辑学家使用的花体字母和特殊符号, 我们将用其他字母或单词来替代, 例如用forall代替$\forall$. 不过, 在理论讨论中我们仍将继续使用通常的符号. 这种不断的转换对于此前未见过或未理解这些符号的读者而言甚至可能是有帮助的.

无论符号表达式是如何读写的, 以一种更能反映其结构的形式来操作它们会更加方便. 考虑普通代数中的表达式$x+y\times z-w$. 这种线性形式掩盖了有意义的结构. 要理解哪些运算符作用于哪些子表达式, 甚至要弄清什么构成一个子表达式, 我们需要了解优先级和结合性的规则, 例如$\times$比$+$绑定更紧. 举例来说, 尽管在线性形式中它们看起来很相似, $y\times z$是一个子表达式, 而$x+y$却不是. 即使我们通过完全加括号将结构显式化, 写成$(x+(y\times z))-w$, 对表达式进行基本的有用操作, 如查找子表达式或对变量的特定值求值, 也会变得难以精确描述; 人们需要在公式中来回移动以匹配括号.

树结构则好得多: 正如家谱树能清晰地展示家族成员之间的关系, 表达式的树形表示能够显示其结构, 并使大多数重要的操作变得直截了当. 如同在家谱学中一样, 习惯上将树画成在印刷页面上向下生长的形式, 因此同一个表达式可以表示如下:

通常我们将人们使用的(主要是线性的)格式称为具体句法, 而将用于操作的结构性(通常是树状的)形式称为抽象句法. 像上面这样的树通常被称为抽象句法树 (AST), 它们作为形式语言的内部表示被广泛应用于各种符号处理程序中, 包括将高级编程语言翻译为机器指令的编译器.

尽管树形结构使表达式的结构更加清晰, 大多数人还是不愿意用树来思考或交流, 而更倾向于使用结构性较弱的具体句法. 因此, 在我们的定理证明程序中, 我们需要将输入从具体句法转换为抽象句法, 并将输出从抽象句法转换回具体句法. 这两项任务, 在计算机科学家那里分别被称为句法分析和美观打印, 如今已被很好地理解并且相当常规. 编写解析器和美观打印器的少量额外开销, 可以通过树形结构在内部操作上带来的更大便利得到充分回报. 存在一些对于诸如波兰记号, 逆波兰记号 (RPN), 以及LISP的S-表达式这样的具体句法系统的狂热倡导者, 其中我们的表达式按照这些记号分别会记作

- + x × y z w

x y z × + w -

(- (+ x (× y z)) w)

第1.6节 符号计算和OCaml

现代计算的早期人们普遍相信计算机基本上是用来进行数值计算的设备 (Ceruzzi 1983). 其输入和输出设备确实也在某种程度上偏向于这一方向: 当Samuels在1948年于IBM写下第一个跳棋程序时, 他不得不将输出编码为一个数字, 因为这就是唯一可以打印的内容了. 然而, 远在Turing从理论上构造通用机器 (参见第7.5节) 之前, 人们就已经认识到计算机的潜在应用范围要广泛得多. 例如, Ada Lovelace在1842年就观察到 (Huskey和Huskey 1980):

许多不熟悉数学研究的人想象, 因为[Babbage的分析]引擎的任务是以数字符号给出其结果, 所以其过程的性质必然是算术的和数值的, 而非代数的和解析的. 这是一个错误. 该引擎能够对其数值量进行排列和组合, 恰如它们是字母或任何其他一般性符号一样; 事实上, 如果做了相应的安排, 它完全可以以代数符号形式输出其结果.

如今已有许多执行符号计算的程序, 其中包括各种相当成功的计算机代数系统 (CAS). 定理证明程序与计算机代数系统有着很强的家族相似性, 甚至在它们能够解决的某些问题上存在重叠 (例如参见第5.11节).

从事符号计算的人的关注点影响了他们偏好的编程语言. 许多系统程序员青睐C, 数值分析人员偏好FORTRAN, 诸如此类, 而符号计算程序员通常更喜欢更高级的语言, 这些语言使典型的符号操作更加便捷, 将程序员从内存表示等显式细节中解放出来. 我们选择使用Objective CAML (OCaml)作为本书编程示例的载体. 我们的代码没有使用OCaml中任何较为特殊的特性, 应当很容易移植到相关的函数式语言, 如F#, Standard ML或Haskell.

我们坚持使用显式的OCaml代码, 对于没有计算机编程经验的读者, 或者只了解C或Java等命令式低级语言的读者来说, 可能会感到不安. 然而, 我们希望借助附录2以及本章末尾推荐的一些标准教材的额外学习, 有决心的读者能够掌握足够的OCaml知识来跟上讨论并动手实践代码. 作为OCaml中符号计算的一个温和入门, 我们现在将在普通代数这一许多读者所熟悉的领域中实现一些简单的操作.

第一个任务是定义一个数据类型以表示代数表达式的抽象句法. 我们允许表达式由诸如0, 1, 33这样的数值常量以及诸如x和y这样的命名变量通过加法 (+) 和乘法 (*) 运算构筑而成. 以下是相应的递归数据类型声明:

type expression =
   Var of string
 | Const of int
 | Add of expression * expression
 | Mul of expression * expression;;

也就是说, 一个表达式要么是由一个字符串标识的变量, 要么是由其整数值标识的常量, 要么是一个加法或乘法运算符作用于两个子表达式. (*表示一个类型构造器的定义域是一个笛卡尔积, 因此它可以接受两个表达式作为参数. 这与所定义的乘法运算毫无关系!) 我们可以使用这个类型定义所引入的句法构造器来创建任何特定表达式的符号表示, 例如$2\times x+y$:

# Add(Mul(Const 2,Var "x"),Var "y");;
- : expression = Add (Mul (Const 2, Var "x"), Var "y")

符号计算的一个简单但具有代表性的例子是应用指定的变换规则, 如$0+x⟶x$和$3+5⟶8$, 来化简一个表达式. 每条规则在OCaml中通过一个起始模式和一个终止模式来表达, 例如Add(Const(0),x) -> x对应变换$0+x⟶x$. (特殊模式_可以匹配任何内容, 因此最后一行确保了当没有其他模式匹配时, expr将被原样返回.) 当函数被调用时, OCaml会按顺序遍历这些规则, 并应用第一条起始模式与输入表达式expr匹配的规则, 将像x这样的变量替换为相应的子表达式.

let simplify1 expr =
  match expr with
    Add(Const(m),Const(n)) -> Const(m + n)
  | Mul(Const(m),Const(n)) -> Const(m * n)
  | Add(Const(0),x) -> x
  | Add(x,Const(0)) -> x
  | Mul(Const(0),x) -> Const(0)
  | Mul(x,Const(0)) -> Const(0)
  | Mul(Const(1),x) -> x
  | Mul(x,Const(1)) -> x
  | _ -> expr;;

然而, 仅化简一次并不一定足够; 我们更希望反复化简, 直到无法再取得进展为止. 为此, 让我们以自底向上的方式对表达式树进行遍历来应用上述函数, 这将以级联的方式进行化简. 按照传统的OCaml递归风格, 我们首先尽可能地化简所有直接子表达式, 然后对结果应用simplify1:

let rec simplify expr =
  match expr with
    Add(e1,e2) -> simplify1(Add(simplify e1,simplify e2))
  | Mul(e1,e2) -> simplify1(Mul(simplify e1,simplify e2))
  | _ -> simplify1 expr;;

与简单的自底向上遍历相比, 一种更精细的方法是将自顶向下和自底向上的化简混合使用. 例如, 如果$E$非常大, 那么将$0\times E$直接化简为$0$而不检查$E$的内容似乎更为高效. 然而, 这需要谨慎实现, 以确保所有可化简的子项都被化简, 同时避免无限循环的危险. 不管怎样, 以下是我们的化简函数作用于表达式$(0\times x+1)\times 3+12$的效果:

# let e = Add(Mul(Add(Mul(Const(0),Var "x"),Const(1)),Const(3)),
              Const(12));;
val e : expression =
  Add (Mul (Add (Mul (Const 0, Var "x"), Const 1), Const 3), Const 12)
# simplify e;;
- : expression = Const 15

走到这一步, 使用标准的OCaml函数式编程技术是很直接的: 用递归数据类型表示树结构, 通过模式匹配和递归来定义函数. 我们希望此前未使用过类似语言的读者能够开始理解为什么OCaml对符号计算具有吸引力. 当然, 那些钟爱其他编程语言的读者完全可以将我们的代码翻译成他们所喜欢的语言.

按照计划, 我们将实现一个句法分析器和美观打印器, 用于在抽象句法树和具体字符串 (如x + 0) 之间进行转换, 并将它们设置为由OCaml自动调用, 以完成表达式的输入和输出. 我们的具体句法以普通代数记号为蓝本, 但在两个方面我们将参照计算机语言而非传统数学的做法. 我们允许任意长的词作为变量, 而数学家传统上大多使用带上标和下标的单个字母; 鉴于ASCII字符集的有限性, 这一点尤为重要. 此外, 我们要求乘法必须用一个显式的中缀符号来书写 (x * y), 而不是简单的并置 (x y), 因为后者我们稍后将用于函数应用. 在日常数学中, 我们通常依赖诸如变量名和背景知识之类的非正式线索来一眼看出$f(x+1)$表示函数应用而$y(x+1)$表示乘法, 但这种依赖上下文的解析实现起来要复杂一些.

第1.7节 句法分析 (parsing)

将具体句法转换为抽象句法是一个已被充分理解的课题, 因为它对编程语言的编译器, 解释器和翻译器具有核心重要性. 现在的惯例是将这一转换分为两个独立的阶段:

• 词法分析 (扫描) 将输入的字符序列分解为词元 (token) (粗略地说, 就是词);
• 句法分析将词元的线性序列转换为抽象句法树.

例如, 词法分析可能会将输入v10 + v11拆分为三个词元v10, +和v11, 将相邻的alphanumeric字符合并成词, 并丢弃这些记号之间任意数量的空格 (甚至可能包括换行符). 这样, 句法分析只需处理词元序列, 而可以忽略更底层的细节.

第1.7.1小节 词法分析

第1.7.2小节 句法分析

第1.8节 美观打印 (prettyprinting)

第1.9节 深入阅读

我们在此仅列出一般性的参考文献, 以及那些后续章节中不会深入讨论的主题的相关文献. 更具体和更技术性的参考文献将在后续各章末尾给出.

Davis (2000) 和Devlin (1997) 是关于逻辑及其机械化发展的综合性著作, 同时也涉及计算机科学和语言学中的相关课题. 关于逻辑的入门教材有很多, 如Hodges (1977), Mates (1972) 和Tarski (1941). 有两本逻辑著作与本书一样附带了计算机程序, 分别是Keisler (1996) 以及Barwise和Etchemendy (1991). 此外还有若干著作仔细探讨了逻辑推理在数学中的作用, 例如Garnier和Taylor (1996).

Bochénski (1961), Dumitriu (1977) 以及Kneale和Kneale (1962) 是关于逻辑史的详尽而严谨的学术著作. Kneebone (1963) 是一部数理逻辑综述, 其中也包含大量历史资料, 而Marciszewski和Murawski (1995) 则与本书一样强调机械化这一主题. 关于Jevons的逻辑钢琴以及其他早期推理机器的生动介绍 (可以追溯至十三世纪西班牙神秘主义者Ramon Lull的工作), 参见Gardner (1958). MacKenzie (2001) 是关于自动定理证明发展及其应用的历史概述.

有许多哲学逻辑导论著作更深入地讨论了诸如逻辑后承 (logical consequence) 的概念等议题, 例如Engel (1991), Grayling (1990) 和Haack (1978). 具有哲学倾向的读者或许会有兴趣审视Mill (1865) 和Mauthner (1901) 关于逻辑后承不过是一种心理偶然现象的主张, 以及Frege (1879) 和Husserl (1900) 针锋相对的论战式回应.

关于OCaml和函数式编程的更多参考文献, 请参见附录2. 我们所描述的基本句法分析技术几乎在每一本编译技术著作中都有详细阐述. 由Aho, Sethi和Ullman (1986) 所著的龙书长期以来被视为经典, 不过对于主要兴趣不在句法分析方面的读者来说, 其关于句法分析的论述可能过于详尽. 对哪些句法分析任务是可判定的, 哪些是不可判定的进行详细的理论分析, 自然引向可计算性理论. Davis, Sigal和Weyuker (1994) 不仅全面地涵盖了这方面的内容, 而且本身也是一本逻辑教材. 关于美观打印的更多内容, 参见Oppen (1980b) 和Hughes (1995).

与本书风格相同的, 面向实现的定理证明讨论, 还见于Huet (1986), Newborn (2001) 和Paulson (1992), 而Gordon (1988) 也以类似风格描述了定理证明器在程序验证环境中的应用. 其他关于自动定理证明的综合性教材包括Chang和Lee (1973), Duffy (1991) 和Fitting (1990), 此外还有一些更专门的著作将在后文中提及.

第1.10节 练习

第2章 命题逻辑

我们将会仔细研究命题逻辑, 在OCaml之中定义其形式句法, 连带着句法分析和打印支持. 我们将会讨论一些关键性的命题算法, 并证明紧致性定理, 还会指明命题定理证明的丰富应用.

第2.1节 命题逻辑的句法

命题逻辑是第1.4节所呈现的Boole的命题代数的一种现代版本. {原注: 诚然如此, 命题逻辑有时被称为Boole代数. 但是, 这容易令人感到困惑, 因为数学家将一切满足特定公理的代数结构都称为Boole代数, 大致上这些公理是通常的代数律连带着$x^2=x$ (Halmos 1963).} {译注: 这说的是Boole环, 可以被定义为含幺元的幂等环.} 其牵涉被称为公式的表达式, 而公式的意图是表示命题, 即可以被认为是真或者假的断言. {原注: 当查阅文献时, 读者或许会发现用的是术语合式公式 (缩写为wff) 而非仅仅公式. 这是为了强调在具体句法之中, 我们仅仅关心具有句法合法形式的字符串, 而非任意的符号的(字符)串.} 这些公式可以由常量true和false以及一些基本的原子命题 (或者说原子) 通过各种逻辑联结词 (not, and, or, 等等) 构筑而成. 原子命题类似于通常代数之中的变量, 有时我们将其称为命题变量或者Boole变量. 正如词汇原子所暗示的, 我们并不会分析其内在结构; 当我们在下一章中处理一阶逻辑时则要进行考虑.

第2.1.1小节 OCaml中的表示

我们使用一个OCaml数据类型来表示命题公式, 这可以类比于第1.6节里的表达式类型. 我们允许常量命题False和True以及原子命题Atom p, 并且可以由它们通过使用幺元运算符Not以及二元联结词And, Or, Imp (implies), Iff (if and only if) 构筑公式. 我们将对于这些联结词的确切含义的讨论推后, 先来处理立即有用的部分.

原子命题的潜在集合很大程度上是任意的, 尽管对于某些目的而言其应该是无限的, 以避免限制我们所能考虑的公式的复杂度. 在抽象处理之中原始命题往往就是用数字索引的. 我们令原子命题的潜在类型'a为公式类型的定义的一个参数, 由此许多基本函数可以不管该类型为何而一样工作. 当我们考虑扩展至一阶逻辑时, 这种乍看上去空洞的泛化有助于避免重复工作. 出于相同的理由, 我们包含了两个额外的公式类型构造子Forall和Exists. 这些在本章中大致上会被忽略, 不过其作用将会在之后变得清晰.

type ('a)formula = False
                 | True
                 | Atom of 'a
                 | Not of ('a)formula
                 | And of ('a)formula * ('a)formula
                 | Or of ('a)formula * ('a)formula
                 | Imp of ('a)formula * ('a)formula
                 | Iff of ('a)formula * ('a)formula
                 | Forall of string * ('a)formula
                 | Exists of string * ('a)formula;;

第2.1.2小节 具体句法

正如我们之前所见, Boole对于逻辑联结词使用了传统的代数符号, 例如$+$. 这使得许多逻辑事实看起来令人迷惑地熟悉, 例如$$p(q+r)=pq+pr$$

但是有些逻辑事实看起来就相当奇怪了, 例如若是将第一个公式中的and和or系统地交换, 则可以得到以下事实:$$p+qr=(p+q)(p+r)$${译注: 注意这里遵循惯例, 乘法先于加法进行计算.}

以逻辑的伪装这是在说如果$p$成立或者$q$和$r$都成立, 那么$p$或$q$成立, 且$p$或$r$成立, 反之亦然. 稍加思考则可令读者确信的确如此; 回忆一下$p$或$q$是可兼的, 即包含同时成立的情况.

为了避免困惑或者是由通常代数产生误导性的类比, 我们将会对于联结词使用如今业已标准化了的特殊符号. 下表的每一行我们给出了每种构造的英语读法, 之后跟着的是我们在讨论中所采用的标准符号化, 然后是我们在程序中所支持的ASCII近似化, 相应的抽象句法构造, 以及其他一些可能会用到的符号化. (最后一列如果只是阅读本书则可以忽略, 但是在参考其他文献时则会很有用.)

英语	符号	ASCII	OCaml	其他符号
false	$\perp$	false	False	$0,F$
true	$\top$	true	True	$1,T$
not $p$	$\neg p$	~p	Not p	$\bar{p},-p,~p$
$p$ and $q$	$p\wedge q$	p /\ q	And(p,q)	$pq,p\&q,p\cdot q$
$p$ or $q$	$p\vee q$	p \/ q	Or(p,q)	$p+q,p|q$
$p$ implies $q$	$p\Rightarrow q$	p ==> q	Imp(p,q)	$p\to q,p\supset q$
$p$ iff $q$	$p\iff q$	p <=> q	Iff(p,q)	$p\leftrightarrow q,p\equiv q,p~q$

符号$\vee$来源于拉丁词汇vel的首字母, 其意为可兼或. $\top$的形状类似于true的首字母, 而$\perp$和$\wedge$不过是$\top$和$\vee$的镜像, 体现了一种对偶原则, 这将在第2.4节中加以解释. 否定的符号与算术取负的符号足够相似, 因此容易记忆. 有些读者可能在非形式化的数学中见过推出和当且仅当的符号.

和普通代数一样, 我们需要建立联结词的优先级规则, 并且若有必要可以通过括号来覆写规则. 我们所采用的(颇为标准的)优先级顺序已经在上表中指明, 其中$\neg$是最高的, $\iff$是最低的. 例如, $p\Rightarrow q\wedge \neg r\vee s$意思是$p\Rightarrow ((q\wedge (\neg r))\vee s)$. 或许赋予$\wedge$和$\vee$相等的优先级更为合适, 但是只有少数作者这么做 (Dijkstra和Scholten 1990), 我们还是从众赋予$\wedge$更高的优先级.

我们所有的二元联结词都以向右结合的方式进行句法分析, 于是$p\wedge q\wedge r$的意思是$p\wedge (q\wedge r)$, 诸如此类. 在非形式化的实践里, 形式如$p\Rightarrow q\Rightarrow r$这样的迭代推出经常用作$p\Rightarrow q$且$q\Rightarrow r$的缩写, 就像$x\le y\le z$是$x\le y$且$y\le z$的缩写. 但是对于我们而言, $p\Rightarrow q\Rightarrow r$指的是$p\Rightarrow (q\Rightarrow r)$, 不是一个意思.

在非形式化的讨论里, 我们不会使得Atom构造子显式化, 但是会使用诸如$p,q,r$这样的名字代表一般的公式, 而$x,y,z$代表一般的原子. 例如, 当我们讨论$x\iff p$时, 我们往往指的是具有形式Iff(Atom(x),p)的公式.

{译注: 实际情况是, 这个记号约定基本上废的, $p,q,r$除了用于公式的元变量, 也一般用作原子命题的名字, 虽然一般不用作原子命题的元变量. 问题在于, 这足够引起混淆了, 例如$p\Rightarrow q$到底指的是一个具体的公式, 还是一个公式的形式/模式, 只能通过上下文判断.}

第2.1.3小节 通用句法分析和打印

我们为公式建立了自动化的句法分析和打印支持, 正如我们在第1.7–1.8节中对普通代数表达式所做的那样. 由于具体细节对当前目的而言并不重要, 代码的详细描述推迟到附录3中给出. 不过我们确实想要强调的是, 既然公式的类型是以原子命题的类型为参数的, 那么句法分析和打印函数也同样是参数化的. 函数parse_formula的类型为:

# parse_formula;;
- : (string list -> string list -> 'a formula * string list) *
    (string list -> string list -> 'a formula * string list) ->
    string list -> string list -> 'a formula * string list
= <fun>

第2.1.4小节 原始命题

尽管许多函数将会是通用的 (generic), 但是如果我们固定在一个确定的原始命题类型上, 对于某些操作进行实验会更加简单. 据此我们定义了以下的原始命题类型, 其由名字索引 (即字符串):

type prop = P of string;;

let pname(P s) = s;;

现在我们只需提供一个原子命题的解析器, 这相当直截了当. 出于附录3中解释的原因, 我们需要检查第一个输入字符是否不是左括号, 除此之外, 我们只需将输入流中的第一个标记作为原始命题的名称即可:

let parse_propvar vs inp =
  match inp with
    p::oinp when p <> "(" -> Atom(P(p)),oinp
  | _ -> failwith "parse_propvar";;

第2.1.5小节 句法操作

如果我们能有对应于公式构造子的句法操作作为正常的OCaml函数可用是很方便的:

let mk_and p q = And(p,q) and mk_or p q = Or(p,q)
and mk_imp p q = Imp(p,q) and mk_iff p q = Iff(p,q)
and mk_forall x p = Forall(x,p) and mk_exists x p = Exists(x,p);;

对偶地, 往往能够解构公式而不需要显式的模式匹配也是方便的. 以下这个函数解构了一个等价 (或者说biimplication, 或者说biconditional), 即将具有形式$p\iff q$的公式转换为序对$(p,q)$:

let dest_iff fm =
  match fm with Iff(p,q) -> (p,q) | _ -> failwith "dest_iff";;

类似地, 以下函数将一个合取公式$p\wedge q$分解为两个合取式(conjunct)$p$和$q$:

let dest_and fm =
  match fm with And(p,q) -> (p,q) | _ -> failwith "dest_and";;

let rec conjuncts fm =
  match fm with And(p,q) -> conjuncts p @ conjuncts q | _ -> [fm];;

下列类似的函数将一个析取公式$p\vee q$分解为析取式(disjunct)$p$和$q$, 一个是在顶层, 一个则是递归的:

let dest_or fm =
  match fm with Or(p,q) -> (p,q) | _ -> failwith "dest_or";;

let rec disjuncts fm =
  match fm with Or(p,q) -> disjuncts p @ disjuncts q | _ -> [fm];;

let dest_imp fm =
  match fm with Imp(p,q) -> (p,q) | _ -> failwith "dest_imp";;

一个推出式$p\Rightarrow q$里的公式$p$和$q$分别被称为其前件和后件, 而我们也应该定义相应的函数:

let antecedent fm = fst(dest_imp fm);;
let consequent fm = snd(dest_imp fm);;

我们经常需要通过对公式进行递归来定义函数, 正如我们在第1.6节中对化简所做的那样. 有两种递归模式似乎足够常见, 因此有必要定义通用函数. 下面这个函数将一个函数应用于公式中的所有原子, 但保持其余结构不变. 例如, 它可以用来将某个特定的原子命题系统地替换为另一个公式:

let rec onatoms f fm =
  match fm with
    Atom a -> f a
  | Not(p) -> Not(onatoms f p)
  | And(p,q) -> And(onatoms f p,onatoms f q)
  | Or(p,q) -> Or(onatoms f p,onatoms f q)
  | Imp(p,q) -> Imp(onatoms f p,onatoms f q)
  | Iff(p,q) -> Iff(onatoms f p,onatoms f q)
  | Forall(x,p) -> Forall(x,onatoms f p)
  | Exists(x,p) -> Exists(x,onatoms f p)
  | _ -> fm;;

下面这个函数是列表迭代器itlist之于公式的类比, 它将一个二元函数迭代地作用于公式中的所有原子:

let rec overatoms f fm b =
  match fm with
    Atom(a) -> f a b
  | Not(p) -> overatoms f p b
  | And(p,q) | Or(p,q) | Imp(p,q) | Iff(p,q) ->
        overatoms f p (overatoms f q b)
  | Forall(x,p) | Exists(x,p) -> overatoms f p b
  | _ -> b;;

一个特别常见的应用是收集与原子相关联的某种属性的集合; 最简单的情形就是返回所有原子的集合. 我们可以通过将一个函数$f$连同一个append操作迭代地作用于所有原子来实现这一点, 最后将结果转换为集合以去除重复项. (我们也可以在过程中使用union来逐步去除重复项, 但当涉及的集合较大时, 当前的实现方式可能更为高效.)

let atom_union f fm = setify (overatoms (fun h t -> f(h)@t) fm []);;

我们很快将会看到对于如何使用这些非常一般的函数的刻画.

第2.2节 命题逻辑的语义

既然命题公式意在表示可能为真或者为假的断言, 一个公式的最终含义只是两个真值true和false中的一个. 然而, 正如像$x+y+1$这样的一个代数表达式当我们知道变量$x$和$y$所代表的东西之后只有一个确切的含义, 一个命题公式的含义依赖于被分配给其原子公式的真值. 这种分配在一个赋值(valuation)之中进行编码, 赋值是一个从原子的集合到真值的集合$\{\mathrm{false},\mathrm{true}\}$的函数. 给定一个公式$p$和一个赋值$v$, 然后我们可以根据下列递归定义的函数求得总体的真值:

let rec eval fm v =
  match fm with
    False -> false
  | True -> true
  | Atom(x) -> v(x)
  | Not(p) -> not(eval p v)
  | And(p,q) -> (eval p v) & (eval q v)
  | Or(p,q) -> (eval p v) or (eval q v)
  | Imp(p,q) -> not(eval p v) or (eval q v)
  | Iff(p,q) -> (eval p v) = (eval q v);;

这是我们对于命题逻辑的数学定义, 意在作为对于我们的直觉的自然形式化. {原注: 我们也可以选择将部分求值了的eval p, 即一个从赋值到值的函数, 视为公式p的语义, 而非将赋值当作额外的参数. 这主要只是一种术语问题.} (implication的语义并不显然, 之后我们将详细讨论.) 每个逻辑联结词都由OCaml的内置类型bool上的一个相应的运算子所解释. 为了完全明确这些运算子的含义, 我们可以枚举所有可能的输入组合并观察相应的输出, 例如对于&运算子:

# false & false;;
- : bool = false
# false & true;;
- : bool = false
# true & false;;
- : bool = false
# true & true;;
- : bool = true

我们可以将这些信息排列在一张真值表中, 展示如何由一个公式的立即子公式的真值来确定该公式被赋予的真值:$$\begin{array}{|cccccc|}\hline p& q& p\wedge q& p\vee q& p\Rightarrow q& p\iff q\\ \text{false}& \text{false}& \text{false}& \text{false}& \text{true}& \text{true}\\ \text{false}& \text{true}& \text{false}& \text{true}& \text{true}& \text{false}\\ \text{true}& \text{false}& \text{false}& \text{true}& \text{false}& \text{false}\\ \text{true}& \text{true}& \text{true}& \text{true}& \text{true}& \text{true}\\ \hline\end{array}$$当然了, 出于完整性的考量, 我们也应该包括幺元否定的真值表:$$\begin{array}{|cc|}\hline p& \neg p\\ \text{false}& \text{true}\\ \text{true}& \text{false}\\ \hline\end{array}$$

让我们尝试在一个赋值下对公式$p\wedge q\Rightarrow q\wedge r$求值, 其中$p,q,r$分别被设为true, false和true. (我们不必费心去定义那些未出现在公式中的原子的值, OCaml会发出我们还没有完成的警告.)

# eval <<p /\ q ==> q /\ r>>
       (function P"p" -> true | P"q" -> false | P"r" -> true);;
...
- : bool = true

然而在另一个赋值下, 该公式可以求值为false; 读者可能会发现手动验证这些结果是有益的练习:

eval <<p /\ q ==> q /\ r>>
     (function P"p" -> true | P"q" -> true | P"r" -> false);;

第2.2.1小节 机械化了的真值表

我们期望对于一个公式的求值独立于赋值如何给没有出现在公式之中的原子分配真值. 让我们通过定义一个提取公式之中所出现的原子命题的集合的函数来使得我们的表述精确化. 以抽象的数学术语来说, 我们将通过公式上的递归定义$''atoms''$如下:$$\begin{array}{rcl}''atoms''(\perp )& =& \varnothing \\ ''atoms''(\top )& =& \varnothing \\ ''atoms''(x)& =& \{x\}\\ ''atoms''(\neg p)& =& ''atoms''(p)\\ ''atoms''(p\wedge q)& =& ''atoms''(p)\cup ''atoms''(q)\\ ''atoms''(p\vee q)& =& ''atoms''(p)\cup ''atoms''(q)\\ ''atoms''(p\Rightarrow q)& =& ''atoms''(p)\cup ''atoms''(q)\\ ''atoms''(p\iff q)& =& ''atoms''(p)\cup ''atoms''(q)\end{array}$$

作为公式上的结构归纳证明的一个简单例子 (见附录1和2), 我们将会证明$''atoms''(p)$总是有限的, 因而我们可以基于ML的列表来解释它而并没有曲解其含义. (当然了, 我们需要记住一般情况下列表相等性和集合相等性并不相同.) {译注: 我的理解大概就是这里可以使用列表表示集合, 仅此而已.}

类似地, 我们可以形式化地澄清以上所提及的直觉上显然的事实.

以上$''atoms''$的定义可以被直接翻译为一个OCaml函数, 例如对于$\cup$使用union而对于$\{x\}$使用[x]. 然而, 我们更倾向于基于既有的迭代子atom_union:

let atoms fm = atom_union (fun a -> [a]) fm;;

# atoms <<p /\ q \/ s ==> ~p \/ (r <=> s)>>;;
- : prop list = [P "p"; P "q"; P "r"; P "s"]

鉴于对于一个命题公式$p$的解释只依赖于赋值在有限集合$''atoms''(p)$ (设其有$n$个元素) 上的动作, 并且对于每个原子命题只有两种选择可作, 于是最终的真值完全由对于这些原子的总共$2^n$种选择所确定. 因此, 我们可以自然地将真值表形式的枚举从基本运算推广至任意的公式. 为了在OCaml中实现这个, 我们从定义一个函数开始, 其会测试一个函数subfn是否会在原子ats的所有可能赋值上返回true, 对于其他所有原子则使用既有的赋值v. 所有赋值的空间是通过相继修饰v以设定每个原子p为true和false与递归调用探索的:

let rec onallvaluations subfn v ats =
  match ats with
    [] -> subfn v
  | p::ps -> let v' t q = if q = p then t else v(q) in
             onallvaluations subfn (v' false) ps &
             onallvaluations subfn (v' true) ps;;

我们可以将其应用于一个函数, 这个函数绘制真值表的一行, 然后返回true. (这个返回值是重要的, 因为&只有在其第一个参数是true的情况下才会对于第二个参数进行求值.) 这可以用来绘制一个公式的整个真值表:

let print_truthtable fm =
  let ats = atoms fm in
  let width = itlist (max ** String.length ** pname) ats 5 + 1 in
  let fixw s = s^String.make(width - String.length s) ' ' in
  let truthstring p = fixw (if p then "true" else "false") in
  let mk_row v =
     let lis = map (fun x -> truthstring(v x)) ats
     and ans = truthstring(eval fm v) in
     print_string(itlist (^) lis ("| "^ans)); print_newline(); true in
  let separator = String.make (width * length ats + 9) '-' in
  print_string(itlist (fun s t -> fixw(pname s) ^ t) ats "| formula");
  print_newline(); print_string separator; print_newline();
  let _ = onallvaluations mk_row (fun x -> false) ats in
  print_string separator; print_newline();;

请注意, 我们以宽度为width的列进行打印, 列宽足以容纳所有原子的名字以及true和false, 外加一个末尾空格. 这样, 表格中的所有项就能整齐地对齐. 例如:

# print_truthtable <<p /\ q ==> q /\ r>>;;
p     q     r     | formula
---------------------------
false false false | true
false false true  | true
false true  false | true
false true  true  | true
true  false false | true
true  false true  | true
true  true  false | false
true  true  true  | true
---------------------------
- : unit = ()

第2.2.2小节 形式语言和自然语言

命题逻辑为我们提供了一种形式化的方式, 来表达英语或其他自然语言中某些复杂的命题. 练习将英语中的复合命题形式化 (即翻译为形式逻辑) 是很有益的. 正如在两种自然语言之间进行翻译一样, 我们不能总是期望逐词对应. 但只要对非形式命题的结构有一定的了解, 通常就可以进行相当直接的形式化.

在命题逻辑中, 除了上面给出的优先级规则之外, 我们还可以使用标准的数学括号技术将命题组合在一起, 例如区分$p\wedge (q\vee r)$和$(p\wedge q)\vee r$. 括号在英语和大多数其他语言中的用法截然不同 (用来插入像这样的旁注). 在英语中表示优先级是一件更加临时且笨拙的事情, 通常通过插入额外的标点符号和噪音词来给短语加括号, 从而消除歧义. 例如, 我们可以将上述两个例子分别表述为$p$, and also either $q$ or $r$和either both $p$ and $q$, or else $r$. 对于复杂的命题, 这种方式会变得非常繁琐, 而这实际上也是需要形式语言的部分原因.

一般来说, 像and, or和not这样的结构可以相当直接地从英语翻译为相应的逻辑联结词. 联结词not在英语中也可以隐含在前缀如dis-和un-中, 因此我们可以将You are either honest and kind, or dishonest, or unkind翻译为$H\wedge K\vee \neg H\vee \neg K$. 然而, 有时英语短语暗示着超越纯粹真值函数之外的细微含义. 例如, and常常表示因果关系 (he dropped the plate and it broke) 或时间顺序 (she climbed into bed and turned out the light). but一词可以说与and有着相同的真值函数解释, 但它表达的是各组成命题之间以一种出人意料或令人遗憾的方式相连. 同样, unless可以合理地翻译为or, 但由此导致的$p$ unless $q$与$q$ unless $p$之间的对称似乎令人意外.

更成问题的是推出式或条件式$p\Rightarrow q$与其预期的英语表述$p$ implies $q$或if $p$ then $q$之间的关系. 在这一点上表面上的不协调困扰着许多形式逻辑的初学者, 并且至少使一个人永远放弃了这门学科 (Waugh 1991). 事实上, 关于推出式的意义的争论可以追溯到两千多年前的墨伽拉-斯多噶学派逻辑学家 (Bochénski 1961). 据Sextus Empiricus记载, 公元前二世纪亚历山大图书馆的馆长Callimachus曾说连屋顶上的乌鸦都在争论哪些条件句是真的.

首先, 让我们明确一点: 如果我们对$p\Rightarrow q$采用任何真值函数语义, 即根据$p$和$q$的真值来定义$p\Rightarrow q$的真值, 那么我们所选择的语义是唯一合理的. 按照直觉理解, 推出最基本的原则是: 如果$p$和$p\Rightarrow q$都为真, 那么$q$也为真; 因此, 如果$p$为真而$q$为假, 则$p\Rightarrow q$必须为假. 此外, $p\wedge q\Rightarrow p$总是为真这一点也是合理的, 而只有我们所选择的语义才能在$p$和$q$取任意真值的情况下使之为真.

第2.3节 有效性, 可满足性, 重言

我们称一个赋值$v$满足一个公式$p$, 如果$''eval''pv$为真. 一个公式被称为是:

• 重言或者逻辑有效的, 如果其被所有公式满足, 或者等价地说, 如果其真值表的每一行的值都为真;
• 可满足的, 如果其被某个赋值满足, 即其真值表至少有一行的值为真;
• 不可满足的或者说矛盾, 如果没有赋值可以满足它, 即其真值表的每一行的值都为假.

注意到一个重言也是可满足的, 另外正如名字所暗示的, 一个公式是不可满足的恰当其不是可满足的. 而且, 在任何赋值中, $''eval''(\neg p)v$为假当且仅当$''eval''pv$为真. 因此, $p$是一个重言当且仅当$\neg p$是不可满足的.

最简单的重言是$\top$; 一个稍微有趣点的重言例子是$p\wedge q\Rightarrow p\vee q$ (如果$p$和$q$都为真, 那么$p$和$q$至少有一个为真), 而一个许多人第一眼看上去会比较惊讶的例子是Peirce律$((p\Rightarrow q)\Rightarrow p)\Rightarrow p$:

# print_truthtable <<((p ==> q) ==> p) ==> p>>;;
p     q     | formula
---------------------
false false | true
false true  | true
true  false | true
true  true  | true
---------------------

对于我们首先在OCaml中生成其真值表的公式$p\wedge q\Rightarrow q\wedge r$, 它是可满足的, 因为其真值表的最后一列有true, 但它不是重言, 因为其也有false. 最简单的矛盾是$\perp$, 另一个简单的矛盾是$p\wedge \neg p$ ($p$既为真又为假):

# print_truthtable <<p /\ ~p>>;;
p     | formula
---------------
false | false
true  | false
---------------

从直觉上来说, 重言总是为真, 可满足公式有时(但可能并不总是)为真, 矛盾总是为假. 的确如此, 重言意在形式化地捕获引论章节以非技术性方式所讨论的逻辑真性 (logical truth) 的概念, 到目前为止的话我们是在命题逻辑中定义了重言. 重言恰可以类比于诸如$x^2-y^2=(x+y)(x-y)$这样的代数等式, 其构成变量的值不论为何都是一般为真的 (universally true). 可满足公式可以类比于至少有解的等式, 但不必总是有效, 例如$x^2+2=3x$. {译注: 英语里等式和方程都是equation就是了.} 矛盾可以类比于无解的等式, 例如$0\cdot x=1$. {译注: 这里当然都是在实数域上讨论方程.}

将(不)可满足性的想法从公式推广至公式的集合是有用的: 公式的集合$\mathrm{\Gamma }$被称为是可满足的, 如果存在一个赋值$v$能够同时满足集合里的所有公式. 注意到同时: $\{p\wedge \neg q,\neg p\wedge q\}$是不可满足的, 即便其每个公式都是可满足的. 当所关心的集合有限时, 设$\mathrm{\Gamma }=\{p_1,\dots ,p_n\}$, $\mathrm{\Gamma }$的可满足性等价于单一公式$p_1\wedge \cdots \wedge p_n$的可满足性, 读者可从定义看出来. 然而, 在我们之后的工作里, 考虑无限的公式集合的可满足性也是必要的, 其就无法直接归约为单一公式的可满足性了. 我们也会使用记号$\mathrm{\Gamma }\models q$来表达对于所有使得每个$p\in \mathrm{\Gamma }$都为真的赋值, 该赋值也使得$q$为真. 注意到在有限的$\mathrm{\Gamma }=\{p_1,\dots ,p_n\}$这种情况下, $\mathrm{\Gamma }\models q$等价于断言$p_1\wedge \cdots \wedge p_n\Rightarrow q$是一个重言. 在$\mathrm{\Gamma }=\varnothing$的情况下, $\varnothing \models q$一般记为$\models q$, 意即$q$是一个重言. {译注: $\mathrm{\Gamma }\models q$一般读作$\mathrm{\Gamma }$语义蕴涵$q$.}

第2.3.1小节 重言和可满足性检查

虽然我们可以通过检查真值表来确定公式的状态, 但让计算机完成所有工作会更简单. 以下函数通过检查公式是否在所有赋值下均求值为true来测试该公式是否为重言式.

let tautology fm =
  onallvaluations (eval fm) (fun s -> false) (atoms fm);;

注意到一旦任意的求值碰到false, 那么根据onallvaluations的编写方式, 其会立即返回, 而不是坚持对于所有可能的赋值进行求值. {译注: 说立即返回其实稍有不准确之处, 因为鉴于它是(非尾)递归的, 所以返回时还需要走过之前途径了的and. 这一点其实可以优化, 但就onallvaluations这个函数而言没有必要优化.}

# tautology <<p \/ ~p>>;;
- : bool = true
# tautology <<p \/ q ==> p>>;;
- : bool = false
# tautology <<p \/ q ==> q \/ (p <=> q)>>;;
- : bool = false
# tautology <<(p \/ q) /\ ~(p /\ q) ==> (~p <=> q)>>;;
- : bool = true

使用之前注意到的其间关系, 我们可以基于重言定义可满足性和不可满足性:

let unsatisfiable fm = tautology(Not fm);;

let satisfiable fm = not(unsatisfiable fm);;

第2.3.2小节 替换

和代数恒等式一样, 我们期望能够将一个重言中的原子命题一致地替换为其他公式, 然后仍然得到一个重言. 我们可以将这种用公式去替换原子的函数定义如下, 其中subfn是一个有限部分函数 (见附录2):

let psubst subfn = onatoms (fun p -> tryapplyd subfn p (Atom p));;

例如, 使用替换函数$p|\Rightarrow p\wedge q$, 其将$p$映射为$p\wedge q$, 但在其他情况下则是未定义的, 我们得到:

# psubst (P"p" |=> <<p /\ q>>) <<p /\ q /\ p /\ q>>;;
- : prop formula = <<(p /\ q) /\ q /\ (p /\ q) /\ q>>

我们将会证明重言中的替换将会产生重言, 这是通过一个更为一般的结果完成的, 这个更为一般的结果可以利用公式上的结构归纳直接证明:

{原注: 记号$(x\mapsto a)v$表示这样一个函数$v^{\prime }$, 其映射$v^{\prime }(x)=a$而对于$y\models x$则映射$v^{\prime }(y)=v(y)$; 记号$x|\Rightarrow a$则表示这样的函数, 其将$x$映射为$a$, 对于其他参数则是未定义的. (见附录1) 在我们的OCaml实现里对于有限部分函数使用对应的运算符|->和|=>; 见附录2.}

请注意, 这一结果仅适用于对原子进行替换, 而非对任意命题进行替换. 例如, $p\wedge q\Rightarrow q\wedge p$是一个重言, 但是如果我们将$p\wedge q$替换为$p\vee q$, 就不复如此了. 这与普通代数中的情况完全一样, 而我们的替换函数是一个从原子名字出发的函数, 这一点有助于强制施加这样的限制. 不过, 主要结果可以很容易地推广到同时对多个原子进行替换的情形. 这些替换总是可以通过逐个重复执行单个替换来完成, 但可能需要引入额外的替换来更换变量, 以避免后续替换对先前替换产生虚伪的影响. 例如, 我们期望能够在$x\wedge y$中同时将$y$替换为$x$和$x$替换为$y$, 从而得到$y\wedge x$. 然而, 如果我们按顺序依次执行这些替换, 就会得到:$$\begin{array}{cl}& ''psubst''(x|\Rightarrow y)(''psubst''(y|\Rightarrow x)(x\wedge y))\\ =& ''psubst''(x|\Rightarrow y)(x\wedge x)\\ =& y\wedge y\end{array}$$

然而, 通过使用替换对于变量进行适切的重命名, 这样的问题总是可以避免的. 例如:$$\begin{array}{cl}& ''psubst''(z|\Rightarrow y)(''psubst''(y|\Rightarrow x)(''psubst''(x|\Rightarrow z)(x\wedge y)))\\ =& ''psubst''(z|\Rightarrow y)(''psubst''(y|\Rightarrow x)(z\wedge y))\\ =& ''psubst''(z|\Rightarrow y)(z\wedge x)\\ =& y\wedge x\end{array}$$

通过列举一些常见的重言式来培养对命题逻辑的直觉是很有帮助的. 其中一些简单而直观, 例如排中律$p\vee \neg p$, 它表明每个命题非真即假. 一个更令人意外的重言式——这无疑是因为$\Rightarrow$与直觉上的推出概念之间存在较大出入——为:

# tautology <<(p ==> q) \/ (q ==> p)>>;;
- : bool = true

如果$p\Rightarrow q$是一个重言 {译注: 这里的$p$和$q$是一般公式的元变量}, 即任何满足$p$的赋值也都满足$q$, 那么我们称$q$是$p$的一个逻辑推论. 如果$p\iff q$是一个重言, 即一个赋值满足$p$当且仅当其满足$q$, 那么我们称$p$和$q$是逻辑等价的. {译注: 这里引入的逻辑推论和逻辑等价都是语义而非句法概念.} 许多重要的重言都具有后者的形式, 并且如果$p$是一个重言, 那么平凡地$p\iff \top$也是一个重言, 读者很容易确认这一事实. 在代数里, 给定一个合法的等式如$2x=x+x$, 那么我们可以在任意的其他表达式里将$2x$替换为$x+x$而不改变其值. 类似地, 如果一个赋值满足$p\iff q$, 那么我们可以在另一个公式$r$里将$p$替换为$q$或者反过来而不改变这个赋值是否满足$r$, 即便$p$或$q$并非原子. {译注: 不改变$r$在这个赋值下的解释结果.} 既然我们还没有形式化地定义非原子的替换, 我们可以想象通过使用模式项的某个原子$x$来将替换位置确定下来.

第2.3.3小节 一些重要的重言

闲话少说, 下面列出一些重言式. 其中许多如果用Boole本人的符号重写, 就对应于普通代数的定律, 例如$p\wedge \perp \iff \perp$对应于$p\cdot 0=0$.

以上最后几个重言式或许尤其令人惊讶, 因为我们在日常数学中并不习惯等式中嵌套等式的情形. 实际上, 它们表明$\iff$是一个对称且具有结合律的运算符 (类似于算术中的$+$), 即迭代等价 (iterated equivalences) 的顺序和结合方式在逻辑上没有任何差别. Dijkstra和Scholten (1990) 给出了一些涉及等价的其他重言式, 这些重言式可以在OCaml中加以验证; 他们将其中第二个重言式称为黄金法则.

# tautology <<p \/ (q <=> r) <=> (p \/ q <=> p \/ r)>>;;
- : bool = true
# tautology <<p /\ q <=> ((p <=> q) <=> p \/ q)>>;;
- : bool = true

我们的重言式列表里还有一个对应于逆否原理的重言, 即$p\Rightarrow q$和其逆否式$\neg q\Rightarrow \neg p$的等价, 或者$p\Rightarrow \neg q$和$q\Rightarrow \neg p$的等价. (例如, those who mind don't matter和those who matter don't mind是逻辑等价的.) 与之形成对比的是, 我们可以确认$p\Rightarrow q$和$q\Rightarrow p$并非等价, 这是常见谬误:

# tautology <<(p ==> q) <=> (~q ==> ~p)>>;;
- : bool = true
# tautology <<(p ==> ~q) <=> (q ==> ~p)>>;;
- : bool = true
# tautology <<(p ==> q) <=> (q ==> p)>>;;
- : bool = false

第2.4节 De Morgan律, 充足性, 对偶性

以下重要的重言被称为De Morgan律, 其是以Augustus De Morgan的名字命名的, 他和Boole几乎是同时代的人物, 对于逻辑领域作出了重要贡献.$$\neg (p\vee q)\iff \neg p\wedge \neg q$$$$\neg (p\wedge q)\iff \neg p\vee \neg q$$

第一个重言的一个日常例子是I can not speak either Finnish or Swedish和I can not speak Finnish and I can not speak Swedish意思相同. 第二个重言的一个例子是I am not a wife and mother和either I am not a wife or I am not a mother (or both)是相同的. De Morgan律的变体, 同样也很容易看出来是重言, 为:$$p\vee q\iff \neg (\neg p\wedge \neg q)$$$$p\wedge q\iff \neg (\neg p\vee \neg q)$$

这些重言之所以是有趣的, 是因为它们展示了对于联结词$\wedge$和$\vee$, 如何用其中一个表达另外一个. 根据之前关于替换的定理, 这意味着比如说我们可以重写任意公式为一个与之逻辑等价但并不包含$\vee$的公式, 只需系统地将具有形式$q\vee r$的子公式替换为$\neg (\neg q\wedge \neg r)$. 关于用某些逻辑联结词表达其他逻辑联结词, 还有许多其他选项. 例如, 使用下列等价, 对于任意的公式我们都可以找出一个与之等价的仅仅使用原子公式, $\wedge$, $\neg$的公式. 以术语来说, $\{\wedge ,\neg \}$是联结词的一个充足集合(adequate set).$$\begin{array}{rcl}\perp & \iff & p\wedge \neg p\\ \top & \iff & \neg (p\wedge \neg p)\\ p\vee q& \iff & \neg (\neg p\wedge \neg q)\\ p\Rightarrow q& \iff & \neg (p\wedge \neg q)\\ (p\iff q)& \iff & \neg (p\wedge \neg q)\wedge \neg (\neg p\wedge q)\end{array}$${译注: 所谓的逻辑常量$\perp$和$\top$是零元联结词.}

类似地, 下列经OCaml验证的等价表明$\{\Rightarrow ,\perp \}$也是充足的:

forall tautology
 [<<true <=> false ==> false>>;
  <<~p <=> p ==> false>>;
  <<p /\ q <=> (p ==> q ==> false) ==> false>>;
  <<p \/ q <=> (p ==> false) ==> q>>;
  <<(p <=> q) <=> ((p ==> q) ==> (q ==> p) ==> false) ==> false>>];;
- : bool = true

单独一个联结词是否足以表达所有其他联结词? 对于我们已经引入的联结词而言, 答案是否定的. 我们至少需要一个二元联结词, 否则我们永远无法引入涉及多个变量 (从而依赖于多个变量的赋值) 的公式. 而且事实上, 即使是整个集合$\{\top ,\wedge ,\vee ,\Rightarrow ,\iff \}$, 如果没有$\neg$或$\perp$, 也不构成一个充足集, 因此更不用说其中任何单个二元联结词了. 要看出这一点, 注意所有这些二元联结词在两个参数均为真时都给出结果真. (换言之, 它们各自真值表的最后一行, 最终列都是真.) 因此, 由这些组件构建的任何公式, 在将所有原子都映射为真的赋值下, 必定求值为真, 所以否定是不可表达的.

然而, 对于二元真值函数而言, 存在$2^{2^2}=16$种真值表, 而常规的二元联结词只覆盖了其中四种情况. (真值表有$2^2=4$行, 每一行可以在两种真值里选择一个.) 或许某个以其他$12$种函数之一为其真值表的联结词可以是充足的? 正如以上所论证的, 任意单独的充足联结词都必须以假作为其真值表最后一行的值, 不然的话否定无法表达. 根据类似的论证, 我们也可以看出来真值表第一行的值必然为真. 那么, 留给我们的选择自由就只剩中间两行的情况了, 总计有四种可能性. 其中有两种可能是平凡的, 因为它们只是对于其中一个参数进行否定, 故无法用来构建求值依赖于多于一个单一原子的值的表达式. 不过, 其他两种情况单独都是充足的: 一种是not and运算$pNANDq=\neg (p\wedge q)$, 另一种是not or运算$pNORq=\neg (p\vee q)$. 这两个的真值表如下:$$\begin{array}{|cccc|}\hline p& q& pNANDq& pNORq\\ \text{false}& \text{false}& \text{true}& \text{true}\\ \text{false}& \text{true}& \text{true}& \text{false}\\ \text{true}& \text{false}& \text{true}& \text{false}\\ \text{true}& \text{true}& \text{false}& \text{false}\\ \hline\end{array}$$

例如, 我们可以通过$\neg p=pNANDp$来表达否定, 然后得到$p\wedge q=\neg (pNANDq)$, 不过我们已经知道$\{\wedge ,\neg \}$是充足的了; $NOR$以类似的方式成立. 实际上, 一旦我们有了一个联结词的充足集合, 那么我们也可以找出各种公式, 其语义分别对应于其他$12$种真值函数. 当我们于第2.6节讨论析取范式时, 这会变得清晰起来.

联结词$NAND$和$NOR$的单独充足性对于电子设计师而言是众所周知的: 对应的门是数字电路的基本构建块 (见第2.7节). 在纯粹逻辑学家之间, 这两个联结词其中之一会被习惯上记为$p|q$, 而$|$会被称为Sheffer竖线 (Sheffer 1913).

{原注: 如今人们通常将竖线解释为$NAND$, 但Sheffer最初用他的竖线表示的是$NOR$, 并且Nicod (1917) 将其用于命题逻辑的一个精简表述中. 这一思想早在30年前就已为Peirce所熟知. Schönfinkel (1924) 将其扩展为一种量词竖线, 其中$\varphi (x){|}_x\psi (x)$意为$\neg \exists x.\varphi (x)\wedge \psi (x)$, 这进而引发了人们对将同样的精简方法应用于更一般的数学表达式的兴趣, 并由此推动了他对组合子的发展.}

第2.4.1小节 对偶性

在第1.4节里我们注意到我们需要在或的可兼和不可兼解读之间作出选择. 无疑and和inclusive or之间的令人满意的对称是选择可兼解读的一个强烈动机. 设我们现在有一个公式, 只牵涉联结词$\perp ,\top ,\wedge ,\vee$. {译注: 漏了一个联结词, 即$\neg$.} 当我们言称其对偶(dual)时, 我们指的是系统交换$\wedge$和$\vee$以及$\top$和$\perp$所得到的结果, 因而有以下定义:

let rec dual fm =
  match fm with
    False -> True
  | True -> False
  | Atom(p) -> fm
  | Not(p) -> Not(dual p)
  | And(p,q) -> Or(dual p,dual q)
  | Or(p,q) -> And(dual p,dual q)
  | _ -> failwith "Formula involves connectives ==> or <=>";;

# dual <<p \/ ~p>>;;
- : prop formula = <<p /\ ~p>>

稍加思索即可发现$''dual''(''dual''(p))=p$. 对偶的关键语义性质如下:

第2.5节 化简和否定范式

第2.6节 析取范式和合取范式

第2.6.1小节 通过真值表得到DNF

第2.6.2小节 通过变换得到DNF

第2.6.3小节 基于集合的表示

第2.6.4小节 CNF

第2.7节 命题逻辑的应用

第2.7.1小节 Ramsey定理

第2.7.2小节 数字电路

第2.7.3小节 加法

第2.7.4小节 乘法

第2.8节 定义性CNF

第2.8.1小节 定义性CNF的实现

第2.8.2小节 优化

第2.8.3小节 3-CNF

第2.9节 Davis-Putnam过程

Davis-Putnam过程是一种用于判定具有合取范式的命题公式的可满足性的方法. 实际上有两种显著不同的算法都被常称为Davis-Putnam, 但我们将分别讨论它们, 并尽量在术语上加以区分. Davis和Putnam (1960) 提出的原始算法将简称为Davis-Putnam (DP), 而由Davis, Logemann和Loveland (1962) 发展出的后来更为流行的变体将被称为Davis-Putnam-Loveland-Logemann (DPLL). 按照历史顺序, 我们首先考虑DP.

第2.10节 Stålmarck方法

第2.11节 二元决策图

第2.12节 紧致性

第2.13节 深入阅读

第2.14节 练习

第3章 一阶逻辑

我们现在从命题逻辑移至更为丰富的一阶逻辑, 其中命题可以牵涉全称或者存在量化的非命题变元. 我们将会展现一阶逻辑之中的证明是如何可以藉由Herbrand定理被朴素地机械化的. 接着我们将会引入诸多改进, 特别是合一 (unification), 其可以使得自动化证明更加高效.

第3.1节 一阶逻辑及其实现

命题逻辑只允许我们从原始命题构建公式, 原始命题本身或许是独立地为真或者为假.

第3.2节 句法分析和打印

第3.3节 一阶逻辑的语义

第3.4节 句法操作

第4章 相等性

第5章 可判定问题

第6章 交互式定理证明

我们迄今为止的努力一直致力于让计算机完全自动地证明定理. 然而, 在任何相对现实的计算能力限制下, 全自动方法所能覆盖的范围仅限于当代数学中非常小的一部分. 在这里, 我们提出一种替代方案: 一个交互式证明助手, 它可以帮助精确地陈述和形式化证明, 同时还能自动处理一些繁琐的细节. 此外, 为了确保其可靠性, 我们基于一个非常简单的逻辑内核来设计该证明助手.

第6.1节 面向人类的方法

我们已经投入了大量精力来让计算机完全自动地证明命题. 我们所实现的方法相当强大, 在某些类型的证明上甚至比 (大多数) 人做得更好. 然而, 许多数学领域中那些极其复杂的逻辑推理链, 几乎不可能被我们所介绍的这类系统化算法在合理的时间内发现. 在实践中, 人类数学家通过直觉、对具体实例的实验、与相关结果的类比或外推、对问题背景的大胆推广 (例如在数论中使用复分析方法) 以及纯粹的运气来找到这些推理链——参见Lakatos (1976), Polya (1954) 和Schoenfeld (1985), 他们分别从不同角度尝试对数学发现的过程进行方法论分析. 可以说, 几乎没有人类数学家会用我们所开发的那些方法来从事定理证明.

面对系统化算法方法的局限性, 一种自然的反应是尝试设计能以更接近人类风格进行推理的计算机程序. 甚至在我们迄今讨论的那些方法被正式发展之前, 一些研究者就凭直觉认为系统化方法不会有多大实际用处, 并着手探索更面向人类的方法. 例如, Newell和Simon (1956) 设计了一个程序, 能够证明数学原理 (参见第6.4节) 中许多简单的逻辑定理. 大约同一时期, Gelerntner (1959) 设计了一个证明器, 能够利用人类风格的图形来引导或限制证明过程, 从而证明Euclid几何中的事实. 然而, 事实证明他们的基本思路, 尤其是他们对系统化方法的悲观态度, 并未完全得到验证. 例如, 从Wu开始的几何定理证明的系统化方法 (参见第5.12节) 已经取得了显著成效, 无疑超越了Gelerntner或其他使用面向人类方法的研究者所取得的任何成果. 正如Wang (1960) 在展示他那个用于一阶逻辑AE片段 (第5.2节) 的简洁系统化程序时所评论的——该程序的效果远远超过了Newell和Simon的程序:

作者 [...] 仍然不禁感到, 这一对比揭示了他们方法中的一个根本性缺陷. 杀鸡不必用牛刀. 然而总体印象却是, Newell-Shore-Simon连用牛刀杀鸡都没能成功.

不过, 公平地说, 那些追求面向人类方法的研究者, 其首要目标往往并非制造一个高效的定理证明器, 尽管那可能是个令人心动的附带成果. 他们的目标更多是通过形式化重构来理解人类的思维过程. 从追求这一目标的角度看, 表现平庸可能恰恰意味着成功而非失败, 因为人类本来就不太擅长解决逻辑谜题!

在20世纪50年代对定理证明的系统化和面向人类两种方法进行了最初的探索之后, 前者几乎完全胜出. 只有少数研究者继续追求面向人类的方法, 其中最著名的是Bledsoe, 例如他尝试将人类在证明分析学中关于极限的定理时常用的方法形式化 (Bledsoe 1984). Bledsoe的学生Boyer与Moore一起开发了卓越的NQTHM证明器 (Boyer和Moore 1979), 它往往能够对所提出的定理进行自动推广, 并用归纳法证明推广后的定理. NQTHM的成功, 以及将其方法纳入一个简洁概念框架的巨大困难, 促使Bundy (1991) 在一个基于证明规划的一般推理科学框架中重新构建了它的方法.

面对面向人类方法在计算机化后的有限成功, 一种更为强硬的反应是指出, 在某些情况下, 即使对人类而言, 系统化方法也更为优越. 例如, Knuth和Bendix (1970) 认为完备化 (第4.7节) 是对数学家处理等式公理时所进行的实验的一种有益的系统化. 对计算领域中拟人化倾向的反感 (Dijkstra 1982b) 或许在某些圈子里推动了一种趋势, 即让人类的证明变得更加系统化和句法驱动——简而言之, 更加机器化 (Dijkstra和Scholten 1990). 而Wos则将他在应用自动推理方面取得的巨大成功归因于他充分发挥了计算机的优势, 而非试图让它模仿人类思维:

简单来说, 人的推理方式与本书所介绍的这类程序的推理方式之间存在大量差异. 这些差异或许在一定程度上解释了为什么OTTER能够成功回答那些数十年悬而未决的问题, 也解释了为什么使用它所产出的证明远比此前已知的更加优雅. (即使我知道需要做什么, 我也不会把OTTER重新设计成像数学家, 逻辑学家或任何其他人那样工作, 而这并非出于对人类推理能力的不尊重.) (Wos和Pieper 1999)

第6.2节 交互式证明器和证明检查器

经验表明, 无论是系统化算法方法还是启发式的面向人类方法, 都无法自动证明范围广泛的高难度数学定理. 而且, 没有迹象表明这些方法的渐进改进加上技术进步能够改变这一事实. 有些人甚至可能会认为, 将人类自身都无法发展出来的证明自动化, 本身就不是一件值得追求的事情.

[...] 我将数学证明视为我的理解的反映, 而理解是我们无法委托给他人或机器的东西. (Dijkstra 1976b)

一个更为谦逊的目标是创建一个能够验证人类所发现的证明, 或者在人类指导下提供有限辅助的系统. 计算机至少应当充当一个谦恭的文书助手, 检查证明的正确性, 防范人类常犯的错误, 如隐含假设和遗漏的特殊情况. 理想情况下, 计算机可以通过自动化证明中的某些部分来实质性地辅助这一过程; 毕竟, 证明中往往包含一些只是常规验证或适合自动化处理的部分, 例如代数恒等式. 这种让机器与人类协作, 从证明草稿出发来完成定理证明的想法, 早在Wang (1960) 那里就已经被设想过了, 他在自动定理证明方面的工作仅仅是为这样一个系统奠定基础:

作者最初的目标是以数学教科书为纲要——例如Landau的数系, Hardy-Wright的数论, Hardy的微积分, Veblen-Young的射影几何, 以及Bourbaki的各卷——让机器将所有证明形式化 (即填补其中的空白).

第6.2.1小节 早期证明助手

早期的计算机只支持批处理工作方式, 周转时间很长. 但到了20世纪60年代, 一种更具交互性的工作方式开始普及. 得益于此, 加上人们或许感觉到全自动系统的能力开始趋于平稳, 对证明助手这一理念的兴趣日益增长. 第一个有效的实现是SAM (半自动数学) 系列证明器:

半自动数学是一种定理证明方法, 它试图将自动逻辑程序与常规证明过程相结合, 使得到的过程既高效又能接受人类以控制和引导形式进行的干预. 由于它使数学家成为建立定理过程中的一个不可或缺的因素, 这一方法有别于通常的定理证明尝试——在那些尝试中, 计算机独自寻求建立证明. (Guard, Oglesby, Bennett和Settle 1969)

1966年, 该系列系统中的第五个, 即SAM V, 被用来构造了格论中一个此前未被证明的猜想的证明 (Bumcrot 1965). 这无疑是半自动方法的一次成功, 因为计算机自动证明了一个现在被称为SAM引理的结果, 而数学家则认识到它可以轻松地推导出Bumcrot猜想的证明.

在SAM项目之后不久, 另外两个重要的证明检验系统问世: AUTOMATH (de Bruijn 1970; de Bruijn 1980; Nederpelt, Geuvers和Vrijer 1994) 和Mizar (Trybulec 1978; Trybulec和Blair 1985). 这两个系统都以不同的方式产生了深远的影响, 并且都被用来检验过非平凡的数学内容. 尽管我们也将这些系统称为交互式的, 但我们只是松散地使用这个术语, 作为自动的反义词. AUTOMATH和Mizar实际上都是围绕批处理使用方式设计的. 然而, 它们所处理的文件由一个证明或证明草稿组成, 系统检验其正确性, 而非一个需要自动证明的命题.

第6.2.2小节 LCF

许多成功的证明检查器, 包括Mizar在内, 自动化能力相对较弱, 要求用户以相当详细的方式描述证明, 只留给机器很小的空白去填补. 例如, Mizar的自动化能力相当有限, 仅限于在精确逻辑意义上显然的步骤 (Davis 1981; Rudnicki 1987). 在一定程度上, 这种弱势是一种有意的设计选择. 如果证明草稿中的空白过大, 那么对于没有机器辅助的人类读者来说, 这个草稿就很难理解——而既然现在的重点是帮助人类数学家, 而非展示自动化的高超技艺, 那这似乎是一个不可取的特性. 这一限制还大大缩小了填补证明空白或判断该空白中隐含的推理是否非显然所需的搜索范围, 从而使证明检验过程可以变得相当高效. 由于Mizar是为批处理使用而设计的, 即在一次交互中检验可能很长的证明文本, 这一点尤为重要.

然而, Mizar对显然推理的定义往往与人类对什么是显然的定义不一致, 而且这种偏差似乎是不可避免的. 一个特别的困难在于, 人们认为显然的东西可能包含关于正在被形式化的数学分支的领域特定知识. 例如, 代数恒等式通常是显然或常规的, 但将它们分解为Mizar能接受为显然的步骤却可能十分繁琐. 更重要的是, 一旦某个结果被形式化之后, 可能被视为显然的新事实似乎没有尽头 (Zammit 1999b). 例如, 人们可能已经证明了在某个抽象数学分支中出现的某个二元运算符$\otimes$满足结合律和交换律. 从那时起, 比如说$w\otimes (x\otimes (y\otimes z))=(x\otimes z)\otimes (w\otimes y)$这样的等式可能就被视为显然的, 人们不会在一个更有趣的证明中为此多费笔墨. 然而, 从结合律和交换律出发对此进行纯逻辑推导需要这些律的多个实例, 因此它在Mizar的意义上并非显然.

一个证明检查器的最初设计者几乎不可能预见到它未来的所有应用, 以及那些可能因此而被视为显然的新事实. 这表明理想的证明检验器应该是可编程的, 即普通用户应当能够根据需要扩展其内置的自动化功能. 只要定理证明器的基本机制是简明的且有良好的文档说明, 并且源代码是公开的, 用户就没有理由不能对其进行扩展或修改——我们希望许多读者会对本书中讨论的代码做类似的事情. 然而, 如果我们想要限制用户只进行逻辑上可靠的扩展, 困难就出现了, 因为不可靠性会使机器检验据说更容易出错的人类证明这一整个理念都变得可疑. 即使是我们在本书中实现的那些独立的自动定理证明程序, 往往也比它们表面看上去更加微妙, 如果发现它们偶尔包含导致不正确性的bug, 我们也不会感到意外. 将大量特殊的证明方法集成到一个强大的交互式系统中而不损害可靠性, 这一任务的难度要大得多.

对这一困难的一个有影响力的解决方案是在Robin Milner领导的Edinburgh LCF项目中引入的 (Gordon, Milner和Wadsworth 1979). 最初的Edinburgh LCF系统旨在支持基于可计算函数逻辑 (Scott 1993) 的PPλ逻辑中的证明——LCF这个名称由此而来. 但正如Gordon (1982) 所强调的, 其核心思想同样适用于支持传统数学的更正统的逻辑, 随后许多LCF风格的证明检查器都是基于相同的原则设计的 (Gordon 2000). LCF方法的基础是两个关键思想, 其中一个保证了灵活的可编程性, 另一个则确保了逻辑可靠性.

• 该系统在一种交互式编程语言中实现, 用户通过该编程语言的顶层循环进行交互. 因此, 用户拥有一种通用编程语言的全部能力来实现新的证明过程.
• 系统区分了一个特殊的已证定理类型 (比如说thm), 使得任何thm类型的东西必须是通过构造被证明的, 而非仅仅被断言的. 这通过将thm设为一个抽象类型来强制实现, 其唯一的构造器对应于经过批准的推理方法.

最初的LCF项目引入了一种全新的编程语言, 名为ML (元语言), 专门为实现LCF风格的证明器而设计——我们自己的实现语言Objective CAML就是它的直接后裔. 我们将在OCaml中使用LCF方法实现一个一阶逻辑的证明器, 但首先我们需要确定一组合适的经过批准的推理规则.

第6.3节 一阶逻辑的证明系统

像一阶逻辑这样的形式语言旨在成为非形式数学记号的精确版本. 给定这样一种语言, 一个形式证明系统应当将数学证明中允许的步骤形式化和系统化. (这些正是Leibniz所梦想的characteristica和calculus.) 抽象地说, 我们可以将证明系统简单地视为一种可证明性关系, 通过一组我们视为允许的证明步骤的规则归纳定义. 我们始终用$\mathrm{\Gamma }⊢p$来表示$p$可从假设$\mathrm{\Gamma }$证明, 当我们想要明确指出特定的证明系统时, 偶尔会在turnstile符号$⊢$上附加下标.

对于纯粹的等式推理, 一个自然的证明系统是由Birkhoff规则定义的系统 (参见第4.3节). 这些规则很好地形式化了人们通常使用等式进行推理的方式, 尽管用它们来证明定理可能需要极大的技巧, 但每条规则本身都相当简单. 此外, 这些规则是完备的 {译注: 且是可靠的 (sound)}: $\mathrm{\Delta }⊢s=t$ ($s=t$可从$\mathrm{\Delta }$证明) 当且仅当$\mathrm{\Delta }\models s=t$ ($s=t$是$\mathrm{\Delta }$的逻辑推论). 我们自然希望一般一阶逻辑的证明系统也具备所有这些性质.

第一个适用于一阶逻辑的证明系统是由Frege (1879) 发展出来的. 虽然这项工作现在被视为现代逻辑演化中的关键, 但在Frege生前却未受到多少重视, 类似的思想由Peano, Peirce和Russell等人部分独立地发展起来. Frege的证明系统实际上远远超出了一阶逻辑的范围, 并被用来支持他的逻辑主义论题, 即所有数学都可以归约为逻辑. 在研究Frege的工作时, Russell意识到他自己的许多哲学分析早已被Frege对算术的形式化发展所预见, 而且往往以更精练的形式呈现 (Frege 1893). 但Russell注意到Frege的工作有一个严重的缺陷: 该逻辑系统是不一致的, 实际上可以通过利用一个现在通常被称为Russell悖论的逻辑二律背反来证明任何事实, 无论真假 (参见第7.1节). 尽管Peano对形式系统的表述有限, 但独立发现了Russell悖论的Zermelo (1908) 声称Peano的方法同样受到该悖论的影响.

实际上是Hilbert和Ackermann (1950) 在其简短教科书1928年的原版中分离出了一阶逻辑, 提出了一套精确的形式规则体系, 并提出了这些规则的完备性问题. 可以说, 完备性隐含在Skolem (1922) 的一篇更早的论文中, 但它首先由Gödel (1930) 明确地证明了. 此后, 许多不同类型的一阶逻辑形式证明系统被引入并被证明是完备的. 我们可以大致将其区分为三类:

• Hilbert或Frege系统 (Frege 1879; Hilbert和Ackermann 1950),
• 自然演绎 (Gentzen 1935; Prawitz 1965),
• 相继式演算 (Gentzen 1935).

第6.4节 一阶逻辑的LCF实现

第7章 限制