亞結構邏輯

維基百科,自由的百科全書
跳到: 導覽搜尋

數理邏輯中,特別是聯合上證明論的時候,一些亞結構邏輯已經作為比常規系統弱的命題演算系統被介入了。同常規系統的不同之處在於它們有更少的結構規則可用:結構規則的概念是基於相繼式(sequent)表達,而不是自然演繹的公式化表達。兩個重要的亞結構邏輯是相干邏輯線性邏輯

相繼式演算中,你可以把證明的每一行寫為

這裏的結構規則是重寫相繼式左手端的Γ的規則,Γ是最初被構想為命題的字符串。這個字符串的標準解釋是合取式:我們希望把相繼式符號

讀做

(A B)蘊涵C

這裏我們把右手端的Σ採納為一個單一的命題C(這是直覺主義風格的相繼式);但是所有的東西都同樣的適用於一般情況,因為所有的操作都發生在十字轉門(turnstile)符號的左邊。

因為合取是交換性結合性的操作,相繼式理論的形式架設通常包括相應的結構規則來重寫相繼式的Γ - 例如

演繹自

還有對應於合取特性的冪等性單調性的進一步的結構規則:從

我們可以演繹出

還有從

我們可以演繹出,對於任何B

線性邏輯中有重複的假設(hypothese)'被認為'不同於單一的出現,它排除了這兩個規則。而相干邏輯只排除後者的規則,因為B明顯的與結論無關。

這些是結構規則的基本例子。在應用到常規命題演算的時候,這些規則是沒有任何爭議的。它們自然的出現於證明理論中,並在那裏被首次注意到(在獲得一個名字之前)。

外部連結[編輯]