2025-11-15T18:37:11.030658

A Unified Gentzen-style Framework for Until-free LTL

Kamide, Negri
A unified Gentzen-style framework for until-free propositional linear-time temporal logic is introduced. The proposed framework, based on infinitary rules and rules for primitive negation, can handle uniformly both a single-succedent sequent calculus and a natural deduction system. Furthermore, an equivalence between these systems, alongside with proofs of cut-elimination and normalization theorems, is established.
academic

A Unified Gentzen-style Framework for Until-free LTL

基本信息

  • 论文ID: 2501.00494
  • 标题: A Unified Gentzen-style Framework for Until-free LTL
  • 作者: Norihiro Kamide (Nagoya City University), Sara Negri (University of Genoa)
  • 分类: cs.LO (Logic in Computer Science)
  • 发表会议: Non-Classical Logics Theory and Applications (NCL'24), EPTCS 415, 2024
  • 论文链接: https://arxiv.org/abs/2501.00494

摘要

本文引入了一个统一的Gentzen风格框架，用于无until算子的命题线性时态逻辑。该框架基于无穷规则和原始否定规则，能够统一处理单后继式相继式演算和自然演绎系统。此外，还建立了这些系统之间的等价性，并提供了割消去定理和正规化定理的证明。

研究背景与动机

问题定义

线性时态逻辑(LTL)及其片段在计算机科学和逻辑学中得到了广泛研究。虽然已有许多针对LTL的Gentzen风格相继式演算和自然演绎系统，但这些系统通常是分别研究的，缺乏统一的理论框架。

研究重要性

  1. 理论统一性: 建立相继式演算和自然演绎系统之间的统一框架，有助于从一个形式系统向另一个形式系统导入元理论结果
  2. 割消去与正规化的对应关系: 探索割消去定理与正规化定理之间的深层联系
  3. 兼容性: 所提出的框架与Gentzen的直觉主义逻辑系统LJ和NJ高度兼容

现有方法局限性

  • 现有的LTL相继式演算(如Kawai的LTω)和自然演绎系统(如Baratella和Masini的PNK/PNJ)缺乏统一处理
  • 标准的多后继式相继式演算的割消去定理不能直接推导出对应自然演绎系统的正规化定理
  • 缺乏单后继式相继式演算来建立这种对应关系

核心贡献

  1. 引入了新的单后继式相继式演算SLTω: 这是Kawai的LTω系统的单后继式版本
  2. 提出了统一的自然演绎系统NLTω: 基于无穷前提规则而非归纳规则
  3. 建立了系统间的等价性: 证明了SLTω与LTω以及NLTω与SLTω之间的等价性
  4. 证明了割消去定理: 为SLTω系统证明了割消去定理
  5. 证明了正规化定理: 通过割消去定理间接证明了NLTω的正规化定理
  6. 提供了统一框架: 首次为until-free LTL提供了统一处理相继式演算和自然演绎的框架

方法详解

逻辑语言定义

论文考虑的逻辑包含以下连接词：

  • 命题连接词: → (蕴含), ¬ (否定), ∧ (合取), ∨ (析取)
  • 时态算子: G (全局将来), F (最终将来), X (下一时刻)
  • 嵌套算子: X^i α 表示i次嵌套的下一时刻算子

相继式演算SLTω

基本结构

  • 相继式形式: Γ ⇒ γ，其中γ是公式或空集
  • 初始相继式: X^i p, Γ ⇒ X^i p (对任意命题变量p)

关键规则

  1. 时态排中律规则:
    X^i¬α, Γ ⇒ γ    X^iα, Γ ⇒ γ
────────────────────────────── (ex-middle)
           Γ ⇒ γ
  2. 否定规则:
    Γ ⇒ X^iα              X^iα, Γ ⇒ ∅
─────────────         ─────────────
X^i¬α, Γ ⇒ ∅         Γ ⇒ X^i¬α
  3. 时态算子规则:
    • G算子: 使用无穷前提规则处理"全局将来"
    • F算子: 使用存在性规则处理"最终将来"

自然演绎系统NLTω

特征规则

  1. EXP规则 (爆炸原理的时态版本):
    X^i¬α    X^iα
──────────────
      γ
  2. EXM规则 (排中律的时态版本):
    [X^i¬α]    [X^iα]
   ⋮          ⋮
   γ          γ
──────────────────
       γ
  3. ¬I规则 (否定引入的时态版本):
    [X^iα]     [X^iα]
   ⋮          ⋮
X^j¬γ      X^jγ
─────────────────
    X^i¬α

技术创新点

  1. 单后继式设计: 通过限制相继式右边最多有一个公式，建立了与自然演绎系统的直接对应关系
  2. 时态排中律: 将von Plato的经典逻辑排中律规则扩展到时态逻辑，这是关键的技术创新
  3. 无穷规则: 使用无穷前提规则而非归纳规则来处理时态算子，简化了系统间的对应关系
  4. 原始否定: 将否定作为原始连接词处理，而非通过蕴含和假常量定义

主要定理

割消去定理 (定理2.10)

定理: 割规则在无割的SLTω中是可容许的。

证明思路:

  1. 利用SLTω与LTω的等价性
  2. 应用LTω的割消去定理
  3. 通过引理2.8建立转换关系

等价性定理 (定理2.11)

定理: 对任意公式α，SLTω ⊢ ⇒ α 当且仅当 LTω ⊢ ⇒ α。

正规化定理 (定理4.3)

定理: NLTω中的所有推导都是可正规化的。

证明方法:

  1. 将自然演绎推导转换为带割的相继式推导
  2. 应用割消去得到无割推导
  3. 将无割推导转换回正规的自然演绎推导

系统间的对应关系

推导转换

论文建立了以下转换关系：

  1. NLTω → SLTω: 引理4.1(1)将自然演绎推导转换为相继式推导
  2. SLTω → NLTω: 引理4.1(2)将无割相继式推导转换为正规自然演绎推导
  3. 等价性: 定理4.2建立了两系统的完全等价性

正规化的间接证明

通过以下路径实现正规化：

非正规NLTω推导 → 带割SLTω推导 → 无割SLTω推导 → 正规NLTω推导

相关工作

历史背景

  • Kawai (1987): 引入了LTω相继式演算
  • Baratella & Masini (2003-2004): 提出了2Sω系统和PNK/PNJ自然演绎系统
  • von Plato (1999): 为经典逻辑引入了单后继式相继式演算

本文的位置

本文首次为until-free LTL建立了统一的Gentzen风格框架，填补了时态逻辑中相继式演算与自然演绎系统统一处理的空白。

结论与讨论

主要结论

  1. 成功建立了until-free LTL的统一Gentzen风格框架
  2. 证明了单后继式相继式演算与自然演绎系统的等价性
  3. 通过割消去间接证明了正规化定理
  4. 为时态逻辑的证明论研究提供了新的理论工具

局限性

  1. 间接正规化: 正规化证明是间接的，未提供直接的正规化算法
  2. 单向对应: 目前的对应关系不是双向的，割消去步骤与正规化步骤之间缺乏精确对应
  3. 强正规化: 未讨论强正规化和Church-Rosser定理
  4. 范围限制: 仅考虑until-free片段，不包含until算子

未来方向

  1. 双向对应: 使用一般消去规则改进对应关系
  2. 直接正规化: 提供直接的正规化证明
  3. 强正规化: 研究强正规化性质
  4. 扩展: 考虑包含until算子的完整LTL

深度评价

优点

  1. 理论贡献: 首次为until-free LTL建立了统一的证明论框架，具有重要的理论价值
  2. 技术创新:
    • 时态排中律规则的设计巧妙
    • 单后继式系统的构造有效
    • 无穷规则的使用简化了系统结构
  3. 严谨性: 所有主要定理都有完整的证明，技术细节处理得当
  4. 系统性: 建立了完整的理论体系，包括语法、语义和证明论各个层面

不足

  1. 实用性限制:
    • 仅处理until-free片段，实际应用受限
    • 无穷规则在实际实现中可能存在困难
  2. 证明技术:
    • 正规化证明依赖于割消去，不够直接
    • 缺乏计算复杂性分析
  3. 对应关系:
    • 割消去步骤与正规化步骤之间的精确对应尚未建立
    • 双向转换的效率问题未讨论

影响力

  1. 理论影响: 为时态逻辑的证明论研究提供了新的方法和工具
  2. 方法论贡献: 统一框架的思想可以推广到其他逻辑系统
  3. 实用价值: 虽然目前主要是理论贡献，但为自动定理证明和形式验证提供了基础

适用场景

  1. 形式验证: 为时态性质的形式化验证提供证明论基础
  2. 自动推理: 为时态逻辑的自动定理证明器设计提供理论支撑
  3. 逻辑教学: 为理解时态逻辑的证明论结构提供统一视角
  4. 理论研究: 为进一步研究时态逻辑的元理论性质奠定基础

参考文献

论文引用了32篇相关文献，主要包括：

  • Kawai (1987): Sequential calculus for first order infinitary temporal logic
  • Baratella & Masini (2003-2004): 时态逻辑的证明论研究
  • von Plato (1999, 2001): 结构证明论和单后继式演算
  • Gentzen (1969): 经典的自然演绎和相继式演算理论
  • Negri & von Plato (2001): 结构证明论的现代发展

这篇论文在时态逻辑的证明论研究中具有重要意义，通过巧妙的技术设计建立了相继式演算与自然演绎系统的统一框架，为该领域的进一步发展奠定了坚实的理论基础。