2016年8月11日



邏輯系統有分語意和語法兩個面向,證明系統 (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.)

2 comments:

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


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

    回覆刪除

 
Toggle Footer