Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic

Abstract Proof-theoretic semantics (P-tS) is an innovative approach to grounding logical meaning in terms of proofs rather than traditional truth-conditional semantics. The point is not that one provides a proof system, but rather that one articulates meaning in terms of proofs and provability. To elucidate this paradigm shift, we commence with an introduction that contrasts the fundamental tenets of P-tS with the more prevalent model-theoretic approach to semantics. The contribution of this paper is a P-tS for a substructural logic, intuitionistic multiplicative linear logic (IMLL). Specifically, we meticulously examine and refine the established P-tS for intuitionistic propositional logic. Subsequently, we present two novel and comprehensive forms of P-tS for IMLL. Notably, the semantics for IMLL in this paper embodies its resource interpretation through its number-of-uses reading (restricted to atoms). This stands in contrast to the conventional model-theoretic semantics of the logic, underscoring the value that P-tS brings to substructural logics.