[拼音]：zhengminglun
[外文]：proof theory
数理逻辑的一个分支，以数学证明为研究对象的数学理论。
逻辑学中关于证明的研究由来已久。亚里士多德《工具论》一书中的 《分析后篇》就是讨论有关证明的问题的，并且他是以古希腊时期的数学中所用到的证明作为研究对象的。近代的证明理论开始于20世纪前期，是由德国数学家D.希尔伯特创立的。希尔伯特有时将证明论与元数学（即数学基础）视作同义语。希尔伯特学派所发展的证明论侧重于公理系统的无矛盾性的研究，他们企图用本身无可怀疑的方法（即希尔伯特等人所说的有穷方法，有时又称作初等方法）来论证整个数学是无矛盾的。希尔伯特原来设想，从公理化算术开始，用有穷方法证明它的无矛盾性，然后证明数学分析以及集合论的无矛盾性等等。
1931年K.哥德尔证明了下列事实：在一个复杂到一定程度的公理系统中，如果这个系统是无矛盾的，则它是不完备的，而且它的矛盾性在这个系统中是无法证明的。这就证明了希尔伯特原来的方案是无法实现的。在这以后，有些逻辑学者打算降低原来的要求，采用可靠性比有穷方法低的方法来证明算术和数学分析的无矛盾性。G.根岑在1936年证明了算术的无矛盾性，60年代以来又有些人证明了数学分析的某些片断的无矛盾性。
虽然希尔伯特学派关于证明论的研究专门注重数学系统无矛盾性的证明，但证明论本不应限于无矛盾性的证明的研究。G.克赖泽尔等人60年代以来，开始了关于证明的结构以及复杂度等问题的研究。1977年以来J.帕里斯等人发现了算术中自然的不可判定的命题。后来有些人在从事这方面的研究，又获得了一些重要的成果。
半个世纪以来，证明论的最重要的结果之一是哥德尔不完备性定理。根据这一定理可知，对复杂到一定程度的（这里所说的“一定程度”是可以严格定义的）数学理论T而言，如果T是无矛盾的，则T是不完备的；也就是说，在这些理论中，总有一些命题，它们是真的，但不能由这些理论的公理推出。1977年以来，又发现在算术中存在着自然的不可判定的命题，也就是说，从算术的公理出发，既不能证明也不能否证的算术命题。
1931年时哥德尔就发现了算术中存在有不可判定的命题，后来文献中称之为哥德尔语句。这一语句G 是说：“语句G 是不可证的。”哥德尔语句是一个算术的命题，但不是自然的算术命题。算术中第一个自然的不可判定的命题是直到1977年才由帕里斯等人发现的。这被认为是数理逻辑中一项重大成果。
克赖泽尔派的证明论以证明的结构和复杂度为研究对象。这方面的研究结果是与计算复杂性理论渗透交叉的；在计算机科学中，特别是在定理的机械化证明中可能有应用。
构造主义逻辑和构造性数学方面近年来也有不少成果。构造主义逻辑中最早提出的一种是荷兰数学家布劳威尔在20世纪初提出的直觉主义逻辑。这是一种排中律在其中不成立，因而在其中不能用间接证明的逻辑（这里所说的排中律不成立是指对无穷集而言；在直觉主义逻辑中，对有穷集而言，排中律还是成立的）。L.E.J.布劳威尔提出这种逻辑是为了解决数学基础方面的问题，也就是作为避免悖论的一种方案。实际上，构造倾向(即注重算法的倾向)一直是数学史上的一种重要倾向。20世纪40年代以来，由于电子计算机的发明和计算技术的发展，这一倾向更显出其重要性。而且直觉主义逻辑已被发现与有些数学分支（如集合论中的力迫理论）有出人意料的联系。
证明论的关于算术中的自然的不可判定的命题的研究正在引起越来越多的人注意。已有人猜测，数论中有些著名问题如黎曼猜测、费马大定理和哥德巴赫猜想等都可能是算术中不可判定的命题。并且由于已知这些命题都是可以表示成凬n R(n)的形式的（这里n是自然数，而R(n)是一个递归谓词），而又知道，如果一个命题p可以表示成凬nR(n)的形式，而且p是在算术中不可判定的，则p不可能是假的，必然是真的。因此这一方向的研究更加令人注意。计算机科学中有些未解决的问题(如p=?Np)也有人猜测，是在算术中不可判定的。
- 参考书目
- J.Barwise，ed.，Handbook of MatheMatical Logic，North-Holland， Amsterdam， 1977.