证明论是逻辑学的一个分支，将数学证明作为数学研究的对象。它研究证明如何表示、受哪些规则支配、可以如何变换，以及证明揭示了其所属理论的哪些性质。其核心问题包括一致性、消除不必要的中间步骤，以及论证的构造性内涵。模型论主要研究理论的解释及满足理论的结构，而证明论则侧重于推导及其组织方式。(plato.stanford.edu)
形式证明与基础问题
形式系统规定了一种符号语言、一组公理和若干推理规则。形式证明是每一步都遵循这些规则的推导。记号 表示公式 可以从假设 推导出来。例如，肯定前件式允许从 和 推出 。证明论不仅考察这样的推导是否存在，还考察其结构及可能的变换。(mathweb.ucsd.edu)
有几个基础性质必须加以区分。一致性是指理论无法推导出矛盾。可靠性将可推导性与预期语义下的真联系起来；语义完备性则确立反向的联系。对于经典一阶逻辑，完备性意味着一组前提的每个语义后承都可以形式地推导出来。这并不意味着每个一阶理论都能判定其语言中的每个语句：逻辑演算的完备性与公理化理论的完备性有所不同。(mathweb.ucsd.edu)
历史发展
现代证明论源于十九世纪及二十世纪初将数学推理形式化的努力。戈特洛布·弗雷格创立了一种能够明确表示证明的形式逻辑语言。随后，大卫·希尔伯特提出，通过对符号进行严格的数学推理来研究形式推导。二十世纪二十年代，希尔伯特纲领试图将经典数学形式化，并以有穷方法证明其系统的一致性，从而为经典数学提供依据。(plato.stanford.edu)
1931 年发表的哥德尔不完备定理揭示了这一计划的局限。具体而言，一个一致的、可有效公理化且具有足够算术表达能力的理论，无法证明以标准方式形式化的自身一致性断言。这些结果使证明论转向相对一致性、理论之间的比较，以及对数学推理所需依据的明确分析。(plato.stanford.edu)
格哈德·根岑在 1934—1935 年发表的研究中引入了自然演绎和相继式演算。他于 1936 年给出的一阶皮亚诺算术一致性证明使用了与序数 相关的超限归纳，为后来的序数分析提供了重要范例。(plato.stanford.edu)
证明系统与结构分析
不同的演算以不同方式组织证明。希尔伯特式系统通常采用逻辑公理模式和少量推理规则。自然演绎则使用逻辑联结词的引入规则和消去规则。例如，要引入蕴涵 ，可以先在临时假设 下推导出 ，再解除该假设。(plato.stanford.edu)
相继式演算通过 这样的相继式表示推理。在经典逻辑中，这表示：如果 中的所有公式都成立，那么 中至少有一个公式成立。其规则规定如何处理两侧的联结词。结构规则则支配添加、复制或重排假设等操作。对这些操作加以限制，会产生包括线性逻辑在内的系统；这些系统对假设的使用有更严格的控制。(mathweb.ucsd.edu)
一个基本结果是切消定理。切规则允许将已经证明的公式用作中间引理。根岑证明，在他建立的经典逻辑和直觉主义逻辑演算中，证明里的切都可以消去。无切推导具有子公式性质：在适当处理量词的前提下，推导中的公式都取自最终相继式的结构。这揭示了逻辑上的依赖关系，并为一致性论证和证明搜索提供支持，不过，消去切可能大幅增加证明的规模。(plato.stanford.edu)
与之相关的正规化过程通过去除迂回步骤来简化自然演绎证明，例如先引入一个合取式，随即又消去它以取回其中一个分量。对于直觉主义逻辑，正规化有助于解释证明如何为其结论提供明确的证据。(plato.stanford.edu)
理论强度与序数分析
序数分析利用序数记号系统和超限归纳原理研究数学理论。在根岑对皮亚诺算术的分析中，证明归约由低于 且逐步递减的序数度量控制。适当的良基性原理保证归约过程终止，由此得到一致性论证。(math.stanford.edu)
序数 是满足 的最小序数。它的作用说明，证明论衡量的是归纳的强度，而不只是统计公理或定理的数量。根岑的论证并不与哥德尔第二不完备定理冲突：为完整的一致性论证提供依据的归纳原理，在皮亚诺算术本身中无法证明。同样，证明论中的归约和解释也针对特定类别的语句，比较较强系统与较弱系统。(math.stanford.edu)
计算与证明复杂性
柯里–霍华德对应将证明与程序联系起来。在其基本的直觉主义形式中，命题对应于类型，证明对应于带类型的项，证明的正规化对应于计算。蕴涵对应于函数类型，合取则对应于积类型。这些关系将证明论与类型论、编程语言以及证明助手的设计联系起来；证明助手能够机械地检查形式推导。(homepages.inf.ed.ac.uk)
证明复杂性研究在特定证明系统中证明语句所需的资源，尤其是证明长度。它区分证明的存在与短证明的存在，并比较不同演算表示论证的效率。这使证明论与计算复杂性联系起来：结构简化、自动证明搜索和高效验证是相互关联却又各不相同的问题。(mathweb.ucsd.edu)