Arithmetical completeness for some extensions of the pure logic of necessitation
Haruka Kogure
TL;DR
This work proves arithmetical completeness for the family NA_{m,n}, extensions of the pure logic of necessitation by the axiom Box^n A -> Box^m A, by exhibiting Σ_1 provability predicates Pr_T(x) for which NA_{m,n} matches the provability logic PL(Pr_T) under various regimes. The core method constructs PA-provably recursive encodings and finite (m,n)-accessible N-models to bridge modal principles with arithmetical provability, with distinct treatments depending on whether T is Σ_1-sound or Σ_1-ill and on the relative sizes of m and n. Key results include existence theorems for every m,n≥1 with m≠n and edge-case analyses for n=0 or m=0, plus discussion of the relationship to second incompleteness via D3^n_m and related conditions. The findings illuminate which extensions of N admit arithmetical completeness and how the finite-frame perspective can be leveraged to obtain decidability and completeness results, offering guidance for further explorations of provability logics beyond GL.
Abstract
We investigate the arithmetical completeness theorems of some extensions of Fitting, Marek, and Truszczyński's pure logic of necessitation $\mathbf{N}$. For $m,n \in ω$, let $\mathbf{NA}_{m,n}$, which was introduced by Kurahashi and Sato, be the logic obtained from $\mathbf{N}$ by adding the axiom scheme $\Box^n A \to \Box^m A$. In this paper, among other things, we prove that for each $m,n \geq 1$, the logic $\mathbf{NA}_{m,n}$ becomes a provability logic, that is, there exists a provability predicate $\mathrm{Pr}_T(x)$ of $T$ whose $T$-verifiable modal principles are exactly the logic $\mathbf{NA}_{m,n}$.