线性逻辑

在逻辑学中, 线性逻辑是亚结构逻辑的一种, 只假设结构性规则中的交换规则.

线性逻辑中的蕴涵记作 $A⊸B$, 读作 “棒棒糖” 或者 “线性蕴涵”.

1逻辑连接词

参见: 逻辑连接词

线性逻辑中的命题使用形式文法定义如下:

$$\begin{array}{rl}A,B::=& A⊸B\mid A\otimes B\mid 1\mid A\&B\mid \top \mid A\oplus B\mid 0\end{array}$$

在使用经典相继式演算的线性逻辑中, 还要加入 $A⅋B$ 这个连接词, 但本文使用直觉主义相继式, 因此不需要它.

早期线性逻辑中, 还有$!$ 模态这个连接词, 但实际上它最好在伴随逻辑中讨论.

2规则

线性逻辑中使用相继式演算风格的规则定义如下, 用 $\Delta$ 代表语境. 若有多个语境, 则使用下标区分. 若要使用自然演绎, 请参见相继式演算–自然演绎类比.

对于相继式 $\Delta ⊢A$, 若某规则对 $\Delta$ 中的连接词进行消除, 那么称之为左规则, 反之则称之为右规则.

•	与对应的连接词 $A\otimes B$ (乘性与), 极性为正: $$\frac{{\Delta }_1⊢A{\Delta }_2⊢B}{{\Delta }_1,{\Delta }_2⊢A\otimes B}\frac{\Delta ,A,B⊢C}{\Delta ,A\otimes B⊢C}$$

•	与对应的另一连接词 $A\&B$ (加性与), 极性为负: $$\frac{\Delta ⊢A\Delta ⊢B}{\Delta ⊢A\&B}\frac{\Delta ,A⊢C}{\Delta ,A\&B⊢C}\frac{\Delta ,B⊢C}{\Delta ,A\&B⊢C}$$ 该连接词又叫 “外选择”, 因为在使用它的左规则时需要从两条规则中选择一个. 左规则消除的是前提条件中的命题, 相对于需要证明的命题来说是 “外部”.

•	线性蕴涵对应的连接词: $$\frac{\Delta ,A⊢B}{\Delta ⊢A⊸B}\frac{{\Delta }_1⊢A{\Delta }_2,B⊢C}{{\Delta }_1,{\Delta }_2,A⊸B⊢C}$$在自然演绎中, 第二条规则如下: $$\frac{{\Delta }_1⊢A⊸B{\Delta }_2⊢A}{{\Delta }_1,{\Delta }_2⊢B}$$

•	或对应的连接词: $$\frac{\Delta ⊢A}{\Delta ⊢A\oplus B}\frac{\Delta ⊢B}{\Delta ⊢A\oplus B}\frac{\Delta ,A⊢C\Delta ,B⊢C}{\Delta ,A\oplus B⊢C}$$ 该连接词又叫 “内选择”, 因为在使用它的右规则时需要从两条规则中选择一个. 右规则消除的是作为结论的命题, 相对于需要证明的命题来说是 “内部”.

剩余规则较为简单, 一并列出:

$$\frac{}{⊢1}\frac{\Delta ⊢C}{\Delta ,1⊢C}$$

$$\frac{}{\Delta ⊢\top }\frac{}{\Delta ,0⊢C}$$

另见: 切规则

3应用

•	通信类型和直觉主义线性逻辑之间有 Curry–Howard 对应关系.

•	半公理化逻辑由线性逻辑修改而来.

4相关概念

•	伴随逻辑结合了线性逻辑和结构逻辑,

•	! 模态在部分文献中被认为是线性逻辑的一部分,

•

聚焦始于线性逻辑.

术语翻译

线性逻辑 • 英文 linear logic • 日文 線形論理

$A$ 线性蕴涵 $B$ • 英文 $A$ loli $B$ • 日文 $A$ 線形含意 $B$

外选择 • 英文 external choice

内选择 • 英文 internal choice