A Proof-theoretic Semantics for Intuitionistic Linear Logic

TL;DR

This work extends proof-theoretic semantics to the full Intuitionistic Linear Logic (ILL) by developing a Base-extension Semantics (B-eS) that accounts for resource sensitivity and the exponential modality $!$. It refines atomic derivability and introduces a support relation $ vDash_{ extscr{B}}^{L}$, incorporating additive contexts and a modal box to capture promotion. The author establishes soundness and completeness for ILL within this BeS framework, using a simulation base to bridge semantic validity and syntactic proofs in $ m N_{ILL}$. Additionally, the paper discusses embeddings of IPL into ILL via Girard translations and investigates modal reasoning within this semantic setting, offering a foundation for analyzing substructural logics with exponentials through proof-theoretic semantics.

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.

Figures (6)

• Figure 1: Sandqvist's B-eS for Intuitionistic Propositional Logic
• Figure 2: Gheorghiu, Gu, and Pym's B-eS for IMLL
• Figure 3: The natural deduction system $\rm N_{ILL}$ for Intuitionistic Linear Logic in sequent style. The rules $\mathsf{Prom}$, $\mathsf{\top}_\mathsf{I}$ and $\mathsf{0}_\mathsf{E}$ hold for all $n\geq 0$.
• Figure 4: An alternative representation of the natural deduction system $\rm N_{ILL}$ for Intuitionistic Linear Logic in tree style. The rules $\mathsf{\top}_\mathsf{I}$ and $\mathsf{0}_\mathsf{E}$ again hold for all $n\geq 0$.
• Figure 5: Support for Intuitionistic Linear Logic

Theorems & Definitions (66)

• Theorem 1.1: IPL Soundness
• Theorem 1.2: IPL Completeness
• Definition 2.1: Intuitionistic linear formulae
• Definition 2.2: Sequent
• Definition 2.3: Intuitionistic linear derivability
• Definition 2.4: Additive box
• Definition 2.5: Inference schema
• Definition 2.6: Alternative intuitionistic linear derivability
• Theorem 2.7
• proof