查看“︁分类:证明论”︁的源代码

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

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


[[分类:数理逻辑]]