Abstract We show that there is no theory that is minimal with respect to interpretability among recursively enumerable essentially undecidable theories.

Abstract Japaridze’s provability logic ${\operatorname {GLP}}$ has one modality $[n]$ for each natural number and has been used by Beklemishev for a proof theoretic analysis of Peano arithmetic (${\operatorname {PA}}$) and related theories. Among other benefits, this analysis yields the so-called Every Worm Dies (${\operatorname {EWD}}$) principle, a natural combinatorial statement independent of ${\operatorname {PA}}$. Recently, Beklemishev and Pakhomov have studied notions of provability corresponding to transfinite modalities in ${\operatorname {GLP}}$. We show that indeed the natural transfinite extension of ${\operatorname {GLP}}$ is sound for this interpretation and yields independent combinatorial principles for the second-order theory ${\operatorname {ACA}}$ of arithmetical comprehension with full induction. We also provide restricted versions of ${\operatorname {EWD}}$ related to the fragments ${\operatorname {I\varSigma }}_n$ of PA. In order to prove the latter, we show that standard Hardy functions majorize their variants based on tree ordinals.

Abstract It is well-known that natural axiomatic theories are well-ordered by consistency strength. However, it is possible to construct descending chains of artificial theories with respect to consistency strength. We provide an explanation of this well-orderedness phenomenon by studying a coarsening of the consistency strength order, namely, the $\Pi ^1_1$ reflection strength order. We prove that there are no descending sequences of $\Pi ^1_1$ sound extensions of $\mathsf {ACA}_0$ in this ordering. Accordingly, we can attach a rank in this order, which we call reflection rank, to any $\Pi ^1_1$ sound extension of $\mathsf {ACA}_0$ . We prove that for any $\Pi ^1_1$ sound theoryTextending $\mathsf {ACA}_0^+$ , the reflection rank ofTequals the $\Pi ^1_1$ proof-theoretic ordinal ofT. We also prove that the $\Pi ^1_1$ proof-theoretic ordinal of $\alpha $ iterated $\Pi ^1_1$ reflection is $\varepsilon _\alpha $ . Finally, we use our results to provide straightforward well-foundedness proofs of ordinal notation systems based on reflection principles.

Abstract Presburger arithmetic is the true theory of natural numbers with addition. We study interpretations of Presburger arithmetic in itself. The main result of this paper is that all self-interpretations are definably isomorphic to the trivial one. Here we consider interpretations that might be multi-dimensional. We note that this resolves a conjecture by Visser (1998, An overview of interpretability logic. Advances in Modal Logic, pp. 307–359). In order to prove the result, we show that all linear orderings that are interpretable in $({\mathbb{N}},+)$ are scattered orderings with the finite Hausdorff rank and that the ranks are bounded in the terms of the dimensions of the respective interpretations.

Abstract In this paper, we study finitely axiomatizable conservative extensions of a theoryUin the case whereUis recursively enumerable and not finitely axiomatizable. Stanisław Krajewski posed the question whether there are minimal conservative extensions of this sort. We answer this question negatively. Consider a finite expansion of the signature ofUthat contains at least one predicate symbol of arity ≥ 2. We show that, for any finite extensionαofUin the expanded language that is conservative overU, there is a conservative extensionβofUin the expanded language, such that $\alpha \vdash \beta$ and $\beta \not \vdash \alpha$ . The result is preserved when we consider eitherextensionsormodel-conservative extensionsofUinstead ofconservative extensions. Moreover, the result is preserved when we replace $\dashv$ as ordering on the finitely axiomatized extensions in the expanded language by a relevant kind of interpretability, to witinterpretability that identically translates the symbols of the U-language. We show that the result fails when we consider an expansion with only unary predicate symbols for conservative extensions ofUordered by interpretability that preserves the symbols ofU.