内容简介
本书采用独特的叙述方法，引导读者利用Python编程实现基本的逻辑概念和数学证明来学习数理逻辑。这种专为编程基础日益增强的当代学子量身打造的教学方法，充分契合其直觉认知与技术优势，将数理逻辑学习带入他们熟悉的编程语境，通过深度实践构建清晰认知，并借助可运行代码的创作来帮助读者获得成就感。本书主要内容涵盖命题逻辑、一阶谓词逻辑和哥德尔完备性定理证明等，配套资源包括渐进式编程实践任务集、模块化代码框架、自动化测试用例。本书适合已掌握基础数学证明方法并具备Python编程实操能力的读者阅读。
目录
目 录
译者序
前言
第0章 引言和总览 1
0.1 我们的最终目的：哥德尔完备性
定理 2
0.2 我们的教学方法 4
0.3 我们如何进行：用程序来处理逻辑 5
0.4 我们的学习路线图 8
第1部分 命题逻辑
第1章 命题逻辑的语法 10
1.1 命题公式 10
1.2 解析 15
1.3 公式的无限集 18
1.4 选读：波兰表示法 19
第2章 命题逻辑的语义 21
2.1 编程语言的语义 21
2.2 模型与真值 22
2.3 真值表 24
2.4 永真式、矛盾式、可满足性 27
2.5 公式的合成 28
2.6 选读：合取范式 29
2.7 选读：可满足性和搜索问题 31
第3章 逻辑运算符 37
3.1 n元运算符 37
3.2 替换 39
3.3 运算符的完备集 42
3.4 证明不完备性 45
第4章 演绎证明 48
4.1 推理规则 48
4.2 推理规则的特例化 51
4.3 演绎证明示例 54
4.4 证明练习 58
4.5 可靠性定理 60
第5章 关于证明的进一步分析 63
5.1 使用引理 63
5.2 假言推理 66
5.3 演绎定理 70
5.4 反证法 72
第6章 命题逻辑的永真式定理和
完备性 77
6.1 我们的公理系统 77
6.2 永真式定理 79
6.3 有限集的完备性定理 84
6.4 无限集的紧致性定理和完备性
定理 87
6.5 选读：添加其他运算符 90
6.6 选读：其他公理系统 93
第2部分 谓 词 逻 辑
第7章 谓词逻辑的语法和语义 98
7.1 语法 99
7.2 语义 110
第8章 剥离函数和等式 117
8.1 剥离函数 117
8.2 剥离等式 125
第9章 谓词逻辑公式的演绎证明 130
9.1 证明的示例 131
9.2 模式 132
9.2.1 模板常量名 133
9.2.2 模板变量名 133
9.2.3 模板关系名 134
9.2.4 处理参数化公式 135
9.2.5 实例化模式 138
9.3 证明 145
9.3.1 假设/公理行 148
9.3.2 假言推理行 149
9.3.3 全称引入行 150
9.3.4 永真式行 152
9.3.5 证明的可靠性 154
9.4 消除永真式行 155
第10章 谓词逻辑证明 161
10.1 我们的公理系统 161
10.2 三段论 167
10.3 数学基础知识 177
10.3.1 群 177
10.3.2 域 186
10.3.3 皮亚诺算术 187
10.3.4 策梅洛–弗兰克尔
集合论 190
第11章 演绎定理与前束范式 192
11.1 演绎定理 192
11.2 前束范式 195
第12章 完备性定理 211
12.1 推导出闭集的模型或矛盾 215
12.2 闭集 219
12.2.1 原子闭包 220
12.2.2 全称闭包 222
12.2.3 存在闭包 223
12.2.4 联合闭包 227
12.3 完备性定理 230
12.4 紧致性定理和完备性定理的
“可证明性”版本 230
第13章 哥德尔不完备性定理 233
13.1 完备理论和不完备理论 233
13.2 哥德尔数 235
13.3 停机问题的不可判定性 237
13.4 不完备性定理 239
附录 本书中使用的公理和公理推理
规则 242
前言/序言
前 言
数理逻辑入门课是一门极具美感的课程.哥德尔定理毫无疑问是整个本科理论教学中最具影响力和最深刻的真理.尽管如此，在许多计算机科学和工程专业的学生眼里，这门课程却晦涩难懂，因为课程中充满了技术细节繁复又缺乏启发性的证明.学生在无休止的归纳法证明中迷失了自己，并不完全明白这到底是什么意思，比如：“试证明任何为真的命题都是可以被证明的.”确实，一句话中两次出现的“证明”一词具有不同的意义，怎么能不令人困惑呢？这里后面的“证明”是该课程严格定义的数学对象，而前面的“证明”是指我们本科第一年就学习过的自由书写式证明.本书彻底重构了数理逻辑入门课程，虽然传授同样的内容，但将编程思维融入课程教学中.
如何帮助擅长编程的学生避免在无穷无尽的证明细节中迷失方向，从而看不到课程的总体信息呢？我们试图通过计算机编程让这门课程变得不那么抽象、更直观，甚至更令人兴奋，发挥这类学生的认知优势：在通往大目标的过程中，能从容应对无数细节，却始终把握全局，不会因小失大.我们从零开始重新设计了整个理论课程，设计了一系列的编程练习，每个练习都对应某个定理、引理或推论，或者是导向这些定理的一个步骤.
例如，数理逻辑入门课程前半部分的主要结论是“永真式定理”（命题逻辑完备性定理的一个变体），它断言每一个永真式—在所有可能的模型中均成立的命题—都可以用一组小的公理集来证明成立.本书中对应的编程练习就是写一个函数（当然可以是基于前面练习中的函数），其输入是一个公式（学生在之前的练习中实现的Formula类的一个对象），而其输出要么是使这个公式不成立的模型（即该公式为永真式的一个反例），要么是该公式的一个证明（学生在之前的练习中实现的Proof类的一个对象）.显然，能够完整编写这样的函数（包含递归实现的所有辅助函数）的学生，必然能够完全理解永真式定理（以及归纳证明过程中的所有引理）证明中的推理过程.（对于那些自如掌握递归代码远胜于归纳证明的学生来说，情况更是如此.）根据我们的经验，大多数情况下，具有编程背景的学生自己动手编程实现证明功能要比只是被动看老师在黑板上书写证明能更好地理解该证明.在从理论证明转向编程实践的过程中，事实上我们区分了前面提到的命题“试证明任何为真的命题都是可以被证明的”一句中两个“证明”的含义：我们把前面的“证明”转换成了“代码程序”，而后面的“可以被证明”转换成“是一个有效Proof对象的结论”.这种通过对“证明”每一次出现的不同含义进行区分的方式消除了歧义，使概念表述更加清晰，进而让学生更容易重新审视他们对于证明的直觉和下意识的假设.
本书源自2017年以来我们在耶路撒冷希伯来大学教授的一门课程，该课程最初是作为选修课（我们将班级限制在50人，在微调课程时，将学生数限制为100人，但仍需排队候补），后来作为计算机科学与工程系学生必修课—数理逻辑入门课的替代课程，并持续获得了学生们的高度评价.根据我们的经验，每周可以安排一章内容（如果时间安排允许，我们会尝试第10章额外延长一周），对于第一部分（第1～6章），我们要求学生独立完成作业，而对于第二部分（第7～13章），则要求两人一组协作完成作业，这种安排一直运作良好.
首先感谢选修我们课程的希伯来大学的学生提出的有价值的问题和建议，也感谢早期学习该课程的学生对我们的信任.感谢我们的第一位助教和测试解题人Alon Ziv，还有之后的助教Noam Wies、Asaf Yehudai、Ofer Ravid和Elazar Cohen，以及测试解题人Omri Cohen 和Matan Harsat. 特别感谢法律与认知科学专业学生Chagit Schiff-Blass，他向我们展示了我们的教学模式能吸引比预期更广泛的学生群体，他先是作为一个优秀的测试解题人参与课程，之后又加入了我们的教学团队.
我们感谢Henry Cohn 提供的宝贵建议，感谢Aviv Keren 和Shimon Schocken对本书初稿部分章节提供的详细反馈.特别要感谢David Kashtan对本书逻辑方面所做的仔细而有价值的科学编辑工作，书中任何偏离标准定义或术语用法之处，当然都是我们自己的责任.最后，我们感谢 Kaitlin Leach、Rebecca Grainger和剑桥大学出版社全体工作人员的支持以及在新冠疫情期间所提供的极大灵活性.
