绪论 1
什么是数理逻辑？ 1
集合与函数 2
可数集 8
序，Zorn引理 10
良序原理，每个集合可被良序 10
归纳集，递归定义与递归证法 11
变元，函数符号的书写位置 20
元语言与对象语言 21
第一章 命题逻辑（上）——非形式描述 23
1.1 命题与命题联结词 23
1.2 基本联结词及其真值表与真值函数 26
1.3 命题形式及其真值表与真值函数 31
1.4 代入与替换 38
1.5 限制命题形式，范式 39
1.6 推理的有效性 44
1.7 联结词的够用集 47
第二章 命题逻辑（下）——形式描述 54
2.1 重言式公理系统 54
2.2 形式公理系统P1（一）——语言和语义描述基本符号 57
2.3 形式公理系统P1（二）——语法描述 67
2.4 系统P1的发展——定理与导出规则的推导 70
2.5 命题逻辑的自然推理系统 93
2.6 命题逻辑的Gentzen系统 103
2.7 形式系统P2 128
2.8 形式系统P3 131
2.9 形式系统P4与P5 132
2.10 命题逻辑的系统特征 134
第三章 一阶逻辑（上）——非形式描述 145
3.1 个体，谓词与量词 145
3.2 命题函数，约束变元与自由变元 149
3.3 个体函词，项 153
3.4 一阶语言 155
3.5 项的代入 164
3.6 解释（或结构），赋值 170
3.7 可满足性，真性 176
3.8 Hintikka公式集 188
第四章 一阶逻辑（下）——形式描述 191
4.1 一阶形式系统 191
4.2 一阶谓词演算（或一阶演绎系统）K 192
4.3 系统K中推理定理 197
4.4 系统K的发展——定理与导出规则的推导 199
4.5 等值定理 205
4.6 存在引入特化假设规则 207
4.7 一阶谓词演算的自然推理系统K 211
4.8 一阶谓词演算的Gentzen系统LK 215
4.9 一阶谓词演算的另一种描述——系统K1 220
4.10 公式集的K1相容性及系统K1的一般完备性 226
4.11 形式系统的扩张，系统K的完备性 232
4.12 模型 241
4.13 前束范式 247
4.14 πn范式与∑n范式 250
4.15 Skolem范式 250
4.16 系统K的各公理的独立性 257
第五章 带等词的一阶系统 260
5.1 带等词一阶系统的刻划 260
5.2 等词的替换定理 264
5.3 带等词一阶系统的正规模型 266
5.4 带等词一阶系统的完备性 269
5.5 关于等词的其它性质 272
5.6 函词符号与个体常元的消去 276
5.7 函词符号与个体常元的引入 280
5.8 使用定义的扩张 282
第六章 一阶初等算术N 288
6.1 一阶初等算术N的刻划 288
6.2 初等算术N中的一些性质 289
6.3 数论谓词的可表达性与数论函数的可表示性 294
6.4 递归函数 300
6.5 递归谓词 311
6.6 配对函数组 313
6.7 初等数论中的一些结果，孙子定理 315
6.8 G？del的β函数，序列数，序列算子 319
6.9 初等数论中的原始递归函数与原始递归谓词 321
6.10 串值递归式 323
6.11 递归函数在N中的可表示性 326
6.12 Church论点 331
第七章 一阶形式系统的算术化，N的不完全性 333
7.1 G？del编码 333
7.2 相应于形式系统各关系的数论谓词与数论函数 335
7.3 与一阶初等算术N有关的数论谓词与数论函数 342
7.4 一阶初等算术N的不完全性——G？del不完全性定理 343
7.5 N的另一个不可判定句——G？del-Rosser不完全性定理 347
7.6 递归集与递归可枚举集 350
7.7 一阶系统的可判定性 354
第八章 一阶Peano算术P 360
8.1 一阶Peano算术P的划划 360
8.2 系统P的发展 372
8.3 系统P的用定义扩张 381
8.4 G？del第二不完全性定理 395
参考文献 397