四大證明系統



邏輯系統有分語意和語法兩個面向,證明系統 (proof system) 就是純粹在語法面向運作的系統。目前四類主流的證明系統,分別是「自然演繹證明系統」 (natural deduction system) 、「公理證明系統」 (axiomatic proof system) 、「樹枝證明系統」 (tableau proof system) 和「序列證明系統」 (sequent calculus system) 。

左上角是自然演繹法,由 (A→B) 推論 (C→A)→(C→B) 。當中的第3行使用了推導規則 Hypothetical Syllogism (HS) ,由第1行的前提 (A→B) 和第2行的前提 (C→A) 推導出第3行的 (C→B) 。自然演繹法的推導規則的數目視乎設定,有些自然演繹法僅有11條推導規則,有些則多達23條。自然演繹法可證明論證對確 (valid) ,但不可證明論證不對確 (invalid) 。此說有例外,如 Gensler (2010) Introduction to Logic (2nd). Routledge 的命題邏輯系統由於揉合樹枝證明法,除了可證明論證對確,也可證明論證不對確。(圖取自 Causey (2006) Logic, Sets, and Recursion (2nd). Jones & Bartlett Learning.)

右上角是公理證明法,由 (φ→ψ) 和 (ψ→χ) 推論 (φ→χ) 。由於不同書籍用不同符號代表命題 (proposition) 和命題變元 (propositional variable) ,所以有希臘字母和大小細英文字母的分別。這個推論其實就是自然演繹法的規則 HS 。公理證明法往往只有極少規則,相應地會有能夠隨時加入證明過程的公理,例如第2行忽然加了 (φ→ψ)→(φ→(φ→ψ)) ,便是自然演繹法不可出現的步驟。(圖取自 Bostock (2002) Intermediate Logic. Clarendon Press.)

左下角是樹枝證明法,由 (A→B) 和 (B→C) 推論 (A→C) ,同樣是 HS 。樹枝證明法第一步是寫下所有前提,並寫下結論的否定,所以開首有 (A→B), (B→C), ¬(A→C) 。有別於其他證明系統,古典命題邏輯的樹枝證明法可利用規則將論證分拆至簡單命題 A, B, C, etc. ,在限步驟內判斷論證是否對確。可是,一旦延伸至古典述詞邏輯,或者非古典邏輯(如模態邏輯),樹枝證明法便可能出現無限樹枝圖,無法在有限步驟判斷論證是否對確。(圖取自 Priest (2008) An Introduction to Non-Classical Logic (2nd). Cambridge University Press.)

右下角是序列證明法,證明 (P→Q) 和 (Q→R) 可推論出 (P→R) ,也就是證明 HS 。前三個證明法的每一行都是命題,但序列證明法的每一行都是證明序列。例如,第一行 (P→Q)⇒(P→Q) 其實是指「由(P→Q)推導(P→Q)的序列」。(圖取自 Sider (2009) Logic for Philosophy. Oxford University Press.)

除了這四類主流,當然尚有其他證明系統。例如 Anderson & Belnap 的 AB-system 。(參見 Hunter (1973) Metalogic. University of California Press, pp.125-134.)

4 則留言:

  1. Think you have a typo on this one :)


    Celarent
    所有 M 都不是 P
    所有 S 都是 M
    因此,所有 S 都是 P

    回覆刪除
  2. 請問學會自然演繹法之後,一般而言,可以不必學其他三種證明系統嗎?因為有些數理邏輯的書會用tableau或者axiomatic proof system(然後沒提自然演繹法),不知道這只單純只是作者的口味與偏好,還是各有其重要的用途。我在想說這些系統唯一目的只是要教你怎麼用語法推導出東西,並無其他深入用途,那我擇一(好比自然演繹法)熟用即可,其他的我就可以放心略去不看。

    回覆刪除
    回覆
    1. 要視乎目的。自然演繹法的規則(eg. 雙重否定)和證明方法(eg. 條件證法)與我們思考相當類似,熟習這套系統有時可以加快思考速度,讀一些難澀的證明會有不少助益。但由於自然演繹法的規則多,證明這套系統的後設性質(eg. 完備性、妥當性)就要花更多功夫。公理證明法的規則少,有些後設性質證明起來會快得多。樹枝證明法好處在於將論證圖像化,有時可以更易看到怎樣做推論,規則比常見的自然演繹法少,但比公理證明法多,證明後設性質的難度也可謂介乎兩者中間。我提到的四種證明系統之中,只有序列演算法才可以呈現論證與論證之間的關連。若果對這些特徵沒有興趣,只是想學後設邏輯 (meta-logic) ,未必需要熟悉怎樣用各套證明系統做證明(例如用公理證明法證明雙重否定),但必須了解你研究的那套證明系統最基本的性質。

      另一個要學不同系統的原因是:最新的邏輯系統有時只有一種證明系統,例如 relevant logic 目前主要還是公理證明系統,未有相應的自然演繹法和樹枝證明法(至少我未知道發現了沒)。若果你做研究要學最新的邏輯系統,無可避免要多學幾套證明系統。

      刪除

技術提供:Blogger.