希爾伯特演繹系統

在邏輯特別是數理邏輯中，希爾伯特風格演繹系統是歸功於弗雷格和希爾伯特的一類形式演繹系統。這種演繹系統最經常為一階邏輯而研究，但對其他邏輯也是有價值的。

所有演繹系統都在邏輯公理和推理規則之間作出取捨平衡。希爾伯特風格的演繹系統可以刻畫為選擇了大量的邏輯公理模式和少（Hilbert system）量的推理規則。最常研究的希爾伯特風格演繹系統只有一個推理規則即肯定前件和幾個無限公理模式。

自然演繹系統做了相反的取捨，包括了很多演繹規則但有非常少甚至沒有公理模式。

形式定義

演繹系統的圖形表示

在希爾伯特風格演繹系統中，形式演繹是公式的有限序列，其中每個公式要麼是個原子要麼是從前面的公式通過推理規則而獲得。這些形式演繹系統意圖反映自然語言證明，儘管它們要更加詳細。

假設$\Gamma$是被當作假設的公式集合。例如$\Gamma$可以是群論或集合論的公理集合。符號$\Gamma \vdash \phi$意味着有隻使用邏輯公理和$\Gamma$的元素的結束於$\phi$的一個演繹。因此，非形式的說$\Gamma \vdash \phi$意味着假定了$\Gamma$中的所有公式則$\phi$是可證明的。

希爾伯特風格演繹系統可刻畫為使用了眾多邏輯公理模式。公理模式是把所有某種形式的公式代換成特定模式。不只是從這種模式生成的公理，還有這些公理之一的任何普遍化，都包括在邏輯公理集合中。公式的普遍化是通過在公式上前綴上零個或多個全稱量詞而獲得的；因此

$\forall y(\forall xPxy\to Pty)$

是$\forall xPxy\to Pty$的普遍化。

邏輯公理

常見的希爾伯特風格的系統有六個無限公理模式和一個補充公理。為了簡約公理模式的數目，這個系統假定所有公式都已經被重寫為只使用連結詞$\lnot$和$\to$並且只有量詞$\forall$。如下面所討論的那樣，可以把系統擴展為包括額外的邏輯連結詞比如$\land$和$\lor$，而不擴大可演繹的公式類。

前三個邏輯公理模式（與肯定前件一起）允許操縱邏輯連結詞。

1. $\phi \to \left(\psi \to \phi \right)$

2. $\left(\phi \to (\psi \rightarrow \xi \right))\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)$

3. $\left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)$

後三個邏輯公理模式提供了增加、操縱和去除全稱量詞的方式。

4. $\forall x\left(\phi \right)\to \phi [x:=t]$這裡的t可以代換在$\phi$中x

5 $\forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)$

6 $\phi \to \forall x\left(\phi \right)$這裡的x不是$\phi$中的自由變量

需要最後的公理模式來處理涉及等號的公式。

1. $x=x$對於所有變量x
2. $\left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)$

保守擴展

在希爾伯特風格的演繹系統中經常只包含對蘊涵和否定的公理。給定這些公理，有可能形成允許使用補充連結詞的演繹定理的保守擴展。這些擴展被稱為是保守的，因為如果涉及新連結詞的公式φ被重寫為只涉及否定、蘊涵和全稱量詞的邏輯等價的公式θ，則φ在擴展系統中是可導出的，當且僅當θ在最初系統中可導出的。在完全擴展的時候，希爾伯特風格的系統將非常類似於自然演繹系統。

元定理

由於希爾伯特風格系統有非常少的演繹規則，經常證明元定理來展示額外的演繹規則不增加演繹能力，在使用新演繹規則的演繹可以轉換成只使用最初演繹規則的演繹的意義上。

一些常見的這種形式的元定理有：

• 演繹定理：$\Gamma ;\phi \vdash \psi$當且僅當$\Gamma \vdash \phi \to \psi$。
• $\Gamma \vdash \phi \leftrightarrow \psi$當且僅當$\Gamma \vdash \phi \to \psi$並且$\Gamma \vdash \psi \to \phi$。
• 對置（Contraposition）:如果$\Gamma ;\phi \vdash \psi$則$\Gamma ;\lnot \psi \vdash \lnot \phi$。
• 普遍化：如果$\Gamma \vdash \phi$並且x不自由的出現在$\Gamma$的任何公式中，則$\Gamma \vdash \forall x\phi$。

進一步聯繫

公理1、2與演繹規則肯定前件對應於組合子邏輯的基礎組合子K, S與應用的概念。參見Curry-Howard同構。

參考文獻

來源

• Curry, Haskell B.; Feys, Robert. Combinatory Logic Vol. I 1. Amsterdam: North Holland. 1958. 
• Monk, J. Donald. Mathematical Logic. New York; Heidelberg; Berlin: Springer-Verlag. 1976. 
• Ruzsa, Imre; Máté, András. Bevezetés a modern logikába. Budapest: Osiris Kiadó. 1997 （匈牙利語）. 
• Tarski, Alfred. Bizonyítás és igazság. Budapest: Gondolat. 1990 （匈牙利語）.  It is a Hungarian translation of Alfred Tarski's selected papers on semantic theory of truth.

外部連結

• Farmer, W. M. Propositional logic (PDF). （原始內容 (pdf)存檔於2007-09-26）.  It describes (among others) a part of the Hilbert-style deduction system (restricted to propositional calculus).