Semi-honest subrecursive degrees and the collection rule in arithmetic

Semi-honest subrecursive degrees and the collection rule in arithmetic Andrés Cordón-Franco1 · F. Félix Lara-Martín1 Abstract By a result of L.D. Beklemishev, the hierarchy of nested applications of the 1-collection rule over any 2-axiomatizable base theory extending Elementary Arithmetic collapses to its first level. We prove that this result cannot in general be extended to base theories of arbitrary quantifier complexity. In fact, given any recursively enumerable set of true 2-sentences, S, we construct a sound (2∨2)- axiomatized theory Textending Ssuch that the hierarchy of nested applications of the 1-collection rule over Tis proper. Our construction uses some results on subrecursive degree theory obtained by L. Kristiansen. Keywords Fragments of Peano arithmetic ·Collection rule ·Provably total computable functions ·Subrecursive degrees Mathematics Subject Classification 03F30 ·03D20 1 Introduction In this paper we give an application of the subrecursive degree theory to the study of fragments of Peano Arithmetic. Namely, given any recursively enumerable set of true 2-sentences, S, we construct a sound (2∨2)-axiomatized theory TSsuch that TSextends Sand the hierarchy of nested applications of the 1-collection rule over TSis strict. In his thorough investigation of inference rules in arithmetic [4,5], L.D. Beklemishev proved that the hierarchy of nested applications of the 1-collection rule collapses to its first level for any 2-axiomatizable base theory and hence our result BAndrés Cordón-Franco [email protected] F. Félix Lara-Martín f[email protected] 1Dpto. Ciencias de la Computación e Inteligencia Artificial, Universidad de Sevilla, C/ Tarfia s/n, 41012 Sevilla, Spain 164 A. Cordón-Franco, F. F. Lara-Martín shows that Beklemishev’s collapse theorem cannot in general be extended to base theories of arbitrary quantifier complexity. Interestingly, the theories TS we construct have a clear computational content, and for their construction we make use of a number of results on subrecursive degree theory obtained by L. Kristiansen [17, 18]. Subrecursive degrees are partitions of computable functions generated by strong reducibility orderings, such as “being primitive recursive in” or “being elementary in.” The study of subrecursive degrees dates back to the 1970s as a response to the fundamental problem of classifying all computable functions into hierarchies, see, e.g., the work of Basu [3], Meyer and Ritchie [24] and Machtey [21–23]. In these papers the authors considered the notion of an honest subrecursive class and investigated the structure of different systems of honest subrecursive classes by means of traditional computability-theoretic machinery. Some 20 years later, Kristiansen [16, 17] introduced the so-called honest elementary degrees. These degrees are the equivalence classes induced on the set of honest functions by the reducibility relation “being elementary in,” where a computable function f : ω → ω is said to be honest if it is monotone, dominates 2x and has an elementary graph. Let us observe that Kristiansen’s definition of an honest function is different from, but essentially equivalent to, the one considered in the 1970s. The honest elementary degrees can thus be seen as a reformulation of the elementary-honest classes of Meyer and Ritchie [24]. But Kristiansen’s approach possesses a clear technical advantage. By the so-called Growth Theorem, if f and g are honest functions then f is elementary in g if, and only if, there is k ∈ ω such that f is bounded by the k-th iterate of g (i.e. f (x) ≤ gk(x).) Using this fundamental fact, Kristiansen was able to establish the basic properties of the honest elementary degrees in a particularly concise manner avoiding the use of more complicated methods from Computability Theory. On top of the honest degrees, Kristiansen [18] also considered the semi-honest subrecursive degrees. These are the equivalence classes induced on the set of semihonest functions by the reducibility relation “being compositional in,” where for a function f to be semi-honest we only require that f (x) ≥ 2x and that f has elementary graph (in other words, we eliminate the monotonicity condition on f .) In addition to its clear recursion-theoretic interest, the investigation of the semi-honest subrecursive degrees was also motivated by their connections to formal theories of arithmetic. It is well-known that there is a tight relationship between the semi-honest degrees and the set of the 2-sentences true in the standard model of arithmetic; and that this relationship establishes a good correspondence between recursion-theoretical and arithmetical objects. Of special interest to us will be the fact that subrecursive operators acting on the semi-honest degrees correspond to applications of inference rules in formal arithmetic. In sections 4 and 5 of [4], Beklemishev describes in detail this correspondence and, as a salient application, in Theorem 6.1 of [5] he uses a recursion-theoretic construction to produce arithmetic theories which are not closed under the 1-collection rule. Building on Beklemishev’s work, in section 6 of [18] Kristiansen also gives a detailed account of this correspondence and he obtains some interesting arithmetical consequences of his degree-theoretic results. In particular, Kristiansen derives a couple of results comparing the proof-theoretic strength of the 1-collection rule and Semi-honest subrecursive degrees and the collection rule 165 the 1-induction rule in arithmetic. More recently, Kristiansen, Schlage-Puchta and Weiermann [20] introduced the honest α-elementary degrees, where αis an ordinal ≤ 0, and they showed that these subrecursive degrees are tightly connected to provability in Peano Arithmetic PA. As a matter of fact, in the final section of [20] the authors give an example of the type of applications to (un)provability in PAthat the study of this degree structure could have. In a similar vein, in [9] M. Cai introduced the degree structure of the provability degrees, which measure the proof-theoretic strength of arithmetic statements asserting the totality of given computable functions. The present paper is a new contribution to this line of research. We show that (a small modification of) a degree-theoretic construction of Kristiansen [18] allows us to extract interesting consequences on the proof-theoretic strength of the 1-collection rule. In order to state in a precise manner the problem we are interested in and the obtained results, let us introduce some terminology and basic notions on first-order arithmetic. (We assume familiarity with fragments of Peano Arithmetic, all relevant information and full technical background can be found in [14].) We work in the language L= {0,1,+,·,≤,2x}which extends the usual language of first order arithmetic with a unary function symbol for the function 2x.Elementary formulas (or 0-formulas) are bounded formulas in the language L.nand n-formulas are obtained from 0-formulas by adding a quantifier prefix in the standard way. Our basic fragment of arithmetic will be Elementary Arithmetic EA. Axioms of EA consist of a set of open defining axioms for all the symbols in the language together with the induction schema for 0-formulas (the fragment of EA in the language of Peano Arithmetic is also known under the name I0+exp.) We assume that all the theories in the present paper are formulated in the language Land are extensions of EA. Given two theories T1and T2, we will write T1⊆T2if T2extends T1; and T1≡T2if T1and T2are logically equivalent (i.e. both T1⊆T2and T2⊆T1hold.) Ndenotes the standard model of arithmetic and we say that a theory Tis sound if all its axioms are true (i.e. true in N.) The 1-collection principle (B1) is the axiom schema ∀x∃yϕ(x,y)→∀z∃u∀x≤z∃y≤uϕ(x,y), where ϕ(x,y)is a 1-formula, possibly containing other parameters. Note that this principle formalizes the property: every 1definable function on a finite domain has a finite range. B1also denotes the theory given by EA plus the 1-collection schema. The 1-collection rule is defined as follows: 1-CR ∀x∃yϕ(x,y) ∀z∃u∀x≤z∃y≤uϕ(x,y), where ϕ(x,y)is 1.Formulaϕ(x,y)may also contain other parameters, but in this case the presence of extra parameters is inessential, for it is well-known that an application of 1-CR can be reduced to an application of its parameter-free counterpart − 1-CR (see, e.g., Lemma 2.1 in [5].) For every base theory T,T+1-CR denotes the closure of Tunder first-order logic and nested applications of the 1-CR; and 166 A. Cordón-Franco, F. F. Lara-Martín [T, 1-CR]denotes the closure of Tunder first-order logic and unnested applications of the 1-CR. In addition, [T, 1-CR]0denotes Tand, for every k∈ω, [T, 1-CR]k+1denotes [[T, 1-CR]k, 1-CR]. Clearly, T⊆[T, 1-CR]1⊆... ⊆[T, 1-CR]k⊆... ⊆T+1-CR ⊆T+B1. In [5] Beklemishev developed a systematic analysis of the collection rule in arithmetic. Among many other interesting results, he proved the following conservativity and collapse results. Theorem 1.1 [5, Theorem 3.2] If T is 3-axiomatizable then T +B1is 2- conservative over T +1-CR. Theorem 1.2 [5, Corollary 4.3] If T is 2-axiomatizable then T +1-CR ≡ [T, 1-CR]. It is easy to see that Theorem 1.1 is best possible with respect to the quantifier complexity of the base theory: 2-sentences need not be conserved between T+B1 and T+1-CR if the quantifier complexity of the base theory Texceeds 3.For example, consider the 3-axiomatized theory T0=EA +(B1→con(PA)), where con(PA)formalizes the consistency of Peano Arithmetic (recall that B1is 3and finitely axiomatizable over EA.) The 2-consequences of T0coincide with the 2- consequences of EA (see, e.g., Remark 3.10 in [12] for a proof of this fact.) Thus, T0+1-CR ≡T0,forEA is well-known to be closed under 1-CR (see Lemma 4.1 in [5].) As a result, con(PA)is a 1-sentence provable in T0+B1but not in T0+1-CR. The question then naturally arises: is Theorem 1.2 also best possible with respect to the quantifier complexity of the base theory T?Inotherwords: Problem 1 Can the hierarchy of nested applications of 1-collection rule, [T, 1-CR]k with k≥0, be proper if the quantifier complexity of Texceeds 2? Two remarks are in order. Firstly, it should be noted that this question was already mentioned in [5]. In Remark 4.2 of [5], Beklemishev describes how the hierarchy of nested applications of 1-CR over an arbitrary base theory Tlooks like and he writes: “Since the complexity of T can be higher than 2,in principle we may obtain a proper hierarchy.” However, the question of exhibiting an actual example of a theory Tsuch that for each k≥0, [T, 1-CR]k+1is strictly stronger than [T, 1-CR]k was left pending in [5]. Secondly, by using the fact that “2-sentences commute with applications of 1-CR,” it is easy to check that Theorem 1.2 can be extended to (2∪2)-axiomatizable base theories, that is, to base theories that can be axiomatized by putting together a set of 2-sentences and a set of 2-sentences. More concretely, we have Lemma 1.3 1. Suppose θ is a 2-sentence. Then, [T+θ, 1-CR]≡ θ +[T ,1-CR]. 2. Suppose T ⊆ 2 ∪2. Then T + 1-CR ≡[T ,1-CR]. Semi-honest subrecursive degrees and the collection rule 167 Proof (1): We only have to show that θ+[T, 1-CR]extends [T+θ,1-CR].Tothis end, suppose T+θ∀x∃yϕ(x,y), with ϕ∈1. Write θ≡∃vθ 0(v), with θ0∈1. Clearly, T∀v∀x∃y(¬θ0(v) ∨ϕ(x,y)). Then, [T, 1-CR]∀v∀z∃u∀x≤z∃y≤u(¬θ0(v) ∨ϕ(x,y)) and so θ+[T, 1-CR]proves ∀z∃u∀x≤z∃y≤uϕ(x,y), as required. (2): It follows from Theorem 1.2 and part (1). Thus, if we want to find a base theory Tfor which Theorem 1.2 might fail and such that Tis as simple as possible in terms of quantifier complexity, we must look for a (2∨2)-axiomatized theory, that is, a theory every axiom of which can be written as the disjunction of a 2and a 2-sentence. How can we obtain natural examples of such arithmetic sentences? Since the graph of every computable function has a 1-definition in the standard model of arithmetic, any property of the form “if fis a total function then so is g,” where f,gare computable functions, naturally gives rise toatrue(2∨2)-sentence. Using this idea, one can reduce the question of finding the desired base theory Tto the question of constructing an appropriate sequence of computable functions. Actually, in the main result of the present paper (Theorem 2.8 below), given any recursively enumerable set of true 2sentences, S, we construct a sequence of semi-honest functions, {fi:i∈ω}, together with suitable 0-definitions of their graphs, such that the (2∨2)-axiomatized theory Tgiven by EA +“f0is total” +“fM 0is total →f1is total” +“fM 1is total →f2is total” +... where fM(x)=maxi≤xf(i), extends Sand satisfies that for each k≥0, [T, 1-CR]k+1is strictly stronger than [T, 1-CR]k. This answers in the positive Problem 1and settles the question as to whether Theorem 1.2 is best possible with respect to the quantifier complexity of the base theory; namely, Beklemishev’s result on the collapse of the 1-CR holds for every (2∪2)-axiomatizable base theory but not necessarily for (2∨2)-axiomatized base theories. The paper is divided into three sections. The first one is introductory. In the second section we give the proof of the main result, the aforementioned Theorem 2.8.Tothis end, we need to include some notions and results on subrecursive degree theory from [18] as well as a number of basic properties on the relationship between formal arithmetic theories and classes of computable functions described in terms of subrecursive operators. The third section closes the paper with some concluding remarks: firstly, we reinforce a couple of corollaries on the strength of 1-CR obtained by Kristiansen in [18]; and, secondly, we discuss how our main result generalizes to the n-CR for n>1. 2 The main result We begin by introducing some notions and terminology on subrecursive degree theory taken from [18] as well as some fundamental properties on the relationship between 168 A. Cordón-Franco, F. F. Lara-Martín arithmetic theories and classes of computable functions generated by means of subrecursive operators. We assume familiarity with classical computability theory and with the theory of subrecursive operators and we refer the reader to [25] and to [26] for all basic information on these subjects. A number-theoretic function f:ω→ωis semi-honest if it dominates 2x(i.e. f(x)≥2x) and has an elementary graph (i.e. its graph can be defined in the standard model Nby a 0-formula.) If, in addition, fis monotone (i.e. f(x)≤f(x+1)) then fis said to be an honest function. Let Edenote the class of (Kalmar) elementary functions, which is to say, Eis the smallest class containing the functions Z(x)≡0, x+1, x+y,2 xand projections In i(x1,...,xn)=xiand closed under composition and bounded recursion. Given a function f:ωk→ω,C(f)denotes the closure of E∪{f}under composition. We define f≤Cgiff f∈C(g);f<Cgiff f∈C(g)and g/∈C(f); and f≡C giff C(f)=C(g)(or, equivalently, f≤Cgand g≤Cf.) Clearly, ≡Cdefines an equivalence relation over the semi-honest functions, the equivalence classes of which are the so-called semi-honest subrecursive degrees. If we restrict the equivalence relation ≡Cto honest functions only, we obtain the honest subrecursive degrees. Suppose that fis a computable function with an elementary graph and consider a 0-formula θ(x,y)defining the graph of fin the standard model N. For notational convenience, we will also write y=f(x)to denote θ(x,y), and we will write f↓to denote the 2-sentence ∀x∃yθ(x,y). (When using the notation f↓, a fixed definition of f,θ(x,y), should be clear from the context.) A central notion in the proof theory of arithmetic is that of the provably total computable functions of a theory T. A number-theoretic function f:ωk→ωis said to be a provably total computable function (p.t.c.f.) of T, written f∈R(T), if there is a 1-formula of the language of T,ϕ(x1,...,xk,y), such that: 1. ϕdefines the graph of fin N; and 2. T∀x1...∀xk∃yϕ(x1,...,xk,y). It is a more or less direct consequence of Herbrand’s theorem that there is a sharp correspondence between computable functions with elementary graph and finite, sound 2-extensions of EA. Proposition 2.1 Let f be a function with an elementary graph and let y = f (x) be any 0-formula defining in N the graph of f . Then, R(EA + f ↓) = C( f ). Proof See, e.g., Proposition 4.2 of [4]. This correspondence is not exact: some information is being lost when going from a theory T to the corresponding class of provably total functions R(T ), as two nonequivalent theories may well give rise to the same class of provably total computable functions. However, as shown in Corollary 2.4 below, we can recover the 2-theorems of T from the function class R(T ) if we work over the set of all true 1-sentences 1(N) (note that 1(N) is an extension of EA since EA is 1-axiomatizable.) Lemma 2.2 Suppose f and g have elementary graphs and let y = f (x) and y = g(x) be any 0-formulas defining in N the graph of f and g, respectively. Then, g ≤C f if and only if 1(N) + f ↓ g ↓. Semi-honest subrecursive degrees and the collection rule 169 Proof (⇒): Assume g≤Cf. Then, g∈R(EA +f↓)by Proposition 2.1.Take ϕ(x,y)∈1such that EA +f↓ ∀x∃yϕ(x,y)and ϕ(x,y)defines the graph of gin N. Since ∀x∀y(ϕ(x,y)→(y=g(x))) is a true 1-sentence, we obtain that 1(N)+f↓g↓. (⇐): Assume 1(N)+f↓ g↓. By compactness, there is θ(z)∈0such that N| ∀ zθ(z)and EA+∀zθ(z)+f↓ g↓. So, EA+f↓∀x∃y(¬θ(y)∨(y=g(x))). Note that the elementary formula ¬θ(y)∨(y=g(x)) also defines the graph of gin N. Hence, g∈R(EA +f↓)and so g≤Cfby Proposition 2.1. Given a formula class and a theory T, we will write (T)to denote the - consequences of T, i.e., the set of all -sentences which are provable in T. Lemma 2.3 Suppose that T and S are sound extensions of EA. Then, R(S)⊆R(T) if and only if 1(N)+2(T)extends 2(S). Proof (⇒): Assume R(S)⊆R(T). Consider ϕ(x,y)∈0such that S ∀x∃yϕ(x,y)and put ϕ0(x,y)≡ϕ(x,y)∧∀z<y¬ϕ(x,z). It suffices to show that the theory 1(N)+2(T)proves ∀x∃yϕ0(x,y). Since Sis sound, the function g:ω→ωgiven by g(n)=μi.ϕ(n,i)in Nis well-defined. Then, ϕ0(x,y) defines the graph of gin Nand S∀x∃yϕ0(x,y),forSextends EA and EA is well-known to contain the least number principle for 0-formulas. We have thus shown that g∈R(S)and so g∈R(T)by assumption. Hence, there is some θ(x,y)∈1defining the graph of gand such that T∀x∃yθ(x,y). It then follows that 1(N)∀x∀y(θ(x,y)→ϕ0(x,y)) and so 1(N)+2(T)∀x∃yϕ0(x,y), as required. (⇐): Assume that 1(N)+2(T)extends 2(S). Then, we have R(S)=R(2(S)) ⊆R(1(N)+2(T)) =R(2(T)) =R(T). The second equality above follows from the fact that adding true 1-axioms does not change the set of p.t.c.f. of a sound theory (see, e.g., page 20 of [6] for a proof.) The first and third equalities are immediate, as R(S)(resp. R(T)) only depends on the 2-consequences of S(resp. T). From Lemma 2.3 we directly obtain Corollary 2.4 Suppose that T and S are sound extensions of EA. Then, R(S)=R(T) if and only if 2(T)≡2(S)over 1(N). It should be noted that the presence of 1(N)in Lemmas 2.2 and 2.3 and Corollary 2.4 cannot in general be avoided. To see this, let Sbe any set of true sentences satisfying that 1(S)≡ 1(N)and pick ϕ(x)∈0such that N| ∀ xϕ(x)and S∀xϕ(x). Define y=f(x)to be (x=x∧y=0)and y=g(x)to be (ϕ(x)∧y=0). It is clear that both elementary formulas define the graph of the zero function in N.ButS+f↓ does not prove g↓, because S+f↓≡ Swhile g↓implies ∀xϕ(x). 170 A. Cordón-Franco, F. F. Lara-Martín Remark 1 The idea of working modulo 1(N)in order to make a theory of the form EA +f↓independent of the specific 0-definition of the computable function f already appears in [10] and [13]. As a matter of fact, Proposition 1 of [10] is a version of Corollary 2.4 for theories in the usual language of arithmetic (without the symbol 2x); and in [13] the authors use this idea to reformulate a couple of questions on fragments of Peano Arithmetic in terms of recursion-theoretic conditions. Most remarkably, Proposition 12 of [13] reduces the well-known open problem whether I0+¬exp extends B1to a purely recursion-theoretic question. In addition, the ideas in the proof of Lemma 2.2 are tightly related to the content of Section 6 in [19], where Kristiansen discusses the relationship between degrees of algorithms computing total functions and degrees of honest functions, and to this end he works over the base theory PA +≡PA+1(N). We now consider a number of subrecursive operators acting on semi-honest functions (we follow the terminology of [18].) Definition 1 (Collection operator) We define the collection or max operator ·Mon unary functions by fM(x):= maxi≤xf(i). If y=f(x)is a 0-formula defining the graph of a unary function fin the standard model, we will write y=fM(x)to denote the 0-formula ∀z≤x∃u≤y(u=f(z)) ∧∃z≤x(y=f(z)), which naturally defines the graph of fMin N. The theory EA +fM↓is defined accordingly. In [18] it is shown that the collection operator induces an operator on the semihonest degrees (i.e., f≡Cg⇒fM≡CgM.) It is also well-known that there is a tight connection between the collection operator and 1-CR. Proposition 2.5 Suppose f has an elementary graph and let y =f(x)be any 0- formula defining the graph of f in N. Then, we have 1. (EA +f↓)+1-CR ≡[EA +f↓, 1-CR]≡EA +fM↓. 2. R([EA +f↓, 1-CR])=C(fM). Proof It follows from Theorem 4.2 of [5] and Proposition 4.2 of [4]. Definition 2 (Iteration operator) Given a unary function f and k ∈ ω,the k-th iterate of f , f k , is given by: f 0(x) := x and f k+1(x) := f ( f k (x)). We define the iteration operator ·I on unary functions by f I (x) := f x+1(x). The iteration operator behaves nicely when restricted to honest functions. Actually, in [17] Kristiansen shows that ·I induces an operator on the honest degrees that can be seen as a recursion-theoretic version of the jump operator for the Turing degrees. In contrast, the iteration operator does not even induce a well-defined operator on the semi-honest degrees (In the remark after Corollary 5.10 of [18] the author gives an example of two semi-honest functions f and h such that f ≡C h but f I ≡C hI .) Semi-honest subrecursive degrees and the collection rule 171 In order to obtain a jump operator for semi-honest degrees, one needs to consider operators based on enumerations of computable functions, which are much closer to the Turing jump in classical computability theory. The next definition is taken from Kristiansen [18] and we refer the reader to Section 5 in that paper for details. Let T(e,x,t)be the (elementary) Kleene predicate expressing that tis a computation tree for the function of index eon the input x, and let Udenote the elementary function which picks the result of a computation from the computation tree t. Assume that we have fixed some suitable computable index ffor a function f.Lete∈C(f)denote that eis a computable index built up by composing (a suitable index of ) fand elementary functions. Define Tf(e,x,t):= T(e,x,t)if e∈C(f) 2x=totherwise We define the e-th function compositional in fby [e]f(x):= U(μt.Tf(e,x,t)). Definition 3 (Jump operator) We define the jump operator ·Jon semi-honest functions by fJ(x):= μt.Tf((x)0,(x)1,t), where (·)0,(·)1denote the projections of Cantor pairing function. Theorem 5.3 in [18] shows that fJis semi-honest whenever fis semi-honest, and Theorem 5.5 in [18] shows that ·Jdoes induce a well-defined operator on semihonest degrees (i.e., f≡Cg⇒fJ≡CgJ.) It is also known that for an honest function f,fI≡CfJ(Theorem 5.8 of [18]), however this fails in general without the monotonicity condition of f. Interestingly, the jump operator ·Jfor semi-honest functions precisely corresponds to unnested applications of the 1-induction rule 1-IR ϕ(0)∧∀x(ϕ(x)→ϕ(x+1)) ∀xϕ(x), where ϕ(x)∈1, possibly with extra parameters. Proposition 2.6 Suppose f is semi-honest and let y =f(x)be any 0-formula defining the graph of f in N. Then, R([EA +f↓, 1-IR])=C(fJ). Proof Define eval f(e,x):= [e]f(x). It follows from Propositions 4.6 and 6.1 in [4] that R([EA +f↓, 1-IR])=C(eval f)(see also Proposition 2 in [7].) But since fis semi-honest, we have fJ≡Ceval fby Theorem 5.3 in [18] and so the result follows. We are now in a position to give a proof of our main result; namely, to construct an appropriate sequence of semi-honest functions {fi:i∈ω}and use it in order to define a (2∨2)-axiomatized theory Tsuch that the hierarchy [T, 1-CR]k, k≥0, is strict. The next proposition, which is a small variant of Theorem 5.12 of [18], isolates the construction of the required sequence of semi-honest functions. 178 A. Cordón-Franco, F. F. Lara-Martín Assume that it is. It would follow that θ+f↓ fM↓and so fM≤Cfby Lemma 2.2. But this contradicts the construction of the function f. (b) [S+h↓, 1-CR]≡[S+h↓, 1-IR]. It is well-known that for every base theory U,[U, 1-IR]extends [U, 1-CR].For the opposite direction, first observe that [S+h↓, 1-CR]≡[θ+f↓, 1-CR]≡θ+fM↓ θ+[EA +f↓, 1-IR]. By an argument similar to that of Lemma 1.3, it is easy to show that 1-sentences (indeed, 2) also commute with applications of 1-IR. Hence, we have θ+[EA +f↓, 1-IR]≡[θ+f↓, 1-IR]≡[S+h↓, 1-IR]. Thus, [S+h↓, 1-CR]implies [S+h↓, 1-IR], as required. In view of a) and b), it suffices to take π=h↓. Proposition 3.2 There exists a true 2-sentence πsuch that EA +πis not closed under 1-CR and [[EA +π,1-CR], 1-IR]≡[EA +π, 1-IR]. Proof By Corollary 5.14 of [18] there is a semi-honest function fsuch that f<CfM and fJ≡CfMJ.Takea0-formula y=f(x)defining the graph of fin N. Then, we have R([EA +f↓, 1-IR])=C(fJ)=C(fMJ)=R([EA +fM↓, 1-IR]). By Lemma 2.3 and compactness, there is a true 1-sentence, θ, such that the theory θ+[EA +f↓, 1-IR]extends [EA +fM↓, 1-IR]. Write θ≡∀xθ(x)with θ∈0 and define y=h(x)to be θ(x)∧(y=f(x)) (note that θ+f↓≡EA +h↓.) Notice that EA +h↓is not closed under 1-CR, for otherwise it would follow from Lemma 2.2 that fM≤Cf. In addition, we have [[EA +h↓, 1-CR], 1-IR]≡θ+[[EA +f↓, 1-CR], 1-IR] ≡θ+[EA +fM↓, 1-IR] ≡θ+[EA +f↓, 1-IR] ≡[EA +h↓, 1-IR] Note that in the first and the last equivalence we use the fact that 1-sentences commute with both 1-CR and 1-IR; and in the second one we use Proposition 2.5. It then suffices to take π = h ↓. Finally, it is natural to ask ourselves how our results generalize to the n-CR for n > 1. Corollary 4.3 of [5] actually shows that the collapse of the hierarchy of nested applications of n-CR to its first level holds for every n+1-axiomatizable base theory: if n ≥ 1 and T ⊆ n+1 then T +n-CR ≡[T ,n-CR]. Reasoning as in Lemma 1.3, Semi-honest subrecursive degrees and the collection rule 179 one can check that this equivalence can be extended to (n+1∪n+1)-axiomatizable base theories. As a consequence, the first level for which the collapse of the n-CR might fail is (n+1∨n+1). In what follows we will show that, indeed, this is the case. Fix n>1. By Theorem 6.2 in [5] there is a true n+1-sentence πsuch that In−1+πis not closed under n-CR. Define Tnto be EA +(In−1→π). (Recall that the schema of n−1-induction In−1is n+1and finitely axiomatizable over EA.) Clearly, Tnis sound and (n+1∨n+1)-axiomatized. In addition, we have Lemma 3.3 For each n >1,T nis n+1-conservative over EA. Proof Consider ϕ∈n+1provable in Tn. It suffices to show that EA +¬ϕis inconsistent. Towards a contradiction, assume EA +¬ϕis consistent and let Mbe a model of such a theory. By Fact 1 in Claim 1,Mhas a n-elementary extension, N, which is an+1-closed model of EA. Then, ¬ϕis also true in N. In addition, In−1must fail in N, for otherwise it would follow from Fact 2 in Claim 1that there exists a n+1 sentence true in N,δ, such that EA +δIn−1and it is well-known that In−1has no consistent n+1-extensions for n>1, see e.g. Proposition 4.3 in [11]. Hence, N is a model of Tn+¬ϕ, a contradiction. It then follows that [Tn, n-CR]≡Tn+[EA, n-CR]. By Lemmas 2.3 and 4.2 of [5], we get that [EA, n-CR]is equivalent to In−1and so [Tn, n-CR]is equivalent to In−1+π. But by our choice of the n+1-sentence π,In−1+πis not closed under n-CR. Hence, [Tn, n-CR] ≡ Tn+n-CR, as required. Note that the previous theory Tnsatisfies that [Tn, n-CR]2≡Tn+n-CR. It would be desirable to give for every n>1 an example of a theory Tsuch that the full hierarchy of nested applications of the n-CR over Tis proper, as we did in Theorem 2.8 for the case n=1. This seems to be more or less routine using the ideas in the present paper and some standard relativization techniques. We leave it as a pending question to check the details. Acknowledgements This work was partially supported by the Ministerio de Ciencia e Innovación (Spanish Government) under the Grant PID2020-116773GB-I00. Author contributions All authors contributed equally to this work. Declarations Conflict of interest The authors declare no competing interests. References 1. Adamowicz, Z., Bigorajska, T.: Existentially closed structures and Gödel’s second incompleteness theorem. J. Symb. Logic 66, 349–356 (2001) 2. Avigad, J.: Saturated models of universal theories. Ann. Pure Appl. Logic 118, 219–234 (2002) 3. Basu, S.: On the structure of subrecursive degrees. J. Comput. Syst. Sci. 4, 452–464 (1970) 180 A. Cordón-Franco, F. F. Lara-Martín 4. Beklemishev, L.D.: Induction rules, reflection principles, and provably recursive functions. Ann. Pure Appl. Logic 85, 193–242 (1997) 5. Beklemishev, L.D.: A proof-theoretic analysis of collection. Arch. Math. Logic 37, 275–296 (1998) 6. Beklemishev, L.D.: On the Induction Schema for Decidable Predicates. J. Symb. Logic 68, 17–34 (2003) 7. Beklemishev, L.D.: Provability algebras and proof-theoretic ordinals. I. Ann. Pure Appl. Logic 128, 103–123 (2004) 8. Beklemishev, L.D.: Reflection principles and provability algebras in formal arithmetic. Russ. Math. Surv. 60, 197–268 (2005) 9. Cai, M.: Degrees of relative provability. Notre Dame J. Formal Logic 53, 479–489 (2012) 10. Cordón-Franco, A., Fernández-Margarit, A., Lara-Martín, F.F.: Provably Total Primitive Recursive Functions: Theories With Induction. In: Marcinkowski, J., Tarlecki, A. (eds.) Computer Science Logic. CSL 2004. Lecture Notes in Computer Science, vol. 3210, Springer, Berlin, Heidelberg (2004) 11. Cordón-Franco, A., Fernández-Margarit, A., Lara-Martín, F.F.: Fragments of Arithmetic and true sentences. Math. Log. Quart. 51, 313–328 (2005) 12. Cordón-Franco, A., Fernández-Margarit, A., Lara-Martín, F.F.: Envelopes, indicators and conservativeness. Math. Log. Quart. 52, 51–70 (2006) 13. Cordón-Franco, A., Fernández-Margarit, A., Lara-Martín, F.F.: On axiom schemes for T-provably 1 formulas. Arch. Math. Logic 53, 327–349 (2014) 14. Hájek, P., Pudlák, P.: Metamathematics of First-Order Arithmetic. Springer, Berlin, Heidelberg (1993) 15. Kreisel, G., Lévy, A.: Reflection Principles and Their Use for Establishing the Complexity of Axiomatic Systems. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 14, 97–142 (1968) 16. Kristiansen, L.: Papers on subrecursion theory, Dr Scient Thesis, ISSN 0806-3036, ISBN 82-7368- 130-0, Research report 217, Department of Informatics, University of Oslo (1996) 17. Kristiansen, L.: A jump operator on honest subrecursive degrees. Arch. Math. Logic 37, 105–125 (1998) 18. Kristiansen, L.: Subrecursive degrees and fragments of Peano Arithmetic. Arch. Math. Logic 40, 365–397 (2001) 19. Kristiansen, L.: Degrees of total algorithms versus degrees of honest functions. In: Cooper, S.B., Dawar, A., Löwe, B. (eds.) How the World Computes. CiE 2012. Lecture Notes in Computer Science, vol. 7318, Springer, Berlin, Heidelberg (2012) 20. Kristiansen, L., Schlage-Puchta, J.C., Weiermann, A.: Streamlined subrecursive degree theory. Ann. Pure Appl. Logic 163, 698–716 (2012) 21. Machtey, M.: Augmented loop languages and classes of computable functions. J. Comput. Syst. Sci. 6, 603–624 (1972) 22. Machtey, M.: The honest subrecursive classes are a lattice. Inf. Control 24, 247–263 (1974) 23. Machtey, M.: On the density of honest subrecursive classes. J. Comput. Syst. Sci. 10, 183–199 (1975) 24. Meyer, A.R., Ritchie, D.M.: A classification of the recursive functions. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik 18, 71–82 (1972) 25. Odifreddi, P.: Classical Recursion Theory. North-Holland (1989) 26. Rose, H.E.: Subrecursion. Functions and Hierarchies. Clarendon Press, Oxford (1984)