希尔伯特演绎系统

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

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

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

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

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

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

本词条内容贡献者为:

王沛 - 副教授、副研究员 - 中国科学院工程热物理研究所