A Proof-theoretic Semantics for Intuitionistic Linear Logic

问题
证明论语义学（P-tS）旨在通过“证明”的概念而非“真值”的概念来赋予逻辑表达式以意义。虽然 Sandqvist 成功地为直觉主义命题逻辑（IPL）建立了基础-扩展语义（B-eS），且 Gheorghiu, Gu, 和 Pym 将其扩展到了直觉主义线性逻辑的多重片段（IMLL），但完整的直觉主义线性逻辑（ILL）的 P-tS 仍然难以实现。主要的挑战在于 ILL 的亚结构性质，它禁止了通用的弱化（weakening）和收缩（contraction），以及它对加性连接词（additive connectives）和指数模态（exponential modality, !）的包含。现有的方法在基础-扩展框架内处理这些特征之间的相互作用时显得力不从心。具体而言，定义一个既能尊重 ILL 的资源敏感性质，又能正确捕捉“bang”（!）连接词（一种需要严格推导的模态算子）之推理性内容的支撑关系（support relation），存在着显著的困难。此外，标准的 ILL 自然演绎系统通常依赖于关于上下文共享（加性）和前提数量的特设（ad-hoc）侧条件，这些在 B-eS 所要求的刚性的、非模式化的原子规则结构中难以形式化。

方法论
本文通过解决两个主要的数学技术障碍，提出了一种新的 ILL 基础-扩展语义：一是自然演绎规则的形式化，二是定义一个能够处理加性和模态性的支撑关系。

1. 自然演绎的重新表述： 作者引入了一种新的 NILL 自然演绎系统语法，使用“加性框”（用花括号 {...} 表示）和“模态框”（用语义括号 J...K 表示）。

   • 加性框： 这些框划定了共享上下文，使得系统能够表示加性连接词（如 & 和 ⊕）以及具有可变前提的规则（如 ⊤I 和 0E），而无需依赖任意的上下文元变量。这使得加性的系统化处理成为可能，即在框内的推导共享相同的开放假设多重集。
   • 模态框： 这些用于刻画提升规则（Promotion rule, Prom）。该规则被重新定义为：要求结论是从一个上下文中得出的，其中所有假设都是仅包含模态框的规则的结论。这捕捉了指数模态的严格推导要求，而无需在规则的结构定义中显式引用 ! 连接词。
   • 作者证明了这一新系统与标准的序贯风格 NILL 是等价的（定理 2.7）。

2. 原子可推导性与支撑关系：

   • 原子规则： 基础定义为由一个加性框的多重集、单个加性框（结论）和一个原子组成的单位。这镜像了重新表述后的自然演绎规则的结构。
   • 基础扩展： 基础 $B$ 是此类原子规则的一个集合。可推导关系 $\vdash_B$ 通过归纳定义，处理了上下文的乘法拆分以及通过框结构实现的加性共享。
   • 支撑关系 ($\Vdash_B^L$)： 核心语义定义将支撑关系扩展到了 ILL。至关重要的是，指数模态 !ϕ 的子句不仅被定义为一个结构规则，而且是关于 $\phi$ 在基础扩展中有效性的一个条件。具体而言，当对于任何 $B$ 的扩展 $C$，如果 $\phi$ 是 $C$ 的“定理”（即对于所有 $D \supseteq C$，$\Vdash_D^\emptyset \phi$ 成立），则该资源可以被使用，则 $\Vdash_B^L !\phi$ 成立。
   • 处理模态： 本文引入了基础中“持久原子”（persistent atoms）的概念，这些原子对应于形式为 !ϕ 的公式。这些原子在可推导关系中扮演着类似于 ! 连接词的角色，使得语义能够区分标准假设与那些可以进行弱化或收缩的假设。

主要贡献

• 完整的 ILL B-eS： 本文提出了第一个涵盖完整直觉主义线性逻辑（包括加性连接词和指数模态）的基础-扩展语义。
• 加性的系统化处理： 通过引入加性框，作者提供了一种处理自然演绎中上下文共享和可变前提规则的方法，而无需依赖特设侧条件或显式的上下文元变量。这为推理图式提供了一种更简洁、更统一的表示。
• 模态框刻画： 利用模态框对提升规则的重新定义，提供了一种独立于特定连接词语法的指数模态的结构化刻画，促进了其向基础-扩展框架的整合。
• ! 的推理性解释： 本文对 ! 连接词的推理性内容进行了详细讨论。它认为，该语义通过将 ! 视为跨基础扩展的底层公式有效性的一个条件，捕捉了 ! 的模态性质，有效地将“必然化”（necessitation）方面内生化。
• 可靠性与完备性： 本文证明了所提议的语义对于自然演绎系统 NILL 是既可靠又完备的。完备性证明涉及构造一个其中原子规则模仿 NILL 推理规则的“模拟基础” $N$，并使用一个扁平化映射将 ILL 公式转化为原子。

结果

• 定理 2.7： 确立了标准序贯风格可推导性 ($\vdash$) 与新的基于框的可推导性 ($\vdash^*$) 之间的等价性。
• 定理 5.1（可靠性）： 证明了如果一个序贯在 NILL 中是可证明的，则它在所提议的语义中是有效的 ($\Gamma \vdash \phi \implies \Gamma \Vdash \phi$)。
• 定理 6.1（完备性）： 证明了如果一个序 Sequent 在语义中是有效的，则它在 NILL 中是可证明的 ($\Gamma \Vdash \phi \implies \Gamma \vdash \phi$)。
• 定理 4.15： 证明了用于处理带有 ! 的假设的特定 (Inf) 子句与更一般的 (Gen-Inf) 子句是等价的，验证了对模态假设的特定处理。
• 推论 4.11 & 4.12： 确立了关于 ! 与支撑关系相互作用的结构性质，表明如果 $\phi$ 是有效的，那么 !ϕ 也是有效的，并且如果 !Γ 支持 !ϕ，则 !Γ 支持 ϕ。

意义
本文声称填补了将基础-扩展方法从 IPL 和 IMLL 扩展到完整 ILL 这一领域的重要空白。作者指出，虽然 Gheorghiu, Gu, 和 Pym 成功处理了乘法片段，但加性成分和指数模态的加入需要大量新的机制。这项工作在本质上对于模态的证明论方法具有重要意义，它提供了一种理解“bang”连接词的方式，即不仅将其视为一个结构规则，而是将其视为基础-扩展框架内公式有效性的一个条件。作者谦逊地承认，处理提升规则和加性的方案“有些繁琐”，但为了实现推理图式的简洁、系统化表示是必要的。此外，本文强调了将 Sandqvist 的 IPL 语义直接嵌入此 ILL 框架的难度，并将两者之间映射的泛化留作未来研究的开放问题。这项工作表明，当前 P-tS 中的模态处理方法可能需要深层的形而上学或结构性洞察，而这些洞察才刚刚开始得到解决。