Proof (sketch)

Clearly, it is sufficient to prove the claim for $\Delta _0(\exp )$ -formulas. In the proof of [Reference Hájek and Pudlák10, lemma 1.30], which is essentially due to [Reference Gaifman and Dimitracopoulos9] (see also [Reference Beklemishev4, 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 [Reference Hájek and Pudlák10, definition 3.12]).

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 [Reference Adamsson1, lemma 3(a)] and [Reference Shavrukov20, lemma 4].

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.

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.

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}$ .

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.

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.

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 $ .

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.

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}$ .

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.

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.

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.

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.

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$ .

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.

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)$ .

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.

Proof. We only sketch the proof, as it is almost the same as that of [Reference Shavrukov23, 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 [Reference Shavrukov23, 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.

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)$ ?

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?

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 [Reference Paris, Pacholsky, Wierzejewski and Wilkie17, theorem 33] and [Reference Beklemishev5, corollary 4.1]) to strengthen this to