Induction, minimization and collection for Δ n+1 (T)–formulas

INDUCTION, MINIMIZATION AND COLLECTION FOR ∆n+1(T)–FORMULAS A. Fern´andez–Margarit and F. F. Lara–Mart´ın Depto. Ciencias de la Computaci´on e I. A. Fac. de Matem´aticas, Universidad de Sevilla C/Tarfia s/n, Sevilla (Spain) ffla[email protected] Abstract. For a theory T, we study relationships among I∆n+1(T), L∆n+1(T) and B∗∆n+1(T). These theories are obtained restricting the schemes of induction, minimization and (a version of) collection to ∆n+1(T) formulas. We obtain conditions on T (Tis an extension of B∗∆n+1(T) or ∆n+1(T) is closed (in T) under bounded quantification) under which I∆n+1(T) and L∆n+1(T) are equivalent. These conditions depend on ThΠn+2 (T), the Πn+2–consequences of T. The first condition is connected with descriptions of ThΠn+2 (T) as IΣnplus a class of nondecreasing total Πn–functions, and the second one is related with the equivalence between ∆n+1(T)– formulas and bounded formulas (of a language extending the language of Arithmetic). This last property is closely tied to a general version of a well known theorem of R. Parikh. Using what we call Πn–envelopes we give uniform descriptions of the previous classes of nondecreasing total Πn–functions. Πn–envelopes are a generalization of envelopes (see [10]) and are closely related to indicators (see [12]). Finally, we study the hierarchy of theories I∆n+1(IΣm), m≥n, and prove a hierarchy theorem. 1. Introduction This paper is devoted to the study of two main topics: the relationship between induction and minimization, and the description of the class of Πn+2 consequences of a theory. The first one is on Fragments of Arithmetic obtained restricting the schemes of induction, minimization and collection to ∆n+1–formulas. These schemes for Σnand Πn formulas have been thoroughly studied by J. Paris, L. Kirby and others (see [17] or [12]). The parameter free versions of those schemes have been studied by R. Kaye, J. Paris and C. Dimitracopoulos (see [11] and [14]). However, the relationships between those schemes for ∆n+1 formulas are not well known. About 1985, H. Friedman claimed that L∆n+1 and I∆n+1 are equivalent (see [10] pg. 398), but in [6] that equivalence appears as an open problem (problem 34) and it is credited to J. Paris. Here that equivalence will be called the Paris–Friedman’s Conjecture. In [19], T. Slaman proves it for n≥1. Research partially supported by grant PB96–1345 (Spanish Government). 1 In sections 2and 6, we study those schemes restricted to ∆n+1(T) formulas. If ϕ∈Σn+1 and ψ∈Πn+1 then ϕ↔ψis a Πn+2 formula. So, the second topic is related to the first one. In sections 3–5, we analyse the class of Πn+2 consequences of a theory using a class of Πn–functions and extensions of the language of Arithmetic related to that class of functions. Now we present the main results obtained on these topics in this paper. Part I: Induction and minimization for ∆n+1(T)formulas. In order to get a better insight on the Paris–Friedman’s Conjecture we consider the theories I∆n+1(T), L∆n+1(T) and B∗∆n+1(T), where ∆n+1(T) = {ϕ(x,~v)∈Σn+1 : there exists ψ(x,~v)∈Πn+1,T`ϕ↔ψ}. The idea is to change the semantic part of the axioms schemes on ∆n+1 formulas by a syntactic condition: the equivalence between a Σn+1 formula and a Πn+1 formula is proved in a theory. Thus we obtain a relativization of Paris–Friedman’s Conjecture. We study the following problem: (∗) Under which conditions on Tdoes L∆n+1(T)⇐⇒ I∆n+1(T) hold? We first observe that =⇒always holds. In the other way, let us notice that the usual proof of IΣn+1 =⇒LΣn+1 leans upon the closure of Σn+1 under bounded quantification (this property is granted by the collection schemes, BΣn+1). In fact, the closure under bounded quantification of the class of ∆n+1–formulas is the main obstacle in order to adapt the refered proof to obtain that I∆n+1 =⇒L∆n+1. So, to answer problem (∗) the above remarks suggest two natural properties: Thas ∆n+1–collection (that is, T=⇒B∗∆n+1(T)), and Tis ∆n+1–closed (that is, ∆n+1(T) is closed in Tunder bounded quantification). We prove that if Tsatisfies one of the above conditions then L∆n+1(T)⇐⇒ I∆n+1(T), see theorem 1.4. We also study relationships among the above schemes, for distinct theories. The following theorem sums up the results obtained. Theorem 1.1 (see 2.1, 2.10, 2.17, 2.18, 6.12, 6.13, 6.14).For all n∈ω IΣn⇐⇒ L∆n+1(IΣn)⇐⇒ I∆n+1(IΣn)⇐⇒ B∗∆n+1(IΣn) ⇑ ⇑ ⇑ BΣ− n+1,IΠ− n+1 I∆n+1,BΣn+1 ff×⇐⇒ L∆n+1(IΣn+1)⇐⇒ I∆n+1(IΣn+1)|=⇒B∗∆n+1(IΣn+1) ⇑ ⇑ ⇑ . . . . . . . . . ⇑ ⇑ ⇑ IΣ− n+1 IΠ− n+1,BΣ− n+1 ×⇐= ×⇐⇒ L∆n+1(PA)⇐⇒ I∆n+1(PA)|=⇒B∗∆n+1(PA) ⇑ ⇑ ⇑ BΣn+1 IΠ− n+1 BΣ− n+1 ×⇐⇒ ⇐=| ×=⇒ L∆n+1(N)⇐⇒ I∆n+1(N)|=⇒B∗∆n+1(N) ⇑ ⇑ IΣn+1 |=⇒BΣn+1 (Some of those relations for parameter free schemes follow from results in [9], see also [7] and [15]). 2 Part II: Πn+2 consequences of a theory. Properties considered in part I (Thas ∆n+1–collection, Tis ∆n+1–closed and others that we call ∆n+1–properties) depend on ThΠn+2 (T), the class of Πn+2 consequences of T. Here we give characterizations of these properties in a “functional” way. The idea is to describe ThΠn+2 (T) using IΣnand a class of Πn–functions. To this end we introduce the concepts of Πn–functional class (which provides a characterization of the theories having ∆n+1–collection) and Πn–Parikh pair (which corresponds with ∆n+1–closed theories). Essentially, a Πn–functional class is a set of nondecreasing Πn–functions. The concept of Πn–Parikh pair is suggested by the following well known result. Theorem 1.2 (Parikh).Let ϕ(x, y)∈Σ1. If I∆0` ∀x∃y ϕ(x, y)then there exists t(x)∈ Term(L)such that I∆0` ∀x∃y≤t(x)ϕ(x, y). As a consequence of this result (see 3.27) each ∆1(I∆0) formula is equivalent (in I∆0) to a ∆0–formula. So, ∆1(I∆0) is closed (in I∆0) under bounded quantification. We give a general version of this fact. If Tis ∆n+1–closed, then there is a conservative extension of ThΠn+2 (T) (in a language extending the language of Arithmetic) in which each ∆n+1(T) formula is equivalent to a bounded formula. In particular, if Thas ∆n+1–collection then a strong Πn–functional class provides such an extension. One crutial result that relates the schemes of induction and collection is the Friedman– Paris’ conservativeness theorem (see [10] or [12]): Theorem 1.3. For all n∈ω,ThΠn+2 (IΣn) = ThΠn+2 (BΣn+1). Here we study a similar Πn+2–conservativeness property, closely tied to ∆n+1–collection: ThΠn+2 (T) = ThΠn+2 (T+BΣn+1). This property plays a central role in the study of Πn–envelopes that will be developed in section 5. Roughly speaking, a Πn–envelope is a Πn–functional class given in an uniform way and generalizes the concept of envelope (see [10]). In section 6we use results of sections 4and 5to separate the fragments I∆n+1(IΣm), m≥n(see theorem 1.1). The following theorem sums up, for a consistent theory, T, the relationships among the concepts introduced. Theorem 1.4. (see 2.10, 2.11, 3.8, 3.11, 3.28, 4.18, 5.11, 5.21) Tis ∆n+1-PF Thas ∆n+1-min. Tis strong Πn-funct. Thas Πn-s-env. ⇑ m m m3 Tis ∆n+1-closed ⇐=Thas ∆n+1-coll. ⇐⇒ Tis Πn-funct. ⇐⇒2 3Thas Πn-env. m m m1 Tis Πn–Parikh Thas ∆n+1-ind. Tis ∆n+1-closed Tis ΠB n+2-conserv. Where: =⇒1holds if Tis Πn+2 axiomatizable; ⇐=2holds if the Πn–envelope is given by aΠnformula; and =⇒3holds if Tis recursively axiomatizable, and, for n= 0,T`exp. In order to simplify the statement of the above theorem we have used there the following notation: Thas Πn–envelope (Πn–s–envelope) means that there exists a Πn– envelope (strong Πn–envelope) of Tin IΣn; and Tis ΠB n+2–conservative if ThΠn+2 (T) = ThΠn+2 (T+BΣn+1). 3 The analysis of theories I∆n+1(T) and B∗∆n+1(T) that we develop in this paper is related with the work of L. D. Beklemishev in [2], [3] and [4], on induction and collection as inference rules. Some results in those papers, proved there using Proof Theoretic techniques, are similar to those given here for schemes on ∆n+1(T)–formulas. Now we give a more precise description of the relationship between Beklemishev’s work and ours. In the papers cited above, Beklemishev study the schemes of induction and collection as inference rules. The induction rule for a formula ϕ(x) is: ϕ(0),∀x(ϕ(x)→ϕ(x+ 1)) ∀x ϕ(x) If Γ is a class of formulas, then Γ–IR is the class of induction rules for each formula in Γ. Given a theory T, let T+ Σn+1–IR be the closure of Tunder first order logic and applications of Σn+1–IR. We also denote by [T,Σn+1–IR] the closure of Tunder first order logic and unnested applications of Σn+1–IR; that is, the rule of induction can be applied only if the hypothesis of the rule are theorems of T(in first order logic). The rule of collection for a formula ϕ(x, y) is: ∀x∃y ϕ(x, y) ∀z∃u∀x≤z∃y≤u ϕ(x, y) Theories T+ Σn+1–CR and [T,Σn+1–CR] are defined as for the induction rule. In [4] it is also considered the induction rule for ∆n+1 formulas: for each ϕ(x)∈Σn+1 and ψ(x)∈Πn+1 ∆n+1–IR : ∀x(ϕ(x)↔ψ(x)) Iϕ,x As we shall see in 2.19, a theory T(extension of I∆0) has ∆n+1–collection if and only if Tis closed under Σn+1–CR (that is, [T,Σn+1–CR] ⇐⇒ T). For induction we have that Thas ∆n+1–induction if and only if Tis closed under ∆n+1–IR. Our analysis of theories with ∆n+1–collection using Πn–functional classes is also very similar (for n= 0) to the one given by Beklemishev in [2] using what he call monotone formulas. In this way theorem 3.5 can be considered a generalization of theorem 5.4 of [2] (and it is linked with theorem 4.2 of [3]). Nevertheless, we must observe that one of the aims of Beklemishev’s work in [3] is to obtain a proof of Friedman–Paris’ conservativeness theorem. On the other hand, our analysis goes in a reverse direction, since we take that result as basic (due to its easy model theoretic proof) and relate it with a characterization of Πn–envelopes using indicators (Πn–IND property, see theorem 5.6). The relationship of Σn+1–IR with the work developed here is not so obvious. But, as Beklemishev has noted (personal communication), I∆n+1(IΣn+1)⇐⇒ I∆0+ Σn+1–IR. This fact is closely tied to a conservativeness theorem of Parsons (see [18]) ThΠn+2 (IΣn+1)⇐⇒ I∆0+ Σn+1–IR. These results are more deeply studied in [8] in connection with axiomatization properties of the theories I∆n+1(T). We conclude this section with some basic results and notation that we use through this paper. We work in the first–order language of Arithmetic, L={0,1,+,·, <}and N denotes the standard model of Lwhose universe is the set of the natural numbers, ω. As 4 usual, bounded quantifiers are denoted by ∀x≤t ϕ(x) and ∃x≤t ϕ(x) (where xdoes not occur in t). ∆0= Σ0= Π0is the class of bounded formulas and, for each n∈ω, Σn+1 ={∃~x ϕ(~x) : ϕ(~x)∈Πn}and Πn+1 ={∀~x ϕ(~x) : ϕ(~x)∈Σn}. Let ϕ(x,~v) be a formula of L. We shall denote ϕ(x,~v)∧ ∀y < x ¬ϕ(y,~v) by ϕµ,x(x,~v). If A|=ϕµ,x(a,~ b) then we write A|=a= (µx)[ϕ(x,~ b)]. If there is no danger of misunderstanding we omit the subscript xand the parameters ~v and we shall write ϕµ(x). We denote by P−a finite set of Π1axioms such that if A|=P−then Ais the nonnegative part of a commutative discretely ordered ring (see [12]). Let ϕ(x,~v) be a formula. The induction and the least number principle axioms for ϕ(x,~v) with respect to xare, respectively, the following formulas Iϕ,x(~v)≡ϕ(0,~v)∧ ∀x[ϕ(x,~v)→ϕ(x+ 1,~v)] → ∀x ϕ(x,~v), Lϕ,x(~v)≡ ∃x ϕ(x,~v)→ ∃x ϕµ,x(x,~v). Let ϕ(x, y,~v) be a formula. The collection axiom and the strong collection axiom for ϕ with respect to x, y are, respectively, the formulas Bϕ,x,y(z,~v)≡ ∀x≤z∃y ϕ(x, y,~v)→ ∃u∀x≤z∃y≤u ϕ(x, y,~v), Sϕ,x,y(z,~v)≡ ∃u∀x≤z[∃y ϕ(x, y,~v)→ ∃y≤u ϕ(x, y,~v)]. As usual, we write Iϕinstead of Iϕ,x and similarly we use Lϕ,Bϕand Sϕ. If Γ is a class of formulas of L, then IΓ = P−+{Iϕ:ϕ∈Γ}. The theory LΓ is defined similarly using Lϕinstead of Iϕ. For collection, BΓ = I∆0+{Bϕ:ϕ∈Γ}and using Sϕinstead of Bϕ we obtain SΓ. Peano Arithmetic is the theory PA =P−+{Iϕ:ϕformula}. Now we consider schemes for parameter free formulas. Let Γ be a class of formulas. We write ϕ(x1, . . . , xn)∈Γ−if ϕ∈Γ and x1, . . . , xnare all the variables that occur free in ϕ. Then IΓ−=P−+{Iϕ,x :ϕ(x)∈Γ−}(similarly for LΓ−) and BΓ−=I∆0+{B− ϕ,x,y : ϕ(x, y)∈Γ−}, where B− ϕ,x,y ≡ ∀x∃y ϕ(x, y)→ ∀z∃u∀x≤z∃y≤u ϕ(x, y). The parameter free version of the strong collection scheme for Σnformulas is equivalent to SΣn. One of the basic functions used to describe metamathematical properties in the language of Arithmetic, such as truth predicates, is the exponential function. Let E(x, y, z) be a ∆0–formula that defines in the standard model the exponential function, I∆0proves its basic properties and IΣ1proves that it is total (see [10] for details). We shall usually write xy=zinstead of E(x, y, z) and shall denote by exp the Π2sentence ∀x∀y∃zE(x, y, z). We shall write: T=⇒T0, if Tis an extension of T0;T×=⇒T0, if Tis not an extension of T0;T×⇐⇒ T0, if T×=⇒T0and T0×=⇒T;T⇐⇒ T0, if Tand T0are equivalent; and T|=⇒T0, if Tis a proper extension of T0. We recall some definitions and results which are important in the study of the above schemes. Let A|=P−,n∈ωand X⊆A. Then Kn(A, X) (if Xis the empty set, we write Kn(A)) is the substructure of Awhose universe is {b∈A:bis Σndefinable in (A, X)}. In(A, X) is the initial segment of Adetermined by Kn(A, X). It holds the following results. Theorem 1.5. (1) Let A|=IΣnbe nonstandard. Then for all X⊆A (a) Kn+1(A, X)≺n+1 Aand Kn+1(A, X)|=IΣn. (b) Kn+1(A, X)≺c n+1 In+1(A, X)≺e nA. (⊂cand ⊂emean cofinal and initial substructure, respectively). 5 (c) If Kn+1(A, X)is not cofinal in Athen In+1(A, X)|=BΣn+1. (2) Let A|=IΣn+1 be nonstandard such that Kn+1(A)is nonstandard. Then Kn+1(A)6|= BΣ− n+1 and In+1(A)6|=IΣn+1. Finally, we introduce the axiom schemes for ∆n+1 formulas. I∆n+1 =P−+{∀x[ϕ(x,~v)↔ψ(x,~v)] →Iϕ,x(~v) : ϕ∈Σn+1, ψ ∈Πn+1}. Using Lϕinstead of Iϕ, we obtain L∆n+1. Parameter free schemes, I∆− n+1 and L∆− n+1, are defined similarly. Uniform versions of the above fragments have been introduced by R. Kaye (see [11]). UI∆n+1 is P−together with, for all ϕ∈Σn+1, ψ ∈Πn+1, ∀x∀~v [ϕ(x,~v)↔ψ(x,~v)] → ∀~v Iϕ,x(~v). UL∆n+1 is defined accordingly using Lϕ. We introduce a uniform version of collection. UB∆n+1 is I∆0together with, for all ϕ∈Πnand ψ∈Σn, ∀x∀~v [∃y ϕ(x, y,~v)↔ ∀w ψ(x, w,~v)] → ∀z∀~v Bϕ,x,y(z,~v). Theorem 1.6. For all n∈ω,I∆− n+1 ×=⇒UL∆n+1 and IΠ− n+1 |=⇒L∆− n+1 =⇒I∆− n+1 ⇑ ⇑ UB∆n+1 ⇐⇒ BΣ− n+1 ⇐⇒ UL∆n+1 =⇒UI∆n+1 |=⇒IΣn ⇑ ⇑ ⇑ BΣn+1 ⇐⇒ L∆n+1 =⇒I∆n+1 For n≥1,L∆− n+1 ×=⇒UI∆n+1 and I∆− n+1 ×⇐⇒ IΣn, but I∆− 1|=⇒I∆0. R.O. Gandy (see [10]) proved the equivalence between L∆n+1 and BΣn+1; and R. Kaye (see [11]) obtained a similar result for the uniform versions. See [9] for UI∆n+1 |=⇒IΣn, L∆− n+1 ×=⇒UI∆n+1 and I∆− n+1 ×=⇒UL∆n+1; [7] for I∆n+1 |=⇒UI∆n+1;2.14 for UB∆n+1 ⇐⇒ BΣ− n+1; and [4] for UI∆1|=⇒I∆− 1(there UI∆1is denoted by sI∆1). The above diagram contains the following open problems: (–): The Paris–Friedman’s Conjecture: L∆n+1 ⇐⇒ I∆n+1. (–): The Uniform Paris–Friedman’s Conjecture: UL∆n+1 ⇐⇒ UI∆n+1. (–): The Parameter Free Paris–Friedman’s Conjecture: L∆− n+1 ⇐⇒ I∆− n+1. Recently, T. Slaman (see [19]) has obtained a partial answer. He has proved that L∆n+1 +exp ⇐⇒ I∆n+1 +exp. On the other hand, L. Beklemishev (see [4]) has proved that I∆1+exp is a Σ3– conservative extension of UI∆1+exp; hence, UL∆1+exp ⇐⇒ UI∆1+exp. Beklemishev’s result seems to be easily extended to n≥1; so, only the case n= 0 seems to be open in the two first problems. However, Slaman’s proof rests on the equivalence between BΣn+1 and L∆n+1; therefore it can not be adapted to the parameter free problem. 6 2. The theories I∆n+1(T),L∆n+1(T)and B∗∆n+1(T) Through this paper Twill denote a consistent theory in the first–order language of Arithmetic. For such a theory we introduce the classes of formulas ∆n+1(T) = {ϕ(x,~v)∈Σn+1 : there exists ψ(x,~v)∈Πn+1,T`ϕ↔ψ}. When the schemes of induction and minimization are restricted to these classes of formulas we obtain the theories I∆n+1(T) and L∆n+1(T). We also consider the following version of the collection schemes B∗∆n+1(T) = I∆0+{Bϕ,x,y(z,~v) : ϕ∈Πn,∃y ϕ(x, y,~v)∈∆n+1(T)}. Remark 2.1.We shall begin with some basic properties of the theories introduced above. First we observe that IΣn+1 =⇒I∆n+1(T) =⇒IΣn. If ϕ∈Σn+1 and ψ∈Πn+1 then ϕ↔ψis a Πn+2–formula. So, it follows that (a similar result holds for minimization and collection) Claim 2.2. If ThΠn+2 (T) = ThΠn+2 (T0)then I∆n+1(T)⇐⇒ I∆n+1(T0). Let ∆∗ n+1(T) be the dual class of ∆n+1(T). Since the negation of a ∆n+1(T) formula (that is, a ∆∗ n+1(T)–formula) is equivalent (in T) to a ∆n+1(T)– formula, as in the proof of IΠn+1 ⇐⇒ IΣn+1 (see lemma 7.5 in [12]), we get that Claim 2.3. L∆n+1(T) =⇒I∆∗ n+1(T)⇐⇒ I∆n+1(T). For each ψ(x, y)∈Πn−1,∃y[ψ(x, y)∨(¬∃z ψ(x, z)∧y= 0)] ∈∆n+1(T). So, as in the proof of BΣn+1 =⇒IΣn(see I.2.15 in [10]), we obtain Claim 2.4. B∗∆n+1(T) =⇒IΣn. Hence, for n≥1,B∗∆n+1(T)|=⇒BΣn. Suppose that Tis an extension of IΣn. Let ϕ∈Πnand ψ∈Σnsuch that T` ∃y ϕ(x, y)↔ ∀y ψ(x, y). Let us consider the following formulas θ1(x, w)≡x≤w∧ ∃u[ϕµ,u(x, u)∧(∀z)x≤z≤w∃y≤u ϕ(z, y)], θ2(x, w)≡x≤w∧ ∀y ψ(x, y)∧ ∀u[ϕ(x, u)→(∀z)x≤z≤w∃y≤u ϕ(z, u)]. Then T`θ1(x, w)↔θ2(x, w) and θ1∈Σn+1 and θ2∈Πn+1 in Tand in L∆n+1(T). From this, as in lemma I.2.17 in [10], we obtain that Claim 2.5. If Tis an extension of IΣnthen L∆n+1(T) =⇒B∗∆n+1(T). Definition 2.6. (∆n+1 properties) We say that (1) Tis ∆n+1–closed if ∆n+1(T)is closed in Tunder bounded quantifiers. (2) Thas ∆n+1–collection if T=⇒B∗∆n+1(T). (3) Thas ∆n+1–minimization if T=⇒L∆n+1(T). (4) Thas ∆n+1–induction if T=⇒I∆n+1(T). (5) Tis ∆n+1–PF if I∆n+1(T)⇐⇒ L∆n+1(T). 7 Remark 2.7.Let us consider some examples of theories having ∆n+1 properties. Since BΣn+1 =⇒B∗∆n+1(T), we get that every theory extending BΣn+1 has ∆n+1–collection. Now we improve this result. Claim 2.8. If T=⇒BΣ− n+1 then Thas ∆n+1–collection. Proof of Claim. Let ϕ(x, y, v1, . . . , vm)∈Π− nand ψ(x, w,~v)∈Σ− nsuch that T` ∃y ϕ(x, y,~v)↔ ∀w ψ(x, w,~v). Let θ(x, y)∈Σ− n+1 be ϕ((x)0, y, (x)1, . . . , (x)m)∨[y= 0 ∧ ¬∀w ψ((x)0, w, (x)1, . . . , (x)m)]. Since T` ∀x∃y θ(x, y), T` ∀z∃u∀x≤z∃y≤u θ(x, y). Let A|=Tand a,~ b∈A such that A|=∀x≤a∃y ϕ(x, y,~ b) and c=ha,~ bi. Then there exists d∈Asuch that A|=∀x≤c∃y≤d θ(x, y). Since a≤c, then A|=∀x≤a∃y≤d ϕ(x, y,~ b); hence, A|=Bϕ, as required. ¤ There exist theories, e.g. IΣn(see 2.17), that have ∆n+1–collection and are not extension of BΣ− n+1. Now we present a case in which both conditions are equivalent. Claim 2.9. If Tis complete and has ∆n+1–collection then T=⇒BΣ− n+1. Proof of Claim. Let A|=Tand θ(x, y)∈Σ− n+1 such that A|=∀x∃y θ(x, y). Since T is complete, T` ∀x∃y θ(x, y); so, ∃y θ(x, y)∈∆n+1(T). Since Thas ∆n+1–collection, A|=Bθ; hence, A|=∀z∃u∀x≤z∃y≤u θ(x, y). ¤ Next result was, chronologically, the main reason to introduce the theory B∗∆n+1(T). This theory became one of the main tools in this work once we came to the concept of Πn–functional theory (see subsection 3.1). Theorem 2.10. (1) If Tis ∆n+1–closed then Tis ∆n+1–PF. (2) If Thas ∆n+1–collection then Tis ∆n+1–closed. Proof. ((1)): By 2.3, it is enough to see that I∆n+1(T) =⇒L∆n+1(T). Suppose that there exist A|=I∆n+1(T) and ϕ(x)∈∆n+1(T) such that A|=∃x ϕ(x)∧ ∀x¬ϕµ(x). Let θ(z)∈Πn+1 be ∀x≤z¬ϕ(x). We have that A|=θ(0) ∧[θ(z)→θ(z+ 1)]. Since Tis ∆n+1–closed, θ(z)∈∆∗ n+1(T). By 2.3,A|=I∆∗ n+1(T); so, A|=∀x¬ϕ(x), a contradiction. ((2)): Let ϕ(x, y)∈Πn,ψ(x, y)∈Σnsuch that T` ∃y ϕ(x, y)↔ ∀y ψ(x, y). By the closure properties under bounded quantification of BΣn, there exists θ(z)∈Σn+1 such that BΣn`θ(z)↔ ∃u∀x≤z∃y≤u ϕ(x, y) (for n= 0, we do not need BΣn). The following equivalences hold in the given theories. ∀x≤z∀y ψ(x, y)↔ ∀x≤z∃y ϕ(x, y) [in T] ↔ ∃u∀x≤z∃y≤u ϕ(x, y) [in B∗∆n+1(T)] ↔θ(z) [in BΣn] Since Thas ∆n+1–collection, all the above equivalences hold in T. Then, as ∀x≤ z∀y ψ(x, y)∈Πn+1,θ(z)∈∆n+1(T). So, ∀x≤z∃y ϕ(x, y) is equivalent in Tto a ∆n+1(T) formula. ¤ 8 Remark 2.11.Now we describe others elementary relations among ∆n+1 properties of a theory. Claim 2.12. If Thas ∆n+1–collection then Thas ∆n+1–induction. Proof of Claim. Suppose that T` ∃y ϕ(x, y)↔ ∀y ψ(x, y), where ϕ(x, y)∈Πn,ψ(x, y)∈ Σn. Let θ(x, y)∈Πnbe ϕ(x, y)∨ ¬ψ(x, y). Since T` ∀x∃y θ(x, y), then ∃y θ(x, y)∈ ∆n+1(T). Now the proof continues as in 2.4.¤ Claim 2.13. The following conditions are equivalent (i) Thas ∆n+1–collection. (ii) Tis ∆n+1–closed and has ∆n+1–induction. (iii) Thas ∆n+1–minimization. Proof of Claim. (i) =⇒(ii) is 2.10 and 2.12.(ii) =⇒(iii) follows from 2.10–(1). ((iii) =⇒(i)): Suppose that Thas ∆n+1–minimization. Then T=⇒IΣn; so, by 2.5, L∆n+1(T) =⇒B∗∆n+1(T). Hence, T=⇒B∗∆n+1(T). ¤ For each model A,Th(A) has ∆n+1–collection if and only if A|=UB∆n+1 (or A|= BΣ− n+1, see 2.9); and Th(A) has ∆n+1–minimization if only if A|=UL∆n+1. So, as a consequence of 2.13, we obtain that Claim 2.14. BΣ− n+1 ⇐⇒ UB∆n+1 ⇐⇒ UL∆n+1. Remark 2.15 (ThΠn+2 (T)and ∆n+1 properties).Here we shall see that a theory Thas a ∆n+1–property if and only if ThΠn+2 (T) has that property. This is easily seen for ∆n+1–closed. Now we consider ∆n+1–induction. Claim 2.16. T=⇒I∆n+1(T)if and only if ThΠn+2 (T) =⇒I∆n+1(T). Proof of Claim. Let ϕ∈Σn+1 and ψ∈Πn+1 such that T`ϕ↔ψ. Let Iϕ,ψ be ψ(0) ∧ ∀x[ϕ(x)→ψ(x+ 1)] → ∀x ψ(x). Then, ThΠn+2 (T)`Iϕ↔Iϕ,ψ. Suppose that Thas ∆n+1–induction, then T`Iϕ; hence, T`Iϕ,ψ. Since Iϕ,ψ ∈Πn+2,ThΠn+2 (T)`Iϕ,ψ; so, ThΠn+2 (T)`Iϕ, as required. ¤ From this, 2.13 and 2.10 we get a similar result for L∆n+1(T); and from 2.5, using again 2.13, also for B∗∆n+1(T). Claim 2.17. If ThΠn+2 (T) = ThΠn+2 (BΣn+1),Thas ∆n+1–collection. So, IΣn,I∆n+1 and UI∆n+1 have ∆n+1–collection. Remark 2.18.Now we study relations between I∆n+1(T) and IΣn,BΣn+1 and BΣ− n+1. By 2.17,IΣnhas ∆n+1–collection; so, by 2.10 and 2.4, it follows that IΣn⇐⇒ I∆n+1(IΣn)⇐⇒ L∆n+1(IΣn)⇐⇒ B∗∆n+1(IΣn). From this result, 1.3 and 2.2 we get that IΣn⇐⇒ I∆n+1(BΣn+1)⇐⇒ L∆n+1(BΣn+1)⇐⇒ B∗∆n+1(BΣn+1). 9 Claim 3.23. Let ψ(~x, ~y)∈Π− nsuch that T` ∀~x ∃~y ψ(~x, ~y). There is a term of L(Grn(T)), t(~x), such that (IΣn+Funcn(T))Grn(T)` ∀~x ∃~y ≤t(~x)ψ(~x, ~y). Proof of Claim. Let ψ0(u, v) be ∀~x ≤u∀~y ≤v ψc(u, v, ~x, ~y), where ψc(u, v, ~x, ~y) is as in 3.3. Then T` ∀u∃v ψ0(u, v). Let θ(u, v)∈Π− nbe ψ0 f(u, v), see 3.4, and let t(~x) be the term Gθ(Jk(x1, . . . , xk)) (where Jk(x1, . . . , xk) is a term of L(Grn(T)) associated to Cantor’s function used in contraction of quantifiers). Then (IΣn+ Funcn(T))Grn(T)` ∀~x ∃~y ≤t(~x)ψ(~x, ~y). ¤ In what follows (Γ,Γ1) shall denote a Πn–Parikh pair. Claim 3.24. (n≥1) Let ϕ(~x, ~y)∈Πn−1and ψ(~x, ~y)∈Σn−1. Then there exist terms of L(Γ),t(~x),t0(~x), such that (IΣn+ Γ1)Γ` ∃~y ϕ(~x, ~y)↔ ∃~y ≤t(~x)ϕ(~x, ~y), (IΣn+ Γ1)Γ` ∀~y ψ(~x, ~y)↔ ∀~y ≤t0(~x)ψ(~x, ~y). Proof of Claim. Let ϕ1(~x, ~y)∈Πnbe the formula ϕ(~x, ~y)∨(∀~z ¬ϕ(~x, ~z)∧~y = 0). Since IΣn+ Γ1` ∀~x ∃~y ϕ1(~x, ~y), by 3.20–(1), there exists a term of L(Γ), t(~x), such that (IΣn+ Γ1)Γ` ∀~x ∃~y ≤t(~x)ϕ1(~x, ~y); hence, (IΣn+ Γ1)Γ` ∃~y ϕ(~x, ~y)↔ ∃~y ≤t(~x)ϕ(~x, ~y). For ψ∈Σn−1we obtain the result, from the above one, using ¬ψ.¤ Claim 3.25. Let ϕ(~x, ~y)∈∆Γ 0such that (IΣn+ Γ1)Γ` ∀~x ∃~y ϕ(~x, ~y).There is a term t(~x) of L(Γ) such that (IΣn+ Γ1)Γ` ∀~x ∃~y ≤t(~x)ϕ(~x, ~y). Proof of Claim. By 3.20–(2), there exists ψ(~x, ~y, z)∈Πnsuch that ∃z ψ(~x, ~y, z)∈∆n+1(IΣn+ Γ1) and (IΣn+ Γ1)Γ`ϕ(~x, ~y)↔ ∃z ψ(~x, ~y, z). Let t(~x) be a term of L(Γ) such that (IΣn+ Γ1)Γ` ∀~x ∃~y, z ≤t(~x)ψ(~x, ~y, z). Then (IΣn+ Γ1)Γ` ∀~x ∃~y ≤t(~x)ϕ(~x, ~y). ¤ Claim 3.26. Let ϕ(~x)∈∆Γ 1((IΣn+ Γ1)Γ). Then there exists θ(~x)∈∆Γ 0such that (IΣn+ Γ1)Γ`ϕ(~x)↔θ(~x). Proof of Claim. Assume (IΣn+ Γ1)Γ` ∃y ϕ0(~x, y)↔ ∀y ψ0(~x, y), where ϕ0(~x, y) and ψ0(~x, y) are ∆Γ 0and ϕ(~x) is ∃y ϕ0(~x, y). Let δ(~x, y)∈∆Γ 0the formula ϕ0(~x, y)∨ ¬ ψ0(~x, y). Then (IΣn+ Γ1)Γ` ∀~x ∃y δ(~x, y); so, by 3.25, there exists a term t(~x) of L(Γ) such that (IΣn+ Γ1)Γ` ∀~x ∃y≤t(~x)δ(~x, y). Hence, (IΣn+ Γ1)Γ`ϕ(~x)↔ ∃y≤t(~x)ϕ0(~x, y). ¤ Theorem 3.27. Let (Γ,Γ1)be a Πn–Parikh pair, ϕ(~x)∈∆n+1(IΣn+ Γ1). Then there exists θ(~x)∈∆Γ 0such that (IΣn+ Γ1)Γ`ϕ(~x)↔θ(~x). Proof. For n= 0 the result follows from 3.26. Suppose that n≥1. Let ϕ0(~x, ~y, ~z1, . . . , ~zn), ψ0(~x, ~y, ~z1, . . . , ~zn)∈∆0such that (assume neven) (–): ϕ(~x)≡ ∃~y ∀~z1∃~z2. . . ∃~znϕ0(~x, ~y, ~z1, ~z2, . . . , ~zn), (–): ψ(~x)≡ ∀~y ∃~z1∀~z2. . . ∀~znψ0(~x, ~y, ~z1, ~z2, . . . , ~zn), and (–): (IΣn+ Γ1)Γ`ϕ(~x)↔ψ(~x). 16 By 3.24, there exist t1(~x, ~y), t2(~x, ~y, ~z1), . . . , tn(~x, ~y, ~z1, . . . , ~zn−1) terms of L(Γ) such that the following formulas are equivalent in (IΣn+ Γ1)Γ (–): ∀~z1∃~z2...∃~znϕ0(~x, ~y, ~z1, . . . , ~zn). (–): ∀~z1≤t1(~x, ~y)∃~z2≤t2(~x, ~y, ~z1). . . ∃~zn≤tn(~x, ~y, ~z1, . . . , ~zn−1)ϕ0. Let ϕ0(~x, ~y)∈∆Γ 0be the last formula. Analogously, we get that there exist t0 1(~x, ~y), t0 2(~x, ~y, ~z1), . . . , t0 n(~x, ~y, ~z1, . . . , ~zn−1) terms of L(Γ) such that the following formulas are equivalent in (IΣn+ Γ1)Γ (–): ∃~z1∀~z2. . . ∀~znψ0(~x, ~y, ~z1, . . . , ~zn). (–): ∃~z1≤t0 1(~x, ~y)∀~z2≤t0 2(~x, ~y, ~z1). . . ∀~zn≤t0 n(~x, ~y, ~z1, . . . , ~zn−1)ψ0. Let ψ0(~x, ~y)∈∆Γ 0be the last formula. Then (IΣn+ Γ1)Γ` ∃~y ϕ0(~x, ~y)↔ ∀~y ψ0(~x, ~y). So, ∃~y ϕ0(~x, ~y)∈∆Γ 1((IΣn+Γ1)Γ) and, by 3.26, there is θ(~x)∈∆Γ 0such that (IΣn+Γ1)Γ` ∃~y ϕ0(~x, ~y)↔θ(~x); hence, (IΣn+ Γ1)Γ`ϕ(~x)↔θ(~x), as required. ¤ Theorem 3.28. Let Tbe an extension of IΣn. Then Tis Πn–Parikh ⇐⇒ Tis ∆n+1–closed. Proof. (=⇒): Let ϕ(x,~v)∈∆n+1(T) and t(~v)∈Term(L). Let us see that ∀x≤ t(~v)ϕ(x,~v)∈∆n+1(T). Let (Γ,Γ1) be a Πn–Parikh pair for T. Then, using 3.27 and 3.20–(2), there exist θ(x,~v)∈∆Γ 0and ψ(~v)∈∆n+1(T) such that (IΣn+ Γ1)Γproves ϕ(x,~v)↔θ(x,~v) and ∀x≤t(~v)ϕ(x,~v)↔ψ(~v). (⇐=): Let us prove that (Grn(T),Funcn(T)) is a Πn–Parikh pair for T. By 3.23, we only need to prove 3.20–(2). The proof is by induction on the length of ∆Γ 0–formulas. Let θ(~x)∈ ∆Γ 0, we only consider the case where θ(~x) is ∃y≤t(~x)θ0(~x, y). By induction hypothesis there exists ψ0(~x, y)∈∆n+1(T) such that (IΣn+ Funcn(T))Grn(T)`ψ0(~x, y)↔θ0(~x, y). Then, by 3.2–(ii), there exists δ(~x, v)∈∆n+1(IΣn+ Funcn(T)) such that (IΣn+ Funcn(T))Grn(T)` ∃v[δ(~x, v)∧ ∃y≤v ψ0(~x, y)] ↔ ∃y≤t(~x)θ0(~x, y). As Tis ∆n+1–closed, there exists ψ(~x, v)∈∆n+1(T) such that T` ∃y≤v ψ0(~x, y)↔ψ(~x, v). Since ∃v[δ(~x, v)∧ψ(~x, v)] ∈∆n+1(T), this proves the result. ¤ 4. Extended Parikh’s Theorem In this section, we shall see that for some kind of Πn–functional class Γ there exists an extension of Lsuch that each ∆n+1(IΣn+ Γ∗) formula is equivalent to a bounded formula of L(Γ). 4.1. ∆Γ 0formulas as ∆n+1 formulas. Lemma 4.1. Let Γ⊆Πnand Γ1⊆Πn+2 such that Func(Γ) ⊆Γ1and for all s(~x), t(~x, y)∈Term(L(Γ)) there exists ts(~x)∈Term(L(Γ)) such that (BΣn+ Γ1)Γ`y≤s(~x)→t(~x, y)≤ts(~x). 17 (1) Let ϕ(~x)∈∆Γ 0. Then there exist ψ(~x, z)∈Σn,θ(~x, z)∈Πnand t(~x)∈Term(L(Γ)) such that (BΣn+ Γ1)Γ` ∀z≥t(~x) [ϕ(~x)↔ψ(~x, z)↔θ(~x, z)]. (2) Let ϕ(~x)∈∆Γ 0. Then there exists δ(~x)∈∆n+1(BΣn+Γ1)such that (BΣn+Γ1)Γ` ϕ(~x)↔δ(~x). For n= 0,BΣ0can be replaced by I∆0(collection is not needed). Proof. By induction on the length of ϕ(~x) as in lemma I.1.30 in [10]. ¤ Remark 4.2.Let Γ be a Πn–functional class. We have the following results. Claim 4.3. For every t(~x, y), s(~x)∈Term(L(Γ)) there exists a term ts(~x)such that (I∆0+ Γ∗)Γ`y≤s(~x)→t(~x, y)≤ts(~x). So, lemma 4.1 holds for (BΣn+ Γ∗)Γand (Γ,Γ∗)satisfies part (2) of definition 3.20. Proof of Claim. By 3.2–(i), the result follows taking ts(~x) as t(~x, s(~x)). ¤ Claim 4.4. (IΣn+ Γ∗)Γ=⇒I∆Γ∗ 0. Proof of Claim. Let ϕ(x)∈∆Γ 0and A|= (IΣn+ Γ∗)Γsuch that A|=∃x ϕ(x). By 4.1– (1), there exist ψ(x, z)∈Σnand t(x) term of L(Γ) such that (BΣn+ Γ∗)Γ|=∀z≥ t(x) [ϕ(x)↔ψ(x, z)]. Let a∈Asuch that A|=ϕ(a) and let b=t(a). Then A|=ψ(a, b). Since A|=LΣn, there is c∈Asuch that A|=c= (µx)[ψ(x, b)]. Since Γ is a Πn–functional class, by 3.2–(i) A|=c= (µx)[ϕ(x)]; hence, A|=Lϕ.¤ Remark 4.5.Here we prove that Π0–functional classes provide examples of Π0–Parikh pairs. In the next subsection we shall see that for n≥1 this is also true for some kind of Πn–functional classes. In what follows Γ shall denote a Π0–functional class. As in 4.4, using 4.1–(1) for n= 0, we get Claim 4.6. I∆Γ∗ 0⇐⇒ (I∆0+ Γ∗)Γ. Claim 4.7 (Parikh’s theorem).Let Γ0⊆ΠΓ 1. For each ϕ(~x, ~y)∈∆Γ 0such that I∆Γ∗ 0+ Γ0` ∀~x ∃~y ϕ(~x, ~y)there exists a term t(~x)of L(Γ) such that I∆Γ∗ 0+ Γ0` ∀~x ∃~y ≤t(~x)ϕ(~x, ~y). Claim 4.8. (Γ,Γ∗)is a Π0–Parikh pair. Proof of Claim. By 4.7, part (1) of definition 3.20 holds for (Γ,Γ∗). So, the result follows from 4.3.¤ 4.2. ∆n+1 formulas as ∆Γ 0formulas. Strong Πn–functional classes. In order to improve 4.1,4.4 and 4.6–4.8, we consider a special kind of Πn–functional classes. Let Γ be a Πn– functional class and A|=I∆0+ Γ∗. We shall also denote by Athe expansion of Ato L(Γ) given by: for every a, b ∈Aand ϕ∈Γ A(Gϕ(a)) = b⇐⇒ A|=ϕ(a, b). 18 Let a1, . . . , ak∈A. The simple initial segment of Adetermined by a1, . . . , akis SΓ(A, a1, . . . , ak) = {b:b≤t(~a), t(~x)∈Term(L(Γ))}. Observe that if A|= (I∆0+ Γ∗)Γ then SΓ(A,~a) is an L(Γ)–structure. Definition 4.9. Let Γbe a Πn–functional class. We say that Γis a strong Πn–functional class if for every A|=I∆0+ Γ∗and every I if I⊂eAas L(Γ) structures then I≺e nAas L–structures. Let us observe that every Π0–functional class is a strong Π0–functional class. Moreover, if Γ is a strong Πn–functional class and Γ0is a Πn–functional class such that Γ ⊆Γ0, then Γ0is a strong Πn–functional class. Lemma 4.10. (n≥1) Let Γbe a strong Πn–functional class. Then for every k < n, ThΠn+2 (BΣk+2 + Γ∗) = ThΠn+2 (IΣk+ Γ∗) = ThΠn+2 (I∆0+ Γ∗). Proof. Suppose that BΣk+2 + Γ∗` ∀x∃y ϕ(x, y), where ϕ(x, y)∈Πnand IΣk+ Γ∗0 ∀x∃y ϕ(x, y). By compacteness, Tis consistent, where T= (IΣk+ Γ∗)Γ+∀y¬ϕ(c, y) + {t(c)<d:t(x) term of L(Γ)}. Let A|=T,a=A(c) and B=SΓ(A, a). Since Γ is a Πn–functional class, B⊂eAas L(Γ)–structures and, by the last group of axioms of T, it is proper. Also, for all θ(x, y)∈Γ and b∈Bthere exists d∈Bsuch that A|=θ(b, d). Since Γ is a strong Πn–functional class and A|=I∆0+ Γ∗,B≺e nAas L–structures. So, from A|=∀y¬ϕ(a, y) we get that B|=∀y¬ϕ(a, y). Since, B|=I∆0+ Γ∗; and, for k < n,B≺e k+1 A, then B|=BΣk+2. So, B|=BΣk+2 + Γ∗and B|=∃y ϕ(a, y). Contradiction. This proves the first identity. The second one follows from the first by induction on k < n.¤ Remark 4.11.(Strength of 4.4, 4.6, 3.7, 4.1) In what follows let Γ be a strong Πn–functional class. Claim 4.12. (i) I∆Γ∗ 0⇐⇒ (IΣn+ Γ∗)Γ⇐⇒ (I∆0+ Γ∗)Γ. (ii) I∆0+ Γ∗⇐⇒ IΣn+ Γ∗. Proof of Claim. By 4.4, (IΣn+ Γ∗)Γ=⇒I∆Γ∗ 0=⇒(I∆0+ Γ∗)Γ. Let θ∈Σn. Then BΣn+1 `Iθ; so, by 4.10 (for k=n−1), I∆0+ Γ∗`Iθ. This proves (i). Part (ii) follows from (i).¤ By 4.12, we can rewrite 3.7 as follows Claim 4.13. (i) ThΠn+2 (I∆0+ Γ∗) = ThΠn+2 (BΣn+1 + Γ∗). (ii) I∆0+ Γ∗=⇒I∆n+1(IΣn+ Γ∗) =⇒B∗∆n+1(IΣn+ Γ∗). Claim 4.14. (i) Let ϕ(~x)∈∆Γ 0. There are ψ(~x, z)∈Σn,θ(~x, z)∈Πnand t(~x)such that I∆Γ∗ 0` ∀z≥t(~x) [ϕ(~x)↔ψ(~x, z)↔θ(~x, z)]. (ii) Let ϕ(~x)∈∆Γ 0. Then there exists δ(~x)∈∆n+1(BΣn+ Γ∗)such that I∆Γ∗ 0` ϕ(~x)↔δ(~x). 19 Proof of Claim. For n≥1, IΣn=⇒BΣn. So, (IΣn+ Γ∗)Γ=⇒(BΣn+ Γ∗)Γ. Then the result follows from 4.1 and 4.12.¤ Theorem 4.15 (Extended Parikh’s theorem (Strength of 4.7)). Let Γbe a strong Πn–functional class and Γ0⊆Πn+1 ∪ΠΓ 1. For each ϕ(x, y)∈Πn∪∆Γ 0 such that (BΣn+1 + Γ0+ Γ∗)Γ` ∀x∃y ϕ(x, y)there exists a term t(x)of L(Γ) such that I∆Γ∗ 0+ Γ0` ∀x∃y≤t(x)ϕ(x, y). Proof. Deny the proposition’s conclusion. We proceed as in 4.10. By compacteness the following theory is consistent (cand dare new constants) T=½I∆Γ∗ 0+ Γ0+{∀y≤t(c)¬ϕ(c, y) : t(x) term of L(Γ)} +{t(c)<d:t(x) term of L(Γ)} Let A|=T,a=t(c) and B=SΓ(A, a). Since Γ is a Πn–functional class, B⊂eAas L(Γ)–structures. Then B≺e nAas L–structures. So, B|=∀y¬ϕ(a, y) and, since A|=IΣn and Ais a proper extension of B(last set of axioms of T), B|= (BΣn+1 + Γ0+ Γ∗)Γ. Contradiction. ¤ Corollary 4.16. (Strength of 4.8) If Γis a strong Πn–functional class then (Γ,Γ∗)is a Πn–Parikh pair. 4.3. Existence theorems of strong Πn–functional classes. Theorem 4.17. (n≥1) There is a strong Πn–functional class, Hn, such that for all ϕ∈Hn,IΣn−1`IPF(ϕ)and IΣn⇐⇒ IΣn+H∗ n. Proof. For each θ(v, y)∈Π− n−1let θ0(x, w) be the following formula        [¬∃v≤x∃y θ(v, y)∧w= 0] ∨ ∃w1, w2≤w   w=hw1, w2i ∧ w1≤x∧ ∀v≤x[∃y θ(v, y)→ ∃y≤w2θ(v, y)] ∧ θµ,w2(w1, w2)∧ ∀v≤x[θµ,w2(v, w2)→v≤w1] It is clear that there is θ∗(x, w)∈Πnsuch that IΣn−1`θ0(x, w)↔θ∗(x, w). Let Hn= {θ∗(x, w) : θ(v, y)∈Πn−1}. Let θ(v, y)∈Πn−1. It holds that IΣn−1`IPF(θ∗) and IΣn` ∀x∃w θ∗(x, w); so, Hnis a Πn–functional class and IΣn⇐⇒ IΣn+H∗ n. Let us observe that H1⊆H2⊆ · · · ⊆ Hn⊆. . . . Now, by induction on n≥1, we prove that Hn is a strong Πn–functional class. Let A|=I∆0+H∗ nand I⊂eAsuch that (∗) for all ϕ(x, w)∈Hn,a∈Ithere is b∈Isuch that A|=ϕ(a, b). By induction on n≥1, using Tarski–Vaught’s test, we prove that I≺nA. (n= 1): Let us see that I≺1A. Let θ(v, y)∈Π0and a∈Isuch that A|=∃y θ(a, y). Since θ∗(x, w)∈H1and A|=I∆0+H∗ 1, then A|=∀x∃y θ∗(x, w). Since a∈I, by (∗), there exists d∈Isuch that A|=θ∗(a, d). Since I∆0`θ0(x, w)↔θ∗(x, w), A|=θ0(a, d); so, there exists b∈Asuch that b≤dand A|=θ(a, b). Since d∈Iand I⊂eA, then b∈I, as required. (n→n+ 1): Since A|=I∆0+H∗ nand, by induction hypothesis, Hnis a strong Πn– functional class, we get that A|=IΣn+H∗ n. Let θ(x, y)∈Πnand a∈Isuch that 20 A|=∃y θ(a, y). Now as in the case n= 1, using that A|=IΣn+H∗ n, we obtain that there exists b∈Isuch that A|=θ(a, b). ¤ Proposition 4.18 (Strength of 3.8).If Thas ∆n+1–collection, there is a strong Πn– functional class Γsuch that ThΠn+2 (T) = ThΠn+2 (I∆0+ Γ∗). Proof. Suppose that n≥1. By 3.8, there is a Πn–functional class Γ1such that Thn+2(T) = Thn+2(IΣn+ Γ∗ 1). Let Γ = Hn+ Γ1. Then, Γ is a strong Πn–functional class; so, by 4.17 and 4.12,IΣn+ Γ∗ 1⇐⇒ I∆0+ Γ∗. Hence ThΠn+2 (T) = ThΠn+2 (IΣn+ Γ∗ 1) = ThΠn+2 (I∆0+ Γ∗). ¤ Lemma 4.19. Let T=⇒IΣn,A|=ThΠn+2 (T)and a∈A. If (Γ,Γ1)and (Γ0,Γ0 1)are Πn–Parikh pairs for Tthen SΓ(A, a) = SΓ0(A, a). Proof. Let b∈ SΓ(A, a). There are t(x)∈Term(L(Γ)) such that b≤t(a) and ϕ(x, y)∈ ∆n+1(T) such that (IΣn+ Γ1)Γ`t(x) = y↔ϕ(x, y). Let s(x) be a term of L(Γ0) such that (IΣn+ Γ0 1)Γ0` ∀x∃y≤s(x)ϕ(x, y). So, b≤s(a); hence, b∈ SΓ0(A, a). ¤ Theorem 4.20. Let Tbe an extension of IΣnand (Γ,Γ1)aΠn–Parikh pair for T(so, T is ∆n+1–closed). The following conditions are equivalent (1) Thas ∆n+1–collection. (2) (IΣn+ Γ1)Γ=⇒I∆Γ 0. (3) For each s(~v), t(~v, x)∈Term(L(Γ)) there exists ts(~v)∈Term(L(Γ)) such that (IΣn+ Γ1)Γ`x≤s(~v)→t(~v, x)≤ts(~v). (4) ThΠn+2 (T) = ThΠn+2 (BΣn+1 + Γ1). (5) For every A|= (IΣn+ Γ1)Γand a∈A,SΓ(A, a)≺nAas L–structures and SΓ(A, a)|=ThΠn+2 (T). Proof. From 2.8 and 2.15, it follows (4) =⇒(1). ((1) =⇒(5)): By 4.19 and 4.16 we may assume that Γ is a strong Πn–functional class for T(and that Γ1= Γ∗). So, by 4.9,SΓ(A, a)≺nAas L–structures. Let ϕ(x, y)∈Πnsuch that T` ∀x∃y ϕ(x, y). Then there exists t(x)∈Term(L(Γ)) such that (IΣn+ Γ∗)Γ` ∀x∃y≤t(x)ϕ(x, y). Let b∈ SΓ(A, a). Then, it holds that there exist c∈Aand s(x)∈Term(L(Γ)) such that A|=c≤t(b)∧ϕ(b, c)∧b≤s(a). Since Γ is Πn–functional, c≤t(b)≤t(s(a)); hence, c∈ SΓ(A, a). So, SΓ(A, a)|=∃y ϕ(b, y). ((5) =⇒(4)): Let ϕ(x, y)∈Πnsuch that BΣn+1 + Γ1` ∀x∃y ϕ(x, y). Suppose that IΣn+ Γ10∀x∃y ϕ(x, y). Let T0be the theory (IΣn+ Γ1)Γ+∀y¬ϕ(c, y) + {t(c)<d:t(x)∈Term(L(Γ))}. By compacteness, T0is consistent. Let A|=T0and a=A(c). Since SΓ(A, a)≺e nA as L–structures and is proper, SΓ(A, a)|=∀y¬ϕ(a, y) and SΓ(A, a)|=BΣn+1. Then, SΓ(A, a)|=BΣn+1 + Γ1. Contradiction. ((1) =⇒(2)): Let ϕ(x)∈∆Γ 0. There exists ψ(x)∈∆n+1(T) such that (IΣn+ Γ1)Γ` ϕ(x)↔ψ(x). Since Thas ∆n+1–induction, by 2.15,IΣn+Γ1has ∆n+1–induction; hence, IΣn+ Γ1`Iψ. So, (IΣn+ Γ1)Γ`Iϕ. 21 ((2) =⇒(1)): Let ϕ(x)∈∆n+1(T). By 3.27, there exists θ(x)∈∆Γ 0such that (IΣn+ Γ1)Γ`θ(x)↔ϕ(x). Then, by (2),T`Iϕ; so, Thas ∆n+1–induction. Since Tis ∆n+1–closed, by 2.13,Thas ∆n+1–collection. ((1) =⇒(3)): Let s(~v), t(~v, x)∈Term(L(Γ)). By 3.2 there exist ϕ(~v, x), θ(~v, x, z)∈ ∆n+1(IΣn+ Γ1) such that (IΣn+ Γ1)Γ`[s(~v) = x↔ϕ(~v, x)] ∧[t(~v, x) = z↔θ(~v, x, z)]. Let Γ0be a strong Πn–functional class for T. By 4.16, there exist t0(~v, x) and s0(~v) terms of L(Γ0) and ψ(~v, z)∈∆n+1(T) such that (IΣn+ Γ∗ 0)Γ0` ∀~v ∃x≤s0(~v)ϕ(~v, x)∧ ∀~v ∀x∃z≤t0(~v, x)θ(~v, x, z). and (IΣn+ Γ∗ 0)Γ0`t0(~v, s0(~v)) = z↔ψ(~v, z). Then IΣn+ Γ∗ 0`ϕ(~v, x0)∧x≤x0∧θ(~v, x, z)→ ∃z0(ψ(~v, z0)∧z≤z0). Since ThΠn+2 (IΣn+ Γ∗ 0) = ThΠn+2 (T) = ThΠn+2 (IΣn+ Γ1), then IΣn+ Γ1`ϕ(~v, x0)∧x≤x0∧θ(~v, x, z)→ ∃z0(ψ(~v, z0)∧z≤z0). Since T` ∀~v ∃z ψ(~v, z), there exists ts(~v) such that (IΣn+ Γ1)Γ` ∀~v ∃z≤ts(~v)ψ(~v, z). So, (IΣn+ Γ1)Γ`x≤s(~v)→t(~v, x)≤ts(~v), as required. ((3) =⇒(1)): Let ϕ(x, y,~v)∈Π− nsuch that ∃y ϕ(x, y,~v)∈∆n+1(T). Then there exist θ(x,~v), ϕ0(x, y,~v)∈∆Γ 0such that (IΣn+ Γ1)Γ`[∃y ϕ(x, y,~v)↔θ(x,~v)] ∧[ϕ(x, y,~v)↔ϕ0(x, y,~v)]. Let ψ(x,~v, y)∈∆Γ 0be (θ(x,~v)∧ϕ0(x, y,~v)) ∨(¬θ(x,~v)∧y= 0). Then, by 3.25, there exists t(x,~v)∈Term(L(Γ)) such that (IΣn+ Γ1)Γ` ∀x∀~v ∃y≤t(x,~v)ψ(x,~v, y). By (3), there exists t0(u,~v)∈Term(L(Γ)) such that (IΣn+ Γ1)Γ`x≤u→t(x,~v)≤t0(u,~v). So, (IΣn+ Γ1)Γ` ∀u∀~v [∀x≤u∃y ϕ(x, y,~v)→ ∃u0∀x≤u∃y≤u0ϕ(x, y,~v)]. That is, T`Bϕ,x,y. So, Thas ∆n+1–collection. ¤ 5. Πn–envelopes 5.1. General properties of Πn–envelopes. Initial segments. In this section we introduce the concept of Πn–envelope. This generalizes the concept of envelope (see [10]) and is closely related to indicators (see [12]). Some results in this section are generalizations of results on indicators that appear in chapter 14 of [12]. However, Πn–envelopes will provide us with Πn–functional classes defined uniformely. This is why we include these results here. In particular, we will obtain Πn–envelopes that will be used in section 6to prove the hierarchy theorem. For each formula ϕ(u, x, y) let Γϕ={ϕ(k, x, y) : k∈ω}. Definition 5.1. Let ϕ(u, x, y)∈Σ− n+1. We say that (1) ϕ(u, x, y)is a Πn–q–envelope of Tin T0if T`Γ∗ ϕ, and for all k∈ω,T0` ϕ(k+ 1, x, y)→ ∃z < y ϕ(k, x, z). 22 (2) ϕ(u, x, y)satisfies Πn–ENV for Tand T0if for each ψ(x, y)∈Π− nsuch that T` ∀x∃y ψ(x, y), there exists k∈ωsuch that T0`ϕ(k, x, y)→ ∃z < y ψ(x, z). (3) ϕ(u, x, y)is a Πn–envelope of Tin T0if ϕ(u, x, y)is a Πn–q–envelope of Tin T0 and satisfies Πn–ENV for Tand T0. Remark 5.2.Now we shall give some basic properties of envelopes. Let ϕ(u, x, y)∈Σn+1 a Πn–q–envelope of Tin T0. By contraction of quantifiers, part (2) of definition 5.1 is also true for ψ(x, y)∈Σ− n+1. We also have that Claim 5.3. (i) If T=⇒T0then ThΠn+2 (T) = ThΠn+2 (T0+ Γ∗ ϕ). (ii) If ϕ∈Πnand T+IΣnis consistent then Γϕis a Πn–functional class. Definition 5.4. Let ϕ(u, x, y)∈Σn+1. We say that ϕ(u, x, y)satisfies Πn–IND for Tand T0if for every A|=T0countable, nonstandard and a, b ∈A, the following conditions are equivalent: (IND-(i)): For all k∈ω,A|=∃y < b ϕ(k, a, y). (IND-(ii)): There exists I|=Tsuch that I≺e nAand a < I< b. Remark 5.5.Let ϕ(u, x, y)∈Σn+1 such that T` ∀x∃y ϕ(k, x, y), for all k∈ω. Then for all theory T0we have that: IND-(ii) =⇒IND-(i). So, if ϕ(u, x, y) is a Πn–q–envelope, then in order to prove that ϕ(u, x, y) satisfies Πn–IND it is enough to establish that: IND-(i) =⇒IND-(ii). Now we shall study conditions under which it holds that Πn–ENV is equivalent to Πn–IND. Let us note, however, that the proof of part ⇐= of next theorem shows that, if T0=⇒IΣn, then every Πn–q–envelope of Tin T0satisfying Πn–IND is a Πn–envelope. Theorem 5.6. (n≥1) Suppose that T0=⇒IΣnand (i) Tis recursively axiomatizable, and (ii) ThΠn+2 (T) = ThΠn+2 (T+BΣn+1). Let ϕ(u, x, y)∈Σn+1 be a Πn–q–envelope of Tin T0. Then with respect to Tand T0 ϕ(u, x, y)satisfies Πn–ENV ⇐⇒ ϕ(u, x, y)satisfies Πn–IND. Proof. (⇐=): Let ψ(x, y)∈Π− nsuch that T` ∀x∃y ψ(x, y) and suppose that for all k∈ω, T00ϕ(k, x, y)→ ∃z < y ψ(x, z). For all k∈ωlet Tk=T0+{∃y < dϕ(j, c, y)∧ ∀z < d¬ψ(c, z) : j < k}. Since, for all k∈ω,Tkis consistent, T∗=Sk∈ωTkis consistent. Let A∗|=Tcountable nonstandard, A=A∗ |L,a=A∗(c) and b=A∗(d). Then A|=T0and for all k∈ω, A|=∃y < b ϕ(k, a, y). Since ϕsatisfies Πn–IND for Tand T0, there exists I|=Tsuch that I≺e nAand a < I< b. So, there exists e∈Isuch that I|=ψ(a, e); hence, e < b and A|=ψ(a, e). But A∗|=∀z < d¬ψ(c, z); hence, A|=∀z < b ¬ψ(a, z). So, A|=¬ψ(a, e), a contradiction. (=⇒): By 5.5, it is enough to prove IND-(i) =⇒IND-(ii). We follow the proof of theorem 11.7 in [12]. Let A|=T0countable, nonstandard and a, b ∈Asuch that A|= ∃y < b ϕ(k, a, y), for all k∈ω. Let 23 T0=T+BΣn+1 +{∀~z ψ(c, ~z) : ψ(x, ~z)∈Σn,A|=∀~z ≤b ψ(a, ~z)}. By (ii) it follows that T0is consistent. Since A|=IΣnand n≥1, the Σn–type of a, b in A belongs to SSy(A) (the standard system of A); hence, {p∀~z ψ(c, ~z)q:ψ∈Σn,A|=∀~z ≤ b ψ(a, ~z)} ∈ SSy(A). So, by (i),T0∈SSy(A). Since SSy(A) is a Scott system, there exists B|=T0countable which is SSy(A)–saturated; hence, Bis recursively saturated. Let c=B(c). Then, for each θ(x, ~z)∈Πn, if B|=∃~z θ(c, ~z) then A|=∃~z ≤b θ(a, ~z). So, by Friedman’s theorem, there exists H:Be ≺e nAsuch that H(c) = aand b /∈H(B). Let I=H(B). Then I|=T,I≺e nAand a < I< b.¤ Remark 5.7.Condition (ii) in 5.6 cannot be deleted. We have used it there in order to prove that: IND-(i) =⇒IND-(ii). Even more, suppose that T=⇒T0=⇒IΣnand ϕ(u, x, y)∈Σn+1 is a Πn–q–envelope of Tin T0that satisfies Πn-IND for these theories. Let ψ(x, y)∈Πnbe such that T+BΣn+1 ` ∀x∃y ψ(x, y). Then, it holds that there is k∈ωsuch that T0`ϕ(k, x, y)→ ∃z < y ψ(x, z). So, ThΠn+2 (T) = ThΠn+2 (T+BΣn+1). Remark 5.8.For Π0–envelopes we have the following form of 5.6. Claim 5.9. Suppose that T0=⇒I∆0+exp,Tis recursively axiomatizable and ThΠ2(T) = ThΠ2(T+BΣ1). Let ϕ(u, x, y)∈Σ1aΠ0–q–envelope of Tin T0. Then, with respect to Tand T0, ϕ(u, x, y)satisfies Π0–ENV ⇐⇒ ϕ(u, x, y)satisfies Π0–IND. In some cases this result is also true even though T0is not an extension of I∆0+exp. Using methods that appears in [1], mainly the superexponential function (see the proof of lemma 3there), it can be proved that Claim 5.10. Suppose that T=⇒BΣ1+exp =⇒T0=⇒I∆0, and Tis recursively axiomatizable. Let ϕ(u, x, y)∈∆0be a Π0–q–envelope of Tin T0. Then, with respect to Tand T0, ϕ(u, x, y)satisfies Π0–ENV ⇐⇒ ϕ(u, x, y)satisfies Π0–IND. 5.2. Existence theorems of Πn–envelopes. In this and in the next subsection we are going to use formulas in the language and in the metalanguage. In order to write expressions that are easier to read we shall use uppercase Greek letters for formulas in the metalanguage (real formulas) and lowercase Greek letters for formulas in the language (elements of a model that it thinks that are formulas). We shall use σ, τ, . . . as variables (in the language of Arithmetic) for formulas, and pas variable (in the language of Arithmetic) for proofs. Theorem 5.11. If Tis recursively axiomatizable, Πn–functional and, for n= 0,T`exp, then there exists a Πn–envelope of Tin IΣn. Proof. Since Tis Πn–functional, Thas ∆n+1–collection and, for n≥1, T=⇒IΣn=⇒ BΣn. Let us consider the following cases: 24 Case A: n≥1. Since Tis recursively axiomatizable, there is PrfT(x, y)∈Σ1that represents to {(σ, p)∈ω2:pis a proof of σin T}in P−. Let Φ0(u, x, y)∈Πnbe a formula equivalent in BΣn(so, also in T), to ∀p, τ ≤u½FormΠ− n(τ(v0, v1)) ∧PrfT(∀v0∃v1τ(v0, v1), p)→ → ∀x0≤x∃y0≤ySatΠn(τ( ˙x0,˙y0)) ¾ Where SatΠn(v) is a truth definition in IΣ1for Πn–formulas. Let Φ(u, x, y)∈Σn+1 be a formula equivalent in BΣn(so, also in T), to ∃y0≤y[y=y0+u∧Φ0(u, x, y0)∧ ∀y00 < y0¬Φ0(u, x, y00)]. Let k∈ω. Since Thas ∆n+1–collection, T` ∀x∃yΦ(k, x, y). Moreover, as y=y0+k, IΣn`Φ(k+ 1, x, y)→ ∃z < y Φ(k, x, z) and T`IPF(Φ(k, x, y)). Let Ψ(x, y)∈Π− nsuch that T` ∀x∃yΨ(x, y) and k > pΨ(x, y)q. Then IΣn` Φ(k, x, y)→ ∃z < y Ψ(x, z). So, Φ(u, x, y) satisfies Πn–ENV for Tand IΣn. Case B: n= 0. Since Tis recursively axiomatizable, there is PrfT(x, y, w)∈∆0such that ∃wPrfT(x, y, w) represents to {(σ, p) : pis a proof of σin T}in P−. Let Φ0(u, x, y)∈Σ0 be ∀p, ρ, w ≤u    FormΠ− 0(ρ(v0, v1)) ∧PrfT(∀v0∃v1ρ(v0, v1), p, w)→ ∀z, z0≤y   y=hz, z0i → →½z= 2(x+z0+2)cu∧ ∀x0≤x∃y0≤z0V0(ρ, hx0, y0i, z)¾       Where V0(v1, v2, v3)∈∆0is a truth definition in I∆0+exp for ∆0formulas and c∈ω is a constant which depends upon the explicit definition of V0(v1, v2, v3) (see [10], V.5.4). Let Φ(u, x, y)∈Σ0defined as in case A. Now, as there, it is proved that Φ(u, x, y) is a Π0–envelope of Tin I∆0.¤ Remark 5.12.Let Tbe Πn–functional and Φ0(u, x, y, w)∈Πnsuch that ∃wΦ0(u, x, y, w) is a Πn–envelope of Tin IΣn. Let us see that there exists a Πnformula which is a Πn–envelope of Tin IΣn. Let Ψ(u, x, y)∈Πnbe ∃w, y0≤y[y=hw, y0i ∧ Φ0(u, x, y0, w)]. For each k∈ω, let Ψk(x, y) be Ψ(k, x, y). Then T` ∀x∃yΨk(x, y). Let CΨk(x, y) be as in the proof of 3.8. The definition of CΨk(x, y) is uniform in k; so, using kas a parameter we obtain CΨ(u, x, y)∈Πn. Let Θ(u, x, y)∈Πnbe Seq(y)∧lg(y) = u+ 1 ∧ ∀j≤uCΨ(j, x, (y)j). Then Θ(u, x, y)isaΠn–envelope of Tin IΣn. Theorem 5.13. (1) For all m≥n(m≥1, for n= 0) there exists a Πn–envelope of IΣmin IΣn,Φ(u, x, y)∈Πn, such that (a) IΣm+1 ` ∀u∀x∃yΦ(u, x, y). (b) IΣm+1 ` ∀u, x, y1, y2[Φ(u, x, y1)∧Φ(u+ 1, x, y2)→y1< y2]. (2) For all n∈ωthere exists a Πn–envelope, Φ(u, x, y)∈Πn, of PA in IΣnsuch that (a) Th(N)` ∀u∀x∃yΦ(u, x, y). (b) Th(N)` ∀u, x, y1, y2[Φ(u, x, y1)∧Φ(u+ 1, x, y2)→y1< y2]. Proof. Let 1 ≤n≤m. We will prove that the Πn–envelope obtained in 5.12, from the one given in 5.11, satisfies the properties of 1–(a) and 1–(b). Let Φ0(u, x, y)∈Πnthe formula 25 Theorem 6.11 (The Hierarchy Theorem).Let Tbe a Πn–functional theory (if n= 0 we assume that T`exp), ϕ(u, x, y)a strong Πn–envelope of Tin Tand T0an extension of Tsuch that T0` ∀u∀x∃y ϕ(u, x, y), and T0`ϕ(u, x, y1)∧ϕ(u+ 1, x, y2)→y1< y2. Then (1) For each A|=T0 Γϕand a∈Anonstandard, KΓϕ 0(A, a)|=I∆n+1(T)and KΓϕ 0(A, a)6|= I∆n+1(T0). (2) I∆n+1(T0)|=⇒I∆n+1(T). Proof. Part (2) follows from (1). By 6.10–(7),KΓϕ 0(A, a)|=I∆n+1(T). Since ∃y ϕ(u, x, y)∈ ∆n+1(T0) and, by 6.9,∃y ϕ(u, a, y) defines ωin KΓϕ 0(A, a), then KΓϕ 0(A, a)6|=I∆n+1(T0). ¤ Theorem 6.12. (1) For all m≤n,I∆n+1(IΣm)⇐⇒ IΣn. (2) For all m≥n,I∆n+1(IΣm+1)|=⇒I∆n+1(IΣm). (3) I∆n+1(N)|=⇒I∆n+1(PA). Proof. (1) follows from 2.18. Let us see (2). By 5.22–(1), for every m≥nthere exists a strong Πn–envelope that satisfies the hypothesis of 6.11 for T=IΣmand T0=IΣm+1; hence, (2) follows from 6.11–(1). Part (3) is proved in a similar way using 5.22–(2).¤ Lemma 6.13. For every m≥n,BΣn+1 ×=⇒I∆n+1(IΣm+1). Proof. Since I∆n+1(IΣn+1) is a Πn+2–axiomatizable theory (see [8], theorem 1.1, or [7], [15]) and, by 6.12,I∆n+1(IΣn+1)|=⇒IΣn, the result follows from 1.3.¤ Theorem 6.14. (1) For all m≥n,I∆n+1(IΣm+1)|=⇒B∗∆n+1(IΣm+1). (2) I∆n+1(PA)|=⇒B∗∆n+1(PA). (3) I∆n+1(N)|=⇒B∗∆n+1(N). Proof. First observe that for every theory T,BΣn+1 =⇒B∗∆n+1(T), and if Thas ∆n+1– collection then, by 2.10,I∆n+1(T) =⇒B∗∆n+1(T). Since IΣm+1,m≥n,PA and Th(N) have ∆n+1–collection, then (1),(2) and (3) follow from 6.13.¤ 7. Remarks and open questions The main problem we have considered in this work is the Paris–Friedman’s Conjecture in three versions (1) Paris–Friedman’s Conjecture: I∆n+1 ⇐⇒ L∆n+1. (2) Uniform Paris–Friedman’s Conjecture: UI∆n+1 ⇐⇒ UL∆n+1. (3) Parameter Free Paris–Friedman’s Conjecture: I∆− n+1 ⇐⇒ L∆− n+1. From Slaman’s result, it holds I∆n+1 ⇐⇒ L∆n+1, for n≥1. We have studied here the relativization of these problems to ∆n+1 formulas in a theory T. This gives a new version of the Conjecture. 4. Relativized Paris–Friedman’s Conjecture: I∆n+1(T)⇐⇒ L∆n+1(T). 32 We have proved that if Tsatisfies some conditions then the relativized Paris–Friedman’s Conjecture for Tholds. So, we consider the following strong forms of these Conjectures. Problem 1.Does it hold that for all Textension of IΣn (1) If Tis ∆n+1–closed then Thas ∆n+1–collection? (2) If Thas ∆n+1–induction then Thas ∆n+1–collection? (3) If Tis ∆n+1–PF then Thas ∆n+1–collection? Let us observe that if every (complete) extension of IΣnsatisfies 1–(2) then the Uniform Paris–Friedman’s Conjecture holds. Condition 3.10–(2) is related with the Uniform Paris-Friedman’s Conjecture. Let A|= UI∆n+1 and ϕ(x, y)∈Π− nsuch that A|=∀x∃y ϕ(x, y). Let Fϕ:A−→ Abe defined by: Fϕ(a) = (µy)[ϕ(a, y)]. Let F∗ ϕbe, the bounding map of Fϕ, defined by F∗ ϕ(a) = (µx)≤a[∀u≤a(Fϕ(u)≤Fϕ(x))] Claim. Let A|=UI∆n+1. If for each ϕ(x, y)∈Π− nsuch that A|=∀x∃!y ϕ(x, y), it holds that F∗ ϕis a total function on Athen A|=UL∆n+1. Let us consider the following question. Problem 2.In the above conditions. Is F∗ ϕa total function? In 3.12 we have obtained a conservativeness property, ThΠn+2 (T) = ThΠn+2 (T+ BΣn+1), under which Tis Πn–functional and, hence, satisfies the Relativized Paris– Friedman’s Conjecture. We have also extended this result in 3.13 for Σn+2 extensions of Πn+2 axiomatizable theories. Let us consider the following problems. Problem 3.(1) Let Tbe a theory such that T+BΣn+1 is consistent. Are the following conditions equivalent? (a) Tis Πn–functional. (b) ThΠn+2 (T) = ThΠn+2 (T+BΣn+1). (c) ThΠn+2 (T) = ThΠn+2 (T+BΣ− n+1). (2) Let Tbe a Πn+2–axiomatizable extension of IΣnand let T0be Σn+2–axiomatizable such that T+T0is consistent. Does it hold that Tis Πn–functional ⇐⇒ T+T0is Πn–functional? In 5.11 it is proved that if Tis Πn–functional and recursively axiomatizable then Thas a Πn–envelope in IΣn(for n= 0 we add that T`exp). For all n∈ω,ThΠn+2 (N) is Πn–functional and proves exp. Nevertheless, ThΠn+2 (N) does not have a Πn–envelope in IΣn. So, it cannot be omitted that Tis recursively axiomatizable. Now, we will consider if T`exp could be eliminated for n= 0. The theory IΠ− 1has Π0–collection, is recursively axiomatized and IΠ− 10exp. It holds that if ϕ(x, y)∈∆− 0 and IΠ− 1` ∀x∃y ϕ(x, y) then there exists k∈ωsuch that IΠ− 1` ∃z∀x[z < x → ∃y < xkϕ(x, y)] (see [5]). From this it follows that ϕ(u, x, y)≡xu+u=yis a Π0–envelope of IΠ− 1in ThΠ1(N). Let us consider the following problem. 33 Problem 4.Is there a Π0–envelope of IΠ− 1in I∆0? In section 6the models KΓ 0(A, a) have been used to separate the fragments I∆n+1(IΣm), m≥n. Theorem 1.1 sums up results obtained using these models. Let us consider the following problem. Problem 5.Is strict the following chain of theories? B∗∆n+1(N) =⇒B∗∆n+1(PA) =⇒...=⇒B∗∆n+1(IΣn+1) =⇒B∗∆n+1(IΣn) References [1] P. D’Aquino. A sharpened version of McAloon’s theorem on initial segments of models of I∆0. Annals of Pure and Applied Logic 61(1–2):49–62, 1993. [2] L.D. Beklemishev. Induction rules, reflection principles and provably recursive functions. Annals of Pure and Applied Logic 85(3):193–242, 1997. [3] L.D. Beklemishev. A proof-theoretic analysis of collection. Archive for Mathematical Logic 37(5– 6):275–296, 1998. [4] L.D. Beklemishev. On the induction schema for decidable predicates. The Journal of Symbolic Logic 68(1):17–34, 2003. [5] T. Bigorajska. On Σ1–definable Functions Provably Total in IΠ− 1. Mathematical Logic Quarterly, 41:135–137, 1995. [6] P. Clote, J. Kraj´ıcek. Open Problems. In P. Clote, and J. Kraj´ıcek, editors, Arithmetic, Proof Theory and Computational Complexity, pages 1–19. Oxford Logic Guides 23. Oxford University Press, Oxford, 1993. [7] A. Cord´on Franco, A. Fern´andez Margarit, F.F. Lara Mart´ın. Fragments of Arithmetic with Extensions of Bounded Complexity. Preprint, Sevilla, August 2003. [8] A. Cord´on Franco, A. Fern´andez Margarit, F.F. Lara Mart´ın. On the quantifier complexity of ∆n+1(T)–induction. Archive for Mathematical Logic, to appear. [9] A. Fern´andez Margarit, F.F. Lara Mart´ın. Some results on L∆− n+1. Mathematical Logic Quarterly, 47(4):503–512, 2001. [10] P. H´ajek, P. Pudl´ak. Metamathematics of First Order Arithmetic. Springer Verlag, Berlin, Heidelberg, New-York, 1993. [11] R. Kaye. Diophantine and Parameter–free Induction. Ph.D. Thesis. University of Manchester, 1987. [12] R. Kaye. Models of Peano Arithmetic. Oxford Logic Guides 15. Oxford University Press, Oxford 1991. [13] R. Kaye. Model–theoretic properties characterizing Peano Arithmetic. The Journal of Symbolic Logic, 56(3):949–963, 1991. [14] R. Kaye; J. Paris; C. Dimitracopoulos. On parameter free induction schemas. The Journal of Symbolic Logic, 53(4):1082-1097, 1988. [15] F.F. Lara Mart´ın. Inducci´on y Recursi´on: Las teor´ıas I∆n+1(T). Ph.D. Thesis. Universidad de Sevilla, 2000. [16] D. Leivant. The optimality of induction as an axiomatization of arithmetic. The Journal of Symbolic Logic, 48(1):182–184, 1983. [17] J.B. Paris, L.A.S. Kirby. Σn–collection schemas in arithmetic. In A.J. Macintyre et al. editors, Logic Colloquium’77, pages 199–209. North–Holland, Amsterdam, 1978. [18] C. Parsons. On n–quantifier induction. The Journal of Symbolic Logic, 37(3):466–482, 1972. [19] T. Slaman. Σn–Bounding and ∆n–Induction. Proceedings of the American Mathematical Society, to appear. 34