This work is the first exploration of proof-theoretic semantics for a substructural logic. It focuses on the base-extension semantics (B-eS) for intuitionistic multiplicative linear logic (IMLL). The starting point is a review of Sandqvist's B-eS for intuitionistic propositional logic (IPL), for which we propose an alternative treatment of conjunction that takes the form of the generalized elimination rule for the connective. The resulting semantics is shown to be sound and complete. This motivates our main contribution, a B-eS for IMLL, in which the definitions of the logical constants all take the form of their elimination rule and for which soundness and completeness are established.

翻译：本文是首次探讨子结构逻辑的证明论语义学，重点关注直觉乘法线性逻辑（IMLL）的基扩充语义（B-eS）。研究起点是对桑德奎斯特（Sandqvist）直觉命题逻辑（IPL）的基扩充语义的回顾，我们针对其中的合取算子提出了一种替代处理方式，采用该连接词的广义消去规则形式。结果表明该语义具有可靠性和完全性。这启发我们提出主要贡献——IMLL的基扩充语义，其中所有逻辑常项的定义均采用其消去规则形式，并确立了该语义的可靠性和完全性。