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，其中逻辑常数的定义均采用其消去规则形式，并证明了该语义系统的可靠性与完备性。