希爾伯特演繹系統

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

基本介紹

• 中文名：希爾伯特演繹系統
• 外文名：Hilbert-Kalkül

簡介

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

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

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

保守擴展

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

進一步聯繫

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