系统化证明方法

通过证明系统进行证明的方法大致可分为基于公理系统和基于规则系统两种基本子类。这两种系统都有专门的名称，严格地说，基于公理进行推理推演、并具有句法要求的证明系统是形式公理系统，简称形式系统，大致上称之为“希尔伯特风格的证明”系统；而仅仅基于句法规则进行转换的证明系统即自然演绎系统，大致上称之为“根岑风格的证明”系统(“希尔伯特风格”和“根岑风格”还有其他区别，但核心的区别在于此)。质言之，形式系统以公理作为前提来证明命题；自然演绎系统以规则通过语法形式转换来证明命题——可以没有公理，只有规则。1

发展沿革系统化数学证明的历史可以追溯到古希腊数学。从现有的资料看，最早进行公理化证明方法的是泰勒斯，他进行了几何的证明。他的证明得到后来的欧几里德的多次引用。

最早提出数学证明概念的人可能是毕达哥拉斯。他提出数学命题应该给予严格的证明。按照当时的数学证明方法，应指公理化证呀引。

亚里士多德的三段论证明系统是最早的自然演绎系统和形式系统——他不只提出了三段论推理形式，还给出了用规则推导出有效三段论的方法，这属于自然演绎系统的证明方法；同时，基于三段论的第一格第一式(Babara)推导其他格式的三段论方法相当于把第一格第一式作为形式系统进行证明。

欧几里德的公理系统较早并比较完善地创造了公理化数学证明的范例。这一影响是巨大的。后来的许多几何学如希尔伯特几何学、罗巴切夫斯基几何学、黎曼几何学都构建了公理系统。不仅在数学领域，对于科学而言，欧几里德展示了科学作为陈述体系的逻辑图景。例如，在物理学领域，牛顿的《自然哲学的数学原理》也是借鉴欧几里德的公理系统的结构和方法写成的，即命题是逐次、累积证明的。

在现代，在弗雷格和罗素已经建立了形式化的逻辑演算体系背景下，由于希尔伯特提出了数学公理化的倡议，使得公理化成为数学的一个重要目标，公理化方法由此也应该成为数学的一个基本方法。

希尔伯特的公理化思想主要地陈述于他的《数学问题——在1900年在巴黎国际数学家代表大会上的讲演》，以及1922年他在德国的一次数学会议上就这些问题提出的研究大纲。在前一篇文章中，希尔伯特提出了23个待解的数学问题，其中第2个问题是“算术公理的相容性”。他说：“在研究一门科学的基础时，我们必须建立一套公理系统，它包含着对这门科学基本概念之间所存在关系的确切而完备的描述。如此建立起来的公理同时也是这些基本概念的定义；并且，我们正在检验其基础的科学领域里的任何一个命题，除非它能够从这些公理的有限步逻辑推理而得到，否则就不能认为是正确的。”第6个问题是“物理公理的数学处理”。在对这个问题的陈述中，他认为存在这样一个问题，即如何“用同样的方法借助公理来研究那些数学在其中起重要作用的物理科学，首先是概率论和力学”。可以看出，希尔伯特认为存在一种可能，至少在数学物理科学中建立公理系统证明数学或物理科学(数学在其中起重要作用)命题。这实际上是一种将科学公理化的倾向。

随着系统化证明方法的发展，产生了针对专门化的数学知识领域的形式系统。它是系统化证明方法的实例。例如，皮亚诺算术系统(PA)、希尔伯特的几何证明系统，等等，这些证明系统的证明方法首先属于系统化证明方法，还有针对特定领域的方法和关于特定领域的理论。同时，也建立了多个通用的自然演绎系统，如根岑的自然演绎系统。1

原理为推演出或者判定命题，可以通过给定的公理进行推演，也可以仅仅通过一些表述定理的语言的转换规则对给定命题进行转换，直至转换为预期的结果。由此可以将证明系统划分为两个类别：基于公理的证明系统和基于转换规则(简称为规则)的证明系统。它们具有相同的特点，都是依据一个符号集合实现证明，从而使证明成为一个基于原初系统(这个符号集合)的生成过程。换言之，这种证明是构造性的，它是由一个(有限符号的原初)系统构造的。

同时，这两种系统也有区别，这种区别首先在于(原初的符号)系统的构成不同：一种必须包含公理集合，而另一种必须包含规则集合，并且在严格意义下基于规则的系统不要求系统必须预先有公理(但是不排除证明前或证明中加入公理)。当然，在很多情况下，一个证明系统可以将二者都包括在内。具体而言，用于推演的公理和用于转换的规则之间的区别，以及由此导致的两个系统的区别在于：

(1)一个具体的公理一般表示为命题常元(针对特定领域的特殊公理)：而规则一般将命题表示变元。因此，基于公理集合的证明系统允许包含具体命题(公理常元)——尽管并非所有的公理系统都包含命题常元：而基于规则证明系统一般不给出命题常元(除非针对某一专门命题制定规则，这意义就不大了)，基本上只给出命题变元。

(2)公理是永真的；规则允许不是永真的(进行某种转换是否是永真转换，则需要依据操作目的而定。虽然在很多情况下，规则是等值转换，使得被转换的原有的或真或假的逻辑值被保留，但是在很多情况下，规则是语法化的，无所谓真假转换)。

(3)规则是语法化的，它是符号生成转换规则；公理的推导允许是非语法化的，即它的转换不必遵循语法规则，只是基于内容的转换一一如欧几里德公理系统中的公理，它们是与语法形式无关的，因此它们是内容化的。

(4)公理是对象语言表述的：规则是衍语言表述的。例如，数学公理的陈述对象是数学世界的概念，关于“数”“空间”“+”“