演繹定理

維基百科,自由的百科全書
前往: 導覽搜尋

數理邏輯中,演繹定理聲稱如果公式 F 演繹自 E,則蘊涵 E → F 是可證明的(就是或它可以自空集推導出來)。用符號表示,如果  E \vdash F ,則  \vdash E \rightarrow F

演繹定理可以推廣到假定公式的可數序列,使得從

 E_1, E_2, ... , E_{n-1}, E_n \vdash F ,推出  E_1, E_2, ... , E_{n-1} \vdash E_n \rightarrow F ,等等直到  \vdash E_1\rightarrow(...(E_{n-1} \rightarrow (E_n \rightarrow F))...)

演繹定理是元定理: 在給定的理論中使用它來演繹證明,但它不是這個理論自身的一個定理。

演繹元定理是最重要的元定理之一。在某些邏輯系統中,它被接受為是「→」的介入規則的一個推理規則。在其他系統中,從公理證明它是證明這個邏輯是完備的首要任務。不使用演繹元定理在命題邏輯中證明任何東西都是非常困難的。如果你使用了它通常就很容易了。

演繹的例子[編輯]

「證明」公理 1: P→(Q→P)

    • P 1. 假設
      • Q 2. 假設
      • P 3. 重複 1
    • Q→P 4. 演繹自 2 到 3
  • P→(Q→P) 5. 演繹自 1 到 4 QED

「證明」公理 2: (P→(Q→R))→((P→Q)→(P→R))

    • P→(Q→R) 1. 假設
      • P→Q 2. 假設
        • P 3. 假設
        • Q 4. 肯定前件 3,2
        • Q→R 5. 肯定前件 3,1
        • R 6. 肯定前件 4,5
      • P→R 7. 演繹自 3 到 6
    • (P→Q)→(P→R) 8. 演繹自 2 到 7
  • (P→(Q→R))→((P→Q)→(P→R)) 9. 演繹自 1 到 8 QED

使用公理 1 證明 ((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

虛擬的推理規則[編輯]

從例子中,我們可以見到已經我們的正常公理化邏輯增加了三個虛擬(或額外和臨時)的推理規則。它們是「假設」、「重複」和「演繹」。正規的推理規則(比如「肯定前件」和各種公理)仍是可用的。

1. 假設向那些已經獲得的前提增加一個額外的前提的步驟。所以,如果你的前面步驟 S 演繹為:

 E_1, E_2, ... , E_{n-1}, E_n \vdash S

則你增加另一個前提 H 並得到:

 E_1, E_2, ... , E_{n-1}, E_n, H \vdash H

這符號化了從第 n 層縮進移進到第 n+1 層:

  • S 前面的步驟
    • H 假設

2. 重複是重新使用前面的步驟的一個步驟。在實踐中,這只在你希望採用一個不是最近假設的假設,並把它用為在演繹步驟之前的最終步驟的時候才是需要的。

3. 演繹是你去除最近假設(仍可用)並把它前綴於前面步驟的步驟。這被展示為下面這樣的去縮進一層:

    • H 假設
    • ......... (其他步驟)
    • C (結論自 H)
  • H→C 演繹

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

在公理化版本的命題邏輯中,通常有著公理模式和推理規則(這裡的 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

逆定理[編輯]

這個定理的逆命題也成立。它從是蘊涵除去規則的肯定前件立即得出。

參見[編輯]

引用[編輯]

外部連結[編輯]