! 模态

线性逻辑或者线性类型论中, 模态 (又叫指数模态显然模态) 是用来给出某命题的结构逻辑版本的余单子模态. 对于线性的命题 , 有命题 , 它可以一定程度上和 互相转化, 并且 满足结构性规则.

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

1定义

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

这些规则定义了 的互相转化. 然后 满足结构性规则, 即弱化规则收缩规则, 这些规则省略.

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

2性质

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

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

定理 2.2. 对于命题 , 有如下命题等价:

这个等式形式上类似因此 模态又叫指数模态.

范畴语义

(..)

3参考文献

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

术语翻译

模态英文 bang modality

指数模态英文 exponential modality

显然模态英文 of course modality

丢弃英文 dereliction