! 模态

在线性逻辑或者线性类型论中, $!$ 模态 (又叫指数模态、显然模态) 是用来给出某命题的结构逻辑版本的余单子模态.

之所以称之为显然模态, 是因为若一个命题 “显然” 成立, 说明给出它的证明需要费的功夫就可以忽略, 因此随意地复制、丢弃它都是无所谓的. 这对应它满足结构性规则的天性.

1定义

对于命题 $A$, 有命题 $!A$, 作为逻辑连接词的规则如下:

$$\frac{\Delta ,A⊢C}{\Delta ,!A⊢C}!L\frac{!\Delta ⊢A}{!\Delta ⊢!A}!R$$

然后 $!A$ 满足结构性规则, 即弱化规则和收缩规则.

在这些规则中, $!L$ 又叫丢弃.

2性质

命题 2.1. $!$ 的极性既不是正的也不是负的.

对于这一事实的分析, 参见伴随逻辑.

定理 2.2. 对于命题 $A,B$, 有如下命题等价: $$!(A\oplus B)\cong !A\otimes !B$$

这个等式形式上类似$$\exp (a+b)=\exp a\times \exp b$$因此 $!$ 模态又叫指数模态.

范畴语义

(..)

3参考文献

•	Jean-Yves Girard (1987). “Linear logic”. 1–101(doi) (web)

术语翻译

$!$ 模态 • 英文 bang modality

指数模态 • 英文 exponential modality

显然模态 • 英文 of course modality

丢弃 • 英文 dereliction