Relational semantics for full linear logic
Relational semantics for full linear logic
复制标题
全线性逻辑的关系语义
DOI：
10.1016/j.jal.2013.07.005
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
L. V. Rooijen
中科院分区：
文献类型：
--
作者：
Dion Coumans;M. Gehrke;L. V. Rooijen
Kripke框架给出的关系语义在模态逻辑和直觉逻辑的研究中起着重要的作用。在[4]中，它表明，关系语义学的理论也可以在更一般的子结构逻辑的设置，至少在一个代数的幌子。在这些思想的基础上，在[5]中描述了一种框架，它推广了Kripke框架，并以纯粹的关系形式为子结构逻辑提供了语义。主要的额外障碍是指数。我们分析这个操作代数和使用规范的扩展，以获得关系语义。因此，我们扩展了[4]，[5]中的工作，并使用他们的方法来获得全线性逻辑的关系语义。因此，我们说明了使用规范扩展来检索关系语义的优势：它允许对附加操作和公理进行模块化和统一的处理。传统上，所谓的阶段语义被用作线性逻辑（可证明性）的模型[8]。这些有缺点，相反，我们的方法，他们不允许额外的公理模块化处理。然而，正如我们将解释的那样，这两种方法是相关的。
Relational semantics, given by Kripke frames, play an essential role in the study of modal and intuitionistic logic. In [4] it is shown that the theory of relational semantics is also available in the more general setting of substructural logic, at least in an algebraic guise. Building on these ideas, in [5] a type of frames is described which generalise Kripke frames and provide semantics for substructural logics in a purely relational form.In this paper we study full linear logic from an algebraic point of view. The main additional hurdle is the exponential. We analyse this operation algebraically and use canonical extensions to obtain relational semantics. Thus, we extend the work in [4], [5] and use their approach to obtain relational semantics for full linear logic. Hereby we illustrate the strength of using canonical extension to retrieve relational semantics: it allows a modular and uniform treatment of additional operations and axioms.Traditionally, so-called phase semantics are used as models for (provability in) linear logic [8]. These have the drawback that, contrary to our approach, they do not allow a modular treatment of additional axioms. However, the two approaches are related, as we will explain.