結構證明論

結構證明論研究形式系統中證明的結構.《結構證明論》介紹經典邏輯和直覺主義邏輯的自然演繹和矢列演算,它們是結構證明論的基礎理論.根岑式矢列演算的基本定理是切割消除. 運用證明論研究方法, 通過分析證明的結構可以得到一些邏輯性質,如子公式性質、可判定性、插值性質等.《結構證明論》還介紹了經典模態命題邏輯及一些代數邏輯的結構證明論. ^[1] 

叢書序

前言

第1章 命題邏輯 1

1.1 經典命題邏輯 1

1.2 直覺主義命題邏輯 15

1.3 習題 22

第2章 自然演繹 26

2.1 費奇式自然演繹 26

2.2 根岑式自然演繹系統 32

2.3 正規化 39

2.4 完全性 49

2.5 習題 51

第3章 矢列演算 54

3.1 G0型矢列演算 54

3.2 切割消除 61

3.3 可判定性 81

3.4 插值性質 88

3.5 習題 100

第4章 矢列演算的結構規則 104

4.1 G1型矢列演算 104

4.2 G2型矢列演算 118

4.3 G3型矢列演算 120

4.4 G4型矢列演算 140

4.5 嵌入定理 150

4.6 習題 156

第5章 一階邏輯 158

5.1 一階邏輯的公理系統 158

5.2 一階邏輯的矢列演算 170

5.3 直覺主義謂詞邏輯的矢列演算 181

5.4 習題 186？

第6章 經典模態命題邏輯 188

6.1 正規模態邏輯 188

6.2 模態矢列演算 202

6.3 超矢列演算 215

6.4 習題 225

第7章 代數邏輯 228

7.1 偏序代數結構 228

7.2 格與分配格 231

7.3 加算子的分配格 244

7.4 習題 251 ^[3] 

參考文獻 ^[2]