经典线性逻辑语义的证明论方法（技术报告） (A Proof-Theoretic Approach to the Semantics of Classical Linear Logic (Technical Report))

Linear logic (LL) is a resource-aware, abstract logic programming language that refines both classical and intuitionistic logic. Linear logic semantics is typically presented in one of two ways: by associating each formula with the set of all contexts that can be used to prove it (e.g. phase semantics) or by assigning meaning directly to proofs (e.g. coherence spaces). This work proposes a different perspective on assigning meaning to proofs by adopting a proof-theoretic perspective. More specifically, we employ base-extension semantics (BeS) to characterise proofs through the notion of base support. Recent developments have shown that BeS is powerful enough to capture proof-theoretic notions in structurally rich logics such as intuitionistic linear logic. In this paper, we extend this framework to the classical case, presenting a proof-theoretic approach to the semantics of the multiplicative-additive fragment of linear logic (MALL).

翻译：线性逻辑（LL）是一种资源感知的抽象逻辑编程语言，它同时细化了经典逻辑和直觉主义逻辑。线性逻辑的语义通常通过以下两种方式之一呈现：将每个公式与所有可用于证明它的上下文集合相关联（例如相位语义），或直接将意义赋予证明（例如相干空间）。本研究通过采用证明论视角，提出了一种不同的为证明赋予意义的观点。具体而言，我们采用基扩展语义（BeS），通过基支持的概念来刻画证明。最近的研究进展表明，BeS足够强大，能够捕捉结构丰富逻辑（如直觉主义线性逻辑）中的证明论概念。在本文中，我们将此框架扩展到经典情况，提出了线性逻辑乘加片段（MALL）语义的证明论方法。