线性逻辑
外观
(重定向自線性邏輯)
在数理逻辑中,线性逻辑是拒绝“弱化”和“收缩”的结构规则的一种亚结构逻辑。对此解释是“假设是资源”:在证明中所有假设必须被消费“精确一次”。这区别于平常的逻辑比如经典逻辑或直觉逻辑,那里统治判断是“真理”,它可以按需要被自由的使用多次。例如,从命题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)
![]() | 这是一篇與逻辑学相關的小作品。您可以通过编辑或修订扩充其内容。 |