“本书无疑是计算机科学最富成效的入门教科书之一……我们强烈建议把它作为教科书……”
　　　　　　　　　　　　　　　　　　　　　　　　　——美国计算机协会自动机与可计算性理论专业组 (SIGACT)
　　这是一本结合逻辑在计算机科学中的应用来介绍数理逻辑的教科书。书中主要介绍了消解定理证明、逻辑式程序设计和非经典逻辑（模态逻辑和直觉主义逻辑），所用的方法与数理逻辑的经典著作有很大不同，更加适合研究计算机理论的读者，可以帮助他们更好地理解计算机理论中的许多概念，是一本真正面向计算机科学的逻辑著作。另外，每章最后给出了进一步阅读建议，书末又分主题给出了相当多的参考文献，便于读者深入学习。
　　本书不要求读者具备逻辑基础知识，适合计算机科学系和数学系高年级本科生以及低年级研究生使用。

无

我们写这本书的目的是提供一本合适的数理逻辑初级教程，能比传统的教科书更加适应近年来逻辑在计算机科学中应用的迅速增长。因此，我们在题材的选择上受到这些应用的重要影响。当然，本书覆盖了传统的基本内容：语法、语义、可靠性、完全性和紧致性，以及一些更高级的结果，例如斯科朗勒文海姆（SkolemLwenheim)定理和厄布朗（Herbrand）定理。然而，这本书的很大一部分是讨论非传统的内容。消解定理证明在逻辑的处理中，尤其在逻辑式程序设计和PROLOG的应用中，起着重要的作用。因此，本书广泛地讲述了这三个主题的数学基础。此外，本书还加进了两章非经典逻辑——模态逻辑和直觉主义逻辑——它们在计算机科学中变得日益重要。 对于这些逻辑，我们（通过克里普克（Kripke）框架）论述了它们语法和语义的基本内容。在这两种情形中，我们用修正的经典逻辑的表方法研究形式证明、可靠性和完全性，指出了怎样使它适用于其他多种特殊类型的模态逻辑。一些更高级的主题（包括非单调逻辑）在介绍非经典逻辑的章节以及逻辑式程序设计和PROLOG的内容中做了简要的介绍。
　　本书是为数学系和计算机科学系高年级的本科生和低年级的研究生而写。我们假定读者学过任何一门代数或理论计算机科学的入门课程，了解这些课程提供的抽象推理，并且基本熟悉这些课程用到的非形式化的数学概念和论证。本书在开篇第一章的定义11中，给出了关于序和树的基本的集合论术语。在第六章中对基础集合论进行了系统的论述。这些内容可以作为必要时的参考，也可以放在课程的开头或结尾作为课程的一部分。
　　如果本书作为高年级本科生的教程，第一章到第三章的所有主要内容和PROLOG程序设计的相当一部分可以在一学期每周三小时的课程中讲完。如果按照这种方式授课，我们建议每周用一个额外的时间处理作业中的问题和进行编程指导。关于消解定理证明和逻辑式程序设计的内容，当然也可以用有关模态逻辑和直觉主义逻辑的章节来代替，从而构成一门完全不同的课程。作为两个季度的课程，可以在第一种建议中仅仅加进一种非经典的逻辑。我们有意把这两章处理成相互独立的章节，以便于上述选择。然而，这两章的处理有很多相似之处，所以如果两章都讲的话，第二章的相应部分可以更快地讲完。作为研究生教材，整本书的主要内容可以在一个学期之内讲完。
　　这本教材在引入谓词逻辑之前完整地介绍了命题逻辑。然而，根据学生的背景和教师的偏好，可以重新整合这种安排。事实上，作为研究生教材或者对于了解命题逻辑与真值表的学生，这种整合可能更好。如果这么做的话，就从第一章第一、二节开始，然后转到第二章第一至四节。如果计划介绍PROLOG并论述逻辑式程序设计的数学基础，可以用第二章第五节来解释PROLOG的语法和语义。为了让学生开始进行实际的编程，在这一节（还有第一章第十节）之后，可以非形式化地介绍PROLOG的执行方法和程序设计。当然其理论基础要等到我们形式化地论述了消解方法和合一算法之后。不管用不用逻辑式程序设计， 现在都能够（基于表方法）证明第二章第六至七节谓词逻辑的可靠性和完全性定理并在第二章第十节完成厄布朗定理的证明。我们介绍了一个希尔伯特式的证明系统，但是没有用它来证明第一章第七节和第二章第八节中的结果。
　　作为PROLOG的基础，消解式证明系统与其命题情形的论述联系更加紧密，因为基本的定理证明是根据厄布朗定理把谓词逻辑中的结论归约到相应的命题逻辑中的结论。因此，如果要涵盖这些内容，有必要先讨论命题逻辑的情形。介绍PROLOG要用到的章节是第一章的第八节、第十节以及第二章的第十一至十三节。第一章的第九节所考虑的加细消解是真正的备选内容。线性消解（第二章第十四节）与PROLOG有很大关系，而完全性定理是本书中最难的部分之一。因此，第三章第一节对于Horn逻辑和PROLOG的结果提供了一个替代的研究方法，这种方法只用到线性消解的基本定义（第二章的定义141~143）。
　　下面给出了本书（除了第六章外）各章节之间的逻辑依赖关系示意图。除非用箭头额外标出，否则依赖关系都是从右向左的。虚线（例如经典逻辑中从命题逻辑到谓词逻辑的那条线）表示相关但不严格的逻辑依赖。应该指出，最前面的一节，即第一章第一节，仅仅集中了一些在后面很多地方会用到的关于序和树的定义和事实。这个内容可以放在开头讲，也可以在用到的时候加以穿插。尤其库尼西（Knig）引理（第一章的定理14）直到第一章第四节讲完全系统表的时候才用到。类似地，第六章中的集合论的内容（第二版新增的内容）可以在任何时候讲述。只有第六节需要假定读者熟悉谓词逻辑，那里简单地列举了集合论公理的形式化版本。在这一章中，第一至五节和第七节包含了本书和大多数本科课程中所需的集合论的基本知识。其余部分，即第八至十一节，介绍了无穷的（甚至是不可数的）序数、基数和超穷递归理论，还有选择公理的一些不同的版本。对于数学系和计算机系的大部分研究生课程来说，这些集合论的背景知识应该足够了，但这些在本书的其他部分是用不到的。
　　在本书的很多地方，某些段落或整节对于后面的内容不是必要的，这些内容用星号(*)做了标记，以此表明它们脱离了本书内容的主线。另外，对于上面指出的内容安排有三个可能的例外，这些例外和那些不包含很多PROLOG内容的课程尤其相关。
　　第一个例外还有一点需要注意。本书对逻辑所做的基本研究不包含一个专用的等号谓词。尽管已不再是数理逻辑教材的通常做法，但对于消解定理证明、逻辑式程序设计以及PROLOG等主题，这是一个恰当的处理方法。 因此，在第三章的第五节分析了等号谓词，一方面把它视为特殊的谓词，其语义解释是真正的相等，从而满足相应的逻辑公理模式，另一方面把它作为一个普通的谓词，在所考虑的每一个系统中添加适当的等词公理。然而，把第三章第五节中定义53之前的相关内容和其中关于等号解释的可靠性和完全性定理的证明移到第二章第七节之后也是相当可行的。
　　第二个例外是关于谓词逻辑永真性不可判定的丘奇（Church）定理的证明。在第三章的第八节中给出的一个证明，甚至可应用于PROLOG所表示的谓词逻辑部分。但是，在第三章第五节的习题3中我们指出，对证明稍加改动即可绕开PROLOG的概念和方法，从而可在第二章第七节之后给出丘奇定理的一个证明。
　　最后，在第三章第七节中定义76之前引入的非单调逻辑独立于逻辑式程序设计和PROLOG的内容。第三章第七节的剩余内容是用非单调逻辑分析带否定的逻辑式程序设计的稳定模型。此外，作为更加独立的内容，第三章第七节的习题8~9给出了非单调逻辑在图和偏序上的其他应用。
　　应该指出，在第四章和第五章关于模态逻辑和直觉主义逻辑的基本内容中有相当多的重叠。实际上，一个无重叠的论述是可能的，但那样做会降低易读性。我们分别编写这两章，以便于读者独立地阅读其中之一。对于需要深入了解这两种逻辑的读者，我们在第五章第六节比较了经典逻辑、模态逻辑和直觉主义逻辑，试图指出这些逻辑的相似和不同之处。
　　本书几乎每一节的最后都有很多习题，这其中也包含一些PROLOG的程序设计问题，有的是作理论分析，有的是具体执行。特别地，有一系列关于《圣经》人物的家谱数据库的习题，这个家谱是根据《旧约历代记》编写的。我们还将它列在附录B中。（有电子版可用，请发送电子邮件至 shore@mathcornelledu 索取。）我们给出的这些习题可以用作使用类似数据库的范例，或者经过适当的修改后可以用于其他情形。然而这不是一本PROLOG程序设计的书，在讲授这些内容的同时，我们总是选择一本标准的PROLOG程序设计的教材作为补充，这些书目列在第三章最后的进一步阅读建议中。本书内容并不局限于特殊版本的PROLOG语言；我们仅使用标准的语法和讨论典型的执行方法。我们自己曾用过多种执行方法和平台。程序运行过程的打印件来自PC上运行的ARITY PROLOG。
　　当（偶尔）引用当代文献中的结果时，我们一般给出其出处。然而，由于这是一本基础的教科书，除了一些按通常做法以姓名命名的定理以外，我们并没有针对每个标准结果指明它的发现者。但是，在附录中给出了一个逻辑学的简史，这应该会让学生对于这门学科的发展有一个感性认识。另外，在每一章的最后给出了可能对学生或教师有用的进一步阅读建议。最后，在本书的末尾根据主题给出了相当多的参考文献。
　　多年以来，本书的部分内容以各种形式出现。关于经典逻辑和集合论的较早的版本出现在Nerode多年前在康奈尔大学的讲义中。 这些内容中的一部分，由George Metakides独立地重新编写，形成了与Nerode合作的英文讲义和他自己的在佩特雷大学的希腊文讲义。Nerode ［1990， 42］和［1991，44］包含了基于表方法的直觉主义逻辑和模态逻辑处理的早期版本，这两种方法分别于1988年和1989年在Montecatini Terme和Marktoberdorf所做的演讲中提出。 我们的消解方法也受到Richard Platek在康奈尔大学关于程序验证课程的影响。过去的几年中，这些内容的较新版本已经被很多数学系和计算机科学系的教师阅读和使用过，他们提出的意见和建议让我们受益匪浅。我们感谢Uri Abraham（以色列班固利恩大学数学系)、 John Crossley（澳大利亚莫纳什大学数学和计算机科学系）、 Ward Henson（乌尔班纳伊利诺斯大学数学系）、 Nils Klarlund（丹麦奥尔胡斯大学计算机科学系）、 Dexter Kozen（康奈尔大学计算机科学系）、 George Metakides（希腊佩特雷大学，欧洲经济共同体信息技术研究所） 和Jacob Plotkin（密歇根州立大学数学系）。这一版第一章所采用的定理411及其证明由Perry Smith（《MathReviews》杂志）提供。 Bakhadyr Khussainov指出了上一版中第五章的定理220的一处错误。 Warren Goldfarb（哈佛大学哲学系）帮助弥补了很多在历史附录里的缺陷。将本书的某些版本用于教学的Wiktor Marek（肯塔基大学计算机科学系）、George Odifreddi（意大利都灵大学计算机科学系） 和Robert Soare（芝加哥大学数学和计算机科学系）提出很多（而且非常有益的）建议。还应该感谢过去几年作为我们逻辑课程助教的研究生们： Jennifer Davoren、Steven Kautz、James Lipton、Sherry Marcus 和Duminda Wijesekera，他们提供了许多勘误和建议。
　　我们要感谢在过去几年里得到的资助：美国国家科学基金会（NSF）的DMS8601048、DMS8902797、DMS9204308、DMS9503503的资助；陆军研究办公室（ARO）在康奈尔大学数学科学研究所ACSyAM的DAAG2985C0018和DAAL0391C0027的资助和IBM在康奈尔大学的Ezra计划的设备支持。 我们还要感谢Arletta Havlik和Graeme Bailey帮助我们用TEX软件编辑前一版的原始文本，同时感谢Geraldine Brady、Jennifer Davoren、Nathaniel Miller、Robert Milnikel、George Odifreddi和David Solomon的校对工作。
　　最后，我们要把这本书献给我们的妻子Sally和Naomi，感谢她们不断的支持。

　　康奈尔大学
　　Anil Nerode，Richard A. Shore
　　1996年6月于纽约伊萨卡岛

本书讲述了逻辑及其在计算机科学中的应用。在当今这个信息时代，扎实的逻辑与逻辑应用功底同时惠及数学和计算机工作者。本书的前两版（英文版）在中国的数学和计算机界取得了积极反响，因此，对于本书被翻译成中文我们感到特别高兴。我们希望该中文版能够推动逻辑研究与应用的发展，同时我们也祝愿中国在逻辑、可计算性和计算机科学等领域不断取得进步。很多老师和学生使用过本书前两版并向我们提出了意见和建议，我们对此表示感谢并在此中文版里采纳了很多有益的建议。最后，我们特别感谢丁德成教授和他的学生徐亚涛、吴永成、金陈园，感谢他们花费时间和精力将我们的教材介绍给了更广大的中国读者。

　　Anil Nerode，Richard A. Shore
　　2006年11月于美国纽约伊萨卡岛
　　附原文
　　This book integrates logic with its computer science applications. In this Age of Information, a firm command of logic and its applications benefits both mathematicians and computer scientists. We have been very pleased with the positive reception accorded the first two (English) editions of this book by the mathematics and computer science communities in China. It is therefore especially gratifying to have it translated into Chinese. We hope that this Chinese edition will be of service in promoting the study and applications of logic and we look forward to the continuing development of logic, computability and computer science in China. We also thank all those, teachers and students, who used the previous editions and send us their comments and suggestions. Many of these have been incorporated into this edition. Finally, we are grateful to Prof. Ding Decheng and his students Xu Yatao, Wu Yongcheng and Jin Chenyuan who have taken the time and effort to make our textbook available to a wider Chinese audience.

　　Anil Nerode
　　Richard A. Shore
　　Cornell University
　　Ithaca NY USA
　　November, 2006

Anil Nerode;Richard A.Shore：Anil Nerode: 康奈尔大学数学系的创始人和教授，于1956年在芝加哥大学获得博士学位。他的研究领域包括数理逻辑、自动机、可计算理论、混合系统等。除本书外，他还与其他人合著了《Effective Completeness Theorems for Modal Logic》、《Tableaux for Constructive Concurrent Dynamic Logic》、《Logic, Categories, Lambda Calculus》等书。
Richard A.Shore: 康奈尔大学数学教授，于1972年在麻省理工学院获得博士学位。他的研究领域包括数理逻辑、递归论、集合论等。

丁德成 徐亚涛 吴永成 金陈园：暂无简介

本书是介绍数理逻辑的基础教材。与一般的数理逻辑教材相比，本书有两个较为显著的特点。其一，本书花了很大篇幅讨论逻辑在计算机科学中的应用，例如消解定理证明、逻辑式程序设计和非经典逻辑（模态逻辑和直觉主义逻辑），而且所用的方法与数理逻辑的经典著作有很大不同，更加适合研究计算机理论的读者，可以帮助读者更好地理解计算机理论中的许多概念，是一本真正面向计算机科学的逻辑著作。其二，本书在每章最后给出了一些进一步阅读建议，并在参考文献中对所列书目逐一做了简短有趣的点评，十分有利于读者的深入学习。
　　本书作者Anil Nerode和Richard A.Shore是国际知名逻辑学家、美国康奈尔大学教授，Richard A.Shore还是上一届符号逻辑协会（the Association for Symbolic Logic）主席。
　　本书曾在南京大学作为研究生教材使用多年，取得了很好的效果。鉴于本书的前两版（英文版）在中国数学和计算机界取得的积极反响，我们决定将它译成中文。在本书的翻译过程中我们得到了Nerode教授和Shore教授的大力支持，在此谨表衷心的感谢。根据本书作者发来的最新勘误表，我们在译稿中对这些错误全部作了改正。此外，我们对翻译过程中发现的少量其他错误也作了修正。
　　全书由丁德成教授统稿。其中，第一、二章由徐亚涛翻译，第三、四、五章由吴永成翻译，第六章、前言、绪论、附录和参考文献由金陈园翻译。译者排名按照章节顺序，不分先后。

　　译者
　　2007年1月于南京大学

出版者的话
专家指导委员会
译者序
中文版序
前言绪论
第一章命题逻辑
第一节序和树
第二节命题、联结词和真值表
第三节真值指派和赋值
第四节命题演算中的表证明
第五节表证明的可靠性和完全性
第六节前件演绎和紧致性
*第七节公理方法
第八节消解
第九节加细消解
第十节线性消解、Horn子句和PROLOG
进一步阅读建议
第二章谓词逻辑
第一节谓词和量词
第二节语言：项和公式
第三节形成树、结构和列表
第四节语义：含义与真值
第五节PROLOG程序解释
第六节证明：完全系统表
第七节表证明的可靠性和完全性
*第八节公理化方法
第九节前束范式和斯科朗化
第十节厄布朗定理
第十一节合一
第十二节合一算法
第十三节消解
第十四节加细消解：线性消解
进一步阅读建议
第三章PROLOG
第一节SLD消解
第二节执行:搜索与回溯
第三节执行的控制:cut
第四节PROLOG程序终止的条件
第五节相等
第六节因失败而否定
第七节否定和非单调逻辑
第八节可计算性与不可判定性
进一步阅读建议
第四章模态逻辑
第一节可能性与必然性；知识或信念
第二节框架和力迫
第三节模态表
第四节可靠性和完全性
第五节模态公理和特殊的可达关系
*第六节公理化方法
进一步阅读建议
第五章直觉主义逻辑
第一节直觉主义与构造主义
第二节框架和力迫
第三节直觉主义表
第四节可靠性和完全性
第五节可判定性和不可判定性
第六节比较指南
进一步阅读建议
第六章集合论基础
第一节集合论中的一些基本公理
第二节集合的布尔代数
第三节关系、函数和幂集公理
第四节自然数、算术和无穷
第五节替换、选择和基础
第六节谓词逻辑中的策梅洛弗兰克尔集
合论
第七节基数：有穷和可数
第八节序数
第九节序数算术和超穷归纳
第十节超穷递归、选择和有秩全域
第十一节基数和基数算术
进一步阅读建议
附录 A历史回顾
附录B一个家谱数据库
参考文献