证明论

证明论（Proof theory），是数理逻辑的一个分支，它将数学证明表达为形式化的数学客体，从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达，例如链表，盒链表，或者树，它们根据逻辑系统的公理和推理规则构造。因此，证明论本质上是语法逻辑，和本质上是语义学的模型论形相反。和模型论，公理化集合论，以及递归论一起，证明论被称为数学基础的四大支柱之一。

基本方法

表系统使用结构证明论的解析证明的中心思想来为一大类的逻辑提供决策或者准决策进程。序分析是为形式化算术和分析的理论提供组合式自洽性证明的有力技术。

表系统

表系统使用结构证明论的解析证明的中心思想来为一大类的逻辑提供决策或者准决策进程。

序分析

序分析是为形式化算术和分析的理论提供组合式自洽性证明的有力技术。

发展历史

数学中的证明一向是逻辑学家研究的对象，但证明论是数学家D.希尔伯特于20世纪初期建立的，目的是要证明公理系统的无矛盾性，希尔伯特提出一整套严格的方案，规定只能用有限长的证明，要无可辩驳地给出整个数学的无矛盾性。他打算先给出公理化的算术系统的无矛盾性，再证明数学分析，集合论的无矛盾性。但1931年，K.哥德尔证明：一个包含公理化的算术的系统中不能证明它自身的无矛盾性。这就是著名的哥德尔不完备性定理。这个结果使希尔伯特方案成为不可能。但1936年，G.根岑降低了希尔伯特的要求，允许使用无穷长的证明，证明了算术公理系统的无矛盾性。到1960年，数学分析的一些片断的无矛盾性也被证明。20世纪60年代以后，证明论不再局限于无矛盾性的证明。数学证明中的结构，证明的复杂性，数学中不可判定问题都成为证明论的研究课题，1977年，J.帕里斯发现算术理论中的一个自然的而又是不可判定的命题，这是一个重大发现。它使算术中自然的不可判定命题的研究越来越受人注意。

亚结构逻辑

在数理逻辑中，特别是联合上证明论的时候，一些亚结构逻辑已经作为比常规系统弱的命题演算系统被介入了。同常规系统的不同之处在于它们有更少的结构规则可用：结构规则的概念是基于相继式（sequent）表达，而不是自然演绎的公式化表达。两个重要的亚结构逻辑是相干逻辑和线性逻辑。

在相继式演算中，你可以把证明的每一行写为

这里的结构规则是重写相继式左手端的Γ的规则，Γ是最初被构想为命题的字符串。这个字符串的标准解释是合取式：我们希望把相继式符号

读做(A与B)蕴涵C。

这里我们把右手端的Σ采纳为一个单一的命题C（这是直觉主义风格的相继式）;但是所有的东西都同样的适用于一般情况，因为所有的操作都发生在十字转门（turnstile）符号的左边。

因为合取是交换性和结合性的操作，相继式理论的形式架设通常包括相应的结构规则来重写相继式的Γ - 例如

演绎自

还有对应于合取特性的幂等性和单调性的进一步的结构规则：从

我们可以演绎出

还有从

我们可以演绎出，对于任何B