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）提出的B-eS，我们针对其中的合取联结词提出了基于广义消去规则形式的替代处理方案，并证明所得语义具有可靠性与完备性。这启发了我们的核心贡献：为IMLL构建一套B-eS，其中所有逻辑常量的定义均采用其消去规则的形式，同时建立了该语义系统的可靠性与完备性证明。