摘 要：有关证明的思想由来已久，然而直到十九世纪末证明论才得以从古希腊的欧式几何和三段论等简单的思想中逐步丰富和完善，发展成为一门成熟的学科，并逐步从传统数学领域逐步扩展到计算机等其他学科。对证明论历史发展脉络的把我，对证明论的学习至关重要。
关键词：证明论；证明；数学
证明论是数理逻辑的分支，主要以形式化方法研究数学证明，它是一种研究数学证明一般结构的学科。对证明的研究并不是近现代才出现的，从古希腊开始，证明就被逻辑学家所关注，从亚里士多德的《后分析篇》中可以看到，古希腊人就已经开始关注如何从假设的命题必然地得到结论。如欧氏几何学，它是由公认的五条几何学知识描绘而成的公理系统，通过有限的公理必然地得出所有的欧式几何的真命题。再如，亚里士多德三段论，逻辑学家将正确判断推理的逻辑形式抽象出来，用若干规则加以规定并从这些规则出发判定一个推理是否有效。这些简单的与证明有关的理论几乎统治了逻辑学超过两千年。
对一般数学证明的考察，必须对数学证明进行符号化，历史发展也证明了形式化方法对逻辑的发展产生了巨大推动作用。最早旗帜鲜明地主张符号化的是莱布尼兹，他提出将推理符号化，然后交付机器进行计算，这被称为演算推论器的思想。虽然莱布尼兹的研究重点并不是数学证明，但他的符号化的思想无疑是超前的，并对后世作为逻辑主义创始人之一的弗雷格产生了重要影响。1879年弗雷格《概念文字》一书出版，他用形式化方法创造了一种表意语言，消除了自然语言的歧义和含混，保证了推理过程的绝对严格性。除此之外，他将数学中的函数概念引入逻辑，建立了量词理论，后来他用九条公理和四条变形规则构造了历史上第一个严格的逻辑演算系统，并认为算数定理可以从逻辑系统中推导出来，甚至整个数学可以被划归到逻辑中来，后来罗素、怀特海和维特根斯坦等人都直接受益于弗雷格，弗雷格的思想对后来现代证明论的产生具有极大的影响。
十九世纪下半叶，康托尔的集合论已经渗透到了数学的各个分支，受到了广大数学家的接受，并且他们发现从自然数和康托尔集合论出发能够构筑整个数学大厦，因此集合论也被现代数学家奉为现代数学的基石。然而根据集合论，集合可以由任意元素（包括不属于自己的元素）组成，如果集合A由不属于A的元素构成，那么显然会陷入两难境地，这就是著名的罗素悖论，它动摇了数学的基础，并且引起了数学家和逻辑学家关于数学基础问题的大讨论。
“数学与逻辑结合，或者说数理逻辑发展的一个重要起点，就是数学求助于逻辑来证明自己的一致性。”[1]在数学基础大讨论的历史背景下，大卫·希尔伯特创立了证明论，并试图证明整个数学的无矛盾性。历史上对数学无矛盾性的讨论仅限于采用化归方法对非欧几何的无矛盾性的证明，即在欧式几何中构造非欧几何模型，用欧式几何的无矛盾性证明非欧几何的无矛盾性，这种做法将A理论的无矛盾性归结为B理论的无矛盾性，但是B理论的无矛盾性又需要证明，显然数学理论的无矛盾性必须给出绝对的证明，并且为了避免循环论证，不能采用数学中的理论来证明数学自身的无矛盾性，而必须使用数学理论之外的理论来证明，为此，希尔伯特提出了证明论的方法。这种方法将数学中的所有概念通过形式化的方法[2]由公理和推理规则确定下来。这样，数学中的命题就变成了形式化的公式，命题之间的推演也就变成了形式化了的数学命题依据公理和推理规则进行的变换。如果能够证明这个公理系统不能得出两个相互矛盾的公式，也就证明了数学的无矛盾性。希尔伯特的证明论思想一经提出便备受关注，算术系统等一些简单的数学理论的无矛盾性被证明，这无疑增强了人们对证明整个数学无矛盾性的信念。虽然历史证明希尔伯特的理想是无法实现的，“但他所创立的证明论却使得一门普通数学理论整体地作为一个确定的、可用数学方法来研究的对象”[3]。
1931年哥德尔不完全性定理的提出否定了希尔伯特从形式逻辑出发证明数学无矛盾性的构想。哥德尔起初也是希尔伯特宏大构想的追随者，并试图证明形式算术系统的无矛盾性，但发现这是不可能得证的，由此得到哥德尔不完全性定理。哥德尔不完全性定理的证明打破了希尔伯特的构想，并且迫使希尔伯特及其追随者修补其理论或转向新的理论。
根岑将目光转向数学家实际研究中使用的数学证明，并发现数学家的证明并不是基于类似于希尔伯特式的公理系统，而是基于一些假设的命题，从这些假设的命题得到一些结论，把假设的命题分解为它的组成部分，这个推理过程用“消去规则”来表示，相反，从结论的各个分解部分到结论自身的推理用“引入规则”来刻画。基于此，根岑发明了相较于公理系统更贴近日常推理的证明系统，自然演绎系统。由于没能证出古典自然演绎系统的正规化定理，根岑发明了矢列演算系统，该系统从形式上描绘了自然演绎系统中的可演绎关系，通过证明The Hauptsatz[4]（即cut消去定理）和证明所有的规则都具有子公式性质，可以解决该系统中任意公式的判定性问题。
上世纪六十年代之后，证明论不在仅仅关注系统的无矛盾性问题，开始研究数学证明的一般结构和性质，证明的复杂性，数学中的不可判定性问题，并且逐步走出传统数学，延伸向逻辑编程等计算机领域。
参考文献
[1]陈慕泽. 正确理解哥德尔不完全性定理[J].湖南科技大学学报：社会科学版，2008，11（2）：27-30.
[2]Kreisel G. A survey of proof theory[J].Journal of symbolic Logic，1968：322.
[3]徐云从. 证明论及其发展[J].数学季刊：英文版，1988，（03）.
[4]Gentzen G. Investigations into logical deduction[J].American philosophical quarterly，1964：298.
作者簡介
党学哲（1992-），男，河南洛阳人，西南大学政治与公共管理学院研究生，研究方向：现代逻辑。
（作者单位：西南大学政治与公共管理学院）
推荐访问： 梳理 证明 发展 历史
