A Proof-theoretic Semantics for Intuitionistic Linear Logic

TL;DR

This paper develops a proof-theoretic semantics for the full intuitionistic linear logic, including the modal 'bang' connective, extending previous work on substructural logic semantics.

Contribution

It provides a new semantics for the entire intuitionistic linear logic, especially addressing the challenging 'bang' modality, advancing the understanding of substructural logic semantics.

Findings

Semantics successfully captures the 'bang' modality.

Extends previous semantics from multiplicative fragment to full logic.

Addresses inferentialist aspects of the 'bang' connective.

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 formulas marked with this connective is particularly challenging and a discussion is dedicated to this at the end of the paper.