余直觉主义线性逻辑的范畴证明论
计算机科学中的逻辑
2015-07-01 v5
摘要
为了为余直觉主义逻辑提供范畴语义，必须面对Tristan Crolard指出的一个事实：在范畴Set中，余指数作为余积的伴随的定义不成立，因为余积是不交并。遵循直觉主义线性逻辑带指数“!”的模型的常见构造，我们在具有附加结构的对称幺半左闭范畴中构建了余直觉主义逻辑的模型，在构造自由范畴时使用了Crolard的余直觉主义逻辑项赋值的变体。
引用
@article{arxiv.1407.3416,
title = {Categorical Proof Theory of Co-Intuitionistic Linear Logic},
author = {Gianluigi Bellin},
journal= {arXiv preprint arXiv:1407.3416},
year = {2015}
}