利用PYTHON学习数理逻辑

本书是数理逻辑教学领域的创新之作。作者将Python编程实践巧妙融入数理逻辑理论教学，通过精心设计的编程练习与逻辑概念阐释相结合，为读者搭建起理解抽象逻辑理论的可操作路径。书中涵盖了命题逻辑和谓词逻辑的语法、语义、证明等内容，将符号逻辑、公理系统及形式证明等理论转化为可交互验证的编程任务，使逻辑推理的严密结构直观呈现。作者基于多年本科教学实践经验，确保教学案例典型、知识架构科学，为中国读者提供了理论与实践相结合的学习方案，拓展了数理逻辑的认知维度与学习路径。

本书采用独特的叙述方法，引导读者利用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