2025-11-16T01:34:12.228023

Provability Models

Mojtahedi, Miranda
In this paper, we study a new Kripke-style semantics for classical modal logic, named as provability models. We study provability models for the propositional modal logics K, K4, S4 GL, GLP and the interpretability logic ILM. Provability models combine features of Kripke models with the assignment of logics to individual worlds. Originally introduced in [Mojtahedi, 2022], these models allowed the first author to establish arithmetical completeness for intuitionistic provability logic. Interestingly, we show that the ILM is complete for the same provability models of GL. We improve provability models to predicative and decidable provability models in the case of GL and ILM. Furthermore, we prove a soundness and completeness of GLP for provability models.
academic

Provability Models

基本信息

  • 论文ID: 2510.06696
  • 标题: Provability Models
  • 作者: Mojtaba Mojtahedi (Ghent University), Borja Sierra Miranda (University of Bern)
  • 分类: math.LO (Mathematical Logic)
  • 发表时间: October 15, 2025
  • 论文链接: https://arxiv.org/abs/2510.06696

摘要

本文研究了一种新的类Kripke语义学——可证性模型(provability models)，用于经典模态逻辑。研究涵盖了命题模态逻辑K、K4、S4、GL、GLP以及可解释性逻辑ILM的可证性模型。可证性模型结合了Kripke模型的特征与为个别世界分配逻辑的方法。该模型最初由Mojtahedi在2022年引入，用于建立直觉主义可证性逻辑的算术完备性。有趣的是，本文证明了ILM对于与GL相同的可证性模型是完备的。在GL和ILM的情况下，本文将可证性模型改进为可预测和可判定的可证性模型，并证明了GLP对可证性模型的可靠性和完备性。

研究背景与动机

核心问题

传统的可证性逻辑研究中，模态算子通常被解释为某个一阶算术或集合论系统中的可证性谓词。然而，也可以将□A解释为L ⊢ A（对于给定的命题理论L）。尽管对于任何包含GL的逻辑L，可以证明GL对于L-解释是可靠的，但没有这样的L-解释能给出GL的完备性。

问题的重要性

这种失败与PA-解释形成对比，主要源于逻辑L无法模拟Kripke模型，而Peano算术能够利用其模拟Kripke模型的能力（如Solovay所展示的）。因此，不能期望GL作为单个命题逻辑的可证性逻辑。

现有方法的局限性

  1. 标准Kripke模型的限制：无法直接处理可证性逻辑的算术解释
  2. 命题可证性解释的不完备性：单个命题逻辑无法提供GL的完备性
  3. 复杂的框架性质：如Iemhoff语义学中的复杂框架性质使得建立算术完备性定理变得困难

研究动机

本文通过将Kripke框架显式地融入命题逻辑来弥补这一限制，考虑标准Kripke模型，其中每个世界w都配备一个逻辑Lw，并基于底层可达性关系在这些理论之间施加可达性关系。

核心贡献

  1. 提出可证性模型框架：为经典模态逻辑引入了新的Kripke风格语义学
  2. 建立多种模态逻辑的完备性：证明了K、K4、S4、GL对可证性模型的可靠性和完备性
  3. 构造独立的可证性模型：特别是对于GL和ILM，展示了如何构造独立于标准Kripke模型的可证性模型
  4. 实现可判定性：在GL和ILM的情况下，构造了可判定的可证性模型
  5. 扩展到多模态逻辑：证明了GLP（多模态可证性逻辑）对可证性模型的可靠性和完备性
  6. 建立ILM的完备性：证明了可解释性逻辑ILM对与GL相同的可证性模型是完备的

方法详解

任务定义

研究可证性模型作为模态逻辑的语义学，其中：

  • 输入：模态逻辑公式和可证性模型
  • 输出：公式在模型中的有效性判断
  • 约束：模型必须满足特定的逻辑性质和框架条件

模型架构

可证性预模型定义

可证性预模型P = (W, <, {Lw}w∈W, V)包含：

  • W：非空世界集合
  • <：W上的二元关系
  • Lw：对每个<-可达世界w的逻辑
  • V：原子命题的赋值关系

有效性定义

对于公式A，定义P, w |= A通过归纳：

  • 与布尔连接词可交换
  • P, w |= □A 当且仅当 ∀u ⪯ w (⊢u A)

可证性模型条件

可证性预模型成为可证性模型需满足：

  • 模态完备性：对于每个纯模态公式A，如果P, w |=+ A则⊢w A

技术创新点

1. 框架条件的逻辑化

可证性模型能够将框架条件吸收为分配给个别世界的逻辑的推理规则：

  • 传递性可由必然化规则替代
  • 逆良基性可由Löb规则替代

2. 构造性方法

对于GL和ILM，提供了构造性方法来构建可证性模型：

定理4.4：对于每个逆良基树可证性预模型P，存在具有必然化的可证性模型P̄，使得：

  • P̄具有必然化
  • P ⊆ P̄
  • P̄是包含P的最小可证性模型

3. 可判定性保证

如果P是双有限的，则P̄是可判定的，其中双有限意味着W和每个w∈W的Axiom(Lw)都是有限的。

实验设置

理论验证框架

本文主要进行理论证明，验证框架包括：

1. 可靠性证明

对于各种模态逻辑，证明如果逻辑⊢ A，则P |= A对所有相应的可证性模型P成立。

2. 完备性证明

证明如果P |= A对所有相应的可证性模型P成立，则逻辑⊢ A。

3. 强完备性

特别对于GL，证明了强完备性：Γ |=P A蕴含Γ ⊢GL A。

构造方法验证

通过具体构造验证了：

  • 有限性可证性模型的存在性
  • 可判定性的实现
  • 独立性（不依赖于标准Kripke模型）

实验结果

主要结果

1. 基本模态逻辑的完备性

  • K：对可证性模型可靠且完备（定理3.6, 3.7）
  • K4：对具有必然化或传递性的可证性模型可靠且完备（定理3.8, 3.9）
  • S4：对反射、传递、具有必然化和局部完备性的可证性模型可靠且完备（定理3.11, 3.12）

2. 可证性逻辑GL的结果

  • 可靠性：GL对逆良基可证性模型具有必然化和Löb规则可靠（定理3.14）
  • 完备性：GL对有限传递非反射可证性模型完备（定理3.17）
  • 强完备性：GL对具有必然化和Löb规则的可证性模型强完备（定理3.18）
  • 有限性完备性：GL对有限性可证性模型完备（定理4.6）

3. 可解释性逻辑ILM的结果

  • 可靠性：ILM对逆良基可证性模型具有必然化可靠（定理5.6）
  • 完备性：ILM对有限树逆良基可证性模型具有必然化完备（定理5.10）
  • 有限性完备性：ILM对有限性可证性模型完备（定理5.13）

4. 多模态可证性逻辑GLP的结果

  • 可靠性和完备性：GLP对多可证性GLP-模型可靠且强完备（定理6.2, 6.3）

构造性结果

成功构造了独立于标准Kripke模型的可证性模型，特别是：

  • 对于任何逆良基树框架和任何公式集合到节点的分配，可以构造最小的可证性模型
  • 在双有限情况下，构造的模型是可判定的

相关工作

可证性逻辑传统研究

  • Solovay (1976)：建立了PA的可证性逻辑
  • Boolos (1995), Smoryński (1985)：可证性逻辑的经典教材
  • Artemov and Beklemishev (2004)：综合性调查

语义学方法

  • 标准Kripke语义学：用于各种模态逻辑
  • Veltman模型：用于可解释性逻辑ILM
  • 拓扑语义学：为GLP提供完备性

直觉主义可证性逻辑

  • Iemhoff (2001-2003)：引入了Iemhoff语义学
  • Mojtahedi (2022)：首次使用可证性模型建立直觉主义可证性逻辑的算术完备性

结论与讨论

主要结论

  1. 统一框架：可证性模型为多种模态逻辑提供了统一的语义框架
  2. 构造性：特别是对于GL和ILM，可以构造性地建立独立的可证性模型
  3. 可判定性：在适当条件下，可证性模型是可判定的
  4. 灵活性：框架条件可以被逻辑性质替代，提供了更大的灵活性

局限性

  1. GLP的限制：对于GLP，尚未找到可判定的可证性模型类
  2. 构造的复杂性：某些构造（如GLP的规范模型）可能不是构造性的
  3. 适用范围：主要适用于可证性性质的逻辑

未来方向

论文明确提出了几个开放问题：

  1. 证明逻辑的扩展：为证明逻辑LP和JGL的证明逻辑定义可证性风格模型
  2. 直觉主义模态逻辑：为具有两个模态算子□和◇的直觉主义模态逻辑定义可证性模型
  3. GLP的可判定模型：寻找GLP的可判定可证性模型类
  4. 算术完备性的简化：探索是否可以通过可证性模型简化ILM的算术完备性证明

深度评价

优点

  1. 理论创新：提出了全新的语义框架，统一了多种模态逻辑的处理
  2. 技术深度：提供了详细的数学证明和构造方法
  3. 实用价值：特别是在可判定性方面的改进具有重要意义
  4. 系统性：系统地处理了从基本模态逻辑到复杂可证性逻辑的各种情况

不足

  1. 复杂性：某些构造（特别是GLP）的复杂性可能限制其实际应用
  2. 开放问题：仍有重要的开放问题未解决，如GLP的可判定模型
  3. 应用范围：主要局限于理论研究，实际应用价值有待进一步探索

影响力

  1. 理论贡献：为模态逻辑语义学提供了新的研究方向
  2. 方法论价值：框架条件的逻辑化方法具有普遍意义
  3. 后续研究：为直觉主义逻辑、证明逻辑等领域的研究提供了新工具

适用场景

  1. 可证性逻辑研究：特别适用于需要算术完备性的研究
  2. 模态逻辑语义学：为复杂模态逻辑提供新的语义方法
  3. 计算逻辑：在需要可判定性的应用中具有潜在价值

参考文献

论文引用了丰富的相关文献，包括：

  • 可证性逻辑的经典文献（Boolos, Smoryński, Solovay等）
  • 模态逻辑语义学的重要工作（Blackburn等）
  • 可解释性逻辑的关键研究（Berarducci, Shavrukov等）
  • 直觉主义可证性逻辑的相关工作（Iemhoff等）

本论文在模态逻辑语义学领域做出了重要的理论贡献，提供了一个新的统一框架来处理各种可证性逻辑，同时在构造性和可判定性方面取得了显著进展。尽管仍有一些开放问题，但该工作为后续研究奠定了坚实的基础。