Provability Models

Basic Information

• Paper ID: 2510.06696
• Title: Provability Models
• Authors: Mojtaba Mojtahedi (Ghent University), Borja Sierra Miranda (University of Bern)
• Classification: math.LO (Mathematical Logic)
• Publication Date: October 15, 2025
• Paper Link: https://arxiv.org/abs/2510.06696

Abstract

This paper investigates a novel Kripke-style semantics—provability models—for classical modal logics. The research encompasses provability models for propositional modal logics K, K4, S4, GL, GLP, and the interpretability logic ILM. Provability models combine the characteristics of Kripke models with an approach that assigns logics to individual worlds. The model was originally introduced by Mojtahedi in 2022 to establish arithmetic completeness for intuitionistic provability logic. Notably, this paper demonstrates that ILM is complete with respect to the same provability models as GL. In the cases of GL and ILM, the paper refines provability models into predictable and decidable provability models, and proves soundness and completeness of GLP with respect to provability models.

Research Background and Motivation

Core Problem

In traditional provability logic research, modal operators are typically interpreted as provability predicates in some first-order arithmetic or set-theoretic system. However, □A can alternatively be interpreted as L ⊢ A (for a given propositional theory L). Although GL can be shown to be sound with respect to L-interpretations for any logic L containing GL, no such L-interpretation yields completeness for GL.

Problem Significance

This failure contrasts with PA-interpretations, stemming primarily from the inability of propositional logic L to simulate Kripke models, whereas Peano arithmetic can exploit its capacity to simulate Kripke models (as demonstrated by Solovay). Therefore, one cannot expect GL to be the provability logic of a single propositional logic.

Limitations of Existing Approaches

1. Restrictions of standard Kripke models: Cannot directly handle arithmetic interpretations of provability logic
2. Incompleteness of propositional provability interpretations: A single propositional logic cannot provide completeness for GL
3. Complex frame properties: Complex frame properties in Iemhoff semantics make establishing arithmetic completeness theorems difficult

Research Motivation

This paper addresses this limitation by explicitly incorporating Kripke frameworks into propositional logic, considering standard Kripke models where each world w is equipped with a logic Lw, and imposing accessibility relations between these theories based on the underlying accessibility relation.

Core Contributions

1. Proposes provability model framework: Introduces novel Kripke-style semantics for classical modal logics
2. Establishes completeness for multiple modal logics: Proves soundness and completeness of K, K4, S4, GL with respect to provability models
3. Constructs independent provability models: Particularly for GL and ILM, demonstrates how to construct provability models independent of standard Kripke models
4. Achieves decidability: In the cases of GL and ILM, constructs decidable provability models
5. Extends to multimodal logic: Proves soundness and completeness of GLP (multimodal provability logic) with respect to provability models
6. Establishes ILM completeness: Demonstrates that interpretability logic ILM is complete with respect to the same provability models as GL

Methodology Details

Task Definition

Investigates provability models as semantics for modal logics, where:

• Input: Modal logic formulas and provability models
• Output: Validity judgment of formulas in the model
• Constraints: Models must satisfy specific logical properties and frame conditions

Model Architecture

Provability Premodel Definition

A provability premodel P = (W, <, {Lw}w∈W, V) contains:

• W: Non-empty set of worlds
• <: Binary relation on W
• Lw: Logic for each <-accessible world w
• V: Valuation relation for atomic propositions

Validity Definition

For formula A, define P, w |= A inductively:

• Commutes with boolean connectives
• P, w |= □A if and only if ∀u ⪯ w (⊢u A)

Provability Model Conditions

A provability premodel becomes a provability model if it satisfies:

• Modal completeness: For each pure modal formula A, if P, w |=+ A then ⊢w A

Technical Innovations

1. Logicalization of Frame Conditions

Provability models can absorb frame conditions as inference rules of logics assigned to individual worlds:

• Transitivity can be replaced by necessitation rule
• Converse well-foundedness can be replaced by Löb rule

2. Constructive Methods

For GL and ILM, provides constructive methods to build provability models:

Theorem 4.4: For each converse well-founded tree provability premodel P, there exists a provability model P̄ with necessitation such that:

• P̄ has necessitation
• P ⊆ P̄
• P̄ is the minimal provability model containing P

3. Decidability Guarantee

If P is bifinite, then P̄ is decidable, where bifinite means W and Axiom(Lw) for each w∈W are both finite.

Experimental Setup

Theoretical Verification Framework

The paper primarily conducts theoretical proofs, with verification framework including:

1. Soundness Proofs

For various modal logics, proves that if logic ⊢ A, then P |= A for all corresponding provability models P.

2. Completeness Proofs

Proves that if P |= A for all corresponding provability models P, then logic ⊢ A.

3. Strong Completeness

Particularly for GL, proves strong completeness: Γ |=P A implies Γ ⊢GL A.

Construction Method Verification

Verifies through concrete constructions:

• Existence of finite provability models
• Achievement of decidability
• Independence (not relying on standard Kripke models)

Experimental Results

Main Results

1. Completeness of Basic Modal Logics

• K: Sound and complete with respect to provability models (Theorems 3.6, 3.7)
• K4: Sound and complete with respect to provability models with necessitation or transitivity (Theorems 3.8, 3.9)
• S4: Sound and complete with respect to reflexive, transitive provability models with necessitation and local completeness (Theorems 3.11, 3.12)

2. Results for Provability Logic GL

• Soundness: GL is sound with respect to converse well-founded provability models with necessitation and Löb rule (Theorem 3.14)
• Completeness: GL is complete with respect to finite transitive non-reflexive provability models (Theorem 3.17)
• Strong Completeness: GL is strongly complete with respect to provability models with necessitation and Löb rule (Theorem 3.18)
• Finiteness Completeness: GL is complete with respect to finite provability models (Theorem 4.6)

3. Results for Interpretability Logic ILM

• Soundness: ILM is sound with respect to converse well-founded provability models with necessitation (Theorem 5.6)
• Completeness: ILM is complete with respect to finite tree converse well-founded provability models with necessitation (Theorem 5.10)
• Finiteness Completeness: ILM is complete with respect to finite provability models (Theorem 5.13)

4. Results for Multimodal Provability Logic GLP

• Soundness and Completeness: GLP is sound and strongly complete with respect to multimodal GLP-models (Theorems 6.2, 6.3)

Constructive Results

Successfully constructs provability models independent of standard Kripke models, particularly:

• For any converse well-founded tree frame and any assignment of formula sets to nodes, can construct the minimal provability model
• In the bifinite case, the constructed model is decidable

Related Work

Traditional Provability Logic Research

• Solovay (1976): Establishes provability logic of PA
• Boolos (1995), Smoryński (1985): Classical textbooks on provability logic
• Artemov and Beklemishev (2004): Comprehensive survey

Semantic Approaches

• Standard Kripke semantics: Used for various modal logics
• Veltman models: Used for interpretability logic ILM
• Topological semantics: Provides completeness for GLP

Intuitionistic Provability Logic

• Iemhoff (2001-2003): Introduces Iemhoff semantics
• Mojtahedi (2022): First uses provability models to establish arithmetic completeness for intuitionistic provability logic

Conclusions and Discussion

Main Conclusions

1. Unified Framework: Provability models provide a unified semantic framework for multiple modal logics
2. Constructivity: Particularly for GL and ILM, independent provability models can be constructed constructively
3. Decidability: Under appropriate conditions, provability models are decidable
4. Flexibility: Frame conditions can be replaced by logical properties, providing greater flexibility

Limitations

1. GLP Restrictions: For GLP, decidable provability model classes have not yet been found
2. Construction Complexity: Certain constructions (such as canonical models for GLP) may not be constructive
3. Scope of Application: Primarily applicable to logics with provability properties

Future Directions

The paper explicitly proposes several open problems:

1. Extensions of Proof Logic: Define provability-style models for proof logic LP and JGL
2. Intuitionistic Modal Logic: Define provability models for intuitionistic modal logic with two modal operators □ and ◇
3. Decidable Models for GLP: Seek decidable provability model classes for GLP
4. Simplification of Arithmetic Completeness: Explore whether arithmetic completeness for ILM can be simplified through provability models

In-Depth Evaluation

Strengths

1. Theoretical Innovation: Proposes a novel semantic framework that unifies treatment of multiple modal logics
2. Technical Depth: Provides detailed mathematical proofs and construction methods
3. Practical Value: Improvements in decidability are particularly significant
4. Systematicity: Systematically addresses various cases from basic modal logics to complex provability logics

Weaknesses

1. Complexity: The complexity of certain constructions (particularly GLP) may limit practical applications
2. Open Problems: Important open problems remain unsolved, such as decidable models for GLP
3. Application Scope: Primarily limited to theoretical research; practical application value requires further exploration

Impact

1. Theoretical Contribution: Provides new research directions for modal logic semantics
2. Methodological Value: The logicalization method for frame conditions has universal significance
3. Subsequent Research: Provides new tools for research in intuitionistic logic, proof logic, and other fields

Applicable Scenarios

1. Provability Logic Research: Particularly suitable for research requiring arithmetic completeness
2. Modal Logic Semantics: Provides new semantic methods for complex modal logics
3. Computational Logic: Has potential value in applications requiring decidability

References

The paper cites extensive relevant literature, including:

• Classical provability logic literature (Boolos, Smoryński, Solovay, etc.)
• Important works on modal logic semantics (Blackburn, etc.)
• Key research on interpretability logic (Berarducci, Shavrukov, etc.)
• Related work on intuitionistic provability logic (Iemhoff, etc.)

This paper makes important theoretical contributions to the field of modal logic semantics, providing a new unified framework for handling various provability logics while achieving significant progress in constructivity and decidability. Although some open problems remain, this work establishes a solid foundation for subsequent research.