希尔伯特演绎系统

在逻辑特别是数理逻辑中，希尔伯特风格演绎系统是归功于弗雷格和希尔伯特的一类形式演绎系统。这种演绎系统最经常为一阶逻辑而研究，但对其他逻辑也是有价值的。

所有演绎系统都在逻辑公理和推理规则之间作出取舍平衡。希尔伯特风格的演绎系统可以刻画为选择了大量的逻辑公理模式和少（Hilbert system）量的推理规则。最常研究的希尔伯特风格演绎系统只有一个推理规则即肯定前件和几个无限公理模式。

自然演绎系统做了相反的取舍，包括了很多演绎规则但有非常少甚至没有公理模式。

在希尔伯特风格演绎系统中，形式演绎是公式的有限序列，其中每个公式要么是个原子要么是从前面的公式通过推理规则而获得。这些形式演绎系统意图反映自然语言证明，尽管它们要更加详细。

假设${\displaystyle \mathrm{\Gamma <!--\; \Gamma \; -->}}$是被当作假设的公式集合。例如${\displaystyle \mathrm{\Gamma <!--\; \Gamma \; -->}}$可以是群论或集合论的公理集合。符号${\displaystyle \mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->\mathrm{\varphi <!--\; \varphi \; -->}}$意味着有只使用逻辑公理和${\displaystyle \mathrm{\Gamma <!--\; \Gamma \; -->}}$的元素的结束于${\displaystyle \mathrm{\varphi <!--\; \varphi \; -->}}$的一个演绎。因此，非形式的说${\displaystyle \mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->\mathrm{\varphi <!--\; \varphi \; -->}}$意味着假定了${\displaystyle \mathrm{\Gamma <!--\; \Gamma \; -->}}$中的所有公式则${\displaystyle \mathrm{\varphi <!--\; \varphi \; -->}}$是可证明的。

希尔伯特风格演绎系统可刻画为使用了众多逻辑公理模式。公理模式是把所有某种形式的公式代换成特定模式。不只是从这种模式生成的公理，还有这些公理之一的任何普遍化，都包括在逻辑公理集合中。公式的普遍化是通过在公式上前缀上零个或多个全称量词而获得的；因此

是${\displaystyle \mathrm{\forall <!--\; \forall \; -->}xPxy\to <!--\; \to \; -->Pty}$的普遍化。

常见的希尔伯特风格的系统有六个无限公理模式和一个补充公理。为了简约公理模式的数目，这个系统假定所有公式都已经被重写为只使用连结词${\displaystyle \mathrm{\neg <!--\; \neg \; -->}}$和${\displaystyle \to <!--\; \to \; -->}$并且只有量词${\displaystyle \mathrm{\forall <!--\; \forall \; -->}}$。如下面所讨论的那样，可以把系统扩展为包括额外的逻辑连结词比如${\displaystyle \wedge <!--\; \wedge \; -->}$和${\displaystyle \vee <!--\; \vee \; -->}$，而不扩大可演绎的公式类。

前三个逻辑公理模式（与肯定前件一起）允许操纵逻辑连结词。

后三个逻辑公理模式提供了增加、操纵和去除全称量词的方式。

需要最后的公理模式来处理涉及等号的公式。

在希尔伯特风格的演绎系统中经常只包含对蕴涵和否定的公理。给定这些公理，有可能形成允许使用补充连结词的演绎定理的保守扩展。这些扩展被称为是保守的，因为如果涉及新连结词的公式φ被重写为只涉及否定、蕴涵和全称量词的逻辑等价的公式θ，则φ在扩展系统中是可导出的，当且仅当θ在最初系统中可导出的。在完全扩展的时候，希尔伯特风格的系统将非常类似于自然演绎系统。

由于希尔伯特风格系统有非常少的演绎规则，经常证明元定理来展示额外的演绎规则不增加演绎能力，在使用新演绎规则的演绎可以转换成只使用最初演绎规则的演绎的意义上。

一些常见的这种形式的元定理有：

公理1、2与演绎规则肯定前件对应于组合子逻辑的基础组合子K, S与应用的概念。参见Curry-Howard同构。