Modal logical aspects of provability predicates and consistency statements
Haruka Kogure, Taishi Kurahashi
TL;DR
The paper addresses how different derivability conditions and formulations of consistency statements for arithmetic theories align with modal logics, aiming to classify and prove arithmetical completeness for several logics. It extends Solovay's arithmetical completeness framework and refines Rosser-type provability predicates to handle logics such as $NP$, $ND$, $NP4$, and $ND4$, including challenging cases like $ND4$. The main contributions are (i) modal completeness results for the targeted logics with explicit finite-frame properties, and (ii) constructive arithmetical completeness theorems showing the existence of $ extsf{Σ}_1$ provability predicates that realize these logics as provability logics of arithmetic. These results illuminate the landscape of G2-style theorems by revealing how different derivability conditions and consistency formulations give rise to distinct modal theories, and they provide explicit predicate constructions (via $h_0,g_0$ and $h_1,g_1$) to realize the corresponding arithmetical semantics. The work thus advances a unified, technically intricate account of provability logic in arithmetic with potential implications for understanding the limits and varieties of formal consistency statements.
Abstract
This paper studies the modal logical aspects of provability predicates and consistency statements for theories of arithmetic. First, we provide an overview of previous works on the correspondence between various derivability conditions for provability predicates and different modal logics. The main technical contribution of the present paper is to establish the arithmetical completeness of the logics $\mathsf{NP}$, $\mathsf{ND}$, $\mathsf{NP4}$, and $\mathsf{ND4}$ by extending Solovay's method and refining Arai's construction of Rosser provability predicates.