The approach to giving a proof-theoretic semantics for IMLL taken by Gheorghiu, Gu and Pym is an interesting adaptation of the work presented by Sandqvist in his 2015 paper for IPL. What is particularly interesting is how naturally the move to the substructural setting provided a semantics for the multiplicative fragment of intuitionistic linear logic. Whilst ultimately the authors of the semantics for IMLL used their foundations to provide a semantics for bunched implication logic, it begs the question, what of the rest of intuitionistic linear logic? In this paper, I present a semantics for intuitionistic linear logic, by first presenting a semantics for the multiplicative and additive fragment after which we focus solely on considering the modality "of-course", thus giving a proof-theoretic semantics for intuitionistic linear logic.
翻译:Gheorghiu、Gu和Pym为直觉主义乘法线性逻辑(IMLL)提供证明论语义学的方法,是对Sandqvist在其2015年关于直觉主义命题逻辑(IPL)论文中所提出工作的有趣改编。特别引人注目的是,向子结构框架的迁移如何自然地为直觉主义线性逻辑的乘法片段提供了语义。尽管IMLL语义的作者最终利用其基础为束蕴含逻辑提供了语义,但这引出了一个问题:直觉主义线性逻辑的其余部分该如何处理?在本文中,我首先为乘法与加法片段给出语义,随后专门考虑"当然"模态,从而为直觉主义线性逻辑提供了一种证明论语义学。