線性邏輯
外觀
在數理邏輯中,線性邏輯是拒絕「弱化」和「收縮」的結構規則的一種亞結構邏輯。對此解釋是「假設是資源」:在證明中所有假設必須被消費「精確一次」。這區別於平常的邏輯比如經典邏輯或直覺邏輯,那裏統治判斷是「真理」,它可以按需要被自由的使用多次。例如,從命題A和A ⇒ B能按如下步驟得出結果A ∧ B:
- (1)在假定A和A ⇒ B上應用肯定前件(或蘊涵除去)得到結論B。
- (2)A和(1)的合取的得到結論A ∧ B。
這經常被符號化表示為相繼式:A, A ⇒ B B。在上述證明中"消費"了A為真的事實;這種真理的"自由"通常是在形式化數學中所需要的。
但是,真理經常在應用於關於這個世界的陳述的時候太抽象或不實用。比如,假設我有一夸脫的牛奶,我能用它製作一磅奶酪。如果我決定把我的所有牛奶都製成奶酪,我就不能下結論說我有牛奶和奶酪二者! 上面的邏輯模式讓我們得到結論:牛奶, 牛奶⇒奶酪牛奶∧奶酪(這裏的牛奶表示命題"我有一夸脫牛奶",等等)。普通邏輯建模這個活動失敗是由於牛奶、奶酪一般是資源:資源的數量不像真理是可以隨意使用和支配的自由事實,而是必須在所有"狀態變更"中仔細計量的。關於牛奶制奶酪活動的準確陳述是:
- 從一夸脫牛奶和從一夸脫牛奶轉換出一磅奶酪的過程,我們獲得一磅奶酪。
在線性邏輯中我們寫為:牛奶, 牛奶奶酪奶酪,使用了不同的連結詞(
替代了⇒)和不同的邏輯蘊涵符號。
線性邏輯由法國數學家讓·伊夫·吉拉德(Jean-Yves Girard)在1987年提出。
參見
[編輯]外部連結
[編輯]- Patrick Lincoln (頁面存檔備份,存於互聯網檔案館)'s excellent Introduction to Linear Logic(Postscript)
![]() | 這是一篇與邏輯學相關的小作品。您可以透過編輯或修訂擴充其內容。 |