数学证明的想法非常古老, 尽管精确的证明原则大概只是在过去数百年间才确定下来的. 证明论最初是基于只有一到两个推理规则的公理系统的. 这样的系统作为对于什么是可证明的形式呈现而言可能是有用的, 然而在公理系统中实际发现证明近乎是不可能的. 一个证明从公理的实例开始, 但是并不存在找出这些实例应该是什么的系统方法. 公理证明论最初由David Hilbert建立, 其目的在于研究数学公理系统的一致性, 相互独立性以及完备性.
结构证明论研究数学证明的一般结构和性质. 其由Gerhard Gentzen (1909-1945) 于1930年代初发现并在其1933年的博士论文Untersuchungen über das logische Schliessen中呈现. 在他的论文里, Gentzen给出了对于逻辑规则系统两种主要的形式化, 自然演绎和相继式演算. 前者意在提供定理证明实践的一种近似对应; 而后者, Gentzen通过这种形式化发现了其主要的结果, 其经常被引用为Gentzen的"Hauptsatz". 它是在说证明可以被转换为一种特定的"无切"形式, 而从这种形式可以得到关于证明的一般性结论, 例如规则系统的一致性.
Gentzen开始他的研究的年代发生了一件标志性的大事, 这是一项伟大但却令人费解的发现, 即1931年算术的Gödel不完备性定理: 已知的证明原则不足以推导出算术的一切; 而且, 没有单一的公理和规则系统可以满足此要求. Gentzen对于算术的证明论研究产生了序数证明论, 其主要任务在于研究包含无穷多证明原则的形式系统的演绎强度. 这一部分的证明论我们将不作讨论.
一个逻辑系统由一个形式语言和一个用于进行逻辑推理的公理和规则系统构成.
(a) 逻辑语言: 一个逻辑语言经常通过一集归纳语句被定义为合式公式. 想法在于形式语言的表达式是来源于某个给定的字母表的符号的特定序列, 由归纳定义生成. 另一种定义形式语言的方法是通过范畴文法. 这样的文法对于自然语言领域而言是众所周知的, 亦用于编程语言, 但在逻辑学中不那么常见.
在第一种方法下, 逻辑语言的表达式是由两种语句归纳定义的公式: 1. 陈述何为基本 (prime) 公式. 这些公式不包含其他公式作为其一部分. 2. 陈述何为复合 (compound) 公式. 这些公式由更简单的公式通过逻辑联结词构造, 并且其定义需要引用任意的公式, 以及说明这些公式是如何与逻辑联结词的符号放在一起以给出新的公式的. 给定一个公式, 我们可以找出其是如何由其他公式和逻辑联结词放在一起的. 或许括号对于唯一地指明复合的方式而言是必要的, 然后我们可以明白如何得到公式的各个部分, 直至抵达基本公式. 因此, 到最后, 所有公式都是由基本公式, 逻辑联结词和括号构成的.
我们将定义命题逻辑的语言:
语言的表达式应该表达什么东西, 而不仅仅是以正确方式放在一起的来源于某个字母表的符号的序列. 在逻辑学中, 这样所表达的东西被称为命题. 往往人们并不说"由公式表达的命题", 而仅仅是说"命题". 在哲学中对于命题究竟是什么存在着长期的争辩. 当重心在逻辑学上, 而不是在哲学分析下的逻辑是什么上的时候, 我们以形式上的意义考虑表达式, 讨论公式.
在近来的文献中, 将表达式定义为符号序列被称为是具体句法. 往往从另一个角度看待表达式是有用的, 即抽象句法的角度, 如在范畴文法中. 范畴文法的基本想法在于语言的表达式拥有一种函数式结构 (functional structure). 例如, 英语句子可以藉由将不及物动词表示为从名词词组范畴到句子范畴的函数得到, 在通常的函数记号下即. 是范畴的一个元素, 而将函数应用于它则得到了作为值的, 这是句子范畴的一个元素. 为了隐藏函数式的结构以生成原本的句子, 更进一步的线性化是必要的. 在逻辑学和数学中, 这最后阶段产生的不同无足轻重. 自Frege始, 人们只考虑函数式结构的逻辑内容.
我们将简要从范畴文法的角度看看命题逻辑语言的定义. 存在一个命题的基本范畴, 记作. 原子命题是作为参数被引入的, 其无结构, 带有范畴化谬也是类似的, . 联结词是由给定命题构造新命题的二元函数.