证明论

---

数理逻辑的一个分支。

它将数学理论本身作为研究对象，因此也称之为元数学。

证明论起源于著名的希尔伯特(Hilber)规划。在这个规划中，希尔伯特首先提出用有穷方法证明数学的协调性，用来为数学奠定一个坚实的基础。

希尔伯特规划提出后，人们试图按照规划的要求，证明最基本的数学系统——初等数论系统——的无矛盾的努力一直未获成功。

直到1931年，哥德尔(Godel)发表了他的不完全性定理，人们才知道：如果初等数论系统是无矛盾的，其无矛盾性是不可能用有穷方法证明的。

既然希尔伯特规划中原来的目标是不可能达到的，人们后来便放宽对证明协调性的方法的限制，把有穷性的限制去掉，但仍要求可构造性。在放宽了的条件下，甘岑(Gentzen)首先证明了初等数论的无矛盾性。之后，人们又证明了其他一些数学系统的无矛盾性。所有这些工作对于人们理解数学证明的实质，对于人们了解各种系统的推演能力都是大有帮助的。