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.

Abstract For a class $\varGamma $ of formulas, $\varGamma $ local reflection principle $\textrm{Rfn}_{\varGamma }(T)$ for a theory $T$ of arithmetic is a scheme formalizing the $\varGamma $-soundness of $T$. Beklemishev (1997, Theoria, 63, 139–146) proved that for every $\varGamma \in \{\varSigma _{n}, \varPi _{n+1} \mid n \geq 1\}$, the full local reflection principle $\textrm{Rfn}(T)$ is $\varGamma $-conservative over $T + \textrm{Rfn}_{\varGamma }(T)$. We firstly generalize the conservation theorem to nonstandard provability predicates: we prove that the second condition $\textbf{D2}$ of the derivability conditions is a sufficient condition for the conservation theorem to hold. We secondly investigate the conservation theorem in terms of Rosser provability predicates. We construct Rosser predicates for which the conservation theorem holds and Rosser predicates for which the theorem does not hold.