Towards Automated Proof-Theoretic Semantics: Inference-Behaviour Semantics for 3-Dimensional K3 and LP

技术摘要：迈向自动化的证明论语义：针对三维 K3 与 LP 的推论行为语义

问题陈述
逻辑推理的自动化已趋于成熟（例如，通过消解法、定理证明器以及 Rocq 和 Lean 等交互式辅助工具），但为这类推理提供自动化的“证明论语义”（P-tS）仍是一个开放性挑战。虽然像 MUltlog 这样的系统可以根据模型论真值表自动生成相继式演算、表象法和自然演绎系统，但它们缺乏反向能力：即为这些系统中的联结词生成证明论意义规范。现有的 P-tS 方法（如证明论有效性或基底扩展语义）通常依赖于特定的演算，这阻碍了在不同逻辑（如经典逻辑与直觉主义逻辑）之间进行联结词意义的比较。本文旨在将“推论行为语义”（I-bS）方法——该方法通过建模联结词的最小推论行为来刻画其意义——集成到 MUltlog 框架中，从而实现多值逻辑证明论语义的自动化生成。

方法论
本文扩展了此前仅限于二维相继式演算的 I-bS 框架，将其推广至 $n$ 维相继式演算。其方法论通过以下步骤进行：

1. 形式化装置： 作者将 $n$ 维相继式定义为 $n$ 个公式多重集的 $n$ 元组。为了在不诉诸模型论真值的情况下解释这些相继式，作者采用了“多边主义”（multilateralist）的解读。对于三维相继式（特指强克莱尼逻辑 K3 和悖论逻辑 LP），这涉及三种言语行为：断言（维度 1）、悬置判断（维度 2）和否定（维度 3）。
2. 最小可推导关系： 为了将联结词的意义从特定逻辑的结构特征中分离出来，作者定义了一个由恒等式（$Id_3$）和受限的切断规则（$Cut_2$）组成的最小可推导关系。这避免了标准演算中完整结构规则（如收缩和弱化）所带来的“混淆”效应。
3. 可定义性与推论行为： 遵循 Belnap 式的定义，如果一个联结词能保守地扩展基底演算，并且与对应的联结词具有唯一的相互可推导性，则称该联结词是可定义的。核心度量指标是“推论行为”（$ib$），这是一个追踪联结词在可定义性证明过程中水平位置（维度）和规则应用的函数。
4. 意义扩展： 为了在不同维度（例如 2 维经典逻辑与 3 维旁论逻辑）之间比较联结词，本文引入了“意义扩展”概念。若一个 $m$ 维联结词在 $n$ 维片段内保守地保留了另一个 $n$ 维联结词的推论行为（其中 $m > n$），则称该 $m$ 维联结词扩展了后者的意义。

主要贡献与结果
本文将扩展后的框架应用于两种三值逻辑：K3 和 LP，并利用 MUltlog 生成的三维相继式演算进行研究。

• K3/LP 的语义子句： 作者证明了相对于最小 $\{Id_3, Cut_2\}$ 关系，K3 的乘法型与加法型版本的联结词均具有唯一性和保守性。作者为每种联结词版本推导出了不同的语义子句（例如，乘法合取 $\otimes$ 与加法合取 $\sqcap$），证明了标准的 K3 演算由于其结构规则的存在，会将语义上不同的联结词混淆。
• K3 与 LP 意义的同一性： 一个核心结果是 K3 和 LP 的联结词具有“相同”的意义。尽管 K3 和 LP 在指定值（K3 仅指定维度 3；LP 指定维度 2 和 3）方面存在差异，但它们的垂直可推导属性和运算规则是相同的。因此，它们在可定义性证明中的推论行为是相同的，从而产生相同的语义子句。
• 经典逻辑的意义扩展： 本文证明了 K3 和 LP 的三维联结词是其在 LK（二维）中经典对应物的“意义扩展”。通过将三维语义子句投影到第一和第三维度（移除第二维度），所得规则在语法上与经典 LK 联结词的语义子句一致。这证实了 K3/LP 联结词在不改变经典意义的前提下，保守地扩展了其意义。
• 处理结构规则： 分析表明，为了维持最小推论行为，上下文限制（例如限制相继式组件中的公式数量）是必要的。如果没有这些限制，标准结构规则（如收缩）会改变推论行为，从而有效地改变联结词的意义。

意义与主张
本文声称提供了将 I-bS 扩展到大于两个维度的第一个基础案例研究。其主要意义在于：

1. 跨演算比较： 它建立了一种机制，用于在不同维度的逻辑之间比较联结词的意义，解决了以往 P-tS 文献中难以比较具有不同结构属性之逻辑的问题。
2. 验证逻辑多元论： 关于 K3 和 LP 共享相同联结词意义的发现，支持了证明论视角的逻辑多元论，即不同的逻辑尽管具有不同的指定值或有效性条件，仍可以共享相同的联结词意义。
3. 通往自动化的路径： 通过成功将三维演算映射到 I-bS，本文为将 I-bS 集成到 MUltlog 中奠定了基础。最终目标是实现对任何有限值逻辑的语义子句生成的自动化。作者指出，虽然目前的工作是手动案例研究，但该框架旨在进行计算实现，从而可能实现任意多值逻辑的证明论语义自动生成。

作者对整个过程的即时自动化保持谦逊，承认为任意 $n$ 维演算生成必要的定义性证明仍然是一个计算挑战，尽管其理论框架已经搭建完成。