证明论

数理逻辑的一个分支，是以证明为研究对象的逻辑数学理论。在证明论研究中，以把数学理论形式化的系统为研究对象，因此又称为元数学(metamathematics)。证明论由D．希尔伯特在20世纪20年代创立。20年代初希尔伯特提出了一个证明数学理论的协调性的计划。按照希尔伯特计划，首先从公理化算术开始，证明它的协调性，然后证明数学分析以及集合论的协调性等等。具体的做法是，把要证明它的协调性的数学理论完全形式化，构成一个形式系统，作为研究对象，称为对象理论。然后用一种本身的协调性是无可怀疑的、至少使人们相信它是协调的方法，即所谓有穷性方法，证明对象理论是协调的。这也就是，用作了严格限制的有穷性方法证明，在作为研究对象的形式系统中推不出两个互相矛盾的公式A和A，所以是协调的，从而证明被形式化的原来那个数学理论是协调的。在实现希尔伯特计划的努力中，W．阿克曼(W．Ackermann)在1924年证明了，如果对归纳公理加上一个小的限制，那么这样的算术是协调的。

1931年K．哥德尔发表了他的著名的不完全性定理。他证明了：(1)包含算术系统在内的任何形式系统S，如果S是协调的，则它是不完全的；(2)如果S是协调的，则它的协调性是不能在系统S中证明的。这就表明了希尔伯特的原来的计划是无法实现的。必须放宽对有穷性方法的限制。在这以后，一些逻辑学家采用降低了要求的方法来证明算术和数学分析的协调性。1936年，G．根岑使用直到ε的超穷归纳法证明了算术的协调性。以后一些逻辑学家又证明了数学分析的某些片断的协调性。哥德尔1958年的文章《关于有穷观点的一种迄今未曾利用的扩充》，提出了一种不同的探索途径。他借助原始递归泛函提出了直觉主义算术的一种解释，然后在其中翻译PA(皮亚诺算术)，也得到了PA语句的一种解释。从那时以来，在把哥德尔的解释推广到数学分析以及关于古典数学与直觉主数学之间的相互关系方面，已有很多工作。

自20世纪60年代以来，G．克赖泽尔等人开始关于证明的结构和复杂度的研究。这方面的研究结果与计算复杂性理论交叉渗透，在计算机科学、特别是在定理的机械化证明中可能有应用。近年来，关于皮亚诺算术(PA)的片断与计算机科学的关联，有许多有趣的工作。

证明论研究中一个正在引起越来越多的人注意的领域，是关于算术中的自然的不可判定命题的研究。哥德尔不完全性定理证明，对于包括算术系统在内任何形式系统S，如果S是协调的，那么它是不完全的；也就是说，在其中存在真的，但不能在其中证明的命题，称为不可判定的命题。在哥德尔的文章中证明的不可判定的命题，通常称为哥德尔语句。这一语句G是说：“语句G是不可证明的。”哥德尔语句是一个算术命题，但不是自然的算术命题，需要把象可证性这样的逻辑概念编码。从那时起，人们就企图在像PA这样的系统中发现自然的不可判定的命题。1977年，J．帕里斯等人找到了第一个这样的命题。证明了：加强形式的有穷拉姆齐定理在PA中不是可证的(参见帕里斯—哈林顿定理)。其后，H．弗里德曼又发现了一个在PA中不可证的命题。由于这些重要的进展，已有人猜测，数论中的一些著名的问题如黎曼假设、费马大定理和哥德巴赫猜想等可能都是算术中不可判定的命题。上面这几个问题的共同特点是，它们都具有相当简单的逻辑形式，在PA的语言中都具有形式nF(n)(这里n是自然数，F(n)是一个递归谓词)，并且对每个固定的自然数k，F(k)都能用初等的计算来判定其真假。并且根据一个相当简单的论证就可以知道，一个具有nF(n)形式的命题，如果它是在算术系统中不可判定的，则它不可能是假的，必然是真的。因此，这一方向的研究更加令人注意。

在文献中，经常将证明论与直觉主义，证明论与构造性数学并提。从30年代起，古典逻辑与直觉主义逻辑、古典数学与直觉主义数学之间的关系，直觉主义逻辑的解释，就是证明论研究的一个方面。自60年代以来，这方面有许多吸引人的工作。直觉主义逻辑与构造性数学研究也有不少成果。随着电子计算机的发明和计算技术的发展，构造性逻辑和数学的研究更显出它的重要性。

随着证明论的发展，又相继出现一些新的研究方向，如H．弗里德曼等人自70年代开始的反演数学(reverse mathematics)的研究。所谓反演数学是指与从公理推演定理这一通常的数学实践相反，而是从普通数学(何谓普通数学有定义)的定理推演公理。这种研究是要辨明数学命题的逻辑强度。他们列出二阶算术的5个子系统，证明了许多普通数学的定理都与其中某个子系统等价，如波尔查诺－外尔斯特拉斯定理(实数的每一有界序列有一收敛的子序列)等价于系统ACA。(ACA是指把概括模式xn(n∈x→φ(n))中的公式φ(n)限制为算术公式而得的二阶算术的子系统。)

20世纪20年代以前的数理逻辑的发展是创立证明论的基础，而证明论的创立和发展又成了推动整个数理逻辑发展的巨大动力，证明论与数理逻辑的其它分支有密切联系。