演繹定理

演繹定理是數理邏輯的一個核心規則，它清晰地描述元語言的純符號組合所做的演繹與邏輯語言裡的實質條件的聯繫。

簡介

演繹定理通常被視為元定理，也就是以元語言來描述的符號組合規則（也就是推理規則，如肯定前件）為基礎，配上邏輯公理（被認為＂永遠為真＂的一套合式公式）為前提去證明的某種規則，通常都有以下的形式：（以下 ${\mathcal {A}}_{1},\,\cdots ,\,{\mathcal {A}}_{n}$ 、 ${\mathcal {B}}$ 為任意合式公式）

「若根據前提

{\mathcal {A}}_{1},\,\cdots ,\,{\mathcal {A}}_{n}

和公理與推理規則，可以推出

{\mathcal {B}}

，那對任意

1\leq {\mathcal {i}}\leq n

也可以推出

{\mathcal {A_{i}}}\Rightarrow {\mathcal {B}}

」

視為元定理的例子請參見一階邏輯條目的演繹元定理。

但在某些邏輯系統中，演繹定理被定為基礎的推理規則。這種系統跟視為元定理的系統比較起來，推理的效力是等同的，所以在此並不贅述。

演繹的例子

證明 ((P→(Q→P))→R)→R:

- (P→(Q→P))→R 1. 假設
- P→(Q→P) 2. 公理 1
- R 3. 肯定前件 2,1
((P→(Q→P))→R)→R 4. 演繹自 1 到 3 QED

從使用演繹元定理的演繹轉換到公理化證明

在公理化版本的命題邏輯中，通常有着公理模式和推理規則(這裡的 P、Q 和 H 可以被替換為任何命題)：

公理 1：P→(H→P)
公理 2：(H→(P→Q))→((H→P)→(H→Q))
推理規則肯定前件：從 P 和 P→Q 推出 Q

從這些公理和推理規則你可以快速的演繹出定理模式 P→P (參見命題演算)。選擇這些公理模式使你能夠容易的從它們推導出演繹定理。可以通過使用真值表驗證來證實它們為重言式，而肯定前件保持真理。

假如我們有了 Γ 與 H 證明 C，並且我們希望證實 Γ 證明 H→C。對於在演繹中的每個步驟 S:

如果這個步驟是在 Γ 中的前提(重複步驟)或一個公理，我們可以應用肯定前件於公理 1：S→(H→S)，來得到 H→S。
如果這個步驟是 H 自身(假設步驟)，我們應用這個定理模式來得到 H→H。
如果這個步驟是應用肯定前件於 A 和 A→S 的結果，我們首先確保它們已經被轉換成 H→A 和 H→(A→S)，並接着採用公理 2：(H→(A→S))→((H→A)→(H→S))，並應用肯定前件來得到 (H→A)→(H→S)，並接着再次應用來得到 H→S。

在這個證明的結束處我們有了所需要的 H→C，除了它現在只依賴於 Γ 而不再依賴於 H 之外。所以這個演繹步驟將消失，合併到是從 H 推導出的結論的前面步驟中。

為了最小化結果證明的複雜性，在轉換之前要進行某些預處理。實際上不依賴於 H 的任何步驟(除了結論)都應當被移動到假設步驟之前並去縮進一個層次。並且任何其他不必要步驟(不用來得到結論或可以被繞過的)，比如不是結論的重複應當除去。

在轉換期間，在演繹開始處(緊接着 H→H 步驟之後)放置所有的對公理 1 的肯定前件應用可能是有用的。

在轉換肯定前件的時候，如果 A 在 H 的範圍之外，則必須應用公理 1：A→(H→A)，和肯定前件來得到 H→A。類似的，如果 A→S 在 H 的範圍之外，應用公理 1：(A→S)→(H→(A→S)) 和肯定前件來得到 H→(A→S)。做這二者不是必須的，除非肯定前件步驟是結論，因為二者都在這個範圍之外，那麼肯定前件應當已經被移動到 H 之前並且因此也在這個範圍之外。

在Curry-Howard同構下，上述對演繹元定理的轉換過程類似於從lambda 演算項到組合子邏輯項的轉換過程，這裡的公理 1 對應於 K 組合子，而公理 2 對應於 S 組合子。注意 I 組合子對應於定理模式 P→P。

轉換的例子

要展示如何把自然演繹轉換成公理化形式的證明，我們應用它於重言式 Q→((Q→R)→R)。實際上，知道可以這麼做通常就足夠了。我們通常使用自然演繹形式來替代更長的公理化證明。

首先，我們寫使用自然演繹的證明:

- Q 1. 假設
  - Q→R 2. 假設
  - R 3. 肯定前件 1,2
- (Q→R)→R 4. 演繹自 2 到 3
Q→((Q→R)→R) 5. 演繹自 1 到 4 QED

其次，我們轉換內層的演繹為公理化證明:

(Q→R)→(Q→R) 1. 定理模式 (A→A)
((Q→R)→(Q→R))→(((Q→R)→Q)→((Q→R)→R)) 2. 公理 2
((Q→R)→Q)→((Q→R)→R) 3. 肯定前件 1,2
Q→((Q→R)→Q) 4. 公理 1
- Q 5. 假設
- (Q→R)→Q 6. 肯定前件 5,4
- (Q→R)→R 7. 肯定前件 6,3
Q→((Q→R)→R) 8. 演繹自 5 到 7 QED

第三，我們轉換外層的演繹為公理化證明:

(Q→R)→(Q→R) 1. 定理模式 (A→A)
((Q→R)→(Q→R))→(((Q→R)→Q)→((Q→R)→R)) 2. 公理 2
((Q→R)→Q)→((Q→R)→R) 3. 肯定前件 1,2
Q→((Q→R)→Q) 4. 公理 1
[((Q→R)→Q)→((Q→R)→R)]→[Q→(((Q→R)→Q)→((Q→R)→R))] 5. 公理 1
Q→(((Q→R)→Q)→((Q→R)→R)) 6. 肯定前件 3,5
[Q→(((Q→R)→Q)→((Q→R)→R))]→([Q→((Q→R)→Q)]→[Q→((Q→R)→R))]) 7. 公理 2
[Q→((Q→R)→Q)]→[Q→((Q→R)→R))] 8. 肯定前件 6,7
Q→((Q→R)→R)) 9. 肯定前件 4,8 QED

這三個步驟可以簡潔的使用Curry-Howard同構表述為:

首先，在 lambda 演算中，函數 f = λa. λb. b a 有類型 q → (q → r) → r
其次，通過在 b 上的 lambda 除去，f = λa. s i (k a)
第三，通過在 a 上的 lambda 除去，f = s (k (s i)) k

參見

引用

Introduction to Mathematical Logic by Vilnis Detlovs and Karlis Podnieks （頁面存檔備份，存於網際網路檔案館） Podnieks is a comprehensive tutorial. See Section 1.5.

外部連結

元數學證明探索者主頁（頁面存檔備份，存於網際網路檔案館）