On the quantifier complexity of Δ n+1 (T)– induction

A. Cord´on-Franco · A. Fern´andez-Margarit · F.F. Lara-Mart´ın On the quantifier complexity of n+1(T)– induction Abstract. In this paper we continue the study of the theories In+1(T), initiated in [7]. We focus on the quantifier complexity of these fragments and theirs (non)finite axiomatization. A characterization is obtained for the class of theories such that In+1(T) is n+2–axiomatizable. In particular, In+1(In+1) gives an axiomatization of Thn 2 (In+1) and is not finitely axiomatizable. This fact relates the fragment In+1(In+1) + to induction rule for n +1–formulas. Our arguments, involving a construction due to R. Kaye (see [9]), provide proofs of Parsons’ conservativeness theorem (see [16]) and (a weak version) of a result of L.D. Beklemishev on unnested applications of induction rules for n+2 and n+1 formulas (see [2]). 1. Introduction In [7] we introduced classes n+1(T),n+1–formulas that are equivalent in Tto an+1–formula. Here we continue the study of the theories In+1(T)and the relationship between Thn+2(T)and In+1(T). Through this paper we will use extensively results in [7] (see also [13]). For notation and preliminaries see that paper and [8], [10] for general references. This paper is devoted to the study of two main topics on the theories In+1(T): its axiomatization properties (quantifier complexity and (non)finite axiomatization) and the relationship of these theories with induction rules. The initial motivation for the work we present here was to prove the following result. Theorem 1.1. (see 2.4, 5.5) Thn+2(In+1)⇐⇒ In+1(In+1). So, the theory In+1(In+1)is n+2–axiomatizable. In [7], this result is used to separate the fragments of Arithmetic introduced there: In+1(In+1)and B∗n+1(In+1). A basic result on n+1–induction rule is the following conservativeness theorem of C. Parsons (see [16] and 6.5): In+1is a n+2–conservative extension of A. Cord´on-Franco, A. Fern´andez-Margarit, F.F. Lara-Mart´ın: Dpto. Ciencias de la Computaci´on e I.A. Facultad de Matem´afticas, Universidad de Sevilla, C/Tarfia s/n, Sevilla (Spain) e-mail: [email protected] Research partially supported by grant PB96–1345 (Spanish Goverment) Mathematics Subject Classification (2000): 03F30, 03H15 Key words or phrases: Induction – n+1–formulas – Quantifier complexity I0+n+1–IR (the closure of I0under the n+1–induction rule). From this fact and theorem 1.1, it follows that Theorem 1.2. (Beklemishev) I0+n+1–IR ⇐⇒ In+1(In+1). Even more, L.D. Beklemishev has observed (personal communication) that: modulo Parsons’ theorem, 1.1 and 1.2 are equivalent; and, from the techniques used in the proof of theorem 1.1 (a generalized construction of Ackermann’s function: the sequence of formulas Fn,k(x) =y,k∈ω, in section 4) an alternative proof of Parsons’ conservativeness theorem can be obtained. These facts show the close relation between the topics we deal with here: induction rules and axiomatizations of In+1(T). Now we give another natural connection between the above topics. Theorem 1.1 aims at the following general question on axiomatizations of In+1(T): (P1) For a theory T, determine (a) the quantifier complexity of In+1(T), and (b) when Thn+2(T)⇐⇒ In+1(T). Informally, (P1) asks for an equivalence between recursion and induction: Are there natural classes of recursive functions that can be described in terms of induction principles? A classical problem is the characterization of R(T), the class of provably total recursive functions of T. For theories axiomatizated by induction schemes the problem is: What functions can be proved to be total using only certain form of (restricted) induction? Question (P1) is related to a kind of reverse problem. Let Cbe a class of provably recursive functions of In+1and TotalCa class of 2sentences asserting that each function in Cis total. (P2) Is there a theory Tsuch that In+TotalC⇐⇒ In+1(T)? Remark 1.3. Last question suggests that those theories such that In+1(T)and Thn+2(T)are equivalent can be characterized in a functional way . In particular, for these theories In+1(T)is n+2–axiomatizable. In order to describe this functional approach, let us recall some notations and definitions from [7]. We denote by Lthe language of Arithmetic and by Nthe standard model. If is a class of formulas we write ψ(x1,...,x n)∈−if ψ(x) ∈and x1,...,x nare all the variables that occur free in ψ. Let be a class of formulas of Lwith only two free variables, xand ysay. For a formula ϕ(x,y), the conjunction of (–) ∀x∀y1∀y2[ϕ(x,y1)∧ϕ(x,y2)→y1=y2] and (–) ∀x1∀x2∀y1∀y2[x1≤x2∧ϕ(x1,y 1)∧ϕ(x2,y 2)→y1≤y2], will be denoted by IPF(ϕ). Let IPF() ={IPF(ϕ(x, y)) :ϕ(x,y) ∈}and ∗={∀x∃!y ϕ(x, y) :ϕ∈}+IPF(). Let ⊆n. We say that is a n–functional class if In+∗is consistent. A theory Tis n–functional if there exists a n–functional class, , such that Thn+2(T)=Thn+2(In+∗). We say that ϕ(u,x,y) ∈− n+1isan–envelope of Tin T0if 1. T∗ ϕ, (where ϕ={ϕ(k,x,y) :k∈ω}). 2. For all k∈ω,T0ϕ(k +1,x,y)→∃z <yϕ(k,x,z). 3. For each ψ(x,y) ∈− nsuch that T∀x∃y ψ(x, y), there exists k∈ωsuch that T0ϕ(k,x,y) →∃z < y ψ(x, z). Definition 1.4. 1. A n–functional class is inductive if for all ψ∈ (a) In+1(In+∗)IPF(ψ). (b) In+1(In+∗)∃yψ(0,y)∧∀x[∃y ψ(x, y) →∃yψ(x+1,y)]. 2. A theory Tis inductive n–functional if there is an inductive n–functional class such that Thn+2(T)⇐⇒ In+∗. (In this case we say that is an inductive n–functional class for T). 3. Let ϕ(u,x,y) ∈− nbe a n–envelope. We say that ϕ(u,x,y) is an inductive n–envelope if ϕ={ϕ(k,x,y) :k∈ω}is an inductive n–functional class. Remark 1.5. Part (b) of the definition of inductive n–functional class contains the premises of the induction rule for the formula ∃y ψ(x, y). This shows again the relationship between the two topics we are interested in here. By the next proposition, inductive n–functional classes characterize the n–functional theories such that In+1(T)is equivalent to Thn+2(T). Proposition 1.6. Let Tbean–functional theory. The following properties are equivalent: 1. Every n–functional class for Tis inductive. 2. Tis an inductive n–functional theory. 3. In+1(T)⇐⇒ Thn+2(T). Proof. It is trivial that (1) ⇒ (2). ((2) ⇒ (3)): Let be an inductive n–functional class for T. Then 1.6.1. In+∗⇐⇒ In+1(In+∗). Proof. (⇒ ): This follows from [7]–3.4. (⇐ ): By part (1.a) of 1.4, it is enough to prove that for each ϕ(x,y) ∈, In+1(In+∗)∀x∃y ϕ(x, y). Since In+∗∀x∃y ϕ(x, y), then ∃y ϕ(x, y) ∈n+1(In+∗). So, In+1(In+∗)I∃y ϕ(x,y). Hence, by part (1.b) of 1.4 we get the result.  By 1.6.1, we obtain (3) as follows Thn+2(T)⇐⇒ In+∗⇐⇒ In+1(In+∗)⇐⇒ In+1(T). ((3) ⇒ (1)): Let be a n–functional class for T. For every ϕ(x,y) ∈, IPF(ϕ),∃yϕ(0,y)and ∀x[∃y ϕ(x, y) →∃yϕ(x+1,y)] are n+2–formulas that are provable in T. So, by (3), they are also provable in In+1(T); hence, also in In+1(In+∗). Remark 1.7. Now, in connection with question (P2), we present some inductive 0–functional classes and the recursive functions they describe. Elementary recursive functions. Let us first recall some basic facts on the exponential function. Let exp be the sentence ∀x∃y(2x=y), where 2x=ydenotes a 0formula which defines the exponential function in the standard model and such that (see [8]): (1) I02x1=y1∧2x2=y2∧x1≤x2→y1≤y2. (2) I020=1. (3) I02x=y↔∃z[2x+1=z∧2·y=z]. From (1)–(3) and 1.6.1 we have that 1.7.1. (i) {2x=y}is an inductive 0–functional class. (ii) I0+exp ⇐⇒ I1(I0+exp). By 1.7.1–(ii),ifI0is extended with axioms asserting that every elementary recursive function is total then we obtain induction for every 1(I0+exp)–formula. It also holds that each elementary recursive set is definable by such a formula. Let us also observe that I1(I0+exp)is finitely axiomatizable. Primitive recursive functions. In 4.3 we shall define a sequence of functions: F0(x) =(x +1)2,Fk+1(x) =Fx+2 k(x +1). Let F:ω2−→ ωbe the function defined by: F(k,m) =Fk(m) (Fis essentially Ackermann’s function). In section 5(see also [1] or [18]) it will be proved that there exists ϕ(u,x,y) ∈0such that 1.7.2. (i) ϕ(u,x,y) is an inductive (strong) 0–envelope of I1in I0. (ii) For each k∈ω, and for all m, r ∈ω,Fk(m) =r⇐⇒ N|= ϕ(k,m,r). Let Ack ={ϕ(k,x,y) :k∈ω}. It holds that: 1.7.3. (i) Th2(I1)⇐⇒ I0+∗ Ack ⇐⇒ I1(I1). (ii) I1(I1)is 2–axiomatizable. (iii) I1and I1(I1)have the same class of recursive functions. Proof. (i) follows from 1.6 and 1.7.2. (ii) and (iii) follow from (i). By 1.7.3–(i),ifweaddtoI0axioms expressing that each primitive recursive function is total, then we obtain induction for every 1(I1)–formula. Moreover, each primitive recursive set is definable by such a formula. But, I1(I1)is not finitely axiomatizable (see 5.4). Grzegorczyk’s hierarchy, Ek,k≥3.For each level of Grzegorczyk’s hierarchy, Ek,k≥3, (see [17]) we have a similar result using the theory I0+ ∀x∃y[F0,k−2(x) =y] (see 4.6). So, if I0is extended with axioms asserting that each function in Ekis total, then we obtain induction for every 1(I0+ ∀x∃y[F0,k−2(x) =y])–formula. As it is well known, R(I0)=M2(see [19]). Let us consider the classes M2, Ek,k≥3 and PR (primitive recursive functions). As we have seen, these classes satisfy problem (P2). In section 2, we shall see that (P2) holds for any class Cof nondecreasing provably recursive functions of In+1. We conclude this section presenting the main results that will be obtained through this paper. Next theorem sums up the results on axiomatizations properties of In+1(T). Theorem 1.8. (see 2.4, 5.4) 1. Let Tbe a theory. (a) (n ≥1)In+1(T)is not n+2–axiomatizable. (b) If In+1×⇒ Thn+2(T), then In+1(T)is n+3axiomatizable but it is not n+3axiomatizable. (c) Assume thatThas n+1–induction. If In+1⇒ Thn+2(T), then In+1(T) is n+2axiomatizable. Even more, Thn+2(T)⇐⇒ In+1(T). 2. If Tis a consistent extension of In+1, then Thn+2(T)and In+1(T)are not finitely axiomatizable. Part (1) of the above theorem is proved in section 2through a result on (nonexistence of) n+3–axiomatizable extensions of In+1. As it was noted in 1.5, inductive n–functional classes relates quantifier complexity and induction rules. In sections 3and 4we develop the basic tools (following a construction due to R. Kaye (see [9])) to obtain explicitly inductive n–functional classes. Given a formula ϕ(x,y) ∈n, defining a total function, by iteration and diagonalization, we define uniformily a family of functions Aϕ,u(x) =y. When the function defined by ϕ(x,y) has a good rate of growth, the above family of functions is a n–envelope of Iϕ,n n+1in Iϕ,n n(where Iϕ,n mis a finite extension of Imasserting that ϕ(x,y) has good properties of growth). If Inextends Iϕ,n n, then Aϕ,u(x) =yis an inductive n–envelope. The theories Iϕ ngive every finite n–functional extension of In.As an application of these techniques we get part (2) of 1.8 and a general version of Parsons’ conservativeness theorem. Next theorem sums up the main properties connected with Parsons’ theorem. Theorem 1.9. (see 6.3, 6.4, 6.5) 1. For all k∈ω, [Iϕ n, n+2–IR]k⇐⇒ [Iϕ n, n+1–IR]k⇐⇒ Iϕ n+∀x∃y(Fϕ,k(x) =y) 2. Iϕ n+n+1–IR ⇐⇒ Iϕ n+ACK∗ ϕ. 3. Iϕ n+1isan+2–conservative extension of Iϕ n+n+1–IR. 4. (Parsons) In+1isan+2–conservative extension of I0+n+1–IR. We conclude by giving a proof, for n–functional theories, of a result of Beklemishev on unnested applications of n+1and n+2–induction rules (see [2], corollary 9.1). Theorem 1.10. (see 6.7) Let Tbe n+2–axiomatizable extension of In.IfTis n–functional, then [T, n+1–IR]⇐⇒ [T, n+2–IR]. 2. Quantifier complexity of n+1(T)–induction The aim of this section is to prove theorem 1.8–(1) (see also [6]). To this end we first study n+3extensions of In+1. Next lemma is a generalization of a result of D. Leivant (see [14]), and it is used in [7] to prove 3.7.4. Lemma 2.1. Let Tbe a consistent and n+3axiomatizable theory. Then T×⇒ In+1. Proof. Assume towards a contradiction that T⇒ In+1. Since In+1is finitely axiomatizable, there exists a sentence ϕ∈n+3such that Tϕand ϕ⇒ In+1. Let θ(x) ∈− n+2such that ϕ≡∃x θ(x). Let A|= Tnonstandard. Since Tϕ, there exists a∈Asuch that A|= θ(a). Let b∈Anonstandard and c=a,b.We have that 2.1.1. Kn+1(A,c)|= ϕ. Proof. Since θ(x) ∈n+2,a∈Kn+1(A,c),Kn+1(A,c) ≺n+1Aand A|= θ(a), then Kn+1(A,c)|= θ(a); hence, Kn+1(A,c)|= ϕ. As ϕextends In+1,by2.1.1,Kn+1(A,c) |= In+1. Since Kn+1(A,c) is nonstandard, this gives the desired contradiction.  Theorem 2.2. If A|= Thn+2(T)and A|= In+1(T), then A|= In+1. Proof. Let us see that A|= In+1. Let ϕ(x,v) ∈n+1and a∈Asuch that (1) A|= ϕ(0,a), and A|= ϕ(x,a) →ϕ(x +1,a). Let us see that A|= ∀ x ϕ(x, a). Since A|= Thn+2(T), there exists θ(w) ∈ − n+1such that T¬∃w θ(w), and A|= ∃ w θ(w); so, there exists b∈Asuch that A|= θ(b). Let δ(x,v,w) ∈n+1be the following formula θ(w)∧ϕ(x,v). By (1), A|= δ(0,a,b), and A|= δ(x,a,b) →δ(x +1,a,b). Since T¬δ(x,v,w), then δ(x,v,w) ∈∗ n+1(T).AsA|= I∗ n+1(T), it follows that A|= ∀ xδ(x,a,b); hence, A|= ∀ x ϕ(x, a). Theorem 2.3. Let Tbe a theory with n+1–induction. The following conditions are equivalent. 1. Thn+2(T)⇐⇒ In+1(T). 2. In+1(T)is n+2axiomatizable. 3. In+1(T)is n+3axiomatizable. 4. In+1⇒ Thn+2(T). Proof. ((1) ⇒ (2) ⇒ (3)): Trivial. ((3) ⇒ (1)): Assume towards a contradiction that (1) does not hold. Since Thas n+1–induction, then In+1(T)×⇒ Thn+2(T). Hence, there exists θ∈n+2 such that Tθ, and In+1(T) θ. Then, by 2.2, we get that In+1(T)+¬θ⇒ In+1. So, In+1(T)+¬θis a consistent extension of In+1and, by (3),n+3 axiomatizable. Which contradicts 2.1. ((1) ⇒ (4)): Since In+1⇒ In+1(T), the result follows from (1). ((4) ⇒ (1)): As Thas n+1–induction, Thn+2(T)⇒ In+1(T). For the converse, assume towards a contradiction that In+1(T)×⇒ Thn+2(T). Then there exists Asuch that A|= In+1(T), and A|= Thn+2(T). Then, by 2.2,A|= In+1. So, by (4),A|= Thn+2(T), contradiction.  Theorem 2.4. Let Tbe a theory. 1. (n ≥1)In+1(T)is not n+2–axiomatizable. 2. If In+1×⇒ Thn+2(T), then In+1(T)is n+3axiomatizable but it is not n+3axiomatizable. 3. Assume that Thas n+1–induction. If In+1⇒ Thn+2(T), then In+1(T) is n+2axiomatizable; even more, In+1(T)⇐⇒ Thn+2(T) Proof. ((1)): Since In+1(T)⇒ In, the result follows from 2.1. ((2)): It is obvious that In+1(T)is n+3–axiomatizable. Moreover, by the hypothesis, In+1(T)×⇒ Thn+2(T). Then, as in the proof of (3)⇒ (1) in 2.3, (which now does not need the asumption that Thas n+1–induction) we get that In+1(T) is not a n+3axiomatizable theory. ((3)): It is a consequence of 2.3. Remark 2.5. (On 2–axiomatization). From 2.4–(1),In+1(T),n≥1, is not n+2–axiomatizable. For n=0, there exist theories (for instance, I0) such that I1(T)is 2–axiomatizable (indeed 1–axiomatizable). Next result gives theories such that I1(T)is not 2–axiomatizable. 2.5.1. Let Tbe a 2–axiomatizable extension of I0and ϕ(x,y) ∈0such that T∀x∃y ϕ(x, y). Then there exists a term t(x) such that T∃u∀x[u<x→∃y≤t(x)ϕ(x,y)] Proof. Since 2is closed under conjunction, if T∀x∃y ϕ(x, y) then there exists ψ∈2such that Tψand I0+ψ∀x∃y ϕ(x, y). Let δ(x) ∈1such that ψis ∃x δ(x). By way of contradiction assume that for each term t(x) of L, T∃u∀x[u<x→∃y≤t(x)ϕ(x,y)]. Let cand dbe new constants symbols and Tthe theory T+δ(c)+c<d+ {¬∃y≤t(d)ϕ(d,y):t(x) term of L} By compactness, Tis consistent. Let Abe a model of T;aand b, respectively, the interpretations of cand din Aand Bthe initial segment defined in Aby {t(b) :t(x) term of L}. Then B≺0A. So, as a<b,B|= I0+ψ, which contradicts B|= ∀ x∃y ϕ(x, y). This result generalizes a similar property on I− 1obtained in [5]. The proof we have presented here can be used to obtain the following result for n+2–axiomatizable theories (n ≥1). 2.5.2. (n ≥1)Let ϕ(u,x,y) be a strong n–envelope of Inin In. Let T be a n+2–axiomatizable theory and ψ(x,y) ∈n+1such that Bn+1+T ∀x∃y ψ(x, y) then there exists a term t(x) of L(ϕ)such that (T+In)ϕ∃u∀x[u<x→∃y≤t(x)ψ(x,y)] By 2.5.1,ifTis a 2–axiomatizable sound theory, then every function in R(T) is bounded by a polynomial. From this we get that 2.5.3. Let Tbe an extension of I0such that N|= T. If there exists f∈R(T) not bounded by a polynomial then Tis not 2–axiomatizable. 2.5.4. If Texp then I1(T)is not 2–axiomatizable. Proof. Let 2x=ybe a 0formula as in 1.7. Since T∀x∃y(2x=y), then ∃y(2x=y) is a 1(T)–formula. Hence, I1(T)∀x∃y(2x=y); so, as I1(T) is a sound theory, the result follows from 2.5.3. Remark 2.6. Let us see how we can answer (P2) using the above results. Let Cbe a class of nondecreasing provably recursive functions of In+1. Assume that for each f∈Cthere exists a formula ϕf(x, y) ∈0defining fin Nand such that In+1∀x∃!yϕ f(x, y). Let ={ϕf(x, y) :f∈C}. Then, by 2.4–(3), In+1(In+∗)⇐⇒ In+∗ 3. Ackermann’s functions In this section we give a generalization of Ackermann’s function. Similar constructions have been considered by P. D’Aquino (see [1]), R. Kaye (see [9]) and R. Sommer (see [18]). The aim of the definition we develop here is to describe inductive n–functional subtheories of In+1. To this end, the construction proceeds using iteration and diagonalization as in Grzegorczyk’s Hierarchy. Remark 3.1. (Set Theory in I0)Here we shall see how set theory can be described in I0. We shall informally give a 0formula, denoted by x∈u, such that in each model of I0some of its elements can be considered as finite sets. See [15] for details. Let us consider the following 0–formulas (where y|xis the formula ∃z≤x(y·z=x)), irred(x) ≡2≤x∧∀y≤x(y|x→y=1∨y=x), pot2(x) ≡1≤x∧∀u≤x(irred(u) ∧u|x→u=2), pot4(x) ≡pot2(x) ∧∃y≤x(pot2(y) ∧y·y=x). And Lp2(x) =yand Lp4(x) =y, respectively, are the formulas [x=0∧y=1] ∨[x<y≤2·x∧pot2(y) ∧∀z<y(pot2(z) →z≤x)] [x=0∧y=1] ∨[x<y≤4·x∧pot4(y) ∧∀z<y(pot4(z) →z≤x)] 3.1.1. (i) I0∀x∃!y(Lp2(x) =y) ∧∀x∃!y(Lp4(x) =y). (ii) I01≤x→Lp2(x) ≤2·x∧Lp4(x) ≤4·x. Formula x∈uis given using the formulas pot2(v) and pot4(v). We say that x∈uif (–) xwritten in base 2, as a sequence of 0,1, appears in uwritten in base 4, as a sequence of 0,1,2,3, between two consecutive occurrences of 2. Now we give without proofs some basic properties of the formula x∈u. Let Conj(u) ∈0be the formula (we read Conj(u) as “uis a set”) ¬∃v<u∀x<u(x∈u↔x∈v) 3.1.2. (i) I0x∈u→x<u. (ii) I0x∈u→∃v[2 ·v<u∧∀y(y= x∧y∈u→y∈v)]. (iii) I0Conj(0)∧∀x(x /∈0). (iv) I0Conj(u) ∧Conj(v) ∧∀x(x∈u↔x∈v) →u=v. 3.1.3. (n–separation). Let ϕ(x) ∈n∪n. Then In∀y∃z≤y[Conj(z) ∧∀x(x∈z↔x∈y∧ϕ(x))] Let {x}=zbe the 0formula: Conj(z) ∧∀y<z(y∈z↔y=x). Let x∪y=zbe the 0formula: Conj(z) ∧∀u<z[u∈z↔u∈x∨u∈y]. 3.1.4. (i) I0∀x∃!y≤(6·Lp2(x))2[{x}=y]. (ii) I0∀x∀y∃!z≤x+y·Lp4(x) [x∪y=z]. 3.1. Iteration: ITϕ(z,x,y) Remark 3.2. In what follows we consider a theory T, extension of In, and ϕ(x,y) ∈ − nsuch that (1) TIPF(ϕ(x, y)), and (2) Tϕ(x,y) →x2<y. That is, ϕ(x,y) defines in Ta partial increasing function bigger, when defined, than the square. It is easy to see that 3.2.1. Tϕ(x,y) →(x +1)3<(y+1)2. Informally, we denote ϕ(x,y)by Fϕ(x) =y. In the next results we are going to prove in Tsome properties by induction, it will be easy to verify in each case that T proves enough induction to carry on the argument. We will use Cantor’s function, J:ω2−→ ω, defined by J(x,y) =z≡(x +y) ·(x +y+1)+2·x=2·z Definition 3.3. Let itclϕ(w,z,x,y)∈n(in Bnfor n≥1)be        J(z,y) ∈w∧J(0,x)∈w∧ ∀z,y<w   J(z,y)∈w→   (z=0∧y=x) ∨ 0<z ∧∃v<wϕ(v,y)∧ J(z−1,v)∈w 4. n–envelopes given by iteration Now, we present the main tool that will be used in the remainder of the paper. We follow a similar construction devised by R. Kaye (see [9]) to analyse parameter free induction schemes. Definition 4.1. 1. Let K0(x) =ybe (x +1)2=y. For every n≥1let Kn(x) =y be En(x,x,y), where En(u,x,y)is the n–q–envelope given in [7]–5.13. (Let us observe that Inx2<Kn(x)). 2. Let ϕ(x,y) ∈− n. We will denote by KITFn(ϕ) the formula: IPF(ϕ) ∧∀x∀y (ϕ(x,y) →Kn(x) ≤y) ∧∀x∃y ϕ(x, y) For each theory T, let Tϕ,n be the theory T+KITFn(ϕ). In particular, we will denote by Iϕ,n mthe theory (Im)ϕ,n. When n=m, we shall omit the superscript nand write Iϕ n. Remark 4.2. Let us observe that KITFn(ϕ) ∈n+2and Iϕ n=In+∗+∀x∀y (ϕ(x,y) →Kn(x) ≤y) (where ={ϕ(x,y)}). So, by [7]–3.7.2–(ii), if Iϕ nis consistent, then Iϕ nis a n–functional theory. In particular, if ϕ(x,y) is the formula Kn(x) =ythen, by [7]–5.13,InKITFn(ϕ). Hence, Iϕ n⇐⇒ In. Definition 4.3. Let ACKϕ={Fϕ,k(x) =y:k∈ω}, where (–) Fϕ,0(x) =yis ϕ(x,y). (–) Fϕ,k+1(x) =yis DFϕ,k (x, y). If ϕ(x,y) is the formula Kn(x) =y, then Fn,k(x) =ywill denote the formula Fϕ,k(x) =yand ACKnwill denote the set ACKϕ. Remark 4.4. Let us observe that, as we will see in 4.5,ifInKITFn(ϕ) then ACKϕis an inductive n–functional class. Even more, it holds that 4.4.1. If In+1KITFn(ϕ) and In∀x,y (ϕ(x,y) →Kn(x) ≤y), then ACKϕis an inductive n–functional class. Proof. By induction on k∈ωwe prove that In+1(In+ACK∗ ϕ)proves (–) IPF(Fϕ,k), and (–) ∃y(Fϕ,k(0)=y) ∧∀x[∃y(Fϕ,k(x) =y) →∃y(Fϕ,k(x +1)=y)]. k=0: Since In+1KITFn(ϕ),by5.5–(1),In+1(In+ACK∗ n)KITFn(ϕ). As In∀x,y (ϕ(x,y) →Kn(x) ≤y), then by 6.4 and 6.5, In+ACK∗ ϕ⇐⇒ Iϕ n+ACK∗ ϕ⇒ In+ACK∗ n So, In+1(In+ACK∗ ϕ)KITFn(ϕ), as required. k→k+1: It follows from 4.5. Lemma 4.5. 1. For all k∈ω, (a) Iϕ nFϕ,k(x) =y→Kn(x) ≤y. (b) Iϕ nIPF(Fϕ,k). 2. For all k∈ω,Iϕ n+∀x∃y[Fϕ,k(x) =y]proves (a) ∃y[Fϕ,k+1(0)=y]. (b) ∀x[∃y(Fϕ,k+1(x) =y) →∃y(Fϕ,k+1(x +1)=y)]. 3. Iϕ,n n+1ACK∗ ϕ. Proof. ((1)): We get (1.a) and (1.b) by induction on k∈ωusing 3.7. ((2)): We only need to prove (2.b). Let A|= Iϕ n+∀x∃y[Fϕ,k(x) =y] and a∈A such that A|= ∃ y[Fϕ,k+1(a) =y]. Let b∈Asuch that A|= Fϕ,k+1(a) =b. Then, by induction on d, using 3.7–(6) and (1), it is proved that for all d≤a ∃y1,y 2≤b[Fd ϕ,k(a +2)=y1∧Fd+2 ϕ,k (a +1)=y2∧y1≤y2] From this, for d=a, we have that ∃y[Fa ϕ,k(a +2)=y]. Then, by 3.7–(6), ∃y[Fa+3 ϕ,k (a +2)=y]; hence, ∃y[Fϕ,k+1(a +1)=y]. ((3)): By induction on k, it follows from (1) and (2) that, for all k∈ω, Iϕ,n n+1KITFn(Fϕ,k(x) =y) as required.  Theorem 4.6. For all k∈ω,IT Fϕ,k (z,x,y) ∈nis a n–envelope of Iϕ n+ ∀x∃y[Fϕ,k(x) =y]in Iϕ n. Proof. By 4.5–(1) and 3.7–(3),IT Fϕ,k (z,x,y)is a n–q–envelope. So, by [7]–5.4, to see that ITFϕ,k (z,x,y) isan–envelope is enough to prove that this formula satisfies n–IND. Let A|= Iϕ nand a,b ∈Asuch that for all m∈ω,A|= ∃ y< bITFϕ,k (m, a, y). For all m∈ωlet bm<bsuch that A|= ITFϕ,k (m, a, bm). Let I={c∈A:∃m∈ω(c<b m)}. Then a<I<band Iis a initial segment closed under the n–functions defined in Aby ϕand Fϕ,k. For all c∈I,by4.5–(1), there exists d∈Isuch that A|= Kn(c) =d. So, by [7]–5.13,I≺e nA. Hence, I|= I0+KITFn(ϕ) and I|= ∀ x∃y(Kn(x) =y). So, I|= I0+∗ n, where n={Kn(x) =y}. Since (see [7]–5.13)nis a strong n–functional class, then, by [7]–4.6.1,I0+∗ n⇒ In. So, I|= Iϕ n+∀x∃y(Fϕ,k(x) =y). Theorem 4.7. 1. For all n, k ∈ω,Iϕ nFϕ,k(x) =y↔Aϕ,k(x) =y. 2. Aϕ,u(x) =yisan–envelope of Iϕ,n n+1in Iϕ n. 3. There exists a n–envelope of Iϕ,n n+1in Iϕ n,ψ(u,x,y) ∈n, such that for all k∈ω,Iϕ nFϕ,k(x) =y↔ψ(k,x,y). Proof. ((1)): Let A|= Iϕ n. By induction on k∈ω, let us see that (I)A|= ITFϕ,k (z,x,y)↔Az ϕ,k(x) =y. (k =0): This follows from the definitions of Fϕ,0and Aϕ,0. (k →k+1): Let d∈A. By induction, using 3.18.1, it is proved that for all b∈A, b≥1, (II)∀x,y < d [ITFϕ,k+1(b,x,y)↔Ab ϕ,k+1(x) =y] This proves (I) for all kand completes the proof. ((2)): By 4.5–(3),Iϕ,n n+1ACK∗ ϕand, by 3.7–(5), Iϕ nFϕ,k+1(x) =y→∃v<y(Fϕ,k(x) =v) Then, by (1),Aϕ,u(x) =yis a n–q–envelope of Iϕ,n n+1in Iϕ n. So, by [7]–5.4,it is enough to prove that for every A|= Iϕ nand a,b ∈A,a<b, () if for all k∈ω,A|= ∃ y<b(Aϕ,k(a) =y) then there exists I|= Iϕ,n n+1such that I≺e nAand a<I<b. Through the proof we shall write Au(x) =yand Fk(x) =yinstead of Aϕ,u(x) =yand Fϕ,k(x) =y, respectively. We follow the proof of lemma 4.6 in [18] (which, in turn, follows a construction of Paris and Kirby (see [12])). First of all, let us observe that we can assume that a is nonstandard and A|= exp: (–) We can assume that ω<a: Let I={c∈A:∃k∈ω, c < Ak(a)}. Then for each c<Ak(a), A|= Kn(c) < Fk(Ak(a)) =F2 k(a) < Fa+2 k(a +1)=Ak+1(a) Hence, I≺e nA,a<I<band Iis closed under the n–functions defined by Fk.IfI=ω, then by overspill there exists a∗>Isuch that for all k∈ω, A|= ∃ y<b(Ak(a∗)=y).IfIis a nonstandard segment then there exists a∗∈Isuch, a∗>ω. So, for all k∈ω,A|= ∃ y<b(Ak(a∗)=y). (–) We can assume that A|= exp: We will use the trick of lemma 3in [1]. For all k∈ωit holds that (•)A|= ∃ y<b(Ak(a) =y∧∀x≤y∃z<b(Fk 1(x) =z)) Let ψ(k,a,b) be the nformula: ∃y<b Ak(a) =y∧∀x≤y∃z<b(Fk 1(x) =z) ∧ ∀u≤k∃v<y(Au(a) =v) By (•), for all k∈ω,A|= ψ(k,a,b). So, by overspill, there exists c>ωsuch that A|= ψ(c, a, b). Let b∗such that b∗<b∧Ac(a) =b∗∧∀x≤b∗∃z<b(Fc 1(x) =z) ∧ ∀u≤c∃v<b ∗(Au(a) =v) Let I∗={d∈A:∃k∈ω, d < Fk 1(b∗)}. Then a<I ∗<band I∗is closed under the n–function defined by F1; hence, I∗≺e nA. So, I∗|= Iϕ n+∀x∃y(F1(x) =y). But Iϕ n+∀x∃y(F1(x) =y) exp, and I∗|= ∃ y<b ∗(Ak(a) =y). So, taking a∗and b∗instead of aand b, and I∗instead of A, if needed, we can assume in () that A|= Iϕ n+exp and ω<a. Suppose that for all k∈ω,A|= ∃ y<b(Ak(a) =y). By overspill, there exists c>ω,c<a, such that A|= ∃ y<b(Ac+1(a) =y). Let d=Ac+1(c). Then for all k∈ω,A|= ∃ y<d(Ak(c) =y). We define an initial segment of A,I, as follows. Let {ψk(w, v) :k∈ω}be an enumeration of the class of nformulas such that each nformula appears infinitely often. We define two sequences {ak:k∈ω} and {bk:k∈ω}of elements of Asuch that (1)kk= 0⇒ (ak−1)2<a k, (2)ka0<a 1<···<a k≤bk≤bk−1≤···≤b0, (3)kk= 0∧d1,...,d r≤ak⇒ (µw)[ψk−1(w, d1,...,d r)]/∈(ak,b k], (4)kbk=Ac−k+1(ak). We proceed by recursion on k(at the same time we prove that they satisfy (1)k–(4)k). (k=0): Let a0=cand b0=d. (k→k+1): Suppose that we have aiand bi,0≤i≤k, and they satisfy (1)i–(4)i. Then bk=Ac−k+1(ak). Since Ac−k+1(ak)=Aak+2 c−k(ak+1), then (ak,b k]= 0≤j≤ak+1 (Aj c−k(ak+1), Aj+1 c−k(ak+1)] Now the class M={(µw)[ψk(w, d1,...,d r)]: d1,...,d r≤ak}has at most ak+1 elements; hence, by the Pigeon-Hole Principle, there exists j≤ak+1 such that M∩(Aj c−k(ak+1), Aj+1 c−k(ak+1)]=∅. Let ak+1=Aj c−k(ak+1), and bk+1=Aj+1 c−k(ak+1) By definition of ak+1and bk+1, properties (2)k+1–(4)k+1are trivial and (1)k+1 follows from the definition of Ackermann’s function, A. Let I={d∈A:∃k∈ω(d < a k)}. Then, by (1)k,Iis an initial substructure of A; hence, I|= I0. We also have that Iis closed under Kn(x) =y; hence, I≺nAand I|= Iϕ,n 0.By(3)k(since each n– formula appears in {ψk:k∈ω} infinitely often) it holds that I|= Ln+1. This proves that I|= Iϕ,n n+1. ((3)): It follows from (1) and (2). 5. Non–finite axiomatization of In+1(T) In this section, using Ackermann’s functions, we shall prove 1.8–(2) and present an alternative proof of theorem 1.1. Theorem 5.1. Assume that Iϕ,n n+1is consistent. Then Thn+2(Iϕ,n n+1)⇐⇒ Iϕ n+ACK∗ ϕ⇐⇒ In+1(Iϕ,n n+1)ϕ,n. Proof. By 4.7–(3),Thn+2(Iϕ,n n+1)⇐⇒ Iϕ n+ACK∗ ϕ. Let us see, by induction on k∈ω, that In+1(Iϕ n+ACK∗ ϕ)ϕ,n ∀x∃y[Fϕ,k(x) =y] (k=0): It follows from the definition of Tϕ,n and Fϕ,0(x) =y. (k→k+1): Suppose that In+1(Iϕ n+ACK∗ ϕ)ϕ,n ∀x∃y[Fϕ,k(x) =y]. Then, by 4.5–(2),In+1(Iϕ n+ACK∗ ϕ)ϕ,n proves that ∃y[Fϕ,k+1(0)=y]∧∀x[∃y(Fϕ,k+1(x) =y) →∃y(Fϕ,k+1(x +1)=y)] Since ∃y(Fϕ,k+1(x) =y) ∈n+1(Iϕ n+ACK∗ ϕ), then In+1(Iϕ n+ACK∗ ϕ)ϕ,n ∀x∃y[Fϕ,k+1(x, y)], as required.  Lemma 5.2. If Iϕ,n n+1is consistent, then Thn+2(Iϕ,n n+1)is not finitely axiomatizable. Proof. By way of contradiction suppose that Thn+2(Iϕ,n n+1)is finitely axiomatizable. Then by 5.1 and 3.7-(1,5) there exists k∈ωsuch that Iϕ n+∀x∃y(Fϕ,k(x) =y) ⇐⇒ Thn+2(Iϕ,n n+1) So, by 5.1,Iϕ n+∀x∃y(Fϕ,k(x) =y) ∀x∃y(Fϕ,k+1(x) =y).By4.6, there exists m∈ωsuch that Iϕ nITFϕ,k (m,x,y) →∃z<y(Fϕ,k+1(x) =z) Since ITFϕ,k (z +2,x,y) →∃y<yITFϕ,k (z,x,y), then it holds that the theory Iϕ n+∀x∃y(Fϕ,k(x) =y) proves that ITFϕ,k (m +2,m,y)→∃z<y(Fϕ,k+1(m) =z); ITFϕ,k (m +2,m,y)→∃z<y(ITFϕ,k (m +2,m+1,z)); which contradicts 4.5–(1.b). Lemma 5.3. Let Tbean–functional finite n+2–extension of In. Then there exists ϕ(x,y) ∈− nsuch that T⇐⇒ Iϕ n. Proof. By hypothesis, T⇐⇒ In+∀x∃y θ(x, y), where θ(x,y) ∈− n. Let ϕ(x,y) ∈− nthe formula ∃y1,y 2≤y(Kn(x) =y1∧Cθ(x, y2)∧y=y1+y2) Where the formula Cθ(x, y) is as in the proof of theorem 3.5 in [7]. Then In ∀x∃y ϕ(x, y) →∀x∃y θ(x, y) and T∀x∃y ϕ(x, y) ↔∀x∃y θ(x, y). Hence, T⇐⇒ Iϕ n, as required.  Part (1) of next theorem can be also obtained from corollary 3.3 in [2]. Theorem 5.4. Let Tbe a consistent extension of In+1. Then 1. Thn+2(T)is not finitely axiomatizable. 2. In+1(T)is not finitely axiomatizable. Proof. ((1)): Let us assume that Thn+2(T)is finitely axiomatizable. Then, by 5.3 there exists ϕ(x,y) ∈− nsuch that Thn+2(T)⇐⇒ Iϕ n Hence, Iϕ,n n+1is consistent and Thn+2(T)=Thn+2(Iϕ,n n+1), which contradicts 5.2. ((2)): Assume that In+1(T)is finitely axiomatizable. Then as in the proof of 5.3, there exists ϕ(x,y) ∈− nsuch that Iϕ,n n+1is consistent and T⇒ Iϕ n⇒ In+1(T) Since Tis an extension of In+1, then In+1(T)⇒ In+1(Iϕ,n n+1). As In+1(Iϕ,n n+1)ϕ,n ⇒ Iϕ n, then (second equivalence follows from 5.1) In+1(T)ϕ,n ⇐⇒ In+1(Iϕ,n n+1)ϕ,n ⇐⇒ Thn+2(Iϕ,n n+1) Hence, Thn+2(Iϕ,n n+1)is finitely axiomatizable, which contradicts 5.2. Theorem 5.5. 1. Thn+2(In+1)⇐⇒ In+1(In+1)⇐⇒ In+ACK∗ n. 2. In+1(In+1)is n+2axiomatizable. 3. In+1isan+2–conservative extension of In+1(In+1). 4. In+1and In+1(In+1)have the same class of recursive functions. Proof. Let ϕ(x,y) ∈− nbe the formula Kn(x) =y. Then, InKITFn(ϕ), and Iϕ n⇐⇒ In. Hence, (1) follows from 5.1. Parts (2),(3) and (4) are consequences of (1). Proposition 5.6. 1. (k>0) There does not exist a class of sentences ⊆n+2 such that In+is consistent and In+⇒ In+∀x∃y[Fn,k(x) =y] 2. There does not exist a class of sentences ⊆n+2such that In+is consistent and In+⇒ Thn+2(In+1). Proof. ((1)): By way of contradiction suppose that there is a class such that In+ ⇒ Thn+2(In+∀x∃y[Fn,k(x) =y]). Let ϕ(u,x,y) be ITFn,0(u,x,y). Then, ϕ(u,x,y) is a strong n–envelope of Inin Insuch that In+∀x∃y [Fn,k(x) =y] proves (–) ∀u∀x∃y ϕ(u,x,y), and (–) ∀u, x, y1,y 2[ϕ(u, x, y1)∧ϕ(u +1,x,y 2)→y1<y 2]. Since In+∀x∃y[Fn,k(x) =y] is finitely axiomatizable (for n=0, as k≥1, In+∀x∃y[F0,k(x) =y]exp), then there exists ψ∈such that In+ψ⇒ In+∀x∃y[Fn,k(x) =y]. Let A|= (In+ψ)ϕ,a∈Anonstandard such that A|= ψ0(a) (where ψis ∃xψ 0(x), with ψ0(x) ∈n+1); and let B=Kϕ 0(A,a) as in [7]–6.5. Then, by [7]–6.6,B|= In+1(In). So, B|= In. By [7]–6.5–(2), it holds that B≺nA as L–structures, so, B|= ψ0(a). Hence, B|= ∃ xψ 0(x). So, B|= In+ψ. But, by [7]–6.6,B|= In+1(In+∀x∃y[Fn,k(x) =y]). Hence, B|= In+ ∀x∃y[Fn,k(x) =y]. Contradiction. ((2)): It follows from (1). 6. Induction rules In this section we shall apply the techniques developed in the above sections to obtain a new proof of Parsons’ conservativeness theorem (see [16]) and a weak version of a result of Beklemishev on induction rules (see [2], corollary 9.1). We are mainly interested in the analysis of the induction rule: IR : ϕ(0), ∀x(ϕ(x)→ϕ(x +1)) ∀x ϕ(x) and the collection rule: CR : ∀x∃y ϕ(x, y) ∀z∃u∀x≤z∃y≤uϕ(x,y) Let Tbe a theory and a class of formulas. We shall denote by T+–IR the closure of Tunder first–order logic and applications of IR restricted to formulas ϕ∈. Following the notation introduced in [2], [T,–IR] is the closure of Tunder first–order logic and unnested applications of –IR: that is, we can only apply –IR if the premises are theorems of T. Finally we define (the theories T+–CR and [T,–CR] are defined in a similar way) [T,–IR]0=T [T,–IR]k+1=[[T,–IR]k,–IR]. Proposition 6.1. [Iϕ n, n+2–IR]⇐⇒ Iϕ n+∀x∃yD ϕ(x, y) ⇐⇒ [Iϕ n, n+1–IR] Proof. We recall that Fϕ,0(x) =yis the formula ϕ(x,y)and Dϕ(x, y) is Fϕ,1(x) = y. So, by 4.5–(2), it holds [Iϕ n, n+2–IR] ⇒ [Iϕ n, n+1–IR] ⇒ Iϕ n+∀x∃yD ϕ(x, y), Then, it is enough to prove that Iϕ n+∀x∃y(D ϕ(x, y)) ⇒ [Iϕ n, n+2–IR] We must prove that, for each ψ(u) ∈n+2,if Iϕ nψ(0)∧∀u (ψ(u) →ψ(u+1)) then Iϕ n+∀x∃yD ϕ(x, y) ∀u ψ(u). We can assume that ψ(u) is ∀x∃y θ(u,x,y), where θ(u,x,y) ∈− n. Indeed, n+2–IR is reductible to its parameter free version. This is easily seen in this case, but it holds also for n+1–IR (see lemma 2.1 in [4]). So we have to prove that (•)Iϕ n+∀x∃yD ϕ(x, y) ∀u∀x∃y θ(u,x,y) Next claims will provide bounds which allow us to reduce the quantifier complexity of the formulas considered. 6.1.1. There exists k∈ωsuch that Iϕ n∀x∃y<Fk ϕ,0(x) θ(0,x,y). Proof. By hypothesis Iϕ n∀x∃yθ(0,x,y); so, the result follows from 4.6 (Fu ϕ,0(x) =yisan–envelope of Iϕ nen Iϕ n).  6.1.2. Let fand Fϕbe new function symbols of arity 1. Let Tfbe the theory of language L=L+f+Fϕ, Iϕ n+∀x1,x 2(x1≤x2→f(x 1)≤f(x 2)) + ∀x∀y (ϕ(x,y) ↔Fϕ(x) =y) Then there exist t(x) and s(x) terms of Lsuch that: (i) Tf∀u[∀x∃y<f(x+u) θ(u, x, y) →∀x∃y<t(x+u) θ(u +1,x,y)] (ii) Tf∀u∀x2∀x1<s(x 2+u) ∃y<f(x 1+u) θ(u, x1,y)→ ∃y<t(x 2+u) θ(u +1,x 2,y) Proof. ((i)): Let cbe a new constant symbol. We prove that there exists a term t(x) of Lsuch that Tf∀x∃y<f(x+c)θ(c,x,y)→∀x∃y<t(x+c)θ(c+1,x,y) For the sake of a contradiction, assume that for each t(x) ∈Term(L), there exist At|= Tf+∀x∃y<f(x+c)θ(c,x,y)and a∈Atsuch that At|= ¬ ∃ y<t(x+c)θ(c+1,a,y) Let dbe a new constant symbol and Tthe theory Tf+∀x∃y<f(x+c)θ(c,x,y) + {¬∃y<t(c+d)θ(c+1,d,y):t(x) ∈Term(L)}. By compactness, Tis consistent. Indeed, if t1,...,t nare terms corresponding to a finite part, T,ofT, and tis t1+···+tn, then At|= T (interpreting din Atas a). Let A|= Tand a=A(d). Let Ibe the initial segment I={e∈A: There exists t(x) ∈Term(L), A|= e<t(a+c)}. Then Iis closed under the function defined in Aby Fϕand, as a consequence, under the function defined by Kn. Hence, I≺nAas L–structures, and Iis closed under f. From this we get that I|= Iϕ nand, as θ∈n, I|= ∀ x∃y<f(x+c)θ(c,x,y). So, I|= Tf+∀x∃y<f(x+c)θ(c,x,y). On the other hand, Iϕ n∀u(∀x∃y θ(u,x,y) →∀x∃yθ(u+1,x,y)); hence, I|= ∀ x∃yθ(c+1,x,y). Since I|= ¬ ∃ yθ(c+1,a,y), this provides the required contradiction. ((ii)): From (i) it follows that Tfproves that ∀u∀x2∃x1[∃y<f(x 1+u) θ(u, x1,y)→∃y<t(x 2+u) θ(u +1,x 2,y)] As in (i) it is proved that there exists a term s(x) of Lsuch that Tfproves ∃x1<s(x 2+u) [∃y<f(x 1+u) θ(u, x1,y)→∃y<t(x 2+u) θ(u +1,x 2,y)]. From this it follows (ii). 6.1.3. There exist m, q ∈ωsuch that if A|= Iϕ n+∀x∃yD ϕ(x, y) and a,b ∈A, then the following formulas are true in A: ∀x∃y<Fb ϕ,0(x +a)θ(a,x,y) →∀x∃y<Fb·m ϕ,0(x +a)θ(a +1,x,y), ∀x1<Fq·b ϕ,0(x2+a)∃y<Fb ϕ,0(x1+a)θ(a,x1,y)→ →∃y<Fb·m ϕ,0(x2+a)θ(a +1,x 2,y) Proof. Let Bbe the expansion of Ato Lgiven by f(x) =Fb ϕ,0(x) and Fϕ(x) = Fϕ,0(x). Let t(x) and s(x) be two terms as in 6.1.2. Then, by induction on terms of L, we obtain that there exist m, q ∈ωsuch that B|= t(x) < Fm·b ϕ,0(x) ∧s(x) < Fq·b ϕ,0(x). This concludes the proof of the claim.  Now we prove (•). Let k,myqbe as in 6.1.1 and 6.1.3, and r=max(k,m,q,2). Let A|= Iϕ n+∀x∃yD ϕ(x, y) and a,d ∈A. Let us see that A|= ∃ y<Fra+1 ϕ,0(d +a)θ(a,d,y) For each j≤a, let ej=(a+1)(a+2) 2−(j+1)(j+2) 2. By induction on j≤awe prove that () A|= ∀ j≤a∀x≤Frej ϕ,0(a +d)∃y<Frj+1 ϕ,0(x +j)θ(j,x,y). j=0: Since A|= ∀ x∃yθ(0,x,y), the result follows from 6.1.1. j→j+1: Assume that () holds for j<a. Let a2≤Frej+1 ϕ,0(a +d) and a= max(a2,a). Then a≤Frej+1 ϕ,0(a +d) and A|= x1<Fq·rj+1 ϕ,0(a2+a) →x1<Fq·rj+1 ϕ,0(2a)≤Frj+2 ϕ,0(a)≤Frej ϕ,0(a +d). Hence, by hypothesis, we get that A|= ∀ x1<Fq·rj+1 ϕ,0(a2+a)∃y<Frj+1 ϕ,0(x1+j)θ(j,x1,y). So, by 6.1.3,A|= ∃ y<Frj+1m ϕ,0(a2+j)θ(j +1,a 2,y). Hence, A|= ∀ x2<Frej+1 ϕ,0(a +d)∃y<Frj+2 ϕ,0(x2+j+1)θ(j +1,x 1,y), and this proves (). Taking j=ain (), we obtain that A|= ∀ x≤F0 ϕ,0(a +d)∃y<Fra+1 ϕ,0(x +a)θ(a,x,y) Since d<F0 ϕ,0(a +d) =a+d,wehaveA|= ∃ y<Fra+1 ϕ,0(d +a)θ(a,d,y). This concludes the proof of the proposition.  Lemma 6.2. Let be a class of n+2–sentences. Then the following theories, [Iϕ n+, n+2–IR]and [Iϕ n+, n+1–IR],aren+2–conservative extensions of Iϕ n++∀x∃yD ϕ(x, y). Proof. We only prove the result for n+2–IR, the other case being similar. By 6.1,[Iϕ n+, n+2–IR] is an extension of Iϕ n++∀x∃y(D ϕ(x, y)). Let us see that it is a n+2–conservative one. Let θ(x) ∈n+2such that (–) Iϕ n+θ(0), and (–) Iϕ n+∀x(θ(x)→θ(x +1)). Then there exists ψ∈such that: (–) Iϕ nψ→θ(0), and (–) Iϕ n∀x[(ψ →θ(x)) →(ψ →θ(x +1))]. Since ψ→θ(x) is n+2, then [Iϕ n, n+2–IR] ∀x(ψ →θ(x)). So, by 6.1, Iϕ n+∀x∃yD ϕ(x, y) ∀x(ψ →θ(x)) So, Iϕ n++∀x∃yD ϕ(x, y) ∀x θ(x).  Theorem 6.3. For all k∈ω, [Iϕ n, n+2–IR]k⇐⇒ [Iϕ n, n+1–IR]k⇐⇒ Iϕ n+∀x∃y(Fϕ,k(x) =y) Proof. It is enough to prove, by induction on k, that [Iϕ n, n+2–IR]k⇐⇒ Iϕ n+∀x∃y(Fϕ,k(x) =y). k=0: Since Fϕ,0(x) =yis ϕ(x,y); it holds that [Iϕ n, n+2–IR]0⇐⇒ Iϕ n⇐⇒ Iϕ n+∀x∃y(Fϕ,0(x) =y). k→k+1: Suppose that [Iϕ n, n+2–IR]k⇐⇒ Iϕ n+∀x∃y(Fϕ,k(x) =y).By definition [Iϕ n, n+2–IR]k+1=[[Iϕ n, n+2–IR]k, n+2–IR], so [Iϕ n, n+2–IR]k+1⇐⇒ [Iϕ n+∀x∃y(Fϕ,k(x) =y),n+2–IR].