Computability and Logic（可计算性与逻辑）

引用

Boolos, G. S., Burgess, J. P., & Jeffrey, R. C. (2007). Computability and Logic (5th ed.). Cambridge University Press.

章节概要

第五版正文约340页，共27章，前有第五版序言，末有两页的带注释参考书目。各章大致分为三条互相交叠的线索：可计算性理论、一阶逻辑的元理论，以及建立在二者之上的一组拓展专题。出版社说明，每章末尾附有一组习题。

第1–2章：可枚举性；对角化

全书以两个短章开篇（第3–22页），讲可枚举性与对角化。它们提供了后文各项限制性结果所依赖的计数与对角论证技巧。

第3–5章：图灵可计算性；不可计算性；算盘可计算性

这几章（第23–62页）介绍两种计算模型，即图灵机与算盘机，并有一章讨论哪些东西不可计算。算盘机一章比图灵机一章篇幅更长。

第6–8章：递归函数；递归集与递归关系；可计算性的等价定义

先展开用递归函数刻画可计算性的路径，再把它应用于集合与关系，这条线索的最后一章把各种可计算性定义汇合到一起（第63–98页）。

第9–10章：一阶逻辑概要：句法；一阶逻辑概要：语义

对一阶逻辑句法与语义的压缩回顾（第101–125页）。“概要”一词表明，这是写给已修过相关课程的读者的复习，而不是初次介绍。

第11章：一阶逻辑的不可判定性

可计算性内容的第一项重要收获：一个关于一阶逻辑本身的结果（第126–136页）。

第12–14章：模型；模型的存在性；证明与完全性

元理论中模型论与证明论的核心部分（第137–186页）。章名指向通向完全性定理的模型存在性论证。

第15–18章：算术化；递归函数的可表示性；不可定义性、不可判定性与不完全性；一致性的不可证明性

不完全性的主线（第187–240页）。算术化与可表示性铺垫基础，下一章把不可定义性、不可判定性与不完全性放在一起处理，最后一章转向一致性的不可证明性。出版社称，本版对可表示性的处理是全新的，比以往更简单。

第19–23章：范式；克雷格插值定理；单谓词与双谓词逻辑；二阶逻辑；算术可定义性

狭义逻辑中的进一步专题（第243–294页），从范式和克雷格插值定理，经单谓词与双谓词逻辑、二阶逻辑，到算术可定义性。

第24–27章：不含乘法的算术的可判定性；非标准模型；拉姆齐定理；模态逻辑与可证性

最后几章（第295–340页）依次讨论不含乘法的算术的可判定性、非标准模型、拉姆齐定理，最后是模态逻辑与可证性。

核心概念

可计算性（第1–8章）

• 可枚举性与对角化：开篇的技巧，用于比较无穷集合的大小，并证明某物不可能出现在给定的列表中。
• 图灵可计算性与算盘可计算性：关于有效程序能做什么的两种形式模型。
• 递归函数：可计算性的第三种刻画，第8章表明它与其他刻画等价。

一阶元逻辑（第9–14章）

• 一阶逻辑的句法与语义：元定理所讨论的语言、解释与真。
• 模型与证明：完全性定理所确立的“在所有模型中为真”与“可推导”之间的联系。
• 一阶逻辑的不可判定性：任何判定有效性的一般程序都受到的限制。

不完全性与拓展专题（第15–27章）

• 算术化与可表示性：用数来编码句法，并在算术内部表达可计算函数。
• 不完全性与一致性的不可证明性：全书最终通向的限制性结果。
• 插值、二阶逻辑、非标准模型、拉姆齐定理、模态逻辑与可证性：后面各章章名中列出的专题。

评析

优点

• 一册之内涵盖丰富的主题。 出版社称，本书既涵盖中级逻辑课程的常规主题，包括哥德尔不完全性定理，又包括从图灵可计算性理论到拉姆齐定理的大量选学内容。目录印证了这一点：第19–27章的章名都是接在主线之后的独立专题。
• 面向没有数学背景的学生。 出版社把对这类学生的可读性视为本书成为经典的原因，在图灵机之外使用算盘机，是这一定位的一个具体表现。
• 每章末附习题。 据出版社介绍，每章末都附有一组习题，并已针对第五版作了调整。
• 更简化的可表示性路径。 本版对递归函数可表示性的全新处理，针对的是出版社所说的通向不完全性定理途中的传统难关。

局限

• 对一阶逻辑的回顾很浓缩。 第9、10章只是“概要”，因此本书预设读者已学过一阶逻辑；需要初次讲解的读者应先读别的书。
• 范围固定。 从章名看，本书限于可计算性、一阶元逻辑及若干拓展；想系统学习证明论或集合论的读者需要另找他书。
• 选择路线需要费一番功夫。 全书27章，其中许多是选学，教师或自学者必须自行决定取舍；目录并未标出哪些是核心。

在课程中的定位

在本课程书单中，这是数学要求最高的一本。《forall x（卡尔加里版）》是免费的入门教材，讲真值函数逻辑与一阶逻辑，采用菲奇式自然演绎；科匹的教材涵盖非形式推理、三段论与符号逻辑；两者都是第一门课。Barker-Plummer、Barwise 与 Etchemendy 的《Language, Proof and Logic》把一阶逻辑教材与软件配合使用，并讲到可靠性、完全性和哥德尔第一定理的概述，所以已经触及本书详细处理的领域。赛德的《Logic for Philosophy》是为哲学专业学生设计的第二门逻辑课，先证明命题逻辑与谓词逻辑的结论，再转向模态逻辑；它是最接近的替代选择，两书可以对照阅读。

《Computability and Logic》适合在学完形式逻辑第一门课之后阅读，目的是详细看到图灵机、不可判定性和不完全性定理的证明。

如何使用本书

本书适合已学完形式逻辑第一门课、想看到限制性定理完整证明的哲学、数学和计算机专业学生。出版社强调不要求数学背景，但这是一本以证明为主的教材，需要有耐心读证明。

一个可行的计划：读第1–8章学习可计算性；把第9–10章当作复习略读，需要某个概念时再回头查；读第11–14章学习不可判定性、模型与完全性；把第15–18章作为一个整体读，学习不完全性。第19–27章按兴趣选读：第22章（二阶逻辑）与第27章（模态逻辑与可证性）对哲学专业的学生尤为合适，第24–25章则适合关心算术及其模型的读者。完成每章末的习题，因为用过证明技巧之后，证明会更容易读懂。