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. (shrink)

By a well-known result of Kotlarski et al., first-order Peano arithmetic \ can be conservatively extended to the theory \ of a truth predicate satisfying compositional axioms, i.e., axioms stating that the truth predicate is correct on atomic formulae and commutes with all the propositional connectives and quantifiers. This result motivates the general question of determining natural axioms concerning the truth predicate that can be added to \ while maintaining conservativity over \. Our main result shows that conservativity fails even (...) for the extension of \ obtained by the seemingly weak axiom of disjunctive correctness \ that asserts that the truth predicate commutes with disjunctions of arbitrary finite size. In particular, \ implies \\). Our main result states that the theory \ coincides with the theory \ obtained by adding \-induction in the language with the truth predicate. This result strengthens earlier work by Kotlarski and Cieśliński. For our proof we develop a new general form of Visser’s theorem on non-existence of infinite descending chains of truth definitions and prove it by reduction to Gödel’s second incompleteness theorem, rather than by using the Visser–Yablo paradox, as in Visser’s original proof. (shrink)

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. (shrink)

Let Con↾x denote the finite consistency statement “there are no proofs of contradiction in T with ≤x symbols.” For a large class of natural theories T, Pudlák has shown that the lengths of the shortest proofs of Con↾n in the theory T itself are bounded by a polynomial in n. At the same time he conjectures that T does not have polynomial proofs of the finite consistency statements Con)↾n. In contrast, we show that Peano arithmetic has polynomial proofs of Con)↾n, (...) where Con∗ is the slow consistency statement for Peano arithmetic, introduced by S.-D. Friedman, Rathjen, and Weiermann. We also obtain a new proof of the result that the usual consistency statement Con is equivalent to ε0 iterations of slow consistency. Our argument is proof-theoretic, whereas previous investigations of slow consistency relied on nonstandard models of arithmetic. (shrink)

We consider the well-known provability logic GLP. We prove that the GLP-provability problem for polymodal formulas without variables is PSPACE-complete. For a number n, let L0n\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${L^{n}_0}$$\end{document} denote the class of all polymodal variable-free formulas without modalities ⟨n⟩,⟨n+1⟩,...\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\langle n \rangle,\langle n+1\rangle,...}$$\end{document}. We show that, for every number n, the GLP-provability problem for formulas from L0n\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${L^{n}_0}$$\end{document} (...) is in PTIME. (shrink)

We fix a gap in a proof in our paper Reducing ω-model reflection to iterated syntactic reflection.

Journal of Mathematical Logic, Volume 23, Issue 02, August 2023. In mathematical logic there are two seemingly distinct kinds of principles called “reflection principles.” Semantic reflection principles assert that if a formula holds in the whole universe, then it holds in a set-sized model. Syntactic reflection principles assert that every provable sentence from some complexity class is true. In this paper, we study connections between these two kinds of reflection principles in the setting of second-order arithmetic. We prove that, for (...) a large swathe of theories, [math]-model reflection is equivalent to the claim that arbitrary iterations of uniform [math] reflection along countable well-orderings are [math]-sound. This result yields uniform ordinal analyzes of theories with strength between [math] and [math]. The main technical novelty of our analysis is the introduction of the notion of the proof-theoretic dilator of a theory [math], which is the operator on countable ordinals that maps the order-type of [math] to the proof-theoretic ordinal of [math]. We obtain precise results about the growth of proof-theoretic dilators as a function of provable [math]-model reflection. This approach enables us to simultaneously obtain not only [math], [math] and [math] ordinals but also reverse-mathematical theorems for well-ordering principles. (shrink)