Can you summarize the following document?
        
  在希爾伯特風格演繹系統中,形式演繹是公式的有限序列,其中每個公式要麼是個原子要麼是從前面的公式通過推理規則而獲得。這些形式演繹系統意圖反映自然語言證明,儘管它們要更加詳細。  假設formula_1是被當作假設的公式集合。例如formula_1可以是群論或集合論的公理集合。符號formula_3意味著有隻使用邏輯公理和formula_1的元素的結束於formula_5的一個演繹。因此,非形式的說formula_3意味著假定了formula_1中的所有公式則formula_5是可證明的。  希爾伯特風格演繹系統可刻畫為使用了眾多邏輯公理模式。公理模式是把所有某種形式的公式代換成特定模式。不只是從這種模式生成的公理,還有這些公理之一的任何普遍化,都包括在邏輯公理集合中。公式的普遍化是通過在公式上字首上零個或多個全稱量詞而獲得的;因此 是formula_10的普遍化。

  常見的希爾伯特風格的系統有六個無限公理模式和一個補充公理。為了簡約公理模式的數目,這個系統假定所有公式都已經被重寫為只使用連結詞formula_11和formula_12並且只有量詞formula_13。如下面所討論的那樣,可以把系統擴充套件為包括額外的邏輯連結詞比如formula_14和formula_15,而不擴大可演繹的公式類。  前三個邏輯公理模式(與肯定前件一起)允許操縱邏輯連結詞。  後三個邏輯公理模式提供了增加、操縱和去除全稱量詞的方式。  需要最後的公理模式來處理涉及等號的公式。

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

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

  公理1、2與演繹規則肯定前件對應於組合子邏輯的基礎組合子K, S與應用的概念。參見Curry-Howard同構。
在邏輯特別是數理邏輯中,希爾伯特風格演繹系統是歸功於弗雷格和希爾伯特的一類形式演繹系統。這種演繹系統最經常為一階邏輯而研究,但對其他邏輯也是有價值的。