数理逻辑引论——计算机科学与系统的天然基础

数理逻辑系统是形式语言、形式语义和证明的三位一体。《数理逻辑引论：计算机科学与系统的天然基础》讨论这类系统的核心思想、重要概念、组成部分、构建方法，以及它们与数学和计算机科学的紧密关系，解释数理逻辑系统中符号化语言、解释、模型等概念，研究递归、迭代、分解组合、模块化、等价替换等处理结构复杂性的方法和技术。正是这些概念、结构、方法和技术形成了计算思维的核心，也成为计算机科学和计算机软件与系统的天然基础。

前言
第1章导论1
1.1逻辑的基本概念和术语1
1.2逻辑学3
1.2.1概念与命题3
1.2.2推理论证5
1.2.3自然语言的歧义性与悖论7
1.3从亚里士多德经典逻辑到现代数理逻辑的演化8
1.3.1形式逻辑—推理形式与内容的分离9
1.3.2数理逻辑14
1.4计算机科学中的逻辑19
1.4.1逻辑是计算理论的天然基础19
1.4.2计算机科学技术领域的形式语言20
1.4.3形式证明与验证26
第2章离散数学基础29
2.1集合与集合代数30
2.1.1集合：概念、表示法和意义30
2.1.2子集34
2.1.3集合代数37
2.2关系和关系代数49
2.2.1笛卡儿积49
2.2.2关系52
2.2.3等价关系和划分55
2.2.4关系代数58
2.2.5关系的图示61
2.3函数64
2.4集合、关系、函数和谓词的联系与统一66
2.4.1关系和函数的统一67
2.4.2集合、关系、函数、谓词和布尔代数的统一67
2.5数学归纳法68
2.6集合上的序关系69
2.6.1偏序集70
2.6.2从已知的偏序集构造偏序集72
2.6.3偏序集间的函数74
2.7格、接近格和接近偏序集75
2.7.1偏序集的特殊子集和元素75
2.7.2格和接近格77
2.7.3保持上下确界的函数81
2.7.4塔斯基不动点理论82
2.7.5接近偏序集及不动点理论83
2.8集合的基数87
第3章朴素命题逻辑91
3.1引言91
3.2断言和连接词92
3.3连接词的真值函数和真值表95
3.4断言形式97
3.4.1断言形式的真值函数和真值表98
3.4.2断言形式的语法树101
3.5重言式和矛盾式102
3.6逻辑等价和逻辑蕴涵104
3.6.1逻辑等价104
3.6.2等价替换106
3.6.3逻辑蕴涵的性质111
3.7对偶式和断言范式114
3.7.1对偶式114
3.7.2断言形式的范式116
3.7.3充分连接词集合118
3.7.4子句形式119
3.8推理及推理的有效性120
第4章形式化命题逻辑122
4.1形式逻辑系统123
4.2形式命题逻辑系统L125
4.3L中的演绎推理130
4.3.1演绎定理131
4.3.2关于否定命题的证明与推演134
4.4形式系统L的有效性137
4.5相容性和L的充分性定理138
第5章朴素谓词逻辑147
5.1谓词和量词148
5.1.1谓词149
5.1.2变量、量词和函数149
5.2一阶形式语言154
5.2.1字母表155
5.2.2一阶语言的实例156
5.2.3合式公式157
5.2.4形式语言的语法层次结构158
5.2.5变元的自由与约束出现159
5.2.6换名和代换161
5.3解释165
5.3.1概念166
5.3.2赋值167
5.3.3合式公式可满足性168
5.3.4真值和模型171
5.4重言式和逻辑等价175
5.4.1重言式175
5.4.2逻辑有效的公式177
5.4.3逻辑蕴涵和逻辑等价178
5.5斯科伦定理181
第6章形式化谓词逻辑184
6.1形式系统KL184
6.1.1KL的有效性186
6.1.2KL的演绎定理188
6.2可证明等价和代换192
6.3KL的充分性定理199
6.3.1KL的扩展199
6.3.2充分性定理的证明201
6.4模型206
6.5范式209
6.5.1量词辖域的变换209
6.5.2前束范式211
6.5.3子句形式213
第7章数学系统215
7.1带等词的一阶系统216
7.2公理化群论221
7.2.1群的非形式定义221
7.2.2形式化群论222
7.3公理化布尔代数225
7.4形式化算术226
7.4.1算术的形式化226
7.4.2与皮亚诺算术的关系228
7.4.3形式化算术的模型及完备性问题229
7.5公理集合论230
7.5.1ZF公理系统230
7.5.2ZF公理系统的模型232
7.6相容性和模型之间的关系234
第8章程序设计理论导引236
8.1计算、计算机和计算机程序236
8.1.1可计算性和计算机236
8.1.2程序语法的非形式定义240
8.1.3程序的非形式语义242
8.2程序语言的形式语法244
8.3程序语言的操作语义246
8.3.1栈-状态-控制抽象机解释语义247
8.3.2基于操作语义的程序分析和验证249
8.3.3结构化操作语义251
8.3.4完整的结构化操作语义255
8.4程序语言的指称语义258
8.4.1基本思想和技术258
8.4.2核心问题260
8.4.3Mini的指称语义定义261
8.5指称语义和操作语义的一致性265
8.6程序语言的公理语义268
8.6.1非形式霍尔逻辑269
8.6.2霍尔逻辑271
8.6.3霍尔逻辑可靠性和接近性276
8.7抽象数据类型281
参考文献284
索引285