ON SHAVRUKOV’S NON-ISOMORPHISM THEOREM FOR DIAGONALIZABLE ALGEBRAS

Abstract

We prove a strengthened version of Shavrukov’s result on the non-isomorphism of diagonalizable algebras of two $\Sigma _1$-sound theories, based on the improvements previously found by Adamsson. We then obtain several corollaries to the strengthened result by applying it to various pairs of theories and obtain new non-isomorphism examples. In particular, we show that there are no surjective homomorphisms from the algebra $(\mathfrak {L}_T, \Box _T\Box _T)$ onto the algebra $(\mathfrak {L}_T, \Box _T)$. The case of bimodal diagonalizable algebras is also considered. We give several examples of pairs of theories with isomorphic diagonalizable algebras but non-isomorphic bimodal diagonalizable algebras.

1 Introduction

The equational class of diagonalizable algebras (also known as Magari algebras) was introduced by Magari [14] to study the notion of provability in a formal theory within a general algebraic setting. A diagonalizable algebra is a Boolean algebra $(\mathcal {B}, \Box )$ together with a unary operator $\Box $ satisfying the following identities:

$$ \begin{align*} \Box(a \to b) \to (\Box a \to \Box b) = \top, \quad \Box(\Box a \to a) \to \Box a = \top, \quad \Box\top = \top. \end{align*} $$

Given a formal theory T over classical logic (containing enough arithmetic to reason about its own syntax and, in particular, provability) one can associate with it a specific diagonalizable algebra $\mathfrak {D}_T$ called the diagonalizable algebra of T (the term “provability algebra” is also widely used for such algebras, but we stick with the former following Shavrukov). The construction is as follows. Let $\mathfrak {L}_T$ be the Lindenbaum Boolean algebra of T. The universe of $\mathfrak {L}_T$ is the set of all equivalence classes $[\varphi ]_{\sim _T}$ of T-sentences, where the equivalence relation $\varphi \sim _T \psi $ is a T-provable equivalence, i.e., $\varphi \sim _T \psi $ if and only if $T \vdash \varphi \leftrightarrow \psi $ . The Boolean operations on the equivalence classes are induced by propositional connectives. The algebra $\mathfrak {D}_T$ is then defined as $(\mathfrak {L}_T, \Box _T)$ , where $\Box _T$ is the unary operator induced by the provability predicate $\mathsf {Pr}_T(x)$ of T, a formula in the language of T which expresses the fact that a formula with Gödel number x is provable in T, as follows $\Box _T[\varphi ]_{\sim _T} = [\mathsf {Pr}_T(\ulcorner \varphi \urcorner )]_{\sim _T}$ . The formula $\mathsf {Pr}_T(x)$ should express provability in T in such a way that $\mathfrak {D}_T$ would indeed satisfy the identities above. This is true, e.g., in case when $\mathsf {Pr}_T(x)$ is the standard provability predicate for T, i.e., has the form $\exists p\, \mathsf {Prf}_T(p, x)$ , where $\mathsf {Prf}_T(p, x)$ is the standard proof predicate for (a fixed axiomatization of) T, expressing in a natural way that p codes a Hilbert-style proof of a formula with Gödel number x from the axioms of T. Note that the identities above then correspond to provable closure of the set of theorems of T under modus ponens, formalized Löb’s theorem (asserting that it is provable in T that if $T \vdash \Box _T\varphi \to \varphi $ , then $T \vdash \varphi $ ) and the fact that T can prove the provability of its theorems.

One may also consider the operators induced by non-standard provability predicates as long as the obtained algebra $\mathfrak {D}_T$ satisfies the identities defining diagonalizable algebras. The above discussion implies that the notation $\mathfrak {D}_T$ is ambiguous, since $\mathfrak {D}_T$ depends on the choice of a formula $\mathsf {Pr}_T(x)$ , which itself may depend on a particular axiomatization of T. Nevertheless, we use this notation always assuming that the axiomatization and a formula $\mathsf {Pr}_T(x)$ for a theory T in question are fixed.

The formal study of provability as an operator (or a modality) is traditionally conducted within the field known as provability logic. The diagonalizable algebras of formal theories provide a different way of looking at this field. One of the central results in this area is the famous Solovay arithmetical completeness theorem [25], which can be reformulated in the algebraic setting as follows: for each $\Sigma _1$ -sound theory T the equational theory (or rather the logic) of $\mathfrak {D}_T$ coincides with the propositional modal logic $\mathsf {GL}$ , called the Gödel–Löb logic. The uniform version of this theorem is translated into the existence of an embedding of the countably generated free diagonalizable algebra into $\mathfrak {D}_T$ .

Several of the most prominent results on diagonalizable algebras of formal theories were obtained by Shavrukov (see [20–23]). Among them is the nonarithmeticity of the full first-order theory $\mathsf {Th}(\mathfrak {D}_T)$ of the diagonalizable algebra of a $\Sigma _1$ -sound theory T (and the first-order theory of any collection of diagonalizable algebras of such theories) and the undecidability of its $\forall ^* \exists ^* \forall ^* \exists ^*$ -fragment, a complete description of r.e. subalgebras of $\mathfrak {D}_T$ (later D. Zambella extended this result to arbitrary subalgebras), the existence of non-trivial automorphisms of $\mathfrak {D}_T$ . Shavrukov has also obtained a couple of important results on isomorphisms between the diagonalizable algebras of formal theories (see [20, 22]). It is these results, which are formulated below, that we focus on in the present work. For the precise definitions of the notions and notation used in the statements see the next section.

The first result is a general sufficient condition for the diagonalizable algebras of two $\Sigma _1$ -sound theories to be not elementarily equivalent, whence also not isomorphic (see [20] and [23, theorem 2.11]). In particular, it implies that $\mathfrak {D}_{\mathsf {PA}}$ and $\mathfrak {D}_{\mathsf {ZF}}$ are not isomorphic.

Theorem 1.1. If a theory T proves the following version of the uniform $\Sigma _1$ -reflection principle for a theory S

$$ \begin{align*} \forall x\, \exists y\, \forall \delta(\cdot) \in \Delta_0 \left( \exists p \leqslant x\, \mathsf{Prf}_S(p, \ulcorner \exists z\, \delta(z) \urcorner) \to \exists u \leqslant y\, \mathsf{Tr}_{\Delta_0}(\ulcorner \delta(\underline{u}) \urcorner) \right){\kern-1.5pt}, \end{align*} $$

then $\mathfrak {D}_T \not \cong \mathfrak {D}_S$ . Moreover, in this case $\mathfrak {D}_T$ and $\mathfrak {D}_S$ are not elementarily equivalent.

This may be contrasted with a theorem of Pour-El and Kripke [18] stating that the Lindenbaum algebras $\mathfrak {L}_T$ and $\mathfrak {L}_S$ are recursively isomorphic (for all reasonable theories T and S). It is also worth mentioning that the first-order sentence separating the elementary theories of algebras $\mathfrak {D}_T$ and $\mathfrak {D}_S$ is quite complicated (see Corollary 4.27).

The second important result of Shavrukov is a sufficient condition for the existence of a recursive isomorphism between $\mathfrak {D}_T$ and $\mathfrak {D}_S$ , from which it follows that, e.g., $\mathfrak {D}_{\mathsf {ZF}} \cong \mathfrak {D}_{\mathsf {GB}}$ (see [22]). Here we formulate it in a slightly weakened form, which is sufficient for all applications. Given a class of arithmetical formulas $\Gamma $ , two theories T and S are called $\Gamma $ -coherent if

1. (i) $T \vdash \gamma \Longleftrightarrow S \vdash \gamma $ for each sentence $\gamma \in \Gamma $ ,

2. (ii) both T and S prove the following “uniform” formalization of point $({\rm i})$ ,

   $$ \begin{align*} \forall x\, \exists y\, \forall \gamma \in \Gamma &\Bigl( \left(\exists p \leqslant x\, \mathsf{Prf}_T(p, \ulcorner \gamma \urcorner) \to \exists q \leqslant y\, \mathsf{Prf}_S(q, \ulcorner \gamma \urcorner) \right) \land \Bigr.\\ & \quad \Bigl. \left(\exists p \leqslant x\, \mathsf{Prf}_S(p, \ulcorner \gamma \urcorner) \to \exists q \leqslant y\, \mathsf{Prf}_T(q, \ulcorner \gamma \urcorner) \right) \Bigr). \end{align*} $$

Denote by $\mathcal {B}(\Sigma _1)$ the set of all Boolean combinations of $\Sigma _1$ -sentences.

Theorem 1.2. If T and S are $\mathcal {B}(\Sigma _1)$ -coherent theories, then $\mathfrak {D}_T \cong \mathfrak {D}_S$ .

Later Adamsson obtained the following theorem [1, theorem 17], which improved Shavrukov’s non-isomorphism condition in two ways. By an epimorphism between diagonalizable algebras we mean a surjective homomorphism, i.e., an onto mapping which preserves all Boolean operations and an additional unary operator $\Box $ . Here $\mathscr {P}_T(x)$ is the Parikh speed-up function for T (see [1, definition 5]) defined as follows: the value $\mathscr {P}_T(n)$ is the least upper bound on the length (number of symbols) of T-proofs of all formulas $\psi $ such that $\Box _T\psi $ has a T-proof with at most n symbols.

Theorem 1.3. If there is an epimorphism from $\mathfrak {D}_T$ onto $\mathfrak {D}_S$ , then there is an elementary function $t(x)$ such that the inequality $\mathscr {P}_T(n) \leqslant t(\mathscr {P}_S(\mathscr {P}_S(\mathscr {P}_S(\mathscr {P}_S(n)))))$ holds for infinitely many n.

Firstly, he weakened the condition itself, which allowed to obtain new non-isomorphism results proving that the isomorphism class of $\mathfrak {D}_T$ actually depends on the choice of the formula $\mathsf {Pr}_T(x)$ . In particular, he showed [1, corollary 21] that $(\mathfrak {L}_T, \Box _T) \not \cong (\mathfrak {L}_T, \Box ^{(6)}_T)$ , where $\Box ^{(6)}_T$ is, of course, $\Box _T$ iterated six times. Secondly, he showed that this weakened condition is sufficient to obtain the non-existence of epimorphisms from $\mathfrak {D}_T$ onto $\mathfrak {D}_S$ , rather than just $\mathfrak {D}_T \not \cong \mathfrak {D}_S$ . In his work Adamsson notes that the obtained condition is “by no means optimal” and “sharper bounds are certainly possible.”

Our work is a natural continuation of this line of research. The main theorem we prove (Theorem 4.24) provides a more general version of Adamsson’s condition, demonstrating that sharper bounds are indeed possible. To do so we first discuss several properties of the reflection function $\mathscr {R}_T(x)$ for T (which is closely related to $\mathscr {P}_T(x)$ present in Adamsson’s condition), which are then used to obtain the desired improvements in the main theorem, and introduce the classes of functions $\mathcal {F}^k_{T}(U)$ , which can be seen as the generalizations of the class of provably total computable functions $\mathcal {F}(T)$ , and are implicitly present in Adamsson’s approach. Using the improved non-isomorphism condition we derive that $(\mathfrak {L}_T, \Box _T) \not \cong (\mathfrak {L}_T, \Box _T\Box _T)$ , a result anticipated in [1], and obtain a more general non-isomorphism of this kind. More importantly, we consider several more natural examples of theories with non-isomorphic algebras but the same classes of provably total computable functions, among them two $\Pi _1$ -coherent theories. Finally, we consider the bimodal diagonalizable algebras, where the second modality is interpreted as an operator of 1-provability, i.e., provability in a theory together with all true $\Pi _1$ -sentences added as additional axioms. We naturally focus on pairs of theories with isomorphic diagonalizable algebras, but non-isomorphic bimodal algebras. We start with examples, where non-isomorphism can be established more algebraically (as opposed to Shavrukov’s approach), and also obtain a family of similar examples by applying our improved version of the Shavrukov–Adamsson theorem.

The paper is organized as follows. Section 2 introduces the basic notions and notation used throughout the paper. In Section 3 we define the classes $\mathcal {F}^k_{T}(U)$ , study their properties and prove certain important facts about the reflection function $\mathscr {R}_T(x)$ . Sections 4 and 5 contain the main results of the paper, namely, the theorem on the non-isomorphism of diagonalizable algebras and its various applications to natural pairs of theories. In Section 6 we discuss certain non-isomorphism results on bimodal diagonalizable algebras.

2 Preliminaries

In this paper we consider first-order theories over classical predicate logic that contain some basic arithmetical theory. We always assume that if a theory in question is not formulated in the language of arithmetic, then some standard translation of arithmetical language into the language of the theory is fixed, and we identify arithmetical formulas with their translations. As our basic arithmetical theory we take Elementary arithmetic $\mathsf {EA}$ , also known as $\mathsf {I}\Delta _0(\exp )$ , that is, the first-order theory formulated in the pure arithmetical language $0, (\cdot )', +, \times $ enriched with the unary function symbol $\exp $ for the exponentiation function $2^x$ . It has the standard defining axioms for these symbols and the induction schema for all elementary formulas (or $\Delta _0(\exp )$ -formulas), i.e., formulas in the language with exponent containing only bounded (by the terms in the language with exponent) quantifiers. Along with it we also consider a smaller class of $\Delta _0$ -formulas, which are the formulas in pure arithmetical language (without exponent) containing only bounded quantifiers. We define the classes $\Sigma _0$ and $\Pi _0$ to be $\Delta _0$ . The classes $\Sigma _n$ and $\Pi _n$ of the arithmetical hierarchy are then defined recursively in a standard way for all $n> 0$ (see, e.g., [10]). We also consider the classes of Boolean combinations of $\Sigma _n$ -formulas which are denoted by $\mathcal {B}(\Sigma _n)$ .

Since our base theory $\mathsf {EA}$ is formulated in the language with $\exp $ , it makes sense to define the arithmetical hierarchy starting from $\Delta _0(\exp )$ -formulas rather than $\Delta _0$ -formulas. For example, $\Sigma _1(\exp )$ -formulas are of the form $\exists x_1 \dots \exists x_n\, \delta (x_1, \dots , x_n)$ , where $\delta (x_1, \dots , x_n)$ is a $\Delta _0(\exp )$ -formula (possibly containing other free variables). These classes, of course, strictly contain their counterparts in the language without $\exp $ ; however, they are equivalent in the following strong sense (we explain this equivalence here for the most important case of the classes $\Sigma _1(\exp )$ and $\Sigma _1$ ). The result is essentially folklore, so we only sketch the proof.

Remark 2.4. For each $\Sigma _1(\exp )$ -formula $\varphi (x_1, \dots , x_n)$ there exists a $\Sigma _1$ -formula $\psi (x_1, \dots , x_n)$ such that

$$ \begin{align*} \mathsf{EA} \vdash \forall x_1 \dots \forall x_n \left( \varphi(x_1, \dots, x_n) \leftrightarrow \psi(x_1, \dots, x_n)\right){\kern-1.5pt}. \end{align*} $$

Proof (sketch)

Clearly, it is sufficient to prove the claim for $\Delta _0(\exp )$ -formulas. In the proof of [10, lemma 1.30], which is essentially due to [9] (see also [4, lemma 5.13]) it is shown that for each $\Delta _0(\exp )$ -formula $\delta (x)$ (for simplicity we consider a formula with a single free variable) there is a $\Delta _0$ -formula $\gamma (x, y)$ and a term $t(x)$ (in the language with $\exp $ ) such that

$$ \begin{align*} \mathsf{EA} \vdash \forall x\, \forall y \left[y \geqslant t(x) \to \left(\delta(x) \leftrightarrow \gamma(x, y)\right) \right]. \end{align*} $$

It follows that over $\mathsf {EA}$ the formula $\delta (x)$ is equivalent to $\exists y\, (y \geqslant t(x) \land \gamma (x, y))$ , which is itself equivalent to a $\Sigma _1$ -formula, because the formula $y \geqslant t(x)$ is equivalent to $\exists z \leqslant y \left (t(x) = z\right )$ and each formula of the form $t(x) = z$ is equivalent to a $\Delta _0$ -formula (the proof goes by induction on the complexity of $t(x)$ , where the base case relies on the $\Delta _0$ -definition of $\exp $ ; see [10, definition 3.12]).

In view of this remark, we do not distinguish between the classes of arithmetical hierarchy for the language with and without $\exp $ further in the paper. Let us also mention that the proof of Remark 2.4 can itself be formalized in $\mathsf {EA}$ . This is based on the fact that the proof goes by induction on the complexity of a formula $\delta (x)$ , which is available in $\mathsf {EA}$ , since there is an elementary bound on the size of the required proof.

The theory $\mathsf {EA}^+$ is defined to be an extension of $\mathsf {EA}$ with the axiom asserting the totality of the superexponential function $2^x_y$ (which can be naturally expressed by a $\Pi _2$ -formula in the language of $\mathsf {EA}$ ). If we allow induction for all arithmetical formulas, the resulting theory is Peano arithmetic denoted by $\mathsf {PA}$ . For a fixed class of arithmetical formulas $\Gamma $ the fragment of $\mathsf {PA}$ obtained by restricting the induction schema

$$ \begin{align*} \forall y (\varphi(0, y) \land \forall x (\varphi(x, y) \to \varphi(x + 1, y)) \to \forall x\, \varphi(x, y)), \quad \varphi(x, y) \in \Gamma \end{align*} $$

to $\Gamma $ -formulas is denoted by $\mathsf {I}\Gamma $ . We also consider the following schema of $\Sigma _1$ -collection, denoted by $\mathsf {B}\Sigma _1$ ,

$$ \begin{align*} \forall x < z\, \exists y\, \varphi(x, y, a) \to \exists u\, \forall x < z\, \exists y < u\, \varphi(x, y, a), \quad \varphi(x, y, a) \in \Sigma_1. \end{align*} $$

We assume that some standard arithmetization of syntax and the Gödel numbering of syntactic objects is fixed. In particular, we write $\ulcorner \varphi \urcorner $ for the Gödel number of $\varphi $ . All the theories appearing throughout the paper are assumed to be recursively axiomatizable $\Sigma _1$ -sound extensions of $\mathsf {EA}$ . Recall that $\Sigma _1$ -soundness means that each provable $\Sigma _1$ -sentence is true in the standard model $\mathbb {N}$ . Moreover, (unless explicitly stated otherwise) we also assume that each theory T is given to us by its elementary axiomatization, i.e., an elementary formula $\sigma _T(x)$ , defining the set of axioms of T in the standard model. This formula $\sigma _T$ is used in the construction of the standard proof predicate $\mathsf {Prf}_{\sigma _T}(p, x)$ for T, an elementary formula expressing the relation “p codes a Hilbert-style proof of the formula with Gödel number x from the axiom set defined by the formula $\sigma _T$ .” The standard provability predicate for T (w.r.t. a fixed elementary axiomatization $\sigma _T$ ) is then given by $\exists p\, \mathsf {Prf}_{\sigma _T}(p, x)$ , and we denote this formula by $\Box _{\sigma _T}(x)$ . In practice, almost everywhere we use the following less detailed notation $\mathsf {Prf}_T(p, x)$ and $\Box _T(x)$ to denote $\mathsf {Prf}_{\sigma _T}(p, x)$ and $\Box _{\sigma _T}(x)$ for some fixed axiomatization $\sigma _T$ of a theory T under consideration, which does not lead to confusion if we consider a single axiomatization. But if we are dealing with several axiomatizations of the same theory we revert back to the official notation to make the difference between the proof and provability predicates for different axiomatizations explicit.

Recall that the closed arithmetical term $0^{' \dots '}$ with n primes, which is denoted by $\underline {n}$ , is called the nth numeral. As usual, we often write $\varphi $ or $\ulcorner \varphi \urcorner $ instead of $\underline {\ulcorner \varphi \urcorner }$ , so $\Box _T \varphi $ is a shorthand for $\Box _T(\underline {\ulcorner \varphi \urcorner })$ . We also quantify over (the Gödel numbers of) formulas, their sequences and other syntactic objects freely. The notation $T \vdash _p \varphi $ stands for $\exists q \leqslant p\, \mathsf {Prf}_T(q, \ulcorner \varphi \urcorner )$ . The finite iterations of $\Box _T$ are denoted by $\Box ^{(k)}_T$ .

The standard provability predicate $\Box _T$ satisfies the following Löb’s derivability conditions (see, e.g., [24] or [7]):

1. 1. If $T \vdash \varphi $ , then $\mathsf {EA} \vdash \Box _T\varphi $ .

2. 2. $\mathsf {EA} \vdash \Box _T(\varphi \to \psi ) \to (\Box _T\varphi \to \Box _T\psi )$ .

3. 3. $\mathsf {EA} \vdash \Box _T\varphi \to \Box _T\Box _T\varphi $ .

Moreover these conditions hold provably in $\mathsf {EA}$ with $\varphi $ and $\psi $ being universally quantified over. Point 3 follows from the general fact known as provable $\Sigma _1$ -completeness:

$$ \begin{align*} \mathsf{EA} \vdash \forall x_1\, \dots \forall x_m (\sigma(x_1, \dots, x_m) \to \Box_T\ulcorner \sigma(\underline{x}_1, \dots, \underline{x}_m) \urcorner){\kern-1.5pt}, \end{align*} $$

whenever $\sigma (x_1, \dots , x_m)$ is a $\Sigma _1$ -formula. Here the underline notation $\ulcorner \varphi (\underline {x}) \urcorner $ stands for the elementarily definable term, representing the elementary function that maps k to the Gödel number $\ulcorner \varphi (\underline {k}) \urcorner $ of the formula $\varphi (\underline {k})$ , where $\underline {k}$ is the kth numeral. In what follows we usually write just $\Box _T \varphi (\underline {x})$ instead of $\Box _T \ulcorner \varphi (\underline {x}) \urcorner $ .

We say that two theories T and S are $\Gamma $ -equivalent if $T \vdash \gamma $ if and only if $S \vdash \gamma $ for each sentence $\gamma \in \Gamma $ . In case $\Gamma $ is the class of all arithmetical sentences we say that T and S are deductively equivalent and use the notation $T \equiv S$ .

Among the extensions of a given theory T we consider the reflection principles. The local $\Gamma $ -reflection principle $\mathsf {Rfn}_{\Gamma }(T)$ is the schema $\Box _T \gamma \to \gamma $ , for each sentence $\gamma \in \Gamma $ . Similarly, the uniform $\Gamma $ -reflection principle $\mathsf {RFN}_{\Gamma }(T)$ is the schema $\forall x \left (\Box _T \gamma (\underline {x}) \to \gamma (x) \right )$ , for each formula $\gamma \in \Gamma $ . Usually $\Gamma $ is one of the classes $\Sigma _n$ or $\Pi _n$ for $n> 0$ . If $\Gamma $ is the set of all arithmetical formulas we write $\mathsf {Rfn}(T)$ and $\mathsf {RFN}(T)$ . Let us also mention the following useful principle known as the small reflection (see [10, lemma 4.40] and [7, lemma 2.2]); for each formula $\delta (x)$ we have

$$ \begin{align*} \mathsf{EA} \vdash \forall x\, \forall y\, \Box_T \left(\mathsf{Prf}_T(\underline{y}, \ulcorner \delta(\underline{x}) \urcorner) \to \delta(\underline{x})\right){\kern-1.5pt}. \end{align*} $$

Indeed, denote the formula $\mathsf {Prf}_T(y, \ulcorner \delta (\underline {x}) \urcorner ) \to \delta (x)$ by $\psi (x, y)$ and argue in $\mathsf {EA}$ by considering two cases. If $\mathsf {Prf}_T(y, \ulcorner \delta (\underline {x}) \urcorner )$ , then $\Box _T \delta (\underline {x})$ , whence $\Box _T\psi (\underline {x}, \underline {y})$ follows. Otherwise, we have $\neg \mathsf {Prf}_T(y, \ulcorner \delta (\underline {x}) \urcorner )$ which (by provable $\Sigma _1$ -completeness) implies $\Box _T \neg \mathsf {Prf}_T(\underline {y}, \ulcorner \delta (\underline {x}) \urcorner )$ and so $\Box _T\psi (\underline {x}, \underline {y})$ , as required.

It is known that (see [10]) for each $n> 0$ there exists a $\Pi _n$ -formula $\mathsf {Tr}_{\Pi _n}(x)$ , the truth definition for the class of $\Pi _n$ -formulas (and similarly for $\Sigma _n$ -formulas), such that

$$ \begin{align*} \mathsf{EA} \vdash \forall x_1\,\dots \forall x_m\:(\varphi(x_1, \dots, x_m) \leftrightarrow \mathsf{Tr}_{\Pi_n}(\ulcorner \varphi(\underline{x}_1, \dots, \underline{x}_m) \urcorner)), \end{align*} $$

for every $\Pi _n$ -formula $\varphi (x_1, \dots , x_m)$ , and this fact itself is formalizable in $\mathsf {EA}$ , so

$$ \begin{align*} \mathsf{EA} \vdash \forall \pi \in \Pi_n\, \Box_T \left(\pi \leftrightarrow \mathsf{Tr}_{\Pi_n}(\pi)\right){\kern-1.5pt}. \end{align*} $$

The same also holds for $n = 0$ , but note that the truth predicate for $\Delta _0$ -formulas $\mathsf {Tr}_{\Delta _0}(x)$ used in the construction of the above truth predicates is defined by a $\Delta _0(\exp )$ -formula, rather than a $\Delta _0$ -formula. The truth predicates are used to define the so-called strong provability predicates. In this paper we only consider the predicate of $1$ -provability, i.e., usual provability in T together with all true $\Pi _1$ -sentences taken as additional axioms. Namely, we define the predicate of $1$ -provability in T by the following formula:

$$ \begin{align*} [1]_T \varphi \leftrightharpoons \exists \pi \left(\mathsf{Tr}_{\Pi_1}(\pi) \wedge \Box_T(\pi \to \varphi)\right){\kern-1.5pt}. \end{align*} $$

The predicate $[1]_T$ satisfies the same derivability conditions as $\Box _T$ and is provably $\Sigma _{2}$ -complete. It is not hard to see that $\mathsf {RFN}_{\Sigma _1}(T)$ is equivalent to $\neg [1]_T \bot $ provably in $\mathsf {EA}$ .

A function $f \colon \mathbb {N}^k \to \mathbb {N}$ is called a provably total computable function of T if there is a $\Sigma _1$ -formula $\psi (x_1, \dots , x_k, y)$ defining the graph of f in the standard model and

$$ \begin{align*} T \vdash \forall x_1\, \dots \forall x_k\, \exists y\, \psi(x_1, \dots, x_k, y). \end{align*} $$

Note that in this definition we do not require y to be T-provably unique, although it is well-known that this additional requirement leads to the same notion (cf. Lemma 3.9). The class of provably total computable functions of T is denoted by $\mathcal {F}(T)$ . It is known that $\mathcal {F}(\mathsf {EA}) = \mathcal {E}_3$ , the class of Kalmar elementary functions (see, e.g., [7]). Since we deal only with extensions of $\mathsf {EA}$ , the class $\mathcal {F}(T)$ always contains all elementary functions.

When comparing the growth rate of functions in this paper, we do it up to an elementary transformation of the input, and use the following notation for (partial) functions $f, g \colon \mathbb {N} \to \mathbb {N}$ and $X \subseteq \mathbb {N}$ . We write $f \leqslant _X g$ , if $X \subseteq \mathrm {dom}\, f \cap \mathrm {dom}\, g$ and for each $n \in X$ we have $f(n) \leqslant g(n)$ , and $f \preccurlyeq _X g$ , if there is an elementary function $q(x)$ such that $f \leqslant _X q \circ g$ . We also write $f \approx _X g$ , when both $f \preccurlyeq _X g$ and $g \preccurlyeq _X f$ hold. The notation $f =_X g$ means that for each $n \in X$ we have that either both $f(n)$ and $g(n)$ are undefined, or both values are defined and equal. In case $X = \mathbb {N}$ we just write $f = g$ .

We assume that some standard Gödel numbering of Turing machines and their computations is fixed. In particular, the universal function is denoted by $\varphi _e(x)$ , so $\varphi _e$ is the unary function, computed by the Turing machine with code e. The number e in this case is called a $\varphi $ -index of f (other indexing functions will be introduced later). We also consider the following complexity measure associated with $\varphi _e$ :

$$ \begin{align*}\Phi_e(x) := x + e + \text{the number of steps in the computation }\varphi_e(x), \end{align*} $$

whenever the computation $\varphi _e(x)$ converges. We use these expressions in formalized contexts and assume that the formalization is natural enough, so that the Kleene T-predicate and, in particular, the predicate $\Phi _e(x) \leqslant y$ are expressed by elementary formulas. We also say that $f(x)$ is dominated by $g(x)$ if there is an $m \in \mathbb {N}$ such that for all $n \geqslant m$ we have $f(n) < g(n)$ . The expression $f^{(n)}(x)$ denotes the n-fold composition of $f(x)$ with itself, and $f^{(0)}(x) = x$ . Finally, we say that $f(x)$ is elementarily cumulative (or just cumulative, for short) if there is a $\varphi $ -index a for f such that $\Phi _a \preccurlyeq _{\mathrm {dom}\, f} f$ , so the value $f(x)$ can be computed in time elementary in itself, meaning that the growth rate of the function $f(x)$ honestly reflects the complexity of computing it (see [20]). This notion is very close to the notion of elementarily honest function introduced in [15] (but it is not the same, since, for instance, all elementary $\{0,1\}$ -valued functions are honest yet not cumulative), which turns out to be equivalent to f having an elementary graph. We, however, stick with the notion of cumulativity used in [20], one of the reasons being that in some modern definitions of honesty, e.g., used in the study of honest elementary degrees (see [12]), several additional properties, like being strictly increasing or growing at least as fast as the function $2^x$ , are required.

3 The reflection function $\mathscr {R}_T(x)$ and the classes $\mathcal {F}^k_{T}(U)$

In his work Adamsson introduces several functions (see [1, definition 5]) measuring the proof speed-up obtained by adding a certain inference rule to a theory T, and shows them to be closely related in terms of the growth rate. One of these functions, the Parikh speed-up function $\mathscr {P}_T(x)$ , which is used in the formulation of Theorem 1.3, is based on the so-called Parikh rule: from $\Box _T\psi $ derive $\psi $ . Since we are dealing with $\Sigma _1$ -sound theories, this rule does not add any new theorems. Indeed, if $\Box _T \psi $ is provable in T, then it is true (being a $\Sigma _1$ -sentence), whence $\psi $ is provable in T. However, Parikh showed that the use of this rule allows to obtain significantly shorter proofs for certain sentences [16]; more precisely, for each $f(x) \in \mathcal {F}(T)$ there are $n \in \mathbb {N}$ and a sentence $\psi $ such that $T \vdash _n \Box _T\psi $ , but $T \not \vdash _{f(n)} \psi $ . Since $\mathscr {P}_T(x)$ is defined so that $T \vdash _n \Box _T\psi $ implies $T \vdash _{\mathscr {P}_T(n)} \psi $ , it follows that $\mathscr {P}_T(x)$ is not provably total in T.

Adamsson’s necessary condition (see Theorem 1.3) for the existence of an epimorphism from $\mathfrak {D}_T$ onto $\mathfrak {D}_S$ is formulated as a restriction on the growth rate of Parikh speed-up function for the theory T in terms of the same function for the theory S. Namely, it asserts that the function $\mathscr {P}_T(x)$ cannot dominate all compositions of the form $t(\mathscr {P}^{(4)}_S(x))$ , where $t(x)$ is an elementary function. In this section we obtain a stronger condition of this form.

As a measure of proof size Adamsson uses the number of symbols. In our presentation we (following Shavrukov [20]) use the Gödel number of a proof instead. This does not lead to drastic changes in the growth rate since these two measures are elementarily related. Also, instead of the Parikh speed-up function $\mathscr {P}_T(x)$ we consider the $\Sigma _1$ -reflection function $\mathscr {R}_T(x)$ , which is defined below, for the sake of it being more general and easier to work with. But since these two functions are elementarily related (see [1, proposition 5]), the results can also be reformulated in terms of $\mathscr {P}_T(x)$ .

Define the $\Sigma _1$ -reflection function $\mathscr {R}_T(x)$ for a theory T as follows:

$$ \begin{align*} \mathscr{R}_T(x) = \mu y.\left[ \forall \delta(\cdot) \in \Delta_0 \left( T \vdash_x \exists z\, \delta(z) \to \exists u \leqslant y\, \delta(u) \right) \right], \end{align*} $$

i.e., $\mathscr {R}_T(x)$ gives the least upper bound to the least witnesses of all $\Sigma _1$ -sentences, which have a T-proof with Gödel number less than or equal to x (cf. the reflection principle in Theorem 1.1). Since T is $\Sigma _1$ -sound, the function $\mathscr {R}_T(x)$ is recursive. As can be seen from the definition, it certainly depends on a particular axiomatization of T, since it is defined in terms of a proof predicate for T. So an appropriate notation would rather be $\mathscr {R}_{\sigma _T}(x)$ , where $\sigma _T(z)$ is an elementary formula defining the set of axioms of T. However, as in the case with the provability predicate $\Box _T$ , we usually write just $\mathscr {R}_T(x)$ , since $\sigma _T(z)$ is assumed to be fixed in each particular case. Let us also note the use of $\Delta _0$ -formulas (rather than $\Delta _0(\exp )$ ) in the definition of $\mathscr {R}_T(x)$ , as well as in the definition of the classes of the arithmetical hierarchy, which is related to the lack of an elementary truth predicate for the class of $\Delta _0(\exp )$ -formulas.

Remark 3.5. A typical application of the $\Sigma _1$ -reflection function $\mathscr {R}_T(x)$ is when a formula $\exists z\, \delta (z)$ is taken to be a $\Sigma _1$ -sentence which is $\mathsf {EA}$ -provably equivalent to $\Box _T \psi $ , i. e., $\exists p\, \mathsf {Prf}_T(p, \ulcorner \psi \urcorner )$ . We then can find an upper bound on a (Gödel number of a) T-proof of $\psi $ , given such bound on a T-proof of $\Box _T \psi $ . Namely, if $T \vdash _n \Box _T \psi $ , then $T \vdash _{\mathscr {R}_T(n)} \psi $ .

Proof (sketch)

Indeed, although $\mathsf {Prf}_T(p, \ulcorner \psi \urcorner )$ is an elementary formula (rather than just $\Delta _0$ ), Remark 2.4 ensures that it is $\mathsf {EA}$ -provably equivalent to a $\Sigma _1$ -formula of the form $\exists y\, \gamma (p, \ulcorner \psi \urcorner , y)$ , where $\gamma (p, q, y)$ is a $\Delta _0$ -formula. Thus, we may assume $\Box _T \psi $ to be expressed in the required strict $\Sigma _1$ -form as $\exists z\, \delta (z)$ for the $\Delta _0$ -formula $ \delta (z) \leftrightharpoons \exists p \leqslant z\, \exists y \leqslant z\, \gamma (p, \ulcorner \psi \urcorner , y). $ Denote the least witness to the $\Sigma _1$ -sentence $\exists z\, \delta (z)$ by m. The definition of the function $\mathscr {R}_T(x)$ then guarantees that $m \leqslant \mathscr {R}_T(n)$ , since $T \vdash _n \exists z\, \delta (z)$ . But as $\delta (m)$ is true it follows, in particular, that $\exists p \leqslant m\, \exists y\, \gamma (p, \ulcorner \psi \urcorner , y)$ or, equivalently, $\exists p \leqslant m\, \mathsf {Prf}_T(p, \ulcorner \psi \urcorner )$ is true, whence $T \vdash _m \psi $ and $T \vdash _{\mathscr {R}_T(n)} \psi $ , as required. Similar applications of $\mathscr {R}_T(x)$ in case $T \vdash _n \Box _T\psi $ with $\mathsf {Prf}_T(p, x)$ being an elementary formula rather than $\Delta _0$ are also present in [1, lemma 3(a)] and [20, lemma 4].

We make use of this remark further in the paper, sometimes without explicitly mentioning it. Another possible way would be to define and work with the $\Sigma _1(\exp )$ -reflection function $\mathscr {R}^{\prime }_S(x)$ , where $\delta (\cdot )$ is a $\Delta _0(\exp )$ -formula rather than a $\Delta _0$ -formula. Remarks 2.4 and 3.5 ensure that $\mathscr {R}^{\prime }_S(x) \leqslant \mathscr {R}_S(q(x))$ for some elementary function $q(x)$ , and we also have $\mathscr {R}_S(x) \leqslant \mathscr {R}^{\prime }_S(x)$ , since each $\Delta _0$ -formula is a $\Delta _0(\exp )$ -formula, so these two functions have a very close growth rate.

As noted in [1] the function $\mathscr {R}_T(x)$ is close to being a T-provably total computable function (see Proposition 3.7), although $\mathscr {R}_T(x) \notin \mathcal {F}(T)$ . It is this observation that Adamsson uses to improve Shavrukov’s non-isomorphism condition. The following definition of the classes $\mathcal {F}^k_{T}(U)$ is inspired by this observation. Denote by $\mathcal {F}_{T}(U)$ the class of all functions $f \colon \mathbb {N}^n \to \mathbb {N}$ such that

$$ \begin{align*} U \vdash \forall x_1 \dots \forall x_n \Box_T \left(\exists y\, \psi_f(\underline{x_1}, \dots, \underline{x_n}, y)\right){\kern-1.5pt}, \end{align*} $$

for some $\Sigma _1$ -formula $\psi _f(x_1, \dots , x_n, y)$ defining the graph of $f(x_1, \dots , x_n)$ in the standard model. As usual, the appropriate notation would be $\mathcal {F}_{\Box _T}(U)$ , since the class depends on the provability predicate $\Box _T$ of T. However, as $\Box _T$ is usually assumed to be fixed, we use a less heavy notation $\mathcal {F}_T(U)$ instead. Note that the definition makes sense for an arbitrary provability predicate instead of $\Box _T$ (not necessarily standard). In particular, we can consider a sequence of classes $\mathcal {F}^k_{T}(U)$ for $k \geqslant 1$ , where we use $\Box ^{(k)}_T$ instead of $\Box _T$ above. We also abuse the notation and sometimes write $\Box ^{(0)}_T \psi (\underline {x})$ instead of $\psi (x)$ , when no confusion arises, although $\Box ^{(0)}_T(x)$ is not a formula. It is then natural to define $\mathcal {F}^0_{T}(U)$ to be $\mathcal {F}(U)$ , the class of all provably total computable functions of U. By provable $\Sigma _1$ -completeness we have

$$ \begin{align*} \mathcal{F}(U) = \mathcal{F}^0_{T}(U) \subseteq \mathcal{F}_{T}(U) = \mathcal{F}^1_{T}(U) \subseteq \mathcal{F}^2_{T}(U) \subseteq \dots \subseteq \mathcal{F}(U + \mathsf{RFN}_{\Sigma_1}(T)), \end{align*} $$

and also $\mathcal {F}(T) \subseteq \mathcal {F}_{T}(\mathsf {EA})$ , since $\mathsf {EA} \vdash \Box _T\forall x\, \psi (x) \to \forall x\, \Box _T \psi (\underline {x})$ . Thus, we get an increasing sequence of classes which are not, in general, closed with respect to composition (unlike $\mathcal {F}(U)$ ). We, however, have the following closure property.

Lemma 3.6. If T contains U, then for each $F(x) \in \mathcal {F}^m_{T}(U)$ and $G(x) \in \mathcal {F}^n_{T}(U)$ we have $G(F(x)) \in \mathcal {F}^{m + n}_{T}(U)$ .

Proof. We consider the case $m> 0$ and $n> 0$ . Fix $\Sigma _1$ -formulas $\psi _F(x, y)$ and $\theta _G(x, y)$ defining the graphs of $F(x)$ and $G(x)$ such that

$$ \begin{align*} U \vdash \forall x\, \Box^{(m)}_T \exists y\, \psi_F(\underline{x}, y) \quad \text { and } \quad U \vdash \forall x\, \Box^{(n)}_T \exists y\, \theta_G(\underline{x}, y). \end{align*} $$

Consider a $\Sigma _1$ -formula $\chi (x, z) \leftrightharpoons \exists y \left ( \psi _F(x, y) \land \theta _G(y, z)\right )$ , which defines the graph of $G(F(x))$ . We prove that $ U \vdash \forall x\, \Box ^{(m + n)}_T \exists z\, \chi (\underline {x}, z). $ Indeed, by provable $\Sigma _1$ -completeness we obtain

$$ \begin{align*} U \vdash \psi_F(x, y) &\to \Box^{(n)}_T \left(\psi_F(\underline{x}, \underline{y}) \land \exists z\, \theta_G(\underline{y}, z)\right)\\ &\to \Box^{(n)}_T \exists z\, \chi(\underline{x}, z), \end{align*} $$

whence $U \vdash \forall x \left (\exists y\, \psi _F(x, y) \to \Box ^{(n)}_T \exists z\, \chi (\underline {x}, z) \right )$ . Now, since T contains U, the same is provable in T, and therefore ( $m> 0$ ) we have

$$ \begin{align*} \mathsf{EA} \vdash \Box^{(m)}_T \forall x \left(\exists y\, \psi_F(x, y) \to \Box^{(n)}_T \exists z\, \chi(\underline{x}, z) \right){\kern-1.5pt}, \end{align*} $$

whence we obtain

$$ \begin{align*} \mathsf{EA} \vdash \forall x\, \Box^{(m)}_T \exists y\, \psi_F(\underline{x}, y) \to \forall x\, \Box^{(m + n)}_T \exists z\, \chi(\underline{x}, z). \end{align*} $$

By the assumption the antecedent of this implication is provable in U, whence its consequent is provable in U, as required. The cases $m = 0$ and $n = 0$ can be considered similarly.

The following proposition confirms the above claim that $\mathscr {R}_T(x)$ is close to being a T-provably total computable function. We closely follow Adamsson’s proof (see [1, proposition 9]) and make certain parts more formal (in order to be able to formalize the proof of this proposition).

Proposition 3.7. For each $k \in \mathbb {N}$ , $\mathscr {R}^{(k)}_T(x) \in \mathcal {F}^k_{T}(\mathsf {EA})$ .

Proof. The case $k = 0$ is trivial, since $\mathscr {R}^{(0)}_T(x) \in \mathcal {F}(\mathsf {EA}) = \mathcal {F}^0_{T}(\mathsf {EA})$ . By Lemma 3.6 it is sufficient to prove $\mathscr {R}_T(x) \in \mathcal {F}_{T}(\mathsf {EA})$ . Here we rely on the fact that the definition of $\mathscr {R}_T(x)$ mentions $\Delta _0$ -formulas rather than $\Delta _0(\exp )$ , since in this case the truth predicate is elementary. Consider the following elementary formula:

$$ \begin{align*} \psi(x, y) \leftrightharpoons \forall p \leqslant x\, \forall \delta < p ( ( \delta(\cdot) \in \Delta_0 \land \, \mathsf{Prf}_T(p, \ulcorner \exists z\, \delta(z) \urcorner)) \to \exists u \leqslant y\, \mathsf{Tr}_{\Delta_0}(\ulcorner \delta(\underline{u}) \urcorner) ){\kern-1.5pt}. \end{align*} $$

The graph of $\mathscr {R}_T(x)$ is then defined by $\psi (x, y) \land \forall z < y\, \neg \psi (x, z).$ We prove by induction on x (which is formalizable in $\mathsf {EA}$ , since we have an elementary bound on the Gödel number of the corresponding T-proof) that

$$ \begin{align*} \mathsf{EA} \vdash \forall x\, \Box_T (\exists y\, \psi(\underline{x}, y) ){\kern-1.5pt}, \end{align*} $$

whence $\mathsf {EA} \vdash \forall x\, \Box _T \exists y ( \psi (\underline {x}, y) \land \forall z < y\, \neg \psi (\underline {x}, z))$ , follows by the least element principle applied under $\Box _T$ (since T contains $\mathsf {EA}$ and $\psi (x, y)$ is elementary).

We argue in $\mathsf {EA}$ by induction on x as follows. The base case $x = 0$ is trivial (since $0$ does not code a T-proof of a $\Sigma _1$ -sentence). Assuming $\Box _T \left ( \exists y\, \psi (\underline {x}, y)\right )$ we derive $\Box _T \left (\exists y\, \psi (\underline {x+1}, y)\right )$ . We argue informally under $\Box _T$ . By the induction hypothesis we can fix some $v$ such that $\psi (\underline {x}, v)$ . Consider an arbitrary $p \leqslant \underline {x+1}$ and a $\Delta _0$ -formula $\delta (\cdot )$ such that $\mathsf {Prf}_T(p, \ulcorner \exists z\, \delta (z) \urcorner )$ . Since (it is provable in T that) $\underline {x + 1} = \underline {x} + 1$ we either have $p \leqslant \underline {x}$ or $p = \underline {x + 1}$ . In the former case we obtain $\exists u \leqslant v\, \mathsf {Tr}_{\Delta _0}(\ulcorner \delta (\underline {u}) \urcorner )$ by the induction hypothesis. In the latter case we see that the $\Sigma _1$ -sentence $\exists z\, \delta (z)$ is standard (since its proof $p = \underline {x + 1}$ is), whence by the small reflection principle we get $\exists z\, \delta (z)$ and $\exists z\, \mathsf {Tr}_{\Delta _0}(\ulcorner \delta (\underline {z}) \urcorner )$ . Fix a number t such that $\mathsf {Tr}_{\Delta _0}(\ulcorner \delta (\underline {t}) \urcorner )$ , and let m be the maximum of $v$ and t. It follows that $\psi (\underline {x+1}, m)$ , whence $\exists y\, \psi (\underline {x+1}, y)$ , as required.

The next proposition shows that $\mathscr {R}_T(x) \notin \mathcal {F}(T)$ . Note that the statement and the proof are slightly more cumbersome than the ones presented in [1, lemma 4], since we define $\mathscr {R}_T(x)$ in terms of the Gödel number of a proof rather than the number of symbols.

Proposition 3.8. There is a monotone elementary function $p(x)$ such that for each function $f(x) \in \mathcal {F}(T)$ the function $\max _{y \leqslant x} f(y)$ is dominated by $\mathscr {R}_T(p(x))$ . Consequently, each monotone function $f(x) \in \mathcal {F}(T)$ is dominated by $\mathscr {R}_T(x)$ .

Proof. Fix an arbitrary $f(x) \in \mathcal {F}(T)$ and a constant $c \in \mathbb {N}$ such that $T \vdash _c \forall x\, \exists ! y\, \psi (x, y)$ , where $\psi (x, y)$ is a $\Sigma _1$ -definition of the graph of $f(x)$ (recall that $\psi (x, y)$ can be chosen so that y is T-provably unique). Define $\hat {f}(x)$ to be $\max _{y \leqslant x} f(y)$ . Note that $\hat {f}(x)$ is not necessarily provably total in T; however, for each $n \in \mathbb {N}$ there is a short (relative to n) T-proof of a $\Sigma _1$ -sentence $\theta _n$ , which naturally expresses $\exists y\, (\hat {f}(n) = y)$ , e.g.,

$$ \begin{align*} \theta_n \leftrightharpoons \exists z\, \exists y_0 \leqslant z\, \dots \exists y_n \leqslant z (\psi(\underline{0}, y_0) \land \dots \land \psi(\underline{n}, y_n) ){\kern-1.5pt}. \end{align*} $$

Note that the least witness of $\theta _n$ is at least $\hat {f}(n)$ . Given $n \in \mathbb {N}$ and the above proof of the totality of $f(x)$ one can elementarily obtain a T-proof of $\theta _n$ . Let $q(c, n)$ be a strictly monotone elementary function which, given an upper bound c on the T-proof of the totality of some function $f(x)$ , outputs an upper bound on the T-proof of a $\Sigma _1$ -sentence $\theta _n$ . Finally, define $p(x)$ to be $q(x, x)$ . By the definition of $\mathscr {R}_T(x)$ and monotonicity of $q(c, n)$ it follows that

$$ \begin{align*} f(n) \leqslant \hat{f}(n) \leqslant \mathscr{R}_T(q(c, n)) \leqslant \mathscr{R}_T(p(n)) \end{align*} $$

holds for all $n \geqslant c$ , as required.

Now, assuming $f(x) \in \mathcal {F}(T)$ is monotone, apply the argument above to the monotone function $f(p(x+1)) \in \mathcal {F}(T)$ (since $p(x)$ is elementary). Let $p^{-1}(x)$ to be $\max \{y \mid p(y) \leqslant x\}$ or $0$ , if there is no such y. Using the definition of $p^{-1}(x)$ and monotonicity of $f(x)$ , $p(x)$ and $\mathscr {R}_T(x)$ we obtain

$$ \begin{align*} f(n) \leqslant f(p(p^{-1}(n) + 1)) \leqslant \mathscr{R}_T(p(p^{-1}(n))) \leqslant \mathscr{R}_T(n), \end{align*} $$

for all sufficiently large $n \in \mathbb {N}$ .

The following lemma asserts a well-known fact about the class of provably total computable functions. We show that it also holds for all the classes $\mathcal {F}^k_{T}(U)$ .

Lemma 3.9. For each $k \in \mathbb {N}$ and each $F(x) \in \mathcal {F}^k_{T}(U)$ there is a $\Sigma _1$ -formula $\psi (x, y)$ defining the graph of $F(x)$ in the standard model such that

$$ \begin{align*} U \vdash \forall x\, \Box^{(k)}_T (\exists ! y\, \psi(\underline{x}, y)){\kern-1.5pt}. \end{align*} $$

Proof. Assume $F(x) \in \mathcal {F}^k_{T}(U)$ and fix a corresponding $\Sigma _1$ -formula $\exists z\, \delta (x, y, z)$ where $\delta (x, y, z)$ is a $\Delta _0$ -formula. Define $\psi (x, y)$ to be

$$ \begin{align*} \exists u\, \exists z \leqslant u (u = \langle y, z \rangle \land \delta(x, y, z) \land \forall v < u\, \forall y', z' \leqslant v ( v = \langle y', z' \rangle \to \neg \delta(x, y', z'))){\kern-1.5pt}. \end{align*} $$

This formula still defines the graph of $F(x)$ in the standard model. Note that by the definition of $\psi (x, y)$ we have

$$ \begin{align*} \mathsf{EA} \vdash \forall x\, \forall y_1\, \forall y_2 \left(\psi(x, y_1) \land \psi(x, y_2) \to y_1 = y_2\right){\kern-1.5pt}, \end{align*} $$

since there is only one least (w.r.t. its code) pair satisfying $\delta (x, y, z)$ and hence only one first component y of such a pair. We have $U \vdash \forall x\, \Box ^{(k)}_T \exists y\, \exists z\, \delta (\underline {x}, y, z)$ , so

$$ \begin{align*} U \vdash \forall x\, \Box^{(k)}_T \exists u\, \exists y \leqslant u\, \exists z \leqslant u ( u = \langle y, z \rangle \land \delta(\underline{x}, y, z) ){\kern-1.5pt}, \end{align*} $$

whence by the least element principle (under $\Box _T$ for $k> 0$ and directly in U for $k = 0$ , since both T and U contain $\mathsf {EA}$ ) we get $U \vdash \forall x\, \Box ^{(k)}_T \exists y\, \psi (\underline {x}, y)$ , as required.

The following four lemmas and the corollaries are used in the proof of the main theorem (Theorem 4.24) to obtain the desired improvement of an upper bound in Adamsson’s condition.

Lemma 3.10. For each $k \in \mathbb {N}$ , every function $G(x) \in \mathcal {F}^k_{T}(U)$ is dominated by a cumulative function $F(x) \in \mathcal {F}^k_{T}(U)$ .

Proof. Assume $G(x) \in \mathcal {F}^k_{T}(U)$ and fix a $\Sigma _1$ -formula $\psi (x, y)$ defining the graph of $G(x)$ such that

$$ \begin{align*} U \vdash \forall x\, \Box^{(k)}_T (\exists y\, \psi(\underline{x}, y) ){\kern-1.5pt}. \end{align*} $$

By provable $\Sigma _1$ -completeness it follows that $U \vdash \forall x\, \Box ^{(k)}_T \left (\exists y\, \Box _T \psi (\underline {x}, \underline {y}) \right){\kern-1pt}, $ whence

$$ \begin{align*} U \vdash \forall x\, \Box^{(k)}_T \left(\exists p\, \exists y \leqslant p\, \mathsf{Prf}_T(p, \ulcorner \psi(\underline{x}, \underline{y}) \urcorner) \right){\kern-1.5pt}. \end{align*} $$

Let $F(x)$ be the function which maps n to the Gödel number p of the least T-proof of $\psi (\underline {n}, \underline {m})$ for some $m \in \mathbb {N}$ . The above U-derivation ensures that $F(x) \in \mathcal {F}^k_{T}(U)$ (apply the least element principle available both under the innermost $\Box _T$ (for $k \geqslant 1$ ) and in U (for $k = 0$ ) to derive the existence of the least such p). For each $n \in \mathbb {N}$ , the value $F(n)$ is a Gödel number of a T-proof of $\psi (\underline {n}, \underline {m})$ for some $m \in \mathbb {N}$ . Since $\psi (x, y)$ defines the graph of $G(x)$ and T is $\Sigma _1$ -sound, it must be the case that $m = G(n)$ , whence $G(n) \leqslant F(n)$ , since m is certainly not greater than a Gödel number of a proof containing $\underline {m}$ . The computation of the value $F(n)$ consists of looking through all T-proofs with Gödel numbers $p \leqslant F(n)$ and checking the elementary condition $\exists y \leqslant p\, \mathsf {Prf}_T(p, \ulcorner \psi (\underline {n}, \underline {y}) \urcorner )$ for each such proof. The complexity of this process is elementary in $F(n)$ , whence the cumulativity of $F(x)$ follows.

Lemma 3.11. There is an elementary function $u(x)$ such that for all sentences $\psi , \chi $ and $n \in \mathbb {N}$ ,

$$ \begin{align*} \left(S \vdash_n \psi \to \chi\right) \lor \left(S \vdash_n \psi \to \neg \chi \right) \Longrightarrow S \vdash_{u(n)} \Box_S(\psi \to \chi) \lor \Box_S (\psi \to \neg \chi). \end{align*} $$

Proof. By provable $\Sigma _1$ -completeness (and basic predicate logic) the following is provable in $\mathsf {EA}$ :

$$ \begin{align*} \forall p\, \forall \psi\, \forall \chi (\exists q \leqslant p\, \mathsf{Prf}_S(q, \ulcorner \psi \to \chi \urcorner) &\lor \mathsf{Prf}_S (q, \ulcorner \psi \to \neg \chi \urcorner) \to \\ &\to \Box_S (\Box_S(\psi \to \chi) \lor \Box_S (\psi \to \neg \chi)) ){\kern-1.5pt}, \end{align*} $$

whence the function $p(x, y, z)$ which, given Gödel numbers y and z of $\psi $ and $\chi $ , and an upper bound x on the Gödel number of an S-proof of one of implications $\psi \to \chi $ or $\psi \to \neg \chi $ , outputs a Gödel number of the least S-proof of the disjunction of boxes is elementary (being provably total in $\mathsf {EA}$ ). The required function $u(x)$ can be then defined as follows:

$$ \begin{align*} u(x) = \sum_{y \leqslant x}\sum_{z \leqslant x} p(x, y, z), \end{align*} $$

since the Gödel numbers of $\chi $ and $\psi $ are bounded by n, given $S \vdash _n \psi \to \chi $ or $S \vdash _n \psi \to \neg \chi $ .

Lemma 3.12. There is a strictly monotone elementary function $v(x)$ such that for all $\psi , \chi $ and $n \in \mathbb {N}$ we have

$$ \begin{align*} S \vdash_n \Box_S \psi \lor \Box_S \chi \Longrightarrow \left(S \vdash_{\mathscr{R}_S(v(n))} \psi \right) \lor \left(S \vdash_{\mathscr{R}_S(v(n))} \chi \right){\kern-1.5pt}. \end{align*} $$

Proof. Let $v'(x)$ be the function which transforms a code of an S-proof x of the formula $\Box _S \psi \lor \Box _S \chi $ into that of $ \exists p (\mathsf {Prf}_S(p, \ulcorner \psi \urcorner ) \lor \mathsf {Prf}_S(p, \ulcorner \chi \urcorner )){\kern-1pt}, $ obtained by concatenating the proof of $\Box _S \psi \lor \Box _S \chi $ with a simple derivation in predicate logic of the implication $(\exists y\, \mathsf {Prf}_S(y, \ulcorner \psi \urcorner ) \lor \exists z\, \mathsf {Prf}_S(z, \ulcorner \chi \urcorner )) \to \exists p (\mathsf {Prf}_S(p, \ulcorner \psi \urcorner ) \lor \mathsf {Prf}_S(p, \ulcorner \chi \urcorner ) )$ and applying modus ponens. The code of the proof just described is elementary in x and so is the function $v'(x)$ . Define $v(x)$ to be some strictly monotone elementary upper bound on $v'(x)$ , e.g., $v(x) = 2^x_k$ for some fixed $k \in \mathbb {N}$ . The required implication then follows by the definition of $\mathscr {R}_S(x)$ and Remark 3.5 concerning the use of $\Delta _0$ -formulas rather than elementary formulas in it.

Lemma 3.13. There is an elementary function $w(x, y)$ such that for each $f(x) \in \mathcal {F}(T)$ there is a constant $c \in \mathbb {N}$ such that the inequality $ f(\mathscr {R}_S(n)) \leqslant \mathscr {R}_S(w(c, n)) $ holds for all $n \in \mathbb {N}$ .

Proof. Fix a $\Sigma _1$ -formula $\exists z\, \delta (x, y, z)$ , which defines the graph of $f(x)$ in the standard model, where $\delta (x, y, z)$ is a $\Delta _0$ -formula and

$$ \begin{align*} S \vdash \forall x\, \exists ! y\, \exists z\, \delta(x, y, z). \end{align*} $$

Fix an arbitrary $n \in \mathbb {N}$ and let m be the value $\mathscr {R}_S(n)$ . Fix a $\Sigma _1$ -sentence $\exists x\, \psi (x)$ , where $\psi (x)$ is a $\Delta _0$ -formula, such that $S \vdash _n \exists x\, \psi (x)$ and the least witness for this sentence is m. Since S extends $\mathsf {EA}$ , it follows that $S \vdash \exists x\, ( \psi (x) \land \forall u < x\, \neg \psi (u) )$ , and the Gödel number of this proof is elementary in that of $\exists x\, \psi (x)$ .

Our aim is to construct a short (relative to n) S-proof of a $\Sigma _1$ -sentence with the least witness greater than $f(m)$ . Define a $\Sigma _1$ -sentence $\sigma $ as follows:

$$ \begin{align*} \sigma \leftrightharpoons \exists v\, \exists x, y, z \leqslant v (\psi(x) \land \forall u < x\, \neg \psi(u) \land \delta(x, y, z)){\kern-1.5pt}. \end{align*} $$

Informally, $\sigma $ asserts that the value $f(m)$ , where m is the least witness for $\exists x\, \psi (x)$ , is defined. It follows then that the least witness for $\sigma $ is at least $f(m)$ .

The required S-proof of $\sigma $ is obtained as follows: concatenate the proof of (the totality of $f(x)$ ) $\forall x\, \exists y\, \exists z\, \delta (x, y, z)$ with the proof of $\exists x (\psi (x) \land \forall u < x\, \neg \psi (u) )$ and derive $\sigma $ using basic predicate logic. The Gödel number $w'(c, n)$ of this proof is elementary in Gödel numbers of the proofs of the totality of $f(x)$ and $\exists x\, \psi (x)$ . As usual let $w(x, y) = \sum _{u \leqslant x}\sum _{v \leqslant y} w'(u, v)$ . It follows that $S \vdash _{w(c, n)} \sigma $ and $f(\mathscr {R}_S(n)) \leqslant \mathscr {R}_S(w(c, n))$ for all $n \in \mathbb {N}$ .

Corollary 3.14. There is a strictly monotone elementary function $h(x)$ such that for each $f(x) \in \mathcal {F}(T)$ the inequality $ f(\mathscr {R}_S(n)) \leqslant \mathscr {R}_S(h(n)) $ holds for all sufficiently large $n \in \mathbb {N}$ . More generally, for each $k \in \mathbb {N}$ and each $f(x) \in \mathcal {F}(T)$ we have

$$ \begin{align*} f(\mathscr{R}^{(k+1)}_S(n)) \leqslant \mathscr{R}^{(k+1)}_S(h(n)) \end{align*} $$

for all sufficiently large $n \in \mathbb {N}$ .

Proof. Let $w(x, y)$ be an elementary function as constructed in Lemma 3.13. Let $h(x) = 2^{2x}_m$ , where $m \in \mathbb {N}$ is such that $w(x, y) \leqslant 2^{x + y}_m$ for all $x, y \in \mathbb {N}$ . Using monotonicity of $\mathscr {R}_S(x)$ we get

$$ \begin{align*} f(\mathscr{R}_S(n)) \leqslant \mathscr{R}_S(w(c, n)) \leqslant \mathscr{R}_S(2^{c + n}_m) \leqslant \mathscr{R}_S(h(n)) \end{align*} $$

for all $n \geqslant c$ , as required. The general case is then proved by induction on k, where the base case $k = 0$ has been just proved above.

Assume that for each $f(x) \in \mathcal {F}(T)$ there is some $c \in \mathbb {N}$ such that $f(\mathscr {R}^{(k+1)}_S(n)) \leqslant \mathscr {R}^{(k+1)}_S(h(n))$ holds for all $n \geqslant c$ . Fix an arbitrary function $g(x) \in \mathcal {F}(T)$ . We aim at proving that

$$ \begin{align*} g(\mathscr{R}^{(k+2)}_S(n)) \leqslant \mathscr{R}^{(k+2)}_S(h(n)) \end{align*} $$

holds for all sufficiently large n. Firstly, by the base case, we have $g(\mathscr {R}_S(n)) \leqslant \mathscr {R}_S(h(n))$ for all sufficiently large n, whence

$$ \begin{align*} g(\mathscr{R}^{(k+2)}_S(n)) = g(\mathscr{R}_S(\mathscr{R}^{(k+1)}_S(n))) \leqslant \mathscr{R}_S(h(\mathscr{R}^{k+1}_S(n))), \end{align*} $$

for all sufficiently large n, since is $\mathscr {R}^{(k+1)}_S(x)$ monotone and unbounded. Now, applying the induction hypothesis to $h(x) \in \mathcal {F}(T)$ (since $h(x)$ is elementary and T extends $\mathsf {EA}$ ) we get

$$ \begin{align*} h(\mathscr{R}^{(k+1)}_S(n)) \leqslant \mathscr{R}^{(k+1)}_S(h(n)) \end{align*} $$

for all sufficiently large n, whence, by monotonicity of $\mathscr {R}_S(x)$ , we obtain

$$ \begin{align*} g(\mathscr{R}^{(k+2)}_S(n)) \leqslant \mathscr{R}_S(h(\mathscr{R}^{(k+1)}_S(n))) \leqslant \mathscr{R}^{(k+2)}_S(h(n)) \end{align*} $$

for all sufficiently large n, as required.

Below we prove several properties of the classes $\mathcal {F}_{T}(U)$ (we consider only the case $k = 1$ ) similar to that of the class of provably total computable functions.

Lemma 3.15. If X is any set of true $\Pi _1$ -sentences, then $ \mathcal {F}_{T}(U) = \mathcal {F}_{T}(U + X). $

Proof. Let $\psi _f(x, y)$ be a $\Sigma _1$ -formula defining the graph of $f(x)$ such that

$$ \begin{align*} U + X \vdash \forall x\, \Box_T \left(\exists y\, \psi_f(\underline{x}, y)\right){\kern-1.5pt}. \end{align*} $$

Let $\pi $ be a conjunction of finitely many $\Pi _1$ -sentences from X used in this proof. We then have

$$ \begin{align*} U \vdash \pi & \to \forall x\, \Box_T \left(\exists y\, \psi_f(\underline{x}, y)\right)\\ & \to \forall x\, \Box_T \left(\pi \to \exists y\, \psi_f(\underline{x}, y)\right){\kern-1.5pt}. \end{align*} $$

But since $\neg \pi $ is (provably equivalent to) a $\Sigma _1$ -sentence, by provable $\Sigma _1$ -completeness we obtain

$$ \begin{align*} U \vdash \neg \pi & \to \Box_T \neg \pi\\ & \to \forall x\, \Box_T \left(\pi \to \exists y\, \psi_f(\underline{x}, y)\right){\kern-1.5pt}. \end{align*} $$

Thus, we have $U \vdash \forall x\, \Box _T\exists y \left (\pi \to \psi _f(\underline {x}, y)\right )$ , whence we obtain $f(x) \in \mathcal {F}_{T}(U)$ , since the formula $\pi \to \psi _f(x, y)$ still defines the graph of $f(x)$ and is provably equivalent to $\Sigma _1$ -formula, because $\pi $ is a true $\Pi _1$ -sentence.

We say that S is a $\Pi _1$ -extension of T if $ \mathsf {Ax}_S(x) \leftrightharpoons \mathsf {Ax}_T(x) \lor \delta (x), $ where $\delta (x)$ is an elementary formula such that $\mathbb {N} \models \delta (\underline {n})$ implies $n = \ulcorner \pi \urcorner $ for some $\pi \in \Pi _1$ .

Lemma 3.16. If S is a true $\Pi _1$ -extension of T, then $ \mathcal {F}_{S}(U) = \mathcal {F}_{T}(U). $

Proof. Fix an elementary formula $\delta (x)$ witnessing that S is a $\Pi _1$ -extension of T and let $\psi _f(x, y)$ be a $\Sigma _1$ -formula defining the graph of $f(x)$ such that

$$ \begin{align*} U \vdash \forall x\, \Box_S \left(\exists y\, \psi_f(\underline{x}, y)\right){\kern-1.5pt}. \end{align*} $$

Let $\chi $ be a true (since S is a $\Pi _1$ -extension of T) $\Pi _1$ -sentence $\forall \pi \left (\delta (\ulcorner \pi \urcorner ) \to \pi \in \Pi _1\right )$ . We show that $f(x) \in \mathcal {F}_{T}(U + \chi )$ , whence the result follows by Lemma 3.15. Let $p(x)$ be an elementary function such that it is provable in $\mathsf {EA}$ that, given a sequence of $\Pi _1$ -sentences $\pi _1, \dots , \pi _k$ , the value $p(\ulcorner \bigwedge _{i < k} \pi _i \urcorner )$ is a (Gödel number of a) naturally constructed $\Pi _1$ -sentence, which is provably equivalent to $\bigwedge _{i < k} \pi _i$ . Using the formalized deduction theorem, provable $\Sigma _1$ -completeness, $\chi $ and the definition of $p(x)$ together with the fact that $\mathsf {EA} \vdash \forall \pi \in \Pi _1\, \Box _T \left (\pi \leftrightarrow \mathsf {Tr}_{\Pi _1}(\pi )\right )$ , we derive

$$ \begin{align*} &U + \chi \vdash \forall x\, \Box_S \left(\exists y\, \psi_f(\underline{x}, y)\right)\\ &\quad\vdash \forall x\, \exists \pi\, \exists z \left[ \forall i < z\, \delta(\ulcorner \pi_i \urcorner) \land \Box_T \left( \bigwedge_{i < z} \pi_i \to \exists y\, \psi_f(\underline{x}, y) \right)\right]\\ &\quad\vdash \forall x\, \exists \pi\, \exists z \left[\forall i < z\, (\pi_i \in \Pi_1) \land \Box_T \left[ \forall i < \underline{z}\, \delta(\ulcorner \pi_i \urcorner) \land \left( \bigwedge_{i < z} \pi_i \to \exists y\, \psi_f(\underline{x}, y) \right)\right] \right]\\ &\quad\vdash \forall x\, \exists \pi\, \exists z\, \Box_T \Bigl[ \forall i < \underline{z}\, \delta(\ulcorner \pi_i \urcorner) \land \Bigl( \mathsf{Tr}_{\Pi_1}(p(\ulcorner \bigwedge_{i < z} \pi_i \urcorner)) \to \exists y\, \psi_f(\underline{x}, y) \Bigr)\Bigr]\\ &\quad\vdash \forall x\, \Box_T \exists \pi\, \exists z\, \Bigl[ \forall i < z\, \delta(\ulcorner \pi_i \urcorner) \land \Bigl( \mathsf{Tr}_{\Pi_1}(p(\ulcorner \bigwedge_{i < z} \pi_i \urcorner)) \to \exists y\, \psi_f(\underline{x}, y) \Bigr)\Bigr]\\ &\quad\vdash \forall x\, \Box_T (\exists y\, \theta(\underline{x}, y) ){\kern-1.5pt}, \end{align*} $$

where $\theta (x, y) \leftrightharpoons \exists \pi \, \exists z\, \Bigl [ \forall i < z\, \delta (\ulcorner \pi _i \urcorner ) \land \Bigl ( \mathsf {Tr}_{\Pi _1}(p(\ulcorner \bigwedge _{i < z} \pi _i \urcorner )) \to \psi _f(x, y) \Bigr )\Bigr ]$ is (provably equivalent to) a $\Sigma _1$ -formula and still defines the graph of $f(x)$ , since S is an extension of T with true $\Pi _1$ -sentences.

Lemma 3.15 also allows to obtain the following alternative definition of the class $\mathcal {F}_{T}(U)$ .

Proposition 3.17. For any $f \colon \mathbb {N}^m \to \mathbb {N}$ we have $f(x_1, \dots , x_m) \in \mathcal {F}_{T}(U)$ if and only if there is a $\Sigma _1$ -formula $\psi _f(x_1, \dots , x_m, y)$ defining the graph of f such that the function which maps $n_1, \dots , n_m$ to the least Gödel number of a T-proof of $\exists y\, \psi _f(\underline {n_1}, \dots , \underline {n_m}, y)$ is provably total in U.

Proof. The “only if” part follows from the definition of $\mathcal {F}_{T}(U)$ . Fix a function $f(x)$ (we consider unary functions for simplicity) and its $\Sigma _1$ -definition $\psi _f(x, y)$ . Let $\theta (x, p)$ be a $\Sigma _1$ -definition of a function which maps n to the least Gödel number of a T-proof of $\exists y\, \psi _f(\underline {n}, y)$ , such that $U \vdash \forall x\, \exists p\, \theta (x, p)$ . Consider the following true $\Pi _1$ -sentence:

$$ \begin{align*} \pi \leftrightharpoons \forall x\, \forall p \left( \theta(x, p) \to \mathsf{Prf}_T(p, \ulcorner \exists y\, \psi_f(\underline{x}, y) \urcorner) \right){\kern-1.5pt}. \end{align*} $$

It follows that $U + \pi \vdash \forall x\, \exists p\, \mathsf {Prf}_T(p, \ulcorner \exists y\, \psi _f(\underline {x}, y) \urcorner )$ , whence $f(x) \in \mathcal {F}_{T}(U + \pi ) = \mathcal {F}_{T}(U)$ by Lemma 3.15, as required.

The following proposition gives a more explicit description of the class $\mathcal {F}_{T}(U)$ . We denote by $\mathcal {C}_1 \circ \mathcal {C}_2$ the class of all compositions of the form $f(g_1(\vec {x}), \dots , g_n(\vec {x}))$ , where $f \in \mathcal {C}_1$ and $g_1, \dots , g_n \in \mathcal {C}_2$ . It is always assumed that both $\mathcal {C}_1$ and $\mathcal {C}_2$ contain all projections (if it is not so, we add all the projections to these classes without writing it explicitly), so that both $\mathcal {C}_1$ and $\mathcal {C}_2$ are included in $\mathcal {C}_1 \circ \mathcal {C}_2$ .

Proposition 3.18. $\mathcal {F}_{T}(U) = \mathcal {F}(T) \circ \{\mathscr {R}_T\} \circ \mathcal {F}(U) = \mathcal {E}_3 \circ \{\mathscr {R}_T\} \circ \mathcal {F}(U).$

Proof. Let us first show that $\mathcal {F}(T) \circ \{\mathscr {R}_T\} \circ \mathcal {F}(U) \subseteq \mathcal {F}_{T}(U)$ . For simplicity we consider the following composition $f(\mathscr {R}_T(g_1(x)), \mathscr {R}_T(g_2(x))) \in \mathcal {F}(T) \circ \{\mathscr {R}_T\} \circ \mathcal {F}(U).$ The general case (more functions and variables) can be dealt with similarly. Fix four $\Sigma _1$ -formulas $\chi _{g_1}(x, y)$ , $\chi _{g_2}(x, y)$ , $\theta _{\mathscr {R}_T}(x, y)$ (this formula is given by Proposition 3.7) and $\varphi _f(x, y, z)$ defining the graphs of the corresponding functions such that

$$ \begin{align*} U \vdash \forall x\, \exists z_1\, \chi_{g_1}(x, z_1) \land \forall x\, \exists z_2\, \chi_{g_2}(x, z_2) \land \forall z\, \Box_T \left(\exists u\, \theta_{\mathscr{R}_T}(\underline{z}, u)\right){\kern-1.5pt}, \end{align*} $$

and $T \vdash \forall u_1, u_2\, \exists y\, \varphi _f(u_1, u_2, y)$ . Define the graph of the above composition as follows:

$$ \begin{align*} \psi(x, y) \leftrightharpoons \exists z_1, z_2, u_1, u_2 ( \chi_{g_1}(x, z_1) &\land \chi_{g_2}(x, z_2) \ \land\\ &\land \left. \theta_{\mathscr{R}_T}(z_1, u_1) \land \theta_{\mathscr{R}_T}(z_2, u_2) \land \varphi_f(u_1, u_2, y) \right){\kern-1.5pt}. \end{align*} $$

We claim that $U \vdash \forall x\, \Box _T ( \exists y\, \psi (\underline {x}, y))$ . Indeed, by provable $\Sigma _1$ -completeness we have

$$ \begin{align*} U \vdash \chi_{g_1}(x, z_1) &\land \chi_{g_2}(x, z_2) \to\\ &\to \Box_T \left(\chi_{g_1}(\underline{x}, \underline{z_1}) \land \chi_{g_2}(\underline{x}, \underline{z_2}) \land \exists u_1\, \theta_{\mathscr{R}_T}(\underline{z_1}, u_1) \land \exists u_2\, \theta_{\mathscr{R}_T}(\underline{z_2}, u_2)\right)\\ &\to \Box_T (\exists y\, \psi(\underline{x}, y)){\kern-1.5pt}, \end{align*} $$

where in the second implication we weakened the formula under $\Box _T$ by introducing the existential quantifiers instead of the numerals $\underline {z_1}$ and $\underline {z_2}$ , and applied the T-provable totality of $f(x)$ to get $\exists y\, \varphi _f(u_1, u_2, y)$ . So we have

$$ \begin{align*} U \vdash \forall x ( \exists z_1\, \chi_{g_1}(x, z_1) \land \exists z_2\, \chi_{g_2}(x, z_2) \to \Box_T ( \exists y\, \psi(\underline{x}, y)) ){\kern-1.5pt}, \end{align*} $$

whence $ U \vdash \forall x\, \Box _T\left ( \exists y\, \psi (\underline {x}, y)\right ) $ follows, as required.

The inclusion $\mathcal {E}_3 \circ \{\mathscr {R}_T\} \circ \mathcal {F}(U) \subseteq \mathcal {F}(T) \circ \{\mathscr {R}_T\} \circ \mathcal {F}(U)$ is clear, since T contains $\mathsf {EA}$ . Now we prove the final inclusion $\mathcal {F}_{T}(U) \subseteq \mathcal {E}_3 \circ \{\mathscr {R}_T\} \circ \mathcal {F}(U)$ . Fix some $f(x) \in \mathcal {F}_{T}(U)$ (where for simplicity we again consider unary functions) and a corresponding $\Sigma _1$ -formula $\psi _f(x, y)$ such that $ U \vdash \forall x\, \Box _T \left ( \exists y\, \psi _f(\underline {x}, y)\right ). $ Fix an elementary formula $\delta (x, y, z)$ such that $\psi _f(x, y) \leftrightharpoons \exists z\, \delta (x, y, z)$ . Define $h(x)$ to be a function which maps n to the Gödel number of the least T-proof of $\exists u\, \exists y, z \leqslant u\, \delta (\underline {n}, y, z)$ . The function $h(x)$ is U-provably total, since

$$ \begin{align*} U \vdash \forall x\, \Box_T ( \exists y\, \exists z\, \delta(\underline{x}, y, z)){\kern-1.5pt}, \end{align*} $$

and the least element principle for elementary formulas is available in U, since U contains $\mathsf {EA}$ . By $\mathsf {EA}$ -provable $\Sigma _1$ -completeness we have

$$ \begin{align*} \mathsf{EA} \vdash \forall x, y, z \left(\delta(x, y, z) \to \Box_T \delta(\underline{x}, \underline{y}, \underline{z})\right){\kern-1.5pt}, \end{align*} $$

whence the function which maps $n, m, k$ to the Gödel number of the least T-proof of $\delta (\underline {n}, \underline {m}, \underline {k})$ is elementary (being provably total in $\mathsf {EA}$ ). Let $t(x, y, z)$ be an elementary upper bound for this function which is monotone in all arguments (e.g., we can take $t(x, y, z)$ to be $2^{x + y + z}_l$ for some fixed sufficiently large $l \in \mathbb {N}$ ).

By the definition of $\mathscr {R}_T(x)$ (and Remark 3.5) and $h(x)$ the value $\mathscr {R}_T(h(n))$ is an upper bound on the least witness to $\exists u\, \exists y, z \leqslant u\, \delta (\underline {n}, y, z)$ . We claim that the graph of $f(x)$ can be defined as follows:

$$ \begin{align*} \exists p \leqslant t(x, \mathscr{R}_T(h(x)), \mathscr{R}_T(h(x)))\, \exists z \leqslant p\, \mathsf{Prf}_T(p, \ulcorner \delta(\underline{x}, \underline{y}, \underline{z}) \urcorner). \end{align*} $$

Indeed, if the relation holds for some $n, m \in \mathbb {N}$ , then T proves $\delta (\underline {n}, \underline {m}, \underline {k})$ for some $k \in \mathbb {N}$ , whence $\exists z\, \delta (\underline {n}, \underline {m}, z)$ is true (since T is $\Sigma _1$ -sound) and so $f(n) = m$ . Conversely, assume $f(n) = m$ and choose the least $k \in \mathbb {N}$ such that $\delta (\underline {n}, \underline {m}, \underline {k})$ is true. By the discussion above the least witness to $\exists u\, \exists y, z \leqslant u\, \delta (\underline {n}, y, z)$ is bounded by $\mathscr {R}_T(h(n))$ , whence m (since m is the only witness for $y \leqslant u$ ) and k are also bounded by $\mathscr {R}_T(h(n))$ . By the definition of the function $t(x, y, z)$ there is a T-proof of $\delta (\underline {n}, \underline {m}, \underline {k})$ with the Gödel number bounded by $t(n, m, k)$ , which is itself bounded by $t(n, \mathscr {R}_T(h(n)), \mathscr {R}_T(h(n)))$ since $t(x, y, z)$ is monotone, whence the relation holds.

Now, consider the following elementary function:

$$ \begin{align*} g(x, u) = \mu y_{\leqslant u}\left( \exists p \leqslant u\, \exists z \leqslant p\, \mathsf{Prf}_T(p, \ulcorner \delta(\underline{x}, \underline{y}, \underline{z}) \urcorner) \right){\kern-1.5pt}. \end{align*} $$

We claim that $f(x) = g(x, t(x, \mathscr {R}_T(h(x)), \mathscr {R}_T(h(x))))$ , which belongs to $\mathcal {E}_3 \circ \{\mathscr {R}_T\} \circ \mathcal {F}(U)$ as the composition of $g(x, t(x, y, z)) \in \mathcal {E}_3$ and $\mathscr {R}_T(h(x)) \in \{\mathscr {R}_T\} \circ \mathcal {F}(U)$ . The claim follows from the equivalent definition of the graph of $f(x)$ given above. For a given $n \in \mathbb {N}$ the value $t(n, \mathscr {R}_T(h(n)), \mathscr {R}_T(h(n)))$ gives an upper bound on the Gödel number of a T-proof (and hence the numerals appearing in this proof) of $\delta (\underline {n}, \underline {m}, \underline {k})$ for some m and k. Since $\exists z\, \delta (x, y, z)$ defines the graph of $f(x)$ it must be the case that $f(n) = m$ .

One can check that the above proof also goes through for $k> 1$ (since Proposition 3.7 also holds for such k), so we obtain $\mathcal {F}^k_{T}(U) = \mathcal {F}(T) \circ \{\mathscr {R}^{(k)}_T(x)\} \circ \mathcal {F}(U)$ for each $k \geqslant 1$ , and $\mathcal {F}^0_{T}(U) = \mathcal {F}(U)$ .

4 The non-isomorphism theorem

Shavrukov’s sufficient condition for the non-isomorphism $\mathfrak {D}_T \not \cong \mathfrak {D}_S$ (Theorem 1.1) implies that the theories T and S have distinct classes of provably total computable functions, namely, $\mathscr {R}_S(x) \in \mathcal {F}(T) \setminus \mathcal {F}(S)$ . As a corollary of the improved version (Theorem 1.3) of the non-isomorphism theorem, Adamsson obtained an example demonstrating that the condition $\mathcal {F}(T) \neq \mathcal {F}(S)$ is not necessary for $\mathfrak {D}_T\not \cong \mathfrak {D}_S$ . In fact, he showed that $(\mathfrak {L}_T, \Box _T) \not \cong (\mathfrak {L}_T, \Box ^{(6)}_T)$ , and so the isomorphism class of $\mathfrak {D}_T$ depends on the choice of the provability predicate for T. However, there are no other applications of the improved non-isomorphism condition in the work of Adamsson [1], which provide new non-isomorphism examples (which do not already follow from Shavrukov’s condition).

In this section we strengthen Adamsson’s improved version of Shavrukov’s non-isomorphism theorem. Our strengthening allows to answer positively the question of Adamsson concerning the non-isomorphism $(\mathfrak {L}_T, \Box _T) \not \cong (\mathfrak {L}_T, \Box _T\Box _T)$ . We also obtain new examples of theories with non-isomorphic diagonalizable algebras. In particular, we give a more natural example of theories with non-isomorphic algebras and the same classes of provably total computable functions, and show that the condition of provable $\Pi _1$ -equivalence is not sufficient for the isomorphism (cf. Theorem 1.2). These applications of the main result are discussed in the next section.

Firstly, let us discuss the main ingredients of Shavrukov’s proof [20] of Theorem 1.1 to clarify the proof of our main theorem which follows. The first major idea is that of associating a model of computation $\delta ^T_\gamma (x)$ with the diagonalizable algebra $\mathfrak {D}_T$ . The role of natural numbers is played by the elements

$$ \begin{align*} \mathrm{\#}^n_T \leftrightharpoons \Box^{(n+1)}_T \bot \land \neg \Box^{(n)}_T \bot. \end{align*} $$

The main property of these sentences is the following:

$$ \begin{align*} \mathsf{EA} \vdash \forall x\, \forall y \left(\mathrm{\#}^x_T \land \mathrm{\#}^y_T \to x = y\right){\kern-1.5pt}. \end{align*} $$

Programs correspond to sentences $\gamma $ and computations correspond to T-proofs. Computation complexity is measured by the size of a proof. For a given sentence $\gamma $ define a $\{0,1\}$ -valued partial recursive function $\delta ^T_\gamma (x)$ and the corresponding complexity measure $\Delta ^T_\gamma (x)$ as follows:

$$ \begin{align*} \delta^T_\gamma(n) &= \begin{cases} 0, &\text{ if }T \vdash \mathrm{\#}^n_T \to \gamma,\\ 1, &\text{ if }T \vdash \mathrm{\#}^n_T \to \neg \gamma,\\ \uparrow, &\text{ otherwise,} \end{cases}\\ \Delta^T_\gamma(n) &= \mu p.\left(T \vdash_p \mathrm{\#}^n_T \to \gamma \lor T \vdash_p \mathrm{\#}^n_T \to \neg \gamma \right){\kern-1.5pt}. \end{align*} $$

The main fact about the function $\delta ^T_\gamma (x)$ is the following lemma (see [20, lemma 2]), which asserts that $\delta ^T$ provides an indexing of $\{0, 1\}$ -valued partial recursive functions, and there is a translation between $\delta ^T$ -indexes and $\varphi $ -indexes such that the corresponding complexity measures $\Delta ^T$ and $\Phi $ are elementarily related.

Lemma 4.19. For each $\varphi $ -index c for a $\{0,1\}$ -valued partial recursive function there is a $\delta ^T$ -index $\gamma $ such that

$$ \begin{align*} \delta^T_\gamma = \varphi_c \quad \mbox{and} \quad \Delta^T_\gamma \preccurlyeq_{\mathrm{dom}\, \varphi_c} \Phi_c. \end{align*} $$

Conversely, for each $\delta ^T$ -index $\gamma $ there is a $\varphi $ -index c for a $\{0,1\}$ -valued partial recursive function such that

$$ \begin{align*} \varphi_c = \delta^T_\gamma \quad \mbox{and} \quad \Phi_c \preccurlyeq_{\mathrm{dom}\, \delta^T_\gamma} \Delta^T_\gamma. \end{align*} $$

An important observation concerning $\delta $ -indexes is that if $(\cdot )^* \colon \mathfrak {D}_T \to \mathfrak {D}_S$ is a homomorphism, then $\delta ^S_{\gamma ^*}$ is an extension of $\delta ^T_\gamma $ . If, moreover, $(\cdot )^*$ is an isomorphism, then $\delta ^S_{\gamma ^*} = \delta ^T_\gamma $ . So a homomorphism provides certain kind of translation between $\delta ^T$ -indexes and $\delta ^S$ -indexes. Note that, unlike in Lemma 4.19, in this case there is a loss of the information about the size of proofs and, in particular, about the relationship between $\Delta ^S_{\gamma ^*}$ and $\Delta ^T_\gamma $ .

This is where the second crucial idea of Shavrukov comes into play. Namely, to apply a version of Blum’s compression theorem (see [8, theorem 8]) for the model $\delta ^T_\gamma (x)$ and the corresponding complexity measure $\Delta ^T_\gamma (x)$ . The following lemma is a version of Blum’s compression theorem for $\varphi $ and $\Phi $ , which can be translated to $\delta $ and $\Delta $ by means of Lemma 4.19. For the proof see [20, lemma 7] (there it is stated in a weaker form; however, the proof yields a stronger result).

Lemma 4.20. For each cumulative function f with $\mathrm {dom}\, f = X$ there is a $\varphi $ -index b for a $\{0,1\}$ -valued partial recursive function with $\mathrm {dom}\, \varphi _b = X$ such that

$$ \begin{align*} \Phi_b \approx_X f \preccurlyeq_{X \cap \mathrm{dom}\, \varphi_a} \Phi_a, \end{align*} $$

whenever $\varphi _a =_{X \cap \mathrm {dom}\, \varphi _a} \varphi _b$ .

The next lemma is a special case of Lemma 4.20 (see [20, lemma 3]).

Lemma 4.21. For each r.e.set X there is a $\varphi $ -index c for a $\{0,1\}$ -valued partial recursive function such that $\mathrm {dom}\, \varphi _c = X$ and $\Phi _c \preccurlyeq _{X \cap \mathrm {dom}\, \varphi _d} \Phi _d$ , whenever $\varphi _d =_{X \cap \mathrm {dom}\, \varphi _d} \varphi _c$ .

The following lemmas give several basic results about the notion of cumulativity (see [20, lemma 5] and [20, lemma 6]).

Lemma 4.22. For each sentence $\gamma $ the function $\Delta ^T_\gamma $ is cumulative.

Lemma 4.23. If the functions F and G are cumulative, then so is $F \circ G$ .

We now have everything we need to prove the following main theorem, which is one of our mentioned strengthenings of Adamsson’s result.

Theorem 4.24. Let T and S be theories with standard provability predicates $\Box _T$ and $\Box _S$ . If there is an epimorphism from $\mathfrak {D}_T$ onto $\mathfrak {D}_S$ then for each $k \in \mathbb {N}$ there is a function $G(x) \in \mathcal {F}^{k+1}_{S}(\mathsf {EA})$ which is not dominated by any function $F(x) \in \mathcal {F}^k_{T}(T)$ . More specifically, there is an elementary function $q(x)$ such that for each $k \in \mathbb {N}$ , for each function $F(x) \in \mathcal {F}^k_{T}(T)$ the inequality $ F(n) \leqslant \mathscr {R}^{(k+1)}_S(q(n)) $ holds for infinitely many $n \in \mathbb {N}$ .

Proof. We follow Adamsson’s proof (which itself follows Shavrukov’s proof) very closely and make certain changes to obtain sharper bounds. The general line of the proof is unchanged, so we mainly concentrate on the parts where the modifications are made.

Assume there is an epimorphism $(\cdot )^* \colon \mathfrak {D}_T \to \mathfrak {D}_S$ . As usual we consider $(\cdot )^*$ as a mapping on the set of sentences up to provable equivalence (in the respective theories) and write just $A^*$ for an arbitrary representative of the equivalence class $([A]_{\sim _T})^*$ . By Proposition 3.10 it is sufficient to get the conclusion of the theorem for cumulative functions. So fix an arbitrary cumulative function $F(x) \in \mathcal {F}^k_{T}(T)$ . The proof consists of two main parts, which are embodied in the following two inequalities:

$$ \begin{align*} F \circ \Delta^S_\alpha \preccurlyeq_X \Delta^S_\beta \preccurlyeq_Y \mathscr{R}^{(k+1)}_S \circ q \circ \Delta^S_\alpha \end{align*} $$

for certain sentences $\alpha $ and $\beta $ , infinite sets $Y \subseteq X \subseteq \mathbb {N}$ and an elementary function $q(x)$ (which are constructed in the proof), whence the result follows.

Let X be some r.e. nonrecursive set. Fix a $\varphi $ -index c given by Lemma 4.21 for a partial recursive $\{0,1\}$ -valued function such that $X = \mathrm {dom}\, \varphi _c$ and $\Phi _c \preccurlyeq _{X \cap \mathrm {dom}\, \varphi _d} \Phi _d$ , whenever $\varphi _d =_{X \cap \mathrm {dom}\, \varphi _d} \varphi _c$ . Using Lemma 4.19 find a $\delta ^S$ -index $\alpha $ such that $\varphi _c = \delta ^S_\alpha $ and $\Delta ^S_\alpha \preccurlyeq _X \Phi _c$ . Since $(\cdot )^*$ is surjective, there is some sentence A with $A^* = \alpha $ . Fix such a sentence A. This auxiliary set X and the corresponding sentences $\alpha $ and A are needed in order to preserve some part of the information concerning the size of proofs, which otherwise gets lost when we move from T into S using the homomorphism (which is one of the most significant places in the following proof). Since $(\cdot )^*$ is a homomorphism, the function $\delta ^S_\alpha $ is an extension of $\delta ^T_A$ . By the choice of $\alpha $ we have $\Delta ^S_\alpha \preccurlyeq _X \Phi _c \preccurlyeq _{\mathrm {dom}\, \delta ^T_A} \Phi _d \preccurlyeq _{\mathrm {dom}\, \delta ^T_A} \Delta ^T_A$ , where d is some $\varphi $ -index for $\delta ^T_A$ given by Lemma 4.19. Fix some strictly monotone elementary function $p(x)$ such that $\Delta ^S_\alpha \leqslant _{\mathrm {dom}\, \delta ^T_A} p \circ \Delta ^T_A$ .

In order to be able to formalize certain facts about the function $\Delta ^S_\alpha (x)$ inside T we consider the following modified program ( $\Sigma _1$ -formula defining the graph) for this function. Define $\psi (x, y)$ as $\psi '(x, y) \land \forall z < y\, \neg \psi '(x, z)$ , where

$$ \begin{align*} \psi'(x, y) \leftrightharpoons \mathsf{Prf}_S(y, \ulcorner \mathrm{\#}^x_S \to \alpha \urcorner) \lor \mathsf{Prf}_S(y, \ulcorner \mathrm{\#}^x_S \to \neg \alpha \urcorner)\ &\lor\\ \lor\ \exists z \leqslant y\, ( p(z) = y \lor \mathsf{Prf}_T(y, \ulcorner \mathrm{\#}^x_T \to A \urcorner) &\lor \mathsf{Prf}_T(y, \ulcorner \mathrm{\#}^x_T \to \neg A \urcorner) ){\kern-1.5pt}. \end{align*} $$

Informally, $\psi (x, y)$ asserts that y is the least number such that $\Delta ^S_\alpha (x) = y$ or $y = p(z)$ for some z such that $\Delta ^T_A(x) = z$ . Note that $\psi (x, y)$ is an elementary formula.

The inequality $\Delta ^S_\alpha \leqslant _{\mathrm {dom}\, \delta ^T_A} p \circ \Delta ^T_A$ implies that the formula $\psi (x, y)$ indeed defines the graph of $\Delta ^S_\alpha (x)$ in the standard model. Note that (the fact that the least element principle for elementary formulas available in T is used here)

$$ \begin{align*} T \vdash \forall x \left( \exists z \left(p(\Delta^T_A(x)) = z \right) \to \exists y\, \psi(x, y)\right){\kern-1.5pt}, \end{align*} $$

here $p(\Delta ^T_A(x)) = z$ is an elementary formula defining the graph of $p(\Delta ^T_A(x))$ in the most natural way. By the definition of $\psi (x, y)$ we also have

$$ \begin{align*} \mathsf{EA} \vdash \forall x\, \forall y_1\, \forall y_2 ( \psi(x, y_1) \land \psi(x, y_2) \to y_1 = y_2 ){\kern-1.5pt}. \end{align*} $$

Consider the function $F \circ \Delta ^S_\alpha $ , which is cumulative by Lemmas 4.23 and 4.22 and since $F(x)$ is assumed to be cumulative. By Lemma 4.20 there is a $\varphi $ -index b for a partial recursive $\{0,1\}$ -valued function such that $F \circ \Delta ^S_\alpha \approx _X \Phi _b$ and $\Phi _b \preccurlyeq _{X \cap \mathrm {dom}\, \varphi _a} \Phi _a$ , given $\varphi _a =_{X \cap \mathrm {dom}\, \varphi _a} \varphi _b$ .

By Lemma 4.19 there is some $\delta ^S$ -index $\beta $ with $\varphi _b = \delta ^S_\beta $ , whence $F \circ \Delta ^S_\alpha \preccurlyeq _X \Delta ^S_\beta $ which gives us the first of the two main inequalities; however, an arbitrary chosen sentence $\beta $ with this property bears no relationship to the sentence $\alpha $ , and we will not be able to obtain the second inequality, which requires that $\Delta ^S_\beta $ grows not too much faster than $\Delta ^S_\alpha $ . That is why we need a specifically constructed $\delta ^S$ -index $\beta $ for the function $\varphi _b$ in order to be able to formalize in T certain results, which together with the homomorphism yield the desired relationship between $\Delta ^S_\alpha $ and $\Delta ^S_\beta $ .

We define a specific sentence B such that $\Delta ^T_B$ is T-provably related to $\Delta ^T_A$ (the precise meaning of this is given below), whence $\Delta ^T_\beta $ will be S-provably related to $\Delta ^S_\alpha $ , where $\beta = B^*$ . This will allow us to obtain an upper bound on $\Delta ^S_\beta $ in terms of $\Delta ^S_\alpha $ , as required.

By the choice of a $\varphi $ -index b we can fix an elementary function $s(x)$ satisfying $\Phi _b \leqslant _X s \circ F \circ \Delta ^S_\alpha $ . Define the following formula:

$$ \begin{align*} B(x) \leftrightharpoons \exists u \left(s(F(\Delta^S_\alpha(x))) = u \land \Phi_b(x) \leqslant u \right) \to \varphi_b(x) = 0, \end{align*} $$

where we express the relation $s(F(\Delta ^S_\alpha (x))) = u$ by the following $\Sigma _1$ -formula:

$$ \begin{align*} \exists y\, \exists z ( \psi(x, y) \land \chi(y, z) \land \theta(z, u) ){\kern-1.5pt}, \end{align*} $$

where $\theta (x, y)$ is a $\Sigma _1$ -formula defining the graph of $s(x)$ such that $\mathsf {EA} \vdash \forall x\, \exists ! y\, \theta (x, y)$ , and $\chi (x, y)$ is a $\Sigma _1$ -formula given by Lemma 3.9 applied to the function $F(x)$ . In particular, we have $T \vdash \forall x\, \Box ^{(k)}_T(\exists y\, \chi (\underline {x}, y))$ , and

$$ \begin{align*} \mathsf{EA} \vdash \forall x\, \forall y_1\, \forall y_2 (\chi(x, y_1) \land \chi(x, y_2) \to y_1 = y_2){\kern-1.5pt}. \end{align*} $$

Since the witness for $\exists y\, \psi (x, y)$ is also $\mathsf {EA}$ -provably unique by the definition of $\psi (x, y)$ , it follows that

$$ \begin{align*} \mathsf{EA} \vdash \forall x\, \forall u_1\, \forall u_2 \left( \left(s(F(\Delta^S_\alpha(x))) = u_1 \land s(F(\Delta^S_\alpha(x))) = u_2 \right) \to u_1 = u_2 \right){\kern-1.5pt}. \end{align*} $$

Note that we represent the graph of $\Delta ^S_\alpha (x)$ not in the natural way, but using a modified formula $\psi (x, y)$ constructed above. This will become important later when we formalize certain parts of the following argument in T.

Define the sentence $B \leftrightharpoons \forall x (\mathrm {\#}^x_T \to B(x))$ . We claim that $\delta ^T_B =_X \varphi _b$ . Given $n \in X$ , we have $s(F(\Delta ^S_\alpha (n))) = m$ and $\Phi _b(n) \leqslant m$ , for some $m \in \mathbb {N}$ (since $\mathrm {dom}\, \Delta ^S_\alpha = X$ and by the choice of $s(x)$ ), whence the antecedent of $B(\underline {n})$ is true and provable (being a $\Sigma _1$ -sentence) and

$$ \begin{align*} T \vdash B(\underline{n}) \leftrightarrow \varphi_b(\underline{n}) = 0. \end{align*} $$

If $\varphi _b(n) = 0$ , then $T \vdash B(\underline {n})$ , since T proves (a true $\Sigma _1$ -sentence) $\varphi _b(\underline {n}) = 0$ . In this case

$$ \begin{align*} T \vdash \mathrm{\#}^n_T &\to \forall x ( \mathrm{\#}^x_T \to (x = \underline{n} \land B(\underline{n})) )\\ &\to \forall x ( \mathrm{\#}^x_T \to B(x))\\ &\to B, \end{align*} $$

whence $\delta ^T_B(n) = 0$ . If $\varphi _b(n) = 1$ , then $T \vdash \neg B(\underline {n})$ , since T proves (a true $\Sigma _1$ -sentence) $\varphi _b(\underline {n}) = 1$ which implies $\neg (\varphi _b(\underline {n}) = 0)$ . In this case

$$ \begin{align*} T \vdash \mathrm{\#}^n_T &\to (\mathrm{\#}^n_T \land \neg B(\underline{n}) )\\ &\to \exists x ( \mathrm{\#}^x_T \land \neg B(x))\\ &\to \neg B, \end{align*} $$

whence $\delta ^T_B(n) = 1$ . Since $(\cdot )^*$ is a homomorphism, for $\beta = B^*$ we have $\delta ^T_B \subseteq \delta ^S_\beta $ , and so $\varphi _b =_X \delta ^T_B =_X \delta ^S_\beta $ . The choice of b implies that

$$ \begin{align*} F \circ \Delta^S_\alpha \approx_X \Phi_b \preccurlyeq_X \Phi_a \preccurlyeq_X \Delta^S_\beta, \end{align*} $$

where a is a $\varphi $ -index of $\delta ^S_\beta $ given by Lemma 4.19, which gives the first of the two main inequalities $F \circ \Delta ^S_\alpha \preccurlyeq _X \Delta ^S_\beta $ .

In order to obtain an upper bound on $\Delta ^S_\beta $ in terms of $\Delta ^S_\alpha $ we need to formalize in T the relationship between $\Delta ^T_A$ and $\Delta ^T_B$ present in the proof of the claim $\delta ^T_B =_X \varphi _b$ given above. We have the following derivation:

$$ \begin{align*} T \vdash \forall x\, &\Big(\Box_T \left(\mathrm{\#}^x_T \to A \right) \lor \Box_T \left(\mathrm{\#}^x_T \to \neg A \right) \Big.\\&\quad \to \exists z\, (p(\Delta^T_A(x)) = z) \\&\quad \to \exists y\, \psi(x, y)\\&\quad \to \Box^{(k)}_T \exists u \left(s(F(\Delta^S_\alpha(\underline{x}))) = u\right)\\&\quad \to \Box^{(k)}_T (\Box_T B(\underline{x}) \lor \Box_T \neg B(\underline{x}))\\&\quad \to \left. \Box^{(k)}_T \left(\Box_T\left(\mathrm{\#}^x_T \to B\right) \lor \Box_T \left(\mathrm{\#}^x_T \to \neg B\right) \right)\right){\kern-1.5pt}. \end{align*} $$

Let us make some comments on each of the implications above. The first one follows by the definition of $\Delta ^T_A(x)$ (and we use the most natural formalization of it inside T), elementary induction (to get the existence of the least T-proof) and T-provable totality of $p(x)$ (since $p(x)$ is elementary). The second one was discussed right after the definition of $\psi (x, y)$ (this is the place where we need a modified definition of the graph of $\Delta ^S_\alpha (x)$ and not the natural one we used for $\Delta ^T_A(x)$ in order for the formalization to go through). As for the third one, we use provable $\Sigma _1$ -completeness (if $k \geqslant 1$ ), the above property of $\chi _F(x, y)$ and T-provable totality of (an elementary function) $s(x)$ to get

$$ \begin{align*} T \vdash \forall x\, \forall y\, \Bigl( \psi(x, y) \Bigr. &\to \Box^{(k)}_T \left( \psi(\underline{x}, \underline{y}) \land \exists z \left(\chi_F(\underline{y}, z) \right) \right) \\ &\to \left. \Box^{(k)}_T \exists u \left(s(F(\Delta^S_\alpha(\underline{x}))) = u\right)\right){\kern-1.5pt}. \end{align*} $$

The proof of the final implication is unchanged (as compared to the argument above), since it uses only basic predicate logic and provable properties of the formulas $\mathrm {\#}^x_T$ .

Now, for the fourth implication we need to be more careful, since we do not have the facts like $\Phi _B \preccurlyeq _X s \circ F \circ \Delta ^S_\alpha $ and $\mathrm {dom}\, \varphi _b = X$ inside T. In the following argument we rely on the fact that the ternary relation $\Phi _e(x) \leqslant y$ is expressed using an elementary formula. We argue informally under $\Box _T$ as follows. Assume $\exists u \left (s(F(\Delta ^S_\alpha (\underline {x}))) = u \right )$ . Fix such a number u and consider two cases: $\Phi _b(\underline {x}) \leqslant u$ (in this case $\varphi _b(\underline {x})$ is defined) and $\Phi _b(\underline {x})> u$ (in this case it may be that $\varphi _b(\underline {x})$ is undefined). Assume $\Phi _b(\underline {x}) \leqslant u$ , we then have $\exists y \left (\varphi _b(\underline {x}) = y\right )$ . Let us fix such a y and consider two more cases: $y = 0$ or $y \neq 0$ . In the first case we get $\Box _T \left (\varphi _b(\underline {x}) = 0\right )$ using provable $\Sigma _1$ -completeness, whence $\Box _T B(\underline {x})$ follows. In the second case we also use provable $\Sigma _1$ -completeness to get

$$ \begin{align*} \Box_T \left( s(F(\Delta^S_\alpha(\underline{x}))) = \underline{u} \land \Phi_b(\underline{x}) \leqslant \underline{u} \land \varphi_b(\underline{x}) = \underline{y} \land \underline{y} \neq 0 \right){\kern-1.5pt}, \end{align*} $$

which implies $\Box _T\neg B(\underline {x})$ . Now assume $\Phi _b(\underline {x})> u$ . Again, using provable $\Sigma _1$ -completeness we obtain $\Box _T \left ( s(F(\Delta ^S_\alpha (\underline {x}))) = \underline {u} \land \Phi _b(\underline {x})> \underline {u} \right )$ , whence

$$ \begin{align*} \Box_T \forall z \left( s(F(\Delta^S_\alpha(\underline{x}))) = z \to \Phi_b(\underline{x})> z\right){\kern-1.5pt}, \end{align*} $$

which implies $\Box _T \neg B(\underline {x})$ . Here we rely on the fact that

$$ \begin{align*} \Box_T \forall z \left(s(F(\Delta^S_\alpha(\underline{x}))) = z \to z = \underline{u} \right){\kern-1.5pt}, \end{align*} $$

since we have $\Box _T \left (s(F(\Delta ^S_\alpha (\underline {x}))) = \underline {u}\right )$ and by $\mathsf {EA}$ -provable uniqueness of the witness to the formula $\exists u \left (s(F(\Delta ^S_\alpha (x))) = u \right )$ , which was discussed above when it has been defined.

Thus, we have the following:

$$ \begin{align*} T \vdash \forall x\, \Big(\Box_T &\left(\mathrm{\#}^x_T \to A \right) \lor \Box_T \left(\mathrm{\#}^x_T \to \neg A \right) \Big.\\&\quad \to \left. \Box^{(k)}_T \left(\Box_T\left(\mathrm{\#}^x_T \to B\right) \lor \Box_T \left(\mathrm{\#}^x_T \to \neg B\right) \right)\right){\kern-1.5pt}. \end{align*} $$

In particular, for each $n \in \mathbb {N}$ we have

$$ \begin{align*} T \vdash \Box_T \left(\mathrm{\#}^n_T \to A \right) \lor \Box_T \left(\mathrm{\#}^n_T \to \neg A \right) \to \Box^{(k)}_T \left(\Box_T\left(\mathrm{\#}^n_T \to B\right) \lor \Box_T \left(\mathrm{\#}^n_T \to \neg B\right) \right){\kern-1.5pt}. \end{align*} $$

Applying the homomorphism, for each $n \in \mathbb {N}$ we obtain

(†) $$ \begin{align} S \vdash \Box_S \left(\mathrm{\#}^n_S \to \alpha \right) \lor \Box_S \left(\mathrm{\#}^n_S \to \neg \alpha \right) \to \Box^{(k)}_S \left(\Box_S\left(\mathrm{\#}^n_S \to \beta\right) \lor \Box_S \left(\mathrm{\#}^n_S \to \neg \beta\right) \right){\kern-1.5pt}. \end{align} $$

Denote by $j(x)$ the total (by the above) recursive (since S is r.e.) function which maps n to the Gödel number of the least S-proof of the above implication for this n. For each $n \in \mathbb {N}$ we have

$$ \begin{align*} S \vdash_{j(n)} \Box_S \left(\mathrm{\#}^n_S \to \alpha \right) \lor \Box_S \left(\mathrm{\#}^n_S \to \neg \alpha \right) \to \Box^{(k)}_S \left(\Box_S\left(\mathrm{\#}^n_S \to \beta\right) \lor \Box_S \left(\mathrm{\#}^n_S \to \neg \beta\right) \right){\kern-1.5pt}. \end{align*} $$

Since $j(x)$ is total, the set $\{n \in X \mid j(n)> \Delta ^S_\alpha (n)\}$ is recursive: given n, compute $j(n)$ and search for an S-proof of $\mathrm {\#}^n_S \to \alpha $ or $\mathrm {\#}^n_S \to \neg \alpha $ with Gödel number less than $j(n)$ . It follows that the set $Y = \{n \in X \mid j(n) \leqslant \Delta ^S_\alpha (n)\}$ is nonrecursive and, in particular, infinite, since, otherwise, the set

$$ \begin{align*}X = \{n \in X \mid j(n)> \Delta^S_\alpha(n)\} \cup \{n \in X \mid j(n) \leqslant \Delta^S_\alpha(n)\} \end{align*} $$

would be recursive.

Fix an elementary function $u(x)$ given by Lemma 3.11. Let us estimate the Gödel number of an S-proof of $\Box ^{(k)}_S \left (\Box _S\left (\mathrm {\#}^n_S \to \beta \right ) \lor \Box _S \left (\mathrm {\#}^n_S \to \neg \beta \right ) \right )$ for $n \in Y$ . The proof can be obtained as follows: concatenate the proof of implication (†) and its antecedent and apply modus ponens. Let $m(x, y)$ be an elementary function which, given the upper bounds x and y on the proofs of implication and its antecedent, outputs an upper bound on a Gödel number of a proof of the consequent. We may assume $m(x, y)$ to be monotone in both arguments. The Gödel number of the required S-proof is then bounded by

$$ \begin{align*} m(j(n), u(\Delta^S_\alpha(n))) \leqslant m(\Delta^S_\alpha(n), u(\Delta^S_\alpha(n))) \leqslant r(\Delta^S_\alpha(n)), \end{align*} $$

since $j(n) \leqslant \Delta ^S_\alpha (n)$ for $n \in Y$ . Here $r(x)$ is some strictly monotone elementary bound on $m(x, u(x))$ (e.g., $r(x) = 2^x_l$ for some fixed $l \in \mathbb {N}$ ). It is important to note that the function $r(x)$ does not depend on $F(x)$ (and can be fixed ahead of the proof). For each $n \in Y$ we then have

$$ \begin{align*} S \vdash_{r(\Delta^S_\alpha(n))} \Box^{(k)}_S \left(\Box_S\left(\mathrm{\#}^n_S \to \beta\right) \lor \Box_S \left(\mathrm{\#}^n_S \to \neg \beta\right) \right){\kern-1.5pt}, \end{align*} $$

whence $ S \vdash _{\mathscr {R}^{(k)}_S(r(\Delta ^S_\alpha (n)))} \Box _S\left (\mathrm {\#}^n_S \to \beta \right ) \lor \Box _S \left (\mathrm {\#}^n_S \to \neg \beta \right ), $ via the definition of $\mathscr {R}_S(x)$ and Remark 3.5. Let $v(x)$ be an elementary function given by Lemma 3.12. It follows that for each $n \in Y$ ,

$$ \begin{align*} \Delta^S_\beta(n) \leqslant \mathscr{R}_S(v(\mathscr{R}^{(k)}_S(r(\Delta^S_\alpha(n))))), \end{align*} $$

so $\Delta ^S_\beta \preccurlyeq _Y \mathscr {R}_S \circ v \circ \mathscr {R}^{(k)}_S \circ r$ . Finally, combining this inequality with $F \circ \Delta ^S_\alpha \preccurlyeq _X \Delta ^S_\beta $ (which has been proved above) we obtain

$$ \begin{align*} F \circ \Delta^S_\alpha \preccurlyeq_X \Delta^S_\beta \preccurlyeq_Y \mathscr{R}_S \circ v \circ \mathscr{R}^{(k)}_S \circ r \circ \Delta^S_\alpha. \end{align*} $$

Fix an elementary function $t(x)$ (this is the only function on the right-hand side of the following inequality which depends on $F(x)$ ) such that

$$ \begin{align*} F \circ \Delta^S_\alpha \leqslant_Y t \circ \mathscr{R}_S \circ v \circ \mathscr{R}^{(k)}_S \circ r \circ \Delta^S_\alpha. \end{align*} $$

It follows that $F \leqslant _Z t \circ \mathscr {R}_S \circ v \circ \mathscr {R}^{(k)}_S \circ r$ , where $Z = \{ \Delta ^S_\alpha (n) \mid n \in Y\}$ is an infinite set, since the value $\Delta ^S_\alpha (n)$ is a Gödel number of an S-proof of a certain sentence depending on n, so these proofs are all different for distinct values of n.

What is left to show then is that the right-hand side of the above inequality can be dominated by the function $\mathscr {R}^{(k+1)}_S \circ q$ for some fixed elementary function $q(x)$ (which does not depend on the function $F(x)$ ). Let $h(x)$ be an elementary function given by Corollary 3.14. We have $t(\mathscr {R}_S(y)) \leqslant \mathscr {R}_S(h(y))$ for all sufficiently large y, whence

$$ \begin{align*} t(\mathscr{R}_S(v(\mathscr{R}^{(k)}_S(r(n))))) \leqslant \mathscr{R}_S(h(v(\mathscr{R}^{(k)}_S(r(n))))) \end{align*} $$

for all sufficiently large n, since $v(\mathscr {R}^{(k)}_S(r(x)))$ is monotone and unbounded (as a composition of such functions). Define the function $q(x)$ to be $h(v(r(x)))$ . If $k = 0$ , we are done since the right-hand side of the inequality above is $\mathscr {R}_S(q(x))$ . If $k \geqslant 1$ , using the same corollary we get

$$ \begin{align*} h(v(\mathscr{R}^{(k)}_S(r(n)))) \leqslant \mathscr{R}^{(k)}_S(h(r(n))) \end{align*} $$

for all sufficiently large n, since $r(x)$ is strictly monotone. Combining both inequalities above together with monotonicity of $\mathscr {R}_S(x)$ and strict monotonicity of $h(x), v(x)$ and $r(x)$ we get

$$ \begin{align*} t(\mathscr{R}_S(v(\mathscr{R}^{(k)}_S(r(n))))) \leqslant \mathscr{R}^{(k+1)}_S(h(r(n))) \leqslant \mathscr{R}^{(k+1)}_S(h(v(r(n)))) = \mathscr{R}^{(k+1)}_S(q(n)), \end{align*} $$

for all sufficiently large n, as required.

Finally, we have $\mathscr {R}^{(k+1)}_S(q(x)) \in \mathcal {F}^{k+1}_S(\mathsf {EA})$ by Proposition 3.7.

The following corollary contains several sufficient conditions for the non-existence of an epimorphism from $\mathfrak {D}_T$ onto $\mathfrak {D}_S$ , which are more convenient to use in applications of Theorem 4.24.

Corollary 4.25. Each of the following conditions implies that there are no epimorphisms from $\mathfrak {D}_T$ onto $\mathfrak {D}_S$ :

1. (i) $\mathscr {R}^{(k+1)}_S(x) \in \mathcal {F}^k_{T}(T)$ for some $k \in \mathbb {N}$ .

2. (ii) $\mathcal {F}^{k+1}_{S}(\mathsf {EA}) \subseteq \mathcal {F}^k_{T}(T)$ for some $k \in \mathbb {N}$ .

3. (iii) $T \vdash \forall \sigma \in \Sigma _1 \left (\Box ^{(k+1)}_S \sigma \to \Box ^{(k)}_T \sigma \right )$ for some $k \geqslant 1$ , or $T \vdash \forall \sigma \in \Sigma _1 (\Box _S \sigma \to \mathsf {Tr}_{\Sigma _1}(\sigma ) )$ .

Proof. Firstly, we show that condition $({\rm i})$ implies that there are no epimorphisms from $\mathfrak {D}_T$ onto $\mathfrak {D}_S$ . Assuming there is one, let $q(x)$ be an elementary function given by Theorem 4.24. Condition $({\rm i})$ implies that the function $F(x) = \mathscr {R}^{(k+1)}_S(q(x)) + 1$ also belongs to $\mathcal {F}^k_{T}(T)$ , whence, by Theorem 4.24, it cannot dominate the function $\mathscr {R}^{(k+1)}_S(q(x))$ , a contradiction. Condition $({\rm ii})$ implies $({\rm i})$ since, by Proposition 3.7, $\mathscr {R}^{(k+1)}_S(x) \in \mathcal {F}^{k+1}_{S}(\mathsf {EA}) \subseteq \mathcal {F}^k_{T}(T)$ . Finally, $({\rm ii})$ follows from $({\rm iii})$ by the definition of the classes $\mathcal {F}^{k+1}_{S}(\mathsf {EA})$ and $\mathcal {F}^k_{T}(T)$ .

Further we heavily rely on the following observation when applying Corollary 4.25.

Remark 4.26. Points $({\rm ii})$ and $({\rm iii})$ of Corollary 4.25 imply the non-existence of an epimorphism from $(\mathfrak {L}_T, \Box ^{\prime }_T)$ onto $(\mathfrak {L}_S, \Box ^{\prime }_S)$ even when predicates $\Box ^{\prime }_T$ and $\Box ^{\prime }_S$ are not standard, but are $\mathsf {EA}$ -provably equivalent to some standard predicates $\Box _T$ and $\Box _S$ .

Proof. Indeed, in this case points $({\rm ii})$ and $({\rm iii})$ also hold for $\Box _T$ and $\Box _S$ , whence there are no epimorphisms from $(\mathfrak {L}_T, \Box _T)$ onto $(\mathfrak {L}_S, \Box _S)$ . But $(\mathfrak {L}_T, \Box ^{\prime }_T) = (\mathfrak {L}_T, \Box _T)$ and $(\mathfrak {L}_S, \Box ^{\prime }_S) = (\mathfrak {L}_S, \Box _S)$ (we have pure equality here rather than just isomorphism, since $\Box $ and $\Box '$ induce the same operators being provably equivalent), and the result follows for the diagonalizable algebras with non-standard provability predicates.

As can be seen from the proof of Theorem 4.24, it is quite hard to explicitly specify an algebraic property of diagonalizable algebras which ensures non-isomorphism. Nevertheless, Shavrukov has shown that under the assumptions of Theorem 1.1, the algebras $\mathfrak {D}_T$ and $\mathfrak {D}_S$ are not elementarily equivalent. The distinguishing property and a corresponding formula (in the language of diagonalizable algebras) suggested by Shavrukov, however, is not algebraic in nature and is, in fact, a translation of a certain arithmetical fact about partial recursive functions and their indexing by means of a formal theory (cf. Lemma 4.19) into the language of diagonalizable algebras (see [23, theorem 2.11]). The construction of such a translation (the interpretation of $\mathbb {N}$ inside $\mathfrak {D}_T$ ) is highly non-trivial and even more technical than the proof of non-isomorphism theorem. As mentioned in [1] (see the discussion after [1, theorem 25]) the modified proof of Theorem 1.3 also yields $\mathfrak {D}_T \not \equiv \mathfrak {D}_S$ via the same first-order formula as in [23]. Let us check that our further modification also yields the result. Namely, we have the following.

Corollary 4.27. Any of the conditions $({\rm i})$ , $({\rm ii})$ or $({\rm iii})$ of Corollary 4.25 implies that $\mathfrak {D}_T$ and $\mathfrak {D}_S$ are not elementarily equivalent.

Proof. We only sketch the proof, as it is almost the same as that of [23, theorem 2.11]. As in the proof of Corollary 4.25 we see that under the assumption that $({\rm i})$ holds we get that $F(x) \in \mathcal {F}^k_{T}(T)$ , where $F(x) = \mathscr {R}^{(k+1)}_S(q(x)) + 1$ and $q(x)$ is given by Theorem 4.24 (and may be assumed to be cumulative and monotone).

The first-order sentence in the language of diagonalizable algebras which holds in $\mathfrak {D}_T$ but fails in $\mathfrak {D}_S$ is the translation of the following arithmetical assertion (see [23, theorem 2.11] for more details) (A): for every $\delta $ -index $\alpha $ of $h(x)$ there is a $\delta $ -index $\beta $ for an extension of $f(x)$ such that for each $n \in \mathbb {N}$ it is provable (in the theory under consideration) that

$$ \begin{align*} \Box \left(\mathrm{\#}^n \to \alpha \right) \lor \Box \left(\mathrm{\#}^n \to \neg \alpha \right) \to \Box^{(k)} \left(\Box\left(\mathrm{\#}^n \to \beta\right) \lor \Box \left(\mathrm{\#}^n \to \neg \beta\right) \right){\kern-1.5pt}. \end{align*} $$

Here $h(x)$ and $f(x)$ are $\{0, 1\}$ -valued partial recursive functions fixed in advance as follows. The function $h(x)$ is taken to be $\varphi _c$ from the proof of Theorem 4.24, which is obtained by applying Lemma 4.21 to a fixed r.e. nonrecursive set X. The function $f(x)$ is obtained by applying Lemma 4.20 to the cumulative function $F \circ \Delta ^S_\alpha $ , where $\alpha $ is a fixed $\delta ^S$ -index for $\varphi _c$ obtained via Lemma 4.19.

To check that (A) fails in $\mathfrak {D}_S$ one just goes through the second part of the proof of Theorem 4.24. Indeed, aiming at a contradiction, assume that for the specific $\delta ^S$ -index $\alpha $ chosen above there is some $\delta ^S$ -index $\beta $ for an extension of f such that

$$ \begin{align*} S \vdash \Box_S \left(\mathrm{\#}^n_S \to \alpha \right) \lor \Box_S \left(\mathrm{\#}^n_S \to \neg \alpha \right) \to \Box^{(k)}_S \left(\Box_S\left(\mathrm{\#}^n_S \to \beta\right) \lor \Box_S \left(\mathrm{\#}^n_S \to \neg \beta\right) \right){\kern-1.5pt}. \end{align*} $$

for each $n \in \mathbb {N}$ . The proof of Theorem 4.24 then shows that $F(n) \leqslant \mathscr {R}^{k+1}_S(q(n))$ for infinitely many $n \in \mathbb {N}$ , which contradicts our choice of $F(x)$ .

To check that (A) holds in $\mathfrak {D}_T$ one uses the same reasoning as in the first part of the proof of Theorem 4.24. Namely, given an arbitrary $\delta ^T$ -index A of h we construct a $\delta ^T$ -index B of the function f exactly as above, the only difference being the following. The formula $B(x)$ used in the construction of B is now defined as

$$ \begin{align*} B(x) \leftrightharpoons \exists u \left(s(F(p(\Delta^T_A(x)))) = u \land \Phi_b(x) \leqslant u \right) \to \varphi_b(x) = 0, \end{align*} $$

where $s(x)$ is a monotone elementary function with $\Phi _b \leqslant _X s \circ F \circ \Delta ^S_\alpha $ and $p(x)$ is a monotone elementary function with such that $\Delta ^S_\alpha \leqslant _X p \circ \Delta ^T_A$ . The monotonicity of $F(x)$ then yields

$$ \begin{align*}\Phi_b \leqslant_X s \circ F \circ \Delta^S_\alpha \leqslant_X s \circ F \circ p \circ \Delta^T_A, \end{align*} $$

which is sufficient for the rest of the proof to go through.

Although we improved the inequality obtained by Adamsson (cf. Theorem 1.3), one may still ask about the possible strengthening of Theorem 4.24 by replacing $k+1$ on the S-side with k. Namely, by replacing the class $\mathcal {F}^{k+1}_{S}(\mathsf {EA})$ with a more natural class $\mathcal {F}^k_{S}(S)$ , which would be completely symmetric to the class $\mathcal {F}^k_{T}(T)$ present in the statement of the theorem. In the current formulation this is simply not true: take $T = S$ and $\Box _T = \Box _S$ , then every function in $\mathcal {F}^k_{S}(S)$ is dominated by one in $\mathcal {F}^k_{T}(T) = \mathcal {F}^k_{S}(S)$ . But we may weaken the conclusion of the theorem by swapping the quantifiers to the following one: no function in $\mathcal {F}^k_{T}(T)$ dominates each function in $\mathcal {F}^{k+1}_{S}(\mathsf {EA})$ . Can we replace $\mathcal {F}^{k+1}_{S}(\mathsf {EA})$ with $\mathcal {F}^k_{S}(S)$ in this weakened formulation? Below we show that this is not true for $T = \mathsf {EA}^+ + \mathsf {RFN}_{\Sigma _1}(\mathsf {EA}^+)$ and $S = \mathsf {EA}^+ + \mathsf {Rfn}_{\Sigma _1}(\mathsf {EA}^+)$ , which have isomorphic diagonalizable algebras by Theorem 1.2 (being $\mathsf {EA}^+$ -provably $\Sigma _2$ -equivalent), but $\mathcal {F}(T) = \mathcal {E}_5$ contains a function dominating each function in $\mathcal {F}(S) = \mathcal {E}^4$ (and the same also holds for $\mathcal {F}^k_{T}(T)$ and $\mathcal {F}^k_{S}(S)$ for each $k \in \mathbb {N}$ ).

A plausible hypothesis is that the existence of an epimorphism from $\mathfrak {D}_T$ onto $\mathfrak {D}_S$ implies that no function from $\mathcal {F}_{T}(T)$ dominates each function from $\mathcal {F}_{S}(T)$ (and analogously for $k> 1$ ). This condition holds for all known examples of theories with isomorphic algebras and is related to Shavrukov’s isomorphism condition (see Theorem 1.2). In practice, when the isomorphism theorem is applied, the theories turn out to be (at least) $\mathcal {B}(\Sigma _1)$ -coherent. But if T and S are $\Sigma _1$ -coherent (or even $\Sigma _1$ -equivalent provably in T), then we have $\mathcal {F}_{T}(T) = \mathcal {F}_{S}(T)$ by definition of these classes, whence the condition holds. It seems that to find counterexamples to this claim would require new methods for establishing isomorphisms of diagonalizable algebras. Another hint that this claim may be true lies in the proof of the main theorem. Specifically, the place where we first prove (we consider the case $k = 1$ )

$$ \begin{align*} T \vdash \forall x\, \Big(\Box_T \left(\mathrm{\#}^x_T \to A \right) \lor \Box_T &\left(\mathrm{\#}^x_T \to \neg A \right) \Big. \to\\ &\to \left. \Box^{(k)}_T \left(\Box_T\left(\mathrm{\#}^x_T \to B\right) \lor \Box_T \left(\mathrm{\#}^x_T \to \neg B\right) \right)\right){\kern-1.5pt}. \end{align*} $$

and then weaken this to

$$ \begin{align*} T \vdash \Box_T \left(\mathrm{\#}^n_T \to A \right) \lor \Box_T \left(\mathrm{\#}^n_T \to \neg A \right) \to \Box_T \left(\Box_T\left(\mathrm{\#}^n_T \to B\right) \lor \Box_T \left(\mathrm{\#}^n_T \to \neg B\right) \right){\kern-1.5pt}, \end{align*} $$

for each $n \in \mathbb {N}$ . The first derivation establishes the totality of the function $f(x)$ such that $f(\Delta ^T_A(x))$ gives the least T-proof of $\exists y \left (\Delta ^T_B(\underline {x}) = y\right )$ . It seems that not using this fact (or some variation of it) and just instantiating this derivation for each $n \in \mathbb {N}$ leads to the significant loss of information. And we also have that each function in $\mathcal {F}_{S}(T)$ is dominated by one of the forms $\mathscr {R}_S(f(x))$ for some $f(x) \in \mathcal {F}(T)$ (cf. Proposition 3.18).

Question 4.28. Does the existence of an epimorphism from $\mathfrak {D}_T$ onto $\mathfrak {D}_S$ imply that no function from $\mathcal {F}_{T}(T)$ dominates each function from $\mathcal {F}_{S}(T)$ ?

Another question which is also relevant to the above discussion is the following.

Question 4.29. Can “for infinitely many $n \in \mathbb {N}$ ” be replaced with a more natural “for almost all $n \in \mathbb {N}$ ” in the inequality of the main theorem?

5 Applications of the main result

Now, we would like to apply Theorem 4.24 to obtain new examples of theories with non-isomorphic diagonalizable algebras. In practice we apply Corollary 4.25 and also rely on Remark 4.26 after it, when the provability predicate under consideration is not standard (e.g., $\Box _T\Box _T$ ), i.e., in such cases we prove that the non-standard provability predicate is $\mathsf {EA}$ -provably equivalent to a standard one (note that in [1] this issue is not discussed in details).

Firstly, let us obtain the result about non-isomorphism of the algebras $(\mathfrak {L}_T, \Box _T)$ and $(\mathfrak {L}_T, \Box _T\Box _T)$ anticipated by Adamsson in [1], and a more general result of this kind. We start with the following lemma, which is needed to apply Remark 4.26.

Lemma 5.30. For each $k \geqslant 2$ there is a standard provability predicate which is equivalent to $\Box ^{(k)}_T$ provably in $\mathsf {EA}$ .

Proof. Let us consider the case $k = 2$ (the case $k> 2$ being completely analogous). We construct (using a version of Craig’s trick) an elementary axiomatization $\sigma ^2_T(x)$ of T such that

$$ \begin{align*} \mathsf{EA} \vdash \forall \psi \left( \Box_T\Box_T \psi \leftrightarrow \Box_{\sigma^2_T}\psi \right){\kern-1.5pt}, \end{align*} $$

where $\Box _{\sigma ^2_T}\psi $ is $\exists p\, \mathsf {Prf}_{\sigma ^2_T}(p, \ulcorner \psi \urcorner )$ . Define

$$ \begin{align*} \sigma^2_T(x) \leftrightharpoons \exists p, \theta \leqslant x \left( x = \ulcorner \underline{p} = \underline{p} \to \theta \urcorner \land \mathsf{Prf}_T(p, \ulcorner \Box_T\theta \urcorner) \right){\kern-1.5pt}, \end{align*} $$

where $\mathsf {Prf}_T(p, x)$ is a standard proof predicate for (a fixed elementary axiomatization of) T. Firstly, we have

$$ \begin{align*} \mathsf{EA} \vdash \Box_T\Box_T \psi &\to \exists p\, \mathsf{Prf}_T(p, \ulcorner \Box_T \psi \urcorner)\\ &\to \exists p\, \sigma^2_T(\ulcorner \underline{p} = \underline{p} \to \psi \urcorner)\\ &\to \exists p\, \Box_{\sigma^2_T}\left(\underline{p} = \underline{p} \to \psi\right)\\ &\to \Box_{\sigma^2_T}\psi, \end{align*} $$

since, certainly, $\mathsf {EA} \vdash \forall p\, \Box _{\sigma ^2_T}(\underline {p} = \underline {p})$ .

To show the converse we argue as follows. Let us show that we have $\Box _T\Box _T\psi $ for each $\sigma ^2_T$ -axiom $\psi $ of T. Fix p and $\theta $ such that $\psi \leftrightharpoons (\underline {p} = \underline {p} \to \theta )$ and $\mathsf {Prf}_T(p, \ulcorner \Box _T\theta \urcorner )$ . The latter implies $\Box _T\Box _T\theta $ , whence $\Box _T\Box _T \left (\underline {p} = \underline {p} \to \theta \right )$ , i.e., $\Box _T\Box _T \psi $ , by logic. Formalizing this in $\mathsf {EA}$ we get

$$ \begin{align*} \mathsf{EA} \vdash \forall \psi \left( \sigma^2_T(\ulcorner \psi \urcorner) \to \Box_T\Box_T\psi \right){\kern-1.5pt}. \end{align*} $$

As usual, we use $\Pi _2$ -conservativity of the $\Sigma _1$ -collection schema $\mathsf {B}\Sigma _1$ over $\mathsf {EA}$ (see [17, theorem 33] and [5, corollary 4.1]) to strengthen this to

$$ \begin{align*} \mathsf{EA} \vdash \forall \psi \left( \Box_{\sigma^2_T}\psi \to \Box_T\Box_T\psi \right){\kern-1.5pt}. \end{align*} $$

Indeed, due to the formalized deduction theorem it is sufficient to show that

$$ \begin{align*} \mathsf{EA} \vdash \forall z\, \forall \psi \left( \forall i < z\, \sigma^2_T(\ulcorner \psi_i \urcorner) \to \Box_T\Box_T \bigwedge_{i < z} \psi_i \right){\kern-1.5pt}. \end{align*} $$

We have $\mathsf {EA} \vdash \forall z\, \forall \psi \left ( \forall i < z\, \sigma ^2_T(\ulcorner \psi _i \urcorner ) \to \forall i < z\, \Box _T\Box _T\psi _i\right )$ . Using $\Sigma _1$ -collection to get a sequence of proofs and the possibility of concatenating them in $\mathsf {EA}$ we obtain

$$ \begin{align*} \mathsf{EA} + \mathsf{B}\Sigma_1 \vdash \forall z\, \forall \psi \left( \forall i < z\, \Box_T\Box_T\psi_i \to \Box_T \left(\bigwedge_{i < z} \Box_T\psi_i\right) \right){\kern-1.5pt}. \end{align*} $$

Finally, using induction on z (and distributivity of $\Box _T$ over conjunction), which is formalizable in $\mathsf {EA}$ since we have an elementary bound on the corresponding T-proof, we get

$$ \begin{align*} \mathsf{EA} \vdash \forall z\, \forall \psi\, \Box_T \left( \left(\bigwedge_{i < z} \Box_T\psi_i\right) \to \Box_T \bigwedge_{i < z} \psi_i \right){\kern-1.5pt}. \end{align*} $$

Combining the three derivations above we get

$$ \begin{align*} \mathsf{EA} + \mathsf{B}\Sigma_1 \vdash \forall z\, \forall \psi \left( \forall i < z\, \sigma^2_T(\ulcorner \psi_i \urcorner) \to \Box_T\Box_T \bigwedge_{i < z} \psi_i \right){\kern-1.5pt}, \end{align*} $$

whence the same $\Pi _2$ -sentence is provable in $\mathsf {EA}$ , as required.

Corollary 5.31. There are no epimorphisms from $(\mathfrak {L}_T, \Box _T \Box _T)$ onto $(\mathfrak {L}_T, \Box _T)$ .

Proof. The result follows by point $({\rm iii})$ of Corollary 4.25 with $k = 1$ since, clearly,

$$ \begin{align*} \mathsf{EA} \vdash \forall \sigma \in \Sigma_1 \left( \Box_T \Box_T \sigma \to \Box_T \Box_T \sigma \right){\kern-1.5pt}.\\[-32pt] \end{align*} $$

More generally, we have the following result.

Corollary 5.32. For each $n, m \in \mathbb {N}$ if $n> m \geqslant 1$ , then there are no epimorphisms from $(\mathfrak {L}_T, \Box ^{(n)}_T)$ onto $(\mathfrak {L}_T, \Box ^{(m)}_T)$ .

Proof. Using provable $\Sigma _1$ -completeness and $m + 1 \leqslant n$ we get

$$ \begin{align*} \mathsf{EA} \vdash \forall \sigma \in \Sigma_1 \left( \Box^{((m+1)\cdot m)}_T \sigma \to \Box^{(m \cdot n)}_T \sigma \right){\kern-1.5pt}, \end{align*} $$

whence the result follows by point $({\rm iii})$ of Corollary 4.25 with $k = m$ .

Let us note that there is a more algebraic proof of Corollary 5.31 for which the improved upper bound is not needed. It follows already from Adamsson’s results. Indeed, Adamsson showed that there are no epimorphisms from $(\mathfrak {L}_T, \Box ^{(8)}_T)$ onto $(\mathfrak {L}_T, \Box _T)$ (he used $\Box ^{(6)}_T$ but any larger iteration also works). Assuming the existence of an epimorphism $j \colon (\mathfrak {L}_T, \Box _T\Box _T) \to (\mathfrak {L}_T, \Box _T)$ , one can check that $j \circ j \circ j$ would be an epimorphism from $(\mathfrak {L}_T, \Box ^{(8)}_T)$ onto $(\mathfrak {L}_T, \Box _T)$ , a contradiction. In general, if $j \colon (\mathfrak {L}_T, \Box ^{(n)}_T) \to (\mathfrak {L}_T, \Box ^{(m)}_T)$ is an epimorphism with $n> m \geqslant 1$ , then $j^{(k)}$ is an epimorphism from $(\mathfrak {L}_T, \Box ^{(n^k)}_T)$ onto $(\mathfrak {L}_T, \Box ^{(m^k)}_T)$ for each $k \geqslant 1$ , which leads to the contradiction, since for $n> m$ we have $n^k> 6 \cdot m^k$ for some (sufficiently large) $k \in \mathbb {N}$ . The number $6$ here corresponds to Adamsson’s gap between iterated boxes for which there are no such epimorphisms. In this way one can also obtain a proof of Corollary 5.32, we omit the details.

Although Shavrukov’s non-isomorphism condition (Theorem 1.1) is strictly stronger (so the result is weaker) than that of Adamsson (Theorem 1.3), it seems to be more proof-theoretic in nature and more applicable to particular pairs of theories. The application of Adamsson’s condition requires a more thorough analysis of the size of proofs of $\Sigma _1$ -sentences in both theories in order to compare the growth rates of $\mathscr {R}_T(x)$ and $\mathscr {R}_S(x)$ , yet it yields new non-isomorphism results, which are not covered by Theorem 1.1.

The following theorem (as well as point $({\rm iii})$ of Corollary 4.25) provides a stronger proof-theoretic non-isomorphism condition similar in formulation to that of Shavrukov. As noted in [7], the condition of Theorem 1.1 (T-provability of a specific version of the uniform $\Sigma _1$ -reflection principle for S) already follows from a more natural $T \vdash \mathsf {RFN}_{\Sigma _1}(S)$ . This fact can also be proved more directly as follows. By Proposition 3.7 we have $\mathsf {EA}\vdash \forall x\, \Box _S \exists y\,( \mathscr {R}_S(\underline {x}) = y)$ , where $\mathscr {R}_S(x) = y$ is a $\Sigma _1$ -formula defining the graph of $\mathscr {R}_S(x)$ , constructed in the proof of this proposition. Applying $\mathsf {RFN}_{\Sigma _1}(S)$ , which is provable in T, we get $T \vdash \forall x\, \exists y \left (\mathscr {R}_S(x) = y\right )$ , that, by the definition of $\mathscr {R}_S(x)$ , certainly implies the required form of reflection in Theorem 1.1. It turns out that one can replace uniform $\Sigma _1$ -reflection with the local one as the following result shows (note that since the schema $\mathsf {Rfn}_{\Sigma _1}(S)$ , unlike $\mathsf {RFN}_{\Sigma _1}(S)$ , is not finitely axiomatizable, we need to be more precise when claiming its provability in T in the formal context).

Theorem 5.33. If $T \vdash \mathsf {Rfn}_{\Sigma _1}(S)$ and this fact is formalizable as follows

$$ \begin{align*} T \vdash \forall \sigma \in \Sigma_1\, \Box_T \left( \Box_S \sigma \to \sigma \right){\kern-1.5pt}, \end{align*} $$

then there are no epimorphisms from $\mathfrak {D}_T$ onto $\mathfrak {D}_S$ .

Proof. Applying provable $\Sigma _1$ -completeness and the assumption concerning T-provability of $\mathsf {Rfn}_{\Sigma _1}(S)$ twice, we obtain

$$ \begin{align*} T \vdash \forall \sigma \in \Sigma_1 \Bigl( \Box_S \Box_S \sigma \Bigr. &\to \Box_T \Box_S \Box_S \sigma \\ &\to \Box_T\Box_S \sigma\\ &\to \Bigl. \Box_T\sigma \Bigr). \end{align*} $$

Point $({\rm iii})$ of Corollary 4.25 with $k = 1$ then yields the result.

As a corollary we get a family of pairs of theories with the same class of provably total computable functions (since the schema $\mathsf {Rfn}(T)$ of local reflection for T is contained in the extension of T with set of all true $\Pi _1$ -sentences: either $\varphi $ is provable and so is $\Box _T \varphi \to \varphi $ , or $\neg \Box _T \varphi $ is a true $\Pi _1$ -sentence which implies $\Box _T \varphi \to \varphi $ ) but non-isomorphic diagonalizable algebras.

Corollary 5.34. For each $n \geqslant 1$ , there are no epimorphisms from $\mathfrak {D}_{T + \mathsf {Rfn}_{\Sigma _1}(T)}$ onto $(\mathfrak {L}_T, \Box ^{(n)}_T)$ .

Proof. By Theorem 5.33, since $T + \mathsf {Rfn}_{\Sigma _1}(T)$ proves local $\Sigma _1$ -reflection for T with $\Box ^{(n)}_T$ (apply reflection n times) and this is formalizable in $\mathsf {EA}$ .

The following proposition provides another example of this kind.

Proposition 5.35. There are theories U, S and T such that

$$ \begin{align*} \mathfrak{D}_U \not \cong \mathfrak{D}_S \cong \mathfrak{D}_T, \text{ while } \mathcal{F}(U) = \mathcal{F}(S) \neq \mathcal{F}(T). \end{align*} $$

Proof. Consider the following theories:

$$ \begin{align*} U = \mathsf{EA}^+, \quad S = \mathsf{EA}^+ + \mathsf{Rfn}_{\Sigma_1}(\mathsf{EA}^+), \quad T = \mathsf{EA}^+ + \mathsf{RFN}_{\Sigma_1}(\mathsf{EA}^+). \end{align*} $$

Firstly, Corollary 5.34 implies that $\mathfrak {D}_U \not \cong \mathfrak {D}_S$ . The isomorphism $\mathfrak {D}_S \cong \mathfrak {D}_T$ follows from Theorem 1.2, since $T\equiv _{\Sigma _2} S$ (whence also $T \equiv _{\mathcal {B}(\Sigma _1)} S$ ) provably in $\mathsf {EA}^+$ by [6, proposition 5.4], and $\mathsf {EA}^+$ is closed under the $\Sigma _1$ -collection rule by [5, corollary 5.2], so T and S are $\mathcal {B}(\Sigma _1)$ -coherent.

Now, since S is contained in the extension of U with the set of all true $\Pi _1$ -sentences we get $\mathcal {F}(S) = \mathcal {F}(U)$ . It is known (see, e.g., [6, corollary 3.3]) that $\mathcal {F}(S) = \mathcal {F}(U) = \mathcal {E}_4$ and $\mathcal {F}(T) = \mathcal {E}_5$ , so $\mathcal {F}(T) \neq \mathcal {F}(S)$ , where $\mathcal {E}_i$ is the ith class of the Grzegorczyk hierarchy.

The example given in the above proposition also demonstrates that it is not possible to strengthen the statement of the main theorem in a way discussed after Corollary 4.25 (so in a certain sense, it is optimal). Namely, if there is an epimorphism from $\mathfrak {D}_T$ onto $\mathfrak {D}_S$ , then for each $k \in \mathbb {N}$ , no function in $\mathcal {F}^k_{T}(T)$ dominates each function in $\mathcal {F}^k_{S}(S)$ . Indeed, this is not true already for $k = 0$ (and, in fact, for each k) with $T = \mathsf {EA}^+ + \mathsf {RFN}_{\Sigma _1}(\mathsf {EA}^+)$ and $S = \mathsf {EA}^+ + \mathsf {Rfn}_{\Sigma _1}(\mathsf {EA}^+)$ , since $\mathcal {F}^0_{T}(T) = \mathcal {F}(T) = \mathcal {E}_5$ contains a function which dominates each function in $\mathcal {E}_4 = \mathcal {F}(S) = \mathcal {F}^0_{S}(S)$ . The case $k = 0$ may seem to be degenerate, so let us also show that this does not hold for $k = 1$ . We need to find a function $F(x) \in \mathcal {F}_{T}(T)$ which dominates each function in $\mathcal {F}_{S}(S)$ . Let $f(x) \in \mathcal {E}_5$ be a function dominating each function in $\mathcal {E}_4$ (e.g., the diagonal of superexponential function $2^x_x$ ). We claim that $F(x) = \mathscr {R}_S(f(x))$ has the desired property. Indeed, since $S \subseteq T$ provably in $\mathsf {EA}$ we have $\mathcal {F}_{S}(S) \subseteq \mathcal {F}_{T}(T)$ , whence by Proposition 3.7 we have $\mathscr {R}_S(x) \in \mathcal {F}_{T}(T)$ . But then, since $f(x) \in \mathcal {F}(T)$ , we also have $\mathscr {R}_S(f(x)) \in \mathcal {F}_{T}(T)$ (see the proof of Lemma 3.6 for such type of argument), as required. Now, given any $G(x) \in \mathcal {F}_{S}(S)$ , let $g(x)$ be an S-provably total computable function which gives the (Gödel number of the) least S-proof of $\exists y\, \psi _G(\underline {x}, y)$ , where $\psi _G(x, y)$ is a $\Sigma _1$ -definition of the graph of $G(x)$ . By the definition of $\mathscr {R}_S(x)$ , we then have $G(x) \leqslant \mathscr {R}_S(g(x))$ , which is dominated by $\mathscr {R}_S(f(x))$ by the choice of $f(x)$ , since $g(x) \in \mathcal {F}(S) = \mathcal {E}_4$ , and monotonicity of the function $\mathscr {R}_S(x)$ .

Note that in all examples of theories T and S with non-isomorphic diagonalizable algebras considered so far the theories were not provably equiconsistent (in both T and S). The next theorem gives a natural family of $\mathsf {EA}$ -provably $\Pi _1$ -equivalent whence also $\Pi _1$ -coherent theories (cf. Theorem 1.2), since $\mathsf {EA}$ is closed under the $\Sigma _1$ -collection rule by [5, lemma 4.1], with non-isomorphic algebras. Recall that the theory $T_\omega $ is defined as T together with all its finite iterated consistency assertions, i.e., sentences $\neg \Box ^{(n)}_T\bot $ for all $n \in \mathbb {N}$ . By Goryachev’s theorem we have the equivalence $T_\omega \equiv _{\Pi _1} T + \mathsf {Rfn}_{\Sigma _1}(T)$ , which holds provably in $\mathsf {EA}$ (see [6, proposition 6.1]).

Theorem 5.36. There are no epimorphisms from $\mathfrak {D}_{T + \mathsf {Rfn}_{\Sigma _1}(T)}$ onto $\mathfrak {D}_{T_\omega }$ .

Proof. We apply point $({\rm i})$ of Corollary 4.25. By Lemma 3.16 and Proposition 3.7 we have

$$ \begin{align*} \mathscr{R}_{T_\omega}(x) \in \mathcal{F}_{{T_\omega}}(\mathsf{EA}) = \mathcal{F}_{T}(\mathsf{EA}), \end{align*} $$

whence, by Lemma 3.6, $\mathscr {R}^{(2)} _{T_\omega }(x) \in \mathcal {F}^2_{T}(\mathsf {EA}) \subseteq \mathcal {F}_{{T + \mathsf {Rfn}_{\Sigma _1}(T)}}(T + \mathsf {Rfn}_{\Sigma _1}(T))$ , where the inclusion is due to

$$ \begin{align*} \mathsf{EA} \vdash \forall \sigma \in \Sigma_1 \left( \Box_T\Box_T \sigma \to \Box_{T+ \mathsf{Rfn}_{\Sigma_1}} \sigma \right){\kern-1.5pt}.\\[-35pt] \end{align*} $$

Since the non-isomorphism condition is formulated in terms of the reflection function (and the related classes) one may ask about the relationship between such functions for various extensions of a given theory T. For example, in the proof of Theorem 5.36 we see that $\mathscr {R}_{T_\omega }(x)$ has the same growth rate (up to an elementary transformation of the input) as $\mathscr {R}_T(x)$ (and the same holds for any $\Pi _1$ -extension of T, see Lemma 3.16). An easy argument using Proposition 3.7 shows that $\mathscr {R}_{T + \mathsf {Rfn}_{\Sigma _1}(T)}(x)$ dominates each finite iteration of $\mathscr {R}_T(x)$ . The next proposition gives a more precise description of its growth rate.

Proposition 5.37. The function $\mathscr {R}_{T + \mathsf {Rfn}_{\Sigma _1}(T)}(x)$ has the same rate of growth as the diagonal function $\mathscr {R}^{(x+1)}_T(x)$ up to an elementary transformation of the input.

Proof. Firstly, we show that $\mathscr {R}^{(x+1)}_T(x) \leqslant \mathscr {R}_{T + \mathsf {Rfn}_{\Sigma _1}(T)}(q(x))$ for some elementary function $q(x)$ . We use the fact that the proof of Proposition 3.7 is formalizable in $\mathsf {EA}$ , i.e.,

$$ \begin{align*} \mathsf{EA} \vdash \forall z\, \Box_{\mathsf{EA}} \left( \forall x\, \Box^{(z)}_T \exists y \left( \mathscr{R}^{(z)}_T(\underline{x}) = y \right) \right){\kern-1.5pt}, \end{align*} $$

where for each z the formula $\mathscr {R}^{(z)}_T(\underline {x}) = y$ is constructed in a most natural way (to represent z-fold composition of $\mathscr {R}_T(x)$ with itself) using the formula $\psi (x, y)$ defining the graph of $\mathscr {R}_T(x)$ . It follows that

$$ \begin{align*} \mathsf{EA} \vdash \forall z\, \Box_{\mathsf{EA}} \Bigl( \Bigr. \forall x\, \Box^{(z)}_T &\exists y \left( \mathscr{R}^{(z)}_T(\underline{x}) = y \right) \Bigl. \! \Bigr) \to \\ &\to \forall z\,\Box_{\mathsf{EA}} \Box^{(z+1)}_T \exists y \left( \mathscr{R}^{(z+1)}_T(\underline{z}) = y \right)\\ &\to \forall z\,\Box_{T + \mathsf{Rfn}_{\Sigma_1}(T)} \Box^{(z+1)}_T \exists y \left( \mathscr{R}^{(z+1)}_T(\underline{z}) = y \right)\\ &\to \forall z\,\Box_{T + \mathsf{Rfn}_{\Sigma_1}(T)} \exists y \left( \mathscr{R}^{(z+1)}_T(\underline{z}) = y \right){\kern-1.5pt}, \end{align*} $$

whence $\mathsf {EA} \vdash \forall x\,\Box _{T + \mathsf {Rfn}_{\Sigma _1}(T)} \exists y \left ( \mathscr {R}^{(x+1)}_T(\underline {x}) = y \right )$ , so we have $ T + \mathsf {Rfn}_{\Sigma _1}(T) \vdash _{q(x)} \exists y \left ( \mathscr {R}^{(x+1)}_T(\underline {x}) = y \right ) $ for some elementary function $q(x)$ (being provably total in $\mathsf {EA}$ ). Consequently, we obtain $\mathscr {R}^{(x+1)}_T(x) \leqslant \mathscr {R}_{T + \mathsf {Rfn}_{\Sigma _1}(T)}(q(x))$ , as required.

Now, we show that $\mathscr {R}_{T + \mathsf {Rfn}_{\Sigma _1}(T)}(x) \leqslant \mathscr {R}^{(r(x)+1)}_T(r(x))$ for some elementary function $r(x)$ . To obtain this we prove that there is a monotone elementary function $r(x)$ which, given a (Gödel number of a) $T + \mathsf {Rfn}_{\Sigma _1}(T)$ -proof x of a $\Sigma _1$ -sentence $\sigma $ , transforms it into a T-proof $r(x)$ of $\Box ^{z}_T\sigma $ for some $z < x$ . The required inequality then follows by the definition and monotonicity properties of $\mathscr {R}_T(x)$ . We prove that $\mathsf {EA} \vdash \forall z\, A(z)$ , where

$$ \begin{align*} A(z) \leftrightharpoons \forall \psi\, \forall \sigma \in \Sigma_1 \left( \Box_T \left(\bigwedge_{i < z} \left(\Box_T \psi_i \to \psi_i \right) \to \sigma \right) \to \Box_T \Box^{(z)}_T\sigma \right){\kern-1.5pt}. \end{align*} $$

The proof goes by reflexive induction on z (see [19]), i.e., we show that

$$ \begin{align*} \mathsf{EA} \vdash A(0) \land \forall z \left(\Box_{\mathsf{EA}} A(\underline{z}) \to A(z + 1)\right){\kern-1.5pt}, \end{align*} $$

whence $\mathsf {EA} \vdash \Box _{\mathsf {EA}} \forall z\, A(z) \to \forall z\, A(z)$ follows; therefore $\mathsf {EA} \vdash \forall z\, A(z)$ , by Löb’s theorem.

We argue informally in $\mathsf {EA}$ . Clearly, we have $A(0)$ . Now, assuming $\mathsf {EA} \vdash A(\underline {z})$ we derive $A(z+1)$ . Fix an arbitrary $\psi $ and $\sigma $ such that

$$ \begin{align*} T \vdash \bigwedge_{i < z + 1} \left(\Box_T \psi_i \to \psi_i \right) \to \sigma. \end{align*} $$

By $\Sigma _1$ -completeness we get $T \vdash \Box _T \left ( \bigwedge _{i < z + 1} \left (\Box _T \psi _i \to \psi _i \right ) \to \sigma \right )$ . It follows that for each $j < z + 1$ we have

$$ \begin{align*} T \vdash \Box_T \psi_j &\to \Box_T \left( \psi_j \land \left(\bigwedge_{i < z + 1} \left(\Box_T \psi_i \to \psi_i \right) \to \sigma\right)\right)\\ &\to \Box_T \left( \left(\Box_T \psi_j \to \psi_j \right) \land \left(\bigwedge_{i < z + 1} \left(\Box_T \psi_i \to \psi_i \right) \to \sigma\right)\right)\\ &\to \Box_T \left(\left(\bigwedge_{i < z + 1, i \neq j} \left(\Box_T \psi_i \to \psi_i \right) \to \sigma\right)\right)\\ &\to \Box_T\Box^{(z)}_T\sigma, \end{align*} $$

where the last implication uses the reflexive induction hypothesis $\mathsf {EA} \vdash A(\underline {z})$ . We also have the following derivation:

$$ \begin{align*} T \vdash \bigwedge_{i < z + 1} \neg \Box_T \psi_i &\to \left(\bigwedge_{i < z + 1} \left(\Box_T \psi_i \to \psi_i \right) \right)\\ &\to \sigma\\ &\to \Box_T\Box^{(z)}_T\sigma, \end{align*} $$

where we use provable $\Sigma _1$ -completeness for $\sigma \in \Sigma _1$ . Combining this $z + 2$ derivations (by considering $z + 2$ cases) we derive $T \vdash \Box _T\Box ^{(z)}_T\sigma $ , i.e., $T \vdash \Box ^{(z+1)}_T\sigma $ , as required.

Since the deduction theorem can be formalized in $\mathsf {EA}$ there is a strictly monotone elementary function $t(x)$ such that $T + \mathsf {Rfn}_{\Sigma _1}(T)\vdash _x \sigma $ implies for some $\Sigma _1$ -sentences $\psi _0, \dots , \psi _{z-1}$ we have $T \vdash _{t(x)}\bigwedge _{i < z} \left (\Box _T \psi _i \to \psi _i\right ) \to \sigma $ . From $\mathsf {EA}\vdash \forall z\, A(z)$ we obtain a strictly monotone elementary function $s(y)$ with $T \vdash _y \bigwedge _{i < z} \left (\Box _T \psi _i \to \psi _i\right ) \to \sigma $ implies $T \vdash _{s(y)} \Box ^{(z)}_T \sigma $ .

Finally, we define $r(x) = s(t(x)) + 1$ (to get $r(x)> x$ ) and obtain the following:

$$ \begin{align*} T + \mathsf{Rfn}_{\Sigma_1}(T)\vdash_x \sigma \Longrightarrow T \vdash_{r(x)} \Box^{(z)}_T\sigma, \end{align*} $$

for some $z < x$ (since the number of axioms of $T + \mathsf {Rfn}_{\Sigma _1}(T)$ in the proof is less than its Gödel number). Thus, by the definition of $\mathscr {R}_T(x)$ , we get that the least witness to $\sigma $ is bounded by $\mathscr {R}^{(z+1)}_T(r(x)) \leqslant \mathscr {R}^{(r(x)+1)}(r(x))$ . The last inequality is obtained as follows. Using Proposition 3.8 fix some $c \in \mathbb {N}$ such that $x \leqslant \mathscr {R}_T(x)$ for all $x \geqslant c$ . It follows that for each $y \geqslant 1$ we have $x \leqslant \mathscr {R}^{(y)}_T(x)$ for all $x \geqslant c$ . Since we may assume $r(x) \geqslant c$ for all x (otherwise, consider $r(x) + c$ ), and $z < x < r(x)$ we get $r(x) \leqslant \mathscr {R}^{(r(x) + 1 - z)}(r(x))$ , whence, by monotonicity of $\mathscr {R}_T(x)$ , the required inequality follows.

This proposition may be contrasted with [7, lemma 3.7], asserting that we have $ \mathsf {EA} \vdash \forall x\, \exists y \left (f^{(x+1)}(x) = y\right ) \leftrightarrow \mathsf {RFN}_{\Sigma _1}(\mathsf {EA} + \forall x\, \exists y (f(x) = y )), $ for any elementarily honest function $f(x)$ .

Let us also note that the proof above establishes the following equivalence:

$$ \begin{align*} \mathsf{EA} \vdash \forall \sigma \in \Sigma_1 \left( \Box_{T + \mathsf{Rfn}_{\Sigma_1}(T)}\sigma \leftrightarrow \exists z\, \Box_T\Box_T^{(z)}\sigma\right){\kern-1.5pt}. \end{align*} $$

As an immediate corollary we obtain the equivalence between two times iterated local $\Sigma _1$ -reflection for T with standard provability predicate $\Box _T$ and a local $\Sigma _1$ -reflection for T with provability predicate $\exists z\, \Box _T \Box ^{(z)}_T \varphi $ (which roughly corresponds to the provability with Parikh’s rule; see [6, lemma 10.2]).

6 Bimodal diagonalizable algebras

As has been already mentioned after the proof of the main theorem, the first-order property demonstrating the lack of elementary equivalence between $\mathfrak {D}_T$ and $\mathfrak {D}_S$ found by Shavrukov is not entirely algebraic in its form and relies on the existence of a quite complicated translation from the language of $\mathbb {N}$ into that of $\mathfrak {D}_T$ given in [23].

By enriching the signature of a diagonalizable algebra with new constants or operators one may hope to find a property distinguishing $\mathfrak {D}_T$ and $\mathfrak {D}_S$ , which is more algebraic in nature and provides an easier way to obtain non-isomorphism results. The work in this direction has been done by Beklemishev [3], who showed that the diagonalizable algebras of $\mathsf {EA}$ and $\mathsf {PA}$ enriched with constants for (a $\Pi _2$ -sentence which axiomatizes) the uniform $\Sigma _1$ -reflection schema for a theory are not elementarily equivalent, whence not isomorphic. In [3] Beklemishev also showed that $\mathsf {RFN}_{\Sigma _1}(T)$ is definable by a formula of second order propositional provability logic (it is not definable in the language of $\mathfrak {D}_T$ by the results of [22], since $\mathsf {RFN}_{\Sigma _1}(T)$ is not equivalent to a Boolean combination of $\Sigma _1$ -sentences (see, e.g., [7, proposition 2.16])) and constructed a simple example of such formula that distinguishes $\mathsf {EA}$ and $\mathsf {PA}$ . Note that in this example we have $\mathfrak {D}_{\mathsf {EA}} \not \cong \mathfrak {D}_{\mathsf {PA}}$ (by Theorem 1.1), so the enriched signature here allows to obtain an easier non-isomorphism proof for expansions, but the reducts (to the language of diagonalizable algebras) are already non-isomorphic.

In this section we enrich the signature of diagonalizable algebras with a new modality $[1]$ , which is interpreted as $1$ -provability, and consider an expansion of the algebra $\mathfrak {D}_T$ to a bimodal diagonalizable algebra $(\mathfrak {D}_T, [1]_T)$ . In our proofs we rely on certain descriptions of the set $\mathcal {C}_T$ of sentences, which are provably 1-provable in a given theory T, obtained in [11]. Recall a more general notation

$$ \begin{align*} C_S(T) = \{\varphi \mid T \vdash [1]_S \varphi \} \end{align*} $$

for the set of all sentences which are T-provably 1-provable in S used in [11].

We provide several examples of pairs of theories which, unlike in Beklemishev’s example, have isomorphic diagonalizable algebras, but non-isomorphic bimodal diagonalizable algebras. We start with a quite natural pair of theories with such algebras.

Proposition 6.38. The bimodal algebras $(\mathfrak {D}_{\mathsf {I}\Sigma _1}, [1]_{\mathsf {I}\Sigma _1})$ and $(\mathfrak {D}_{\mathsf {PRA}}, [1]_{\mathsf {PRA}})$ are not isomorphic, while the reducts $\mathfrak {D}_{\mathsf {I}\Sigma _1}$ and $\mathfrak {D}_{\mathsf {PRA}}$ are isomorphic.

Proof. By Parsons’ theorem $\mathsf {I}\Sigma _1 \equiv _{\Pi _2} \mathsf {PRA}$ , and this result is known to hold provably in $\mathsf {EA}^+$ , which is closed under the $\Sigma _1$ -collection rule by [5, corollary 5.2], whence these two theories are $\mathcal {B}(\Sigma _1)$ -coherent. Theorem 1.2 then implies $\mathfrak {D}_{\mathsf {I}\Sigma _1} \cong \mathfrak {D}_{\mathsf {PRA}}$ .

Aiming at a contradiction, assume $(\cdot )^* \colon (\mathfrak {L}_{\mathsf {I}\Sigma _1}, \Box _{\mathsf {I}\Sigma _1}, [1]_{\mathsf {I}\Sigma _1}) \to (\mathfrak {L}_{\mathsf {PRA}}, \Box _{\mathsf {PRA}}, [1]_{\mathsf {PRA}})$ is an isomorphism. Consider the filters defined in these algebras by the formula $F(p) \leftrightharpoons [1] p = \top $ . These are precisely the sets $\mathcal {C}_{\mathsf {I}\Sigma _1}$ and $\mathcal {C}_{\mathsf {PRA}}$ of provably 1-provable sentences (their equivalence classes) in each theory. By the results of [11] the filter $\mathcal {C}_{\mathsf {PRA}} = C_{\mathsf {PRA}}(\mathsf {PRA})$ is generated by $\mathsf {Rfn}(\mathsf {PRA})$ over $\mathsf {PRA}$ (apply [11, corollary 3.3], [11, lemma 4.1] and the axiomatization of $\mathsf {PRA}$ given by [7, proposition 3.9]), i.e., by the elements of the form $\Box _{\mathsf {PRA}} \psi \to \psi $ , while $\mathcal {C}_{\mathsf {I}\Sigma _1} = C_{\mathsf {I}\Sigma _1}(\mathsf {I}\Sigma _1)$ is not, being generated by $\mathsf {Rfn}(\mathsf {I}\Sigma _1)_\omega $ (see [11, corollary 5.3]). Since the set of all instances of the local reflection schema and the filter are definable in the language of bimodal algebra, the generation property must be preserved by an isomorphism, which is a contradiction.

More formally, assume $\varphi \in \mathcal {C}_{\mathsf {I}\Sigma _1}$ , i.e., $\mathsf {I}\Sigma _1 \vdash [1]_{\mathsf {I}\Sigma _1} \varphi $ . By the isomorphism, there is a $\chi $ such that $\mathsf {PRA} \vdash [1]_{\mathsf {PRA}} \chi $ and $(\chi )^* = \varphi $ . In particular, $\chi \in \mathcal {C}_{\mathsf {PRA}}$ , so for some $n \in \mathbb {N}$ there are sentences $\psi _0$ , $\dots $ , $\psi _{n-1}$ , such that

$$ \begin{align*} \mathsf{PRA} \vdash \bigwedge_{i < n} (\Box_{\mathsf{PRA}} \psi_i \to \psi_i) \to \chi. \end{align*} $$

Applying the isomorphism, we get

$$ \begin{align*} \mathsf{I}\Sigma_1 \vdash \bigwedge_{i < n} (\Box_{\mathsf{I}\Sigma_1} (\psi_i)^* \to (\psi_i)^*) \to \varphi, \end{align*} $$

whence $\mathsf {I}\Sigma _1 + \mathsf {Rfn}(\mathsf {I}\Sigma _1) \vdash \varphi $ . It follows that $\mathcal {C}_{\mathsf {I}\Sigma _1 }$ is generated by $\mathsf {I}\Sigma _1 + \mathsf {Rfn}(\mathsf {I}\Sigma _1 )$ , which contradicts the fact that it is generated by $\mathsf {Rfn}(\mathsf {I}\Sigma _1)_\omega $ and, in particular, contains $\mathsf {Rfn}(\mathsf {I}\Sigma _1 + \mathsf {Rfn}(\mathsf {I}\Sigma _1))$ .

Let us note that the non-isomorphism part of Proposition 6.38 is proved by isolating a natural algebraic property, which is relatively easy to formulate (however, we do not claim it to be definable in the language of bimodal diagonalizable algebras): the filter defined by the identity $[1]\theta = \top $ is generated by the elements of the form $\Box \psi \to \psi $ (i.e., there is some finite conjunction of such elements below any given element of this filter).

The above proof also goes through for the pair $S = \mathsf {EA} + \mathsf {Rfn}_{\Sigma _1}(\mathsf {EA})$ and $T = \mathsf {EA} + \mathsf {Rfn}_{\Sigma _2}(\mathsf {EA})$ . The theories S and T are $\mathcal {B}(\Sigma _1)$ -equivalent provably in $\mathsf {EA}$ (see [7, theorem 6]), whence they are $\mathcal {B}(\Sigma _1)$ -coherent, since $\mathsf {EA}$ is closed under the $\Sigma _1$ -collection rule by [5, lemma 4.1]. By the results of [11], we have $\mathcal {C}_S \equiv S + \mathsf {Rfn}(S)$ and $\mathcal {C}_T \equiv T + \mathsf {Rfn}(T + \mathsf {Rfn}(T))$ (see [11, theorem 1]). Note that the above argument relies on the fact that $\mathcal {C}_S$ is generated by local reflection $\mathsf {Rfn}(S)$ (which is definable as a subset of the diagonalizable algebra), and it does not seem to work in case, when $\mathcal {C}_S$ is generated by iterated reflection, e.g., $\mathsf {Rfn}(S + \mathsf {Rfn}(S))$ , and not just $\mathsf {Rfn}(S)$ .

In the following theorem and its corollary we show, however, that even when $\mathcal {C}_S$ contains iterated local reflection it is still possible to obtain the analogue of Proposition 6.38 (or rather the example considered after the proposition). The corollary provides a family of natural pairs of theories with isomorphic diagonalizable algebras, but non-isomorphic bimodal diagonalizable algebras.

We still employ the idea of comparing the filters $\mathcal {C}_S$ and $\mathcal {C}_T$ in terms of the amount of local reflection contained in them. Now, however, the plan is to consider diagonalizable algebras of theories $\mathcal {C}_T = C_T(T)$ and $\mathcal {C}_S = C_S(S)$ instead of the bimodal algebras of T and S, and to apply (a strengthened version of) Shavrukov’s non-isomorphism theorem, i.e., Theorem 5.33. The first part of this plan is contained in the following lemma.

Lemma 6.39. Any epimorphism $(\cdot )^* \colon (\mathfrak {L}_T, \Box _T, [1]_T) \to (\mathfrak {L}_S, \Box _S, [1]_S)$ induces an epimorphism from $(\mathfrak {L}_{\mathcal {C}_T}, \Box _T[1]_T)$ onto $(\mathfrak {L}_{\mathcal {C}_S}, \Box _S[1]_S)$ .

Proof. The Lindenbaum algebra $\mathfrak {L}_{\mathcal {C}_T}$ is (isomorphic to) a quotient of $\mathfrak {L}_T$ by the filter $\mathcal {C}_T$ . Firstly, we show that the operation $\Box _T[1]_T$ is well-defined on $\mathfrak {L}_{\mathcal {C}_T}$ . For all sentences $\varphi $ and $\psi $ we have

$$ \begin{align*} \mathcal{C}_T \vdash \varphi \leftrightarrow \psi \Rightarrow T \vdash [1]_T \left(\varphi \leftrightarrow \psi\right) &\Rightarrow T \vdash \Box_T[1]_T \varphi \leftrightarrow \Box_T[1]_T \psi \\ &\Rightarrow \mathcal{C}_T \vdash \Box_T[1]_T \varphi \leftrightarrow \Box_T[1]_T \psi, \end{align*} $$

since $T \subseteq \mathcal {C}_T$ . The predicate $\Box _T[1]_T$ is a provability predicate for $\mathcal {C}_T$ , so $(\mathfrak {L}_{\mathcal {C}_T}, \Box _T[1]_T)$ is a diagonalizable algebra of $\mathcal {C}_T$ , and likewise for $\mathcal {C}_S$ .

Since $(\cdot )^*$ is a homomorphism, for all sentences $\varphi $ and $\psi $ we have

$$ \begin{align*} \mathcal{C}_T \vdash \varphi \leftrightarrow \psi \Rightarrow T \vdash [1]_T \left(\varphi \leftrightarrow \psi\right) \Rightarrow S \vdash [1]_S\left(\varphi^* \leftrightarrow \psi^*\right) \Rightarrow \mathcal{C}_S \vdash \varphi^* \leftrightarrow \psi^*, \end{align*} $$

so $(\cdot )^*$ is well-defined on $\mathfrak {L}_{\mathcal {C}_T}$ . Since $S \subseteq \mathcal {C}_S$ we also have that $(\cdot )^*$ is an epimorphism from $\mathfrak {L}_{\mathcal {C}_T}$ onto $\mathfrak {L}_{\mathcal {C}_S}$ , which preserves the composition of boxes $\Box [1]$ . Thus, we obtain an epimorphism from $(\mathfrak {L}_{\mathcal {C}_T}, \Box _T[1]_T)$ onto $(\mathfrak {L}_{\mathcal {C}_S}, \Box _S[1]_S)$ .

Theorem 6.40. Let T and S be such that $\mathcal {C}_T \vdash \mathsf {Rfn}_{\Sigma _1}(\mathcal {C}_S)$ , provably in $\mathcal {C}_T$ . Then there are no epimorphisms from $(\mathfrak {D}_T, [1]_T)$ onto $(\mathfrak {D}_S, [1]_S)$ .

Proof. Lemma 6.39 implies that it is sufficient to show that there are no epimorphisms from $(\mathfrak {L}_{\mathcal {C}_T}, \Box _T[1]_T)$ onto $(\mathfrak {L}_{\mathcal {C}_S}, \Box _S[1]_S)$ , which immediately follows from Theorem 5.33 and the assumption, since the predicate $\Box _T[1]_T$ is $\mathsf {EA}$ -provably equivalent to a standard one, which can be proved exactly the same as in Lemma 5.30 (since $[1]_T$ also satisfies Löb’s derivability conditions provably in $\mathsf {EA}$ ), and likewise for S.

Corollary 6.41. Let T be $U + \mathsf {Rfn}_{\Sigma _2}(U)$ and S be $U + \mathsf {Rfn}_{\Sigma _1}(U)$ for some theory U. Then there are no epimorphisms from $(\mathfrak {D}_T, [1]_T)$ onto $(\mathfrak {D}_S, [1]_S)$ , while $\mathfrak {D}_T \cong \mathfrak {D}_S$ .

Proof. The isomorphism part follows from the fact that, just as in the example above, T and S are $\mathcal {B}(\Sigma _1)$ -equivalent provably in $\mathsf {EA}$ by [7, theorem 6], whence $\mathfrak {D}_T \cong \mathfrak {D}_S$ by Theorem 1.2.

The other part is covered by Theorem 6.40 as follows. We show that

(⋆) $$ \begin{align} \mathsf{EA} \vdash \forall \sigma \in \Sigma_1 \left( \Box_T[1]_T \left(\Box_S[1]_S \sigma \to \sigma \right) \right){\kern-1.5pt}. \end{align} $$

Firstly, note that $\mathsf {EA} \vdash \forall \psi \left ( \Box _S\psi \to \Box _T\psi \right )$ and

$$ \begin{align*} \mathsf{EA} \vdash \forall \varphi \left(\Box_S[1]_S\varphi \to \Box_U[1]_S\varphi\right){\kern-1.5pt}. \end{align*} $$

Indeed, formalize the following argument in $\mathsf {EA}$ . Assume $S \vdash [1]_S \varphi $ , i.e., $U + \mathsf {Rfn}_{\Sigma _1}(U) \vdash [1]_S\varphi $ . It follows that $U + \mathsf {RFN}_{\Sigma _1}(U) \vdash [1]_S \varphi $ , so $U \vdash \neg [1]_U \bot \to [1]_S \varphi $ . But also $U \vdash [1]_U \bot \to [1]_S \varphi $ , since $\mathsf {EA} \vdash \forall \psi \left (\Box _U \psi \to \Box _S \psi \right )$ . Thus, we have $U \vdash [1]_S$ , as required.

Now, we obtain (⋆) by formalizing the following argument. Fix an arbitrary $\Sigma _1$ -sentence $\sigma $ . In the following derivations we use the facts proved above and provable $\Sigma _2$ -completeness of $[1]_T$ ,

$$ \begin{align*} U + \mathsf{Rfn}_{\Sigma_2}(U) \vdash \Box_S[1]_S \sigma &\to \Box_U[1]_S\sigma\\ &\to [1]_S\sigma\\ &\to [1]_T\sigma\\ &\to [1]_T \left(\Box_S[1]_S \sigma \to \sigma\right),\\ \vdash \neg \Box_S[1]_S \sigma &\to [1]_T\neg \Box_S [1]_S\sigma\\ &\to [1]_T \left(\Box_S[1]_S \sigma \to \sigma\right){\kern-1.5pt}, \end{align*} $$

whence $T \vdash [1]_T \left (\Box _S[1]_S \sigma \to \sigma \right )$ , as required.

As was discussed above, besides the example $S = \mathsf {EA} + \mathsf {Rfn}_{\Sigma _1}(\mathsf {EA})$ and $T = \mathsf {EA} + \mathsf {Rfn}_{\Sigma _2}(\mathsf {EA})$ , where $\mathcal {C}_S$ is generated by $\mathsf {Rfn}(S)$ , Corollary 6.41 applies in the case when $\mathcal {C}_S$ contains iterated reflection. For instance, if we take $U = \mathsf {I}\Sigma _1$ , we have $\mathcal {C}_S \equiv \mathsf {Rfn}(S)_\omega $ and $\mathcal {C}_T \equiv \mathsf {Rfn}(T)_{\omega + 1}$ (see [11, theorem 1]).

Finally, let us mention the following possible direction of research. Instead of enriching the signature of diagonalizable algebra we can consider its various substructures. Several fragments of diagonalizable algebra of a given theory have been studied in the literature. One example of that is the work [13] of Lindström and Shavrukov where the decidability of the $\forall ^*\exists ^*$ -fragment of the lattice of $\Sigma _1$ -sentences modulo T-provable equivalence is established. Another example is given by the recent study of the so-called relative provability degrees [2], where the authors study the properties of the lattice of all true $\Pi _2$ -sentences modulo T-provable equivalence. Let us note that formulations of many results in [2] and the methods used to obtain the proofs are computability-theoretic in nature and similar to those used for studying the degree structures in computability theory. This is mainly based on the fact that $\Pi _2$ -sentences can be seen as asserting the totality of computable functions and vice versa. As has been noted by Shavrukov, some results of [2] have quite natural proof-theoretic reformulations and can be established using known results and methods of proof theory and provability logic (e.g., [2, theorem 5.1] is an immediate corollary of the Gödel–Rosser theorem). Several operators acting on this lattice are introduced in this work, namely, skip $\varphi \mapsto \Diamond _T \varphi $ , hop $\varphi \mapsto \varphi \land \Diamond _T\varphi $ and jump $\varphi \mapsto \langle 1 \rangle _T \varphi $ . Here we highlight one of the open questions formulated in that work (see [2, question 10.9]).

Question 6.42. To what extent, if any, does the structure of the provability degrees depend on the underlying theory T? Are these structures isomorphic for different theories?