分类:证明论

在数理逻辑的研究中，将问题形式化、公理化成公式， 并通过公式结构本身（形式、语法，而非内容、语义）的变形规则，寻求对任意一个命题即一个公式的，一个证明序列。 相关理论称为证明论(proof theory)。

其中代表性、知名度高的是希尔伯特纲领(Hilbert's program)。 试图将数学形式化， 通过列举出概念、基本公理、基本推理规则， 确认数学体系的完备性、一致性，理论上即等价于一切的命题都可以在这个形式化系统中以有穷序列可证为真或假。 后被证明，任意一个包含一阶谓词逻辑与初等数论的形式系统，都存在不能在这一系统中证明真假的命题； 一个包含初等数论且一致的系统，不能从系统本身中证明其一致性。 这被称为哥德尔不完备定理(Gödel's incompleteness theorems)。