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

在数理逻辑的研究中，将问题形式化、公理化成公式，
并通过公式结构本身（形式、语法，而非内容、语义）的变形规则，对任意一个[[命题]]，即语法上的一个公式，寻求一个[[证明]]序列。
相关理论称为'''证明论'''('''proof theory''')。
因此，证明论天生是一个语法性的理论，谋求通过纯粹的语法变形手段，从某些起点（公理）通过某种方法（推理规则）构造任意需要的定理。

证明论中证明可能表达为不同的公式演算方式，[[Hilbert 表示]]、[[自然演绎系统]]、[[相继式演算]]等。
但无论是哪种演算方式，都可以通过选择不同的公理和规则，适应命题逻辑、谓词逻辑等领域，经典逻辑、直觉主义逻辑、多值逻辑等不同逻辑体系的需要。

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


[[分类:数理逻辑]][{DEFAULTSORT:zheng4ming2lun4}}