Abstract In this paper, we study the employment of $\Sigma _1$ -sentences with certificates, i.e., $\Sigma _1$ -sentences where a number of principles is added to ensure that the witness is sufficiently number-like. We develop certificates in some detail and illustrate their use by reproving some classical results and proving some new ones. An example of such a classical result is Vaught’s theorem of the strong effective inseparability of $\mathsf {R}_0$ . We also develop the new idea of a theory being $\mathsf {R}_{0\mathsf {p}}$ -sourced . Using this notion, we can transfer a number of salient results from $\mathsf {R}_0$ to a variety of other theories.

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.

Abstract We revisit Smullyan’s paper ‘Truth and Provability’ (2013) for three purposes. First, we introduce the notion of Smullyan models to give a precise definition for Smullyan’s framework discussed in that paper. Second, we clarify the relationship between three theorems proved by Smullyan and other newly introduced properties for Smullyan models in terms of both implications and non-implications. Third, we construct two Smullyan models based on arithmetical ideas and show the correspondence between the properties of these Smullyan models and those concerning truth and provability in arithmetic.

Abstract We prove that the provability logic of all provability predicates is exactly Fitting, Marek, and Truszczyński’s pure logic of necessitation $\textsf{N}$. Moreover, we introduce three extensions $\textsf{N4}$, $\textsf{NR}$ and $\textsf{NR4}$ of $\textsf{N}$ and investigate the arithmetical semantics of these logics. In fact, we prove that $\textsf{N4}$, $\textsf{NR}$ and $\textsf{NR4}$ are the provability logics of all provability predicates satisfying the third condition $\textbf{D3}$ of the derivability conditions, all Rosser provability predicates and all Rosser provability predicates satisfying $\textbf{D3}$, respectively.

Abstract We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $\mathsf {PA}$ and intuitionistic arithmetic $\mathsf {HA}$ . Using a generalized negative translation, we first provide a structured proof of the fact that $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over $\mathsf {HA} + {\Sigma _k}\text {-}\mathrm {LEM}$ where ${\Sigma _k}\text {-}\mathrm {LEM}$ is the axiom scheme of the law-of-excluded-middle restricted to formulas in $\Sigma _k$ . In addition, we show that this conservation theorem is optimal in the sense that for any semi-classical arithmetic T, if $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over T, then ${T}$ proves ${\Sigma _k}\text {-}\mathrm {LEM}$ . In the same manner, we also characterize conservation theorems for other well-studied classes of formulas by fragments of classical axioms or rules. This reveals the entire structure of conservation theorems with respect to the arithmetical hierarchy of classical principles.

Abstract Akama et al. [1] systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem [1, Theorem 2.7], then modify it in an appropriate way which still serves to largely justify the arithmetical hierarchy. In addition, we characterize a variety of prenex normal form theorems by logical principles in the arithmetical hierarchy. The characterization results reveal that our prenex normal form theorems are optimal. For the characterization results, we establish a new conservation theorem on semi-classical arithmetic. The theorem generalizes a well-known fact that classical arithmetic is $\Pi _2$ -conservative over intuitionistic arithmetic.

Abstract We introduce and develop a topological semantics of conservativity logics and interpretability logics. We prove the topological compactness theorem of consistent normal extensions of the conservativity logic $\textbf {CL}$ by extending Shehtman’s ultrabouquet construction method to our framework. As a consequence, we prove that several extensions of $\textbf {CL}$ such as $\textbf {IL}$, $\textbf {ILM}$, $\textbf {ILP}$ and $\textbf {ILW}$ are strongly complete with respect to our topological semantics.

Abstract We investigate relationships between versions of derivability conditions for provability predicates. We show several implications and non-implications between the conditions, and we discuss unprovability of consistency statements induced by derivability conditions. First, we classify already known versions of the second incompleteness theorem, and exhibit some new sets of conditions which are sufficient for unprovability of Hilbert–Bernays’ consistency statement. Secondly, we improve Buchholz’s schematic proof of provable $\Sigma_1$ -completeness. Then among other things, we show that Hilbert–Bernays’ conditions and Löb’s conditions are mutually incomparable. We also show that neither Hilbert–Bernays’ conditions nor Löb’s conditions accomplish Gödel’s original statement of the second incompleteness theorem.

Abstract Let T and U be any consistent theories of arithmetic. If T is computably enumerable, then the provability predicate $P{r_\tau }\left( x \right)$ of T is naturally obtained from each ${{\rm{\Sigma }}_1}$ definition $\tau \left( v \right)$ of T. The provability logic $P{L_\tau }\left( U \right)$ of τ relative to U is the set of all modal formulas which are provable in U under all arithmetical interpretations where □ is interpreted by $P{r_\tau }\left( x \right)$ . It was proved by Beklemishev based on the previous studies by Artemov, Visser, and Japaridze that every $P{L_\tau }\left( U \right)$ coincides with one of the logics $G{L_\alpha }$ , ${D_\beta }$ , ${S_\beta }$ , and $GL_\beta ^ -$ , where α and β are subsets of ω and β is cofinite. We prove that if U is a computably enumerable consistent extension of Peano Arithmetic and L is one of $G{L_\alpha }$ , ${D_\beta }$ , ${S_\beta }$ , and $GL_\beta ^ -$ , where α is computably enumerable and β is cofinite, then there exists a ${{\rm{\Sigma }}_1}$ definition $\tau \left( v \right)$ of some extension of $I{{\rm{\Sigma }}_1}$ such that $P{L_\tau }\left( U \right)$ is exactly L.

Abstract Gödel introduced the original provability predicate in the proofs of Gödel’s incompleteness theorems, and Rosser defined a new one. They are equivalent in the standard model ${\mathbb N}$ of arithmetic or any nonstandard model of ${\rm PA} + {\rm Con_{PA}} $ , but the behavior of Rosser’s provability predicate is different from the original one in nonstandard models of ${\rm PA} + \neg {\rm Con_{PA}} $ . In this paper, we investigate several properties of the derivability conditions for Rosser provability predicates, and prove the existence of a Rosser provability predicate with which we can define any consistent complete extension of ${\rm PA}$ in some nonstandard model of ${\rm PA} + \neg {\rm Con_{PA}} $ . We call it a universal Rosser predicate. It follows from the theorem that the true arithmetic ${\rm TA}$ can be defined as the set of theorems of ${\rm PA}$ in terms of a universal Rosser predicate in some nonstandard model of ${\rm PA} + \neg {\rm Con_{PA}} $ . By using this theorem, we also give a new proof of a theorem that there is a nonstandard model M of ${\rm PA} + \neg {\rm Con_{PA}} $ such that if N is an initial segment of M which is a model of ${\rm PA} + {\rm Con_{PA}} $ then every theorem of ${\rm PA}$ in N is a theorem of $\rm PA$ in ${\mathbb N}$ . In addition, we prove that there is a Rosser provability predicate such that the set of theorems of $\rm PA$ in terms of the Rosser provability predicate is inconsistent in any nonstandard model of ${\rm PA} + \neg {\rm Con_{PA}} $ .

Abstract By using a provability predicate of PA, we define ThmPA(M) as the set of theorems of PA in a modelMof PA. We say a modelMof PA is (1) illusory if ThmPA(M) ⊈ ThmPA(ℕ), (2) heterodox if ThmPA(M) ⊈ TA, (3) sane ifM⊨ ConPA, and insane if it is not sane, (4) maximally sane if it is sane and ThmPA(M) ⊆ ThmPA(N) implies ThmPA(M) = ThmPA(N) for every sane modelNof PA. We firstly show thatMis heterodox if and only if it is illusory, and that ThmPA(M) ∩ TA ≠ ThmPA(ℕ) for any illusory modelM. Then we show that there exists a maximally sane model, every maximally sane model satisfies ¬ConPA+ConPA, and there exists a sane model of ¬ConPA+ConPAwhich is not maximally sane. We define that an insane model is (5) illusory by nature if its every initial segment being a nonstandard model of PA is illusory, and (6) going insane suddenly if its every initial segment being a sane model of PA is not illusory. We show that there exists a model of PA which is illusory by nature, and we prove the existence of a model of PA which is going insane suddenly.