第1章 绪论 1
1.1 推理的有效性 1
1.2 形式系统 7
第2章 命题演算 11
2.1 命题形式和真值 11
2.2 真值函项和联结词的完全集 22
2.3 推理形式有效性的判定 32
2.4 范式 41
2.5 命题演算的自然推演系统N 50
2.5.1 N的形式语言和推演规则 50
2.5.2 N内定理的形式推演 55
2.6 命题演算的公理系统P 81
2.6.1 P系统的形式语言、公理和推演规则 81
2.6.2 P内定理的形式证明和演绎定理 83
2.7 命题演算的系统特性 93
2.7.1 N与P的等价性 93
2.7.2 命题演算P的解释 96
2.7.3 P系统的可靠性和完全性 100
第3章 谓词演算 104
3.1 简单命题逻辑结构的符号化 104
3.2 一阶语言 114
3.3 一阶语言L的语义 121
3.4 前束范式 132
3.5 一阶谓词演算的自然推演系统NL 137
3.5.1 NL自然推演的出发点 137
3.5.2 NL内定理的形式推演 139
3.5.3 NL带等词的内定理的形式推演 152
3.6 一阶谓词演算的公理系统KL 156
3.6.1 KL公理系统的形式证明或推演的出发点 156
3.6.2 KL内定理的形式证明和形式推演 157
3.7 一阶谓词逻辑的系统特性 161
3.7.1 NL与KL的等价性 161
3.7.2 KL的可靠性 163
3.7.3 KL的完全性 165
第4章 模态逻辑演算 170
4.1 模态词与可能世界 171
4.2 模态命题逻辑的T，S4，S5系统 175
4.3 模态命题逻辑的T，S4，S5的语义 185
4.4 模态谓词逻辑QT（B），QS4（B），QS5系统 190
4.5 模态谓词逻辑QT（B），QS4（B），QS5系统的语义 194
4.6 模态逻辑的可靠性和完全性 198
第5章 构造性逻辑演算 203
5.1 构造性证明和命题的构造性解释 203
5.2 构造性一阶谓词演算的自然推演系统INL 206
5.3 构造性一阶谓词演算INL的语义 218
参考书目 223