Refutation calculi for lattice-based logics: from display to tableaux

技术摘要：基于格逻辑的归谬演算：从显示演算到表列

问题陈述
归谬演算（Refutation calculi）是旨在推导给定逻辑中无效公式（或反序列）的形式系统。尽管这一方法在表列演算的发展历史上曾起到关键作用，但尚未成功适配到显示演算（display calculi）的框架中。由 Belnap 引入的显示演算是一种强大的演绎系统，能够为包括模态逻辑和次结构逻辑在内的广泛非经典逻辑提供无割（cut-free）的表述。然而，其标准应用侧重于证明构造（即推导有效序列）。本文旨在填补在显示演算框架内建立系统化归谬方法的空白，特别是针对基本 LE-逻辑族（即与任意签名的基本正规格扩张规范关联的逻辑）。

方法论
作者提出了一种方法论，反转了显示演算的标准角色。他们不是为有效序列构造证明，而是调整显示演算的机制以生成无效序列（反序列）的推导。

1. 基础框架：该工作基于基本正规 LE-逻辑理论，该理论在格扩张上推广了各种逻辑系统（例如，正交模逻辑、兰贝克演算）。其语言包含命题字母以及两组与特定序型相关的连接词 $F$ 和 $G$。
2. 归谬显示演算（$D.LE^r$）：核心贡献在于定义了归谬显示演算 $D.LE^r$。该系统操作形如 $\Pi \nvdash \Sigma$ 的反序列。$D.LE^r$ 的规则源自标准显示演算 $D.LE$，但经过调整以推导无效性。
   • 公理：系统始于代表明显无效性的初始反序列（例如，$\hat{\top} \nvdash \check{\bot}$，$p \nvdash q$）。
   • 规则：系统采用显示规则、结构规则和逻辑引入规则。关键在于，这些规则旨在将复杂的反序列分解为更简单的反序列。
   • 侧条件：为确保可靠性，施加了特定的侧条件，特别是关于某些规则的终序列中是否存在“剩余项”（对应于运算连接词剩余项的结构连接词）。
3. 证明分析：作者通过对标准演算 $D.LE$中可推导序列的证明分析，确立了$D.LE^r$ 的性质。他们利用了有效性与无效性之间的逆否关系。
4. 表列构造：最后，作者通过取 $D.LE^r$ 规则的逆否形式，定义了针对 LE-逻辑的终止表列演算。在此表列系统中，若一个分支包含初始反序列（表明原序列无效），则该分支为“开放”；若在不重复的情况下无更多规则可应用，则该分支为“封闭”。

主要贡献与结果

• $D.LE^r$ 的引入：本文首次引入了针对基本正规 LE-逻辑的归谬显示演算。这些演算系统地推导反序列，为标准的证明论方法提供了对偶视角。
• 可靠性与完备性：
  • 可靠性（定理 1）：作者证明了 $D.LE^r$ 的规则相对于完全 $L$-代数类是可靠的。这是通过展示若一个反序列可推导，则对应的序列无效来证明的。证明涉及对序列复杂度的详细归纳以及对 $D.LE$ 中无割推导的分析。
  • 完备性（定理 2 与推论 1）：本文证明了，若序列 $\Pi \vdash \Sigma$ 在标准演算 $D.LE$中不可推导（且不包含剩余项），则对应的反序列$\Pi \nvdash \Sigma$在$D.LE^r$ 中可推导。这确立了归谬演算的完备性。
• 可判定性：作为 $D.LE^r$ 完备性及 $D.LE$ 性质的直接推论，作者得出结论：基本正规 LE-逻辑在语法上是可判定的。
• 终止表列：本文展示了如何将 $D.LE^r$ 转化为终止表列演算。定理 3 确立，一个序列有效当且仅当存在针对它的封闭表列树。终止性由规则结论中连接词数量的减少以及通过显示规则上的侧条件防止循环来保证。

意义与主张
本文声称，这项工作代表了将归谬方法与显示演算的结构力量相结合的重要一步。通过成功地将显示演算适配用于归谬，作者为处理广泛一类基于格逻辑的无效性提供了一个统一的框架。

其意义在于：

1. 扩展显示演算：它将显示演算的传统用途从证明构造扩展到包含归谬，从而扩大了分析非经典逻辑的工具箱。
2. 统一性：该方法适用于整个基本 LE-逻辑族，在单一理论框架下涵盖了正交模逻辑和兰贝克演算等多样化的系统。
3. 可判定性与表列：从归谬显示演算推导出的终止表列为这些逻辑提供了实用的判定过程，将抽象的证明论性质与具体的算法方法联系起来。

作者最后指出，这项工作为未来的研究方向开辟了道路，例如将平台扩展到分配性 LE-逻辑、处理公理化扩展，以及探索包含序列和反序列的系统中“抗割”（anticut）消除问题。他们保持谦逊的态度，将这些视为有希望的初步步骤和进一步研究的潜在途径，而非解决该领域所有未决问题的定论。