目录

绪论 1
0.1　对证明论学科发展的一些看法 1
0.2　本书的一些尝试 9
参考文献 11
第1部分  预备知识
第1章　基本概念的定义和举例 14
参考文献 23
第2章　基础知识 24
2.1　集合论概述 24
2.2　逻辑学概述 29
参考文献 32
第2部分　证明方法
第3章　关系运算证明方法 38
参考文献 44
第4章　三段论证明方法 45
4.1　亚里士多德三段论简述 45
4.2  亚里士多德三段论的改进 51
4.3  量化扩展的三段论有效命题的确定方法 56
参考文献 63
第5章　数学归纳法 65
5.1　数学归纳法的发展概况 65
5.2　第一、第二数学归纳法 65
5.3　超穷（超限）归纳法（广义归纳法） 68
5.4　结构归纳法 72
参考文献 75
第6章　反证法 76
第7章　构造性证明方法 78
参考文献 80
第8章　同态证明方法和解释性证明方法 81
8.1　同态证明方法 81
8.2　解释性证明方法 82
参考文献 83
第9章　系统化证明方法（含截消方法） 84
9.1　系统化证明方法导论 84
9.2　亚里士多德的三段论自然演绎系统和形式系统 86
9.3　量化扩展的三段论自然推理系统 91
9.4　弗雷格的形式系统F 96
9.5　罗素的形式系统R 100
9.6　希尔伯特公理系统H 105
9.7　根岑的自然演绎系统G与截消证明方法 106
9.8　算术形式系统举例 113
9.9　几何证明公理系统举例 119
参考文献 122
第10章　归结证明方法 125
10.1　归结的基础理论 125
10.2　归结定理与归结方法 134
参考文献 137
第11章　自动化证明方法 138
11.1　自动化证明方法的思想渊源 138
11.2　自动证明机器原型之一：图灵机 139
11.3　自动证明机器原型之二：线性有界自动机 143
11.4　自动证明机器原型之三：下推自动机 146
11.5　自动证明机器原型之四：确定型有穷自动机 148
11.6　自动证明机器原型之五：不确定型有穷自动机 150
11.7　自动机接受的语言 153
11.8　自动机与数学证明的关系 155
11.9　定理证明器和推理机基本原理和证明实例 156
参考文献 161
第3部分　证明理论
第12章　可判定性理论 165
12.1　基本概念和历史背景 165
12.2　可计算性理论 166
12.3　一阶语言的可判定理论 181
12.4　不可判定理论 186
12.5　可判定性与可证明性的关系 189
参考文献 190
第13章　相容性理论 192
13.1　相容性问题产生的根源、过程和现状 192
13.2　悖论的结构和特征 196
13.3　解悖理论（1）—— 类型理论 201
13.4　解悖理论（2）—— 情境语义学理论 205
13.5　解悖理论（3）—— ZFC公理系统 208
13.6　解悖理论（4）—— 新基础公理系统 214
13.7　集合论公理系统概览 215
13.8　数学系统相容性的其他障碍及其解决 216
13.9　算术系统的相容性 221
13.10　几何系统的相容性 238
参考文献 239
第14章　不完全性理论 242
14.1　哥德尔第一不完全性定理 242
14.2　哥德尔第二不完全性定理 247
14.3　哥德尔第一不完全性定理的发展和争议 248
14.4　哥德尔第二不完全性定理的争议和某些应用 250
参考文献 252
第15章　可靠性理论与完全性理论 254
参考文献 258
第4部分　附　录
附录1　算术公理系统 260
附录2　On Formally Undecidable Propositions of Principia Mathematica
and Related Systems（Ⅰ） 265
附录3　论《数学原理》及其相关系统的形式不可判定命题（Ⅰ） 286
附录4　人名索引 301
附录5　定义索引 308
附录6　核心命题索引 313
附录7　例题索引 316

内容摘要

　　本书阐述数学证明的基本原理，主要包括证明方法和证明理论，是探讨证明方法和证明理论内在联系和本质特征的数学专著。
　　“证明方法”集成了常见或具有重要影响并具有逻辑独立性和形式化特征的数学证明方法，分别给出了这些方法的表示公式、例题、相关的定理以及当前的研究前沿状况。
　　“证明理论”阐述了自希尔伯特倡导建立证明论以来该学科的主要理论，介绍了这些理论的发展脉络，分别给出了这些理论的公理、定理及其证明、例题、当前的研究前沿状况。
　　本书力图解决以下问题：什么是数学证明？数学证明的通用方法有哪些？关于数学证明取得了哪些重要认识？
　　作为跨学科研究的尝试，本书可作为证明论、逻辑、计算机科学与技术、数学哲学等相关领域专业工作者的教材或参考书。