A Proof-theoretic Semantics for Intuitionistic Linear Logic

Abstract

The approach taken by Gheorghiu, Gu and Pym in their paper on giving a base-extension semantics for Intuitionistic Multiplicative Linear Logic is an interesting adaptation of the work of Sandqvist for IPL to the substructural setting. 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 Gheorghiu, Gu and Pym 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 just such a semantics. This is particularly of interest as this logic has as a connective the bang, a modal connective. Capturing the inferentialist content of formulae marked with this connective is particularly challenging and a discussion is dedicated to this at the end of the paper.