查看“︁线性逻辑”︁的源代码

在[[数理逻辑]]中，'''线性逻辑'''是拒绝“弱化”和“收缩”的[[结构规则]]的一种[[亚结构逻辑]]。对此解释是“假设是资源”:在[[证明]]中所有假设必须被消费“精确一次”。这区别于平常的逻辑比如[[经典逻辑]]或[[直觉逻辑]]，那里统治判断是“真理”，它可以按需要被自由的使用多次。例如，从[[命题]]''A''和''A'' ⇒ ''B''能按如下步骤得出结果''A'' ∧ ''B'':

#（1）在假定''A''和''A'' ⇒ ''B''上应用[[肯定前件]]（或蕴涵除去）得到结论''B''。
#（2）''A''和（1）的合取的得到结论''A'' ∧ ''B''。

这经常被符号化表示为[[相继式]]：''A'', ''A'' ⇒ ''B'' <math>\vdash</math> ''B''。在上述证明中"消费"了''A''为真的事实；这种真理的"自由"通常是在形式化数学中所需要的。

但是，真理经常在应用于关于这个世界的陈述的时候太抽象或不实用。比如，假设我有一[[夸脱]]的[[牛奶]]，我能用它制作一磅[[奶酪]]。如果我决定把我的所有牛奶都制成奶酪，我就不能下结论说我有牛奶和奶酪二者! 上面的逻辑模式让我们得到结论：<tt>牛奶</tt>, <tt>牛奶</tt>⇒<tt>奶酪</tt><math>\vdash</math><tt>牛奶</tt>∧<tt>奶酪</tt>（这里的<tt>牛奶</tt>表示命题"我有一夸脱牛奶"，等等）。普通逻辑建模这个活动失败是由于牛奶、奶酪一般是资源：资源的数量不像真理是可以随意使用和支配的自由事实，而是必须在所有"状态变更"中仔细计量的。关于牛奶制奶酪活动的准确陈述是：

:从一夸脱牛奶和从一夸脱牛奶转换出一磅奶酪的过程，我们获得一磅奶酪。

在线性逻辑中我们写为：<tt>牛奶</tt>，<tt>牛奶</tt>⊸<tt>奶酪</tt > <math>\Vdash</math> <tt>奶酪</tt>，使用了不同的连结词（{{math|⊸}}替代了⇒）和不同的逻辑蕴涵符号。

线性逻辑由[[法国]][[数学家]]让·伊夫·吉拉德（Jean-Yves Girard）在1987年提出。

==参见==
* [[证明网络]]
* [[博弈语义]]
* [[直觉逻辑]]
* [[可计算性逻辑]]
* [[直觉主义]]
* [[BHK释义]]
* [[直觉类型论]]
* [[经典逻辑]]
* [[中间逻辑]]
* [[构造性证明]]
* [[Curry-Howard对应]]
* [[可计算性逻辑]]

==外部链接==
* [http://www.csl.sri.com/users/lincoln/ Patrick Lincoln] {{Wayback|url=http://www.csl.sri.com/users/lincoln/ |date=20190403120845 }}'s excellent [http://www.csl.sri.com/~lincoln/papers/sigact92.ps Introduction to Linear Logic]（Postscript）

{{Logic-stub}}
[[Category:亚结构逻辑]]
[[Category:非經典邏輯]]