第一章 绪论 1
1.3 逻辑演算的解释 4
1.4 数理逻辑与模态逻辑 5
1.5 对象语言与元语言 6
第二章 命题逻辑 8
2.1 形式语言L1 8
2.2 命题演算P 11
2.3 推导与推导定理 14
2.4 P中的一些定理 19
2.5 命题演算P的解释 31
2.6 P常真、P可满足与P语义后承 36
2.7 逻辑等值 39
2.8 范式 42
2.9 形式语言L1的表达能力 47
2.10 命题演算P的可靠性 51
2.11 命题演算P的一致性 52
2.12 命题演算P的完全性 53
2.13 命题演算P的判定问题 59
第三章 狭谓词逻辑 61
3.1 形式语言L2 62
3.2 谓词演算Q 66
3.3 推导定理与等值替换定理 69
3.4 谓词演算Q的一些定理 75
3.5 谓词演算Q的解释 82
3.6 Q可满足，Q常真与Q语义后承 85
3.7 谓词演算Q的可靠性 88
3.8 谓词演算Q的一致性 93
3.9 谓词演算Q的完全性 95
3.10 谓词演算Q的判定问题 115
第四章 模态命题演算T 117
4.1 形式语言L3 119
4.2 模态命题演算T 120
4.3 模态命题演算T的一些定理 122
4.4 模态命题演算T的解释 132
4.5 克瑞普克的T语义图 136
4.6 模态命题演算T的可靠性 145
4.7 模态命题演算T的一致性 152
4.8 模态命题演算T的完全性 154
4.9 模态命题演算T是可判定的 166
第五章 模态命题演算S4 167
5.1 模态命题演算S4 167
5.2 模态命题演算S4的一些定理 168
5.3 S4真的推导定理与等值替换定理 171
5.4 模态命题演算S4的解释 173
5.5 克瑞普克的S4语义图 174
5.6 模态命题演算S4的可靠性 179
5.7 模态命题演算S4的一致性 182
5.8 模态命题演算S4的完全性 182
5.9 模态命题演算S4的判定问题 185
第六章 模态命题演算S4 187
6.1 模态命题演算S5 187
6.2 模态命题演算S5的定理 188
6.3 S5的推导定理和等值替换定理 194
6.4 模态命题演算Ss的解释 200
6.6 克瑞普克的S5语义图 202
6.6 模态命题演算S5的可靠性 204
6.7 模态命题演算S5的一致性 206
6.8 模态命题演算Ss的完全性 206
6.9 模态命题演算S5的判定问题 210
第七章 模态命题演算的其他判定方法 211
7.1 休斯与克雷斯韦尔的T语义图 211
7.2 休斯与克雷斯韦尔的S4语义图 217
7.3 休斯与克雷斯韦尔的S5语义图 218
7.4 T(S4与S5)常真公式 220
7.5 模态级和模态公式的归约 220
7.6模态真值表 223
7.7卡尔纳普的模态合取范式 233
第八章 模态谓词演算QTB与QS4B 241
8.1 形式语言L4 242
8.2 模态谓词演算QTB 244
8.3 模态谓词演算QTB的一些定理 245
8.4 模态谓词演算QTB的解释 249
8.5 模态谓词演算QTB的可靠性和一致性 251
8.6 模态谓词演算QTB的完全性 253
8.7 模态谓词演算QTB的判定问题 270
8.8 模态谓词演算QS4B 270
8.9 模态谓词演算QS4B的完全性 272
8.10 模态谓词演算QS4B的判定问题 276
9.1 模态谓词演算QT 277
第九章 模态谓词演算QT、QS4与QS5 277
9.2 模态谓词演算QT的解释 278
9.3 模态谓词演算QT的可靠性与一致性 283
9.4 模态谓词演算QT的完全性 287
9.5 模态谓词演算QS4 296
9.6 模态谓词演算QS5 297
第十章 模态逻辑的自然推导系统 304
10.1 命题逻辑的自然推导系统PN 305
10.2 谓词逻辑的自然推导系统QN 321
10.3 模态命题逻辑的自然推导系统TN 331
10.4 模态命题逻辑的自然推导系统SN4 340
10.5 模态命题逻辑的自然推导系统SN5 343
10.6 模态谓词逻辑的自然推导系统QTN与QSN4 346
10.7 模态谓词逻辑的自然推导系统QTBN与QS4BN 348
10.8 模态谓词逻辑的自然推导系统QSN5 349
第十一章 模态逻辑简史 352
11.1 亚里士多德的模态逻辑 352
11.2 德奥弗劳斯德 363
11.3 麦加拉和斯多葛学派论必然和可能 364
11.4 中世纪的模态逻辑 369
11.5 莱布尼兹关于必然与可能的理论 376
11.6 休谟论必然性 383
11.7 康德论必然性与可能性 385
11.8 麦克柯尔 387
11.9 路易士的模态逻辑 389
11.10 路易士以后到本世纪六十年代的模态逻辑 396