A mixed linear and non-linear logic: Proofs, terms and models
A mixed linear and non-linear logic: Proofs, terms and models
复制标题
DOI：
10.1007/bfb0022251
复制
发表时间：
1995-01-01
期刊：
影响因子：
--
通讯作者：
Benton, PN
中科院分区：
文献类型：
--
作者：
Benton, PN
直觉线性逻辑通过！重新获得了直觉逻辑的表达能力。(‘当然’)情态。Benton，Bierman，Hyland和De Paiva给出了一种术语分配系统以及与之相关的范畴模型的概念。情态是由满足某些额外条件的复合词构成的。本文试图通过给出一个逻辑、术语演算和范畴模型来更直接和对称地解释ILL和IL之间的联系。在这个系统中，线性世界和非线性世界是平等存在的，运算可以双向通过。我们从Benton，Bierman，Hyland和De Paiva给出的ILL的范畴模型出发，证明了这等价于对称么半闭范畴和笛卡尔闭范畴之间的对称么半伴随。然后，我们推导出对应于新的模型概念的逻辑的顺序演算和自然演绎表示。
Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! ('of course') modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed category' which arises as a full subcategory of the category of coalgebras for the comonad.This paper attempts to explain the connection between ILL and IL more directly and symmetrically by giving a logic, term calculus and categorical model for a system in which the linear and non-linear worlds exist on an equal footing, with operations allowing one to pass in both directions. We start from the categorical model of ILL given by Benton, Bierman, Hyland and de Paiva and show that this is equivalent to having a symmetric monoidal adjunction between a symmetric monoidal closed category and a cartesian closed category. We then derive both a sequent calculus and a natural deduction presentation of the logic corresponding to the new notion of model.