查看“︁希尔伯特演绎系统”︁的源代码

在[[逻辑]]特别是[[数理逻辑]]中，'''希尔伯特风格演绎系统'''是归功于[[弗雷格]]<ref name="#1">Máté & Ruzsa 1997:129</ref>和[[希尔伯特]]的一类[[演绎推理|形式演绎]]系统。这种演绎系统最经常为[[一阶逻辑]]而研究，但对其他逻辑也是有价值的。

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

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

== 形式定义 ==
[[File:Deduction architecture_cn.png|right|300px|演绎系统的图形表示]]

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

假设<math>\Gamma</math>是被当作'''假设'''的公式集合。例如<math>\Gamma</math>可以是[[群论]]或[[集合论]]的公理集合。符号<math>\Gamma \vdash \phi</math>意味着有只使用'''逻辑公理'''和<math>\Gamma</math>的元素的结束于<math>\phi</math>的一个演绎。因此，非形式的说<math>\Gamma \vdash \phi</math>意味着假定了<math>\Gamma</math>中的所有公式则<math>\phi</math>是可证明的。

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

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

前三个逻辑公理模式（与肯定前件一起）允许操纵逻辑连结词。
:1. <math>\phi \to \left( \psi \to \phi \right) </math>
:2. <math>\left( \phi \to (\psi \rightarrow \xi \right)) \to \left(\left( \phi \to \psi \right) \to  \left( \phi \to \xi \right) \right)</math>
:3. <math>\left( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right) </math>

后三个逻辑公理模式提供了增加、操纵和去除全称量词的方式。
:4. <math> \forall x \left( \phi \right) \to \phi[x:=t]</math>这里的''t''可以代换在<math>\phi</math>中''x''
:5 <math>\forall x \left( \phi \to \psi \right)\to \left(\forall x \left( \phi \right) \to \forall x \left( \psi \right) \right)</math>
:6 <math> \phi \to \forall x \left( \phi \right) </math>这里的''x''不是<math>\phi</math>中的[[自由变量]]

需要最后的公理模式来处理涉及等号的公式。
#<math>x = x</math>对于所有变量''x''
#<math>\left( x = y \right) \to \left( \phi[z:=x] \to \phi[z:=y] \right)</math>

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

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

一些常见的这种形式的元定理有：
* '''[[演绎定理]]'''：<math>\Gamma;\phi \vdash \psi</math>当且仅当<math>\Gamma \vdash \phi \to \psi</math>。
* <math>\Gamma \vdash \phi \leftrightarrow \psi</math>当且仅当<math>\Gamma \vdash \phi \to \psi</math>并且<math>\Gamma \vdash \psi \to \phi</math>。
* 对置（Contraposition）:如果<math>\Gamma;\phi \vdash \psi</math>则<math>\Gamma;\lnot \psi \vdash \lnot \phi</math>。
* 普遍化：如果<math>\Gamma \vdash \phi</math>并且''x''不自由的出现在<math>\Gamma</math>的任何公式中，则<math>\Gamma \vdash \forall x \phi</math>。

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

== 参考文献 ==
=== 引用 ===
{{Reflist}}

=== 来源 ===
{{refbegin}}
* {{cite book
| last1 = Curry
| first1 = Haskell B.
| last2 = Feys
| first2 = Robert 
| title = Combinatory Logic Vol. I
| volume = 1
| year = 1958
| publisher = North Holland
| location = Amsterdam
}}
* {{cite book |last=Monk |first=J. Donald |title=Mathematical Logic |url=https://archive.org/details/mathematicallogi00jdon |publisher=Springer-Verlag |location=New York; Heidelberg; Berlin |year=1976 }}
* {{cite book |last1 = Ruzsa |first1 = Imre |last2 = Máté |first2 = András |title=Bevezetés a modern logikába |publisher=Osiris Kiadó |location=Budapest |year=1997 |language=hu }}
* {{cite book |last=Tarski |first=Alfred |title=Bizonyítás és igazság |publisher=Gondolat |location=Budapest |year=1990 |language = hu }} It is a Hungarian translation of [[Alfred Tarski]]'s selected papers on [[semantic theory of truth]].
{{refend}}

== 外部链接 ==
* {{cite web |last=Farmer |first=W. M |title = Propositional logic |url = http://www.cas.mcmaster.ca/~wmfarmer/SE-2F03-05/slides/02-prop-logic.pdf |format=pdf |dead-url=yes |archive-url = https://web.archive.org/web/20070926223055/http://www.cas.mcmaster.ca/~wmfarmer/SE-2F03-05/slides/02-prop-logic.pdf |archive-date=2007-09-26 }} It describes (among others) a part of the Hilbert-style deduction system (restricted to [[propositional calculus]]).

[[Category:证明论]]
[[Category:逻辑演算]]