Local induction and provably total computable functions

Local Induction and Provably Total Computable Functions Andr´es Cord´on–Franco, F. F´elix Lara–Mart´ın Depto. Ciencias de la Computaci´on e Inteligencia Artificial, University of Seville C/ Tarfia, s/n, 41012 Sevilla (Spain) Abstract Let IΠ− 2denote the fragment of Peano Arithmetic obtained by restricting the induction scheme to parameter free Π2formulas. Answering a question of R. Kaye, L. Beklemishev showed that the provably total computable functions of IΠ− 2are, precisely, the primitive recursive ones. In this work we give a new proof of this fact through an analysis of certain local variants of induction principles closely related to IΠ− 2. In this way, we obtain a more direct answer to Kaye’s question, avoiding the metamathematical machinery (reflection principles, provability logic,...) needed for Beklemishev’s original proof. Our methods are model–theoretic and allow for a general study of IΠ− n+1 for all n≥0. In particular, we derive a new conservation result for these theories, namely that IΠ− n+1 is Πn+2–conservative over IΣnfor each n≥1. Keywords: First order Arithmetic, conservation results, parameter free induction, primitive recursive functions. 2000 MSC: 03F30, 03D20 1. Introduction An important notion in studying the computational content of a fragment of Arithmetic is that of its provably total computable functions. A number– theoretic computable function f:Nk→Nis said to be a provably total computable function (p.t.c.f.) of a theory T, written f∈ R(T), if there is a Σ1formula ϕ(~x, y) such that: Email addresses: [email protected] (Andr´es Cord´on–Franco), [email protected] (F. F´elix Lara–Mart´ın) Preprint submitted to Annals of Pure and Applied Logic February 17, 2014 1. ϕdefines the graph of fin the standard model of Arithmetic N; and 2. T` ∀~x ∃!y ϕ(~x, y). Since it was introduced by G. Kreisel in the 1950s this notion has been widely studied, and nice recursion–theoretic and computational complexity characterizations of the sets R(T) have been obtained for a good number of theories T. For instance, by a classical result due independently to G. Mints, C. Parsons and G. Takeuti, the class of p.t.c.f. of the scheme of induction for Σ1–formulas IΣ1equals to the class of the primitive recursive functions PR. Indeed, all classes R(IΣn), n≥1, can be characterized in terms of the Fast Growing Hierarchy up to the ordinal ε0. As for weak fragments below IΣ1, their p.t.c.f. have been characterized in terms of subrecursive operators (bounded recursion, bounded minimization, ...) as well as in terms of computational complexity classes. In fact, their classes of p.t.c.f. have been intensively investigated in connection with important open problems in Complexity Theory, mainly in the context of Bounded Arithmetic. In spite of the wide range of the theories considered, a number of uniform methods for characterizing the p.t.c.f. of an arithmetic theory are available. E.g. Herbrand analyses as developed by W. Sieg in [13], S. Buss’ witnessing method [5] or, in general, proof–theoretic techniques using Cut elimination theorem. However, for some particular fragments of Peano Arithmetic none of these standard methods seems to be applicable. Of special interest is the case of the scheme of parameter free Π2–induction, IΠ− 2, given by the induction scheme Iϕ:ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)) → ∀x ϕ(x), restricted to ϕ(x)∈Π− 2(as usual, we write ϕ(x)∈Γ−to mean that ϕis in Γ and contains no other free variables than x). Since IΣ− 1⊆IΠ− 2and IΣ1 is Σ3–conservative over IΣ− 1[10], it follows that every primitive recursive function is provably total in IΠ− 2; and R. Kaye asked whether the p.t.c.f. of IΠ− 2are exactly the primitive recursive ones. This question remained elusive until [4], where L. Beklemishev gave a positive answer using modal provability logic techniques. Although quite elegant, Beklemishev’s answer only provides an indirect solution. Firstly, he reformulated IΠ− 2in terms of local reflection principles (reflection principles in Arithmetic are axiom schemes expressing the statement that “if a formula ϕis provable in a theory Tthen ϕis valid”). Secondly, he derived the result as an application of a 2 conservation theorem for local reflection principles whose proof leans upon properties of G¨odel–L¨ob provability logic GL. In this work we obtain a more direct answer to Kaye’s question, avoiding the metamathematical machinery needed for Beklemishev’s proof. In fact, our proof that R(IΠ− 2) = PR will follow the lines of standard arguments for characterizing classes R(T). Let us consider, for instance, a proof that R(IΣ1) = PR. Such a proof typically proceeds in two steps. •Step 1: IΣ1is Π2–conservative over the inference rule version of the principle of Σ1–induction Σ1–IR. So, R(IΣ1) = R(Σ1–IR). •Step 2: Applications of Σ1–IR correspond to applications of the primitive recursion operator. The main obstacle to apply this argument to IΠ− 2is that there is no simple, direct argument to reduce IΠ− 2to an inference rule version of it. Here we solve this problem by showing that IΠ− 2is equivalent to I(Σ− 2,K2), a certain local version of the parameter free Σ2–induction scheme where the elements xfor which the induction axiom claims ϕ(x) to hold are restricted to be Σ2– definable elements. Equipped with this result, it is easy to obtain that IΠ− 2 is Π2(in fact, Π3) conservative over the corresponding local inference rule version (Σ2,K2)–IR. Then, we show that applications of (Σ2,K2)–IR correspond to (restricted forms) of the iteration operator and thus all functions in R(IΠ− 2) are primitive recursive. Local induction schemes and local induction rules play a crucial role in our methods. Interestingly, these local subsystems can be applied in considerable generality to study fragments of arithmetic. Actually, in this work we also make use of these ideas to develop a general study of the theories IΠ− n+1 for all n≥1. As a result, we are able to give new proofs of some well–known results on these fragments as well as to obtain a novel conservation result. Namely, we prove that IΠ− n+1 is Πn+2–conservative over IΣn for all n≥1. This improves on a previous result by Beklemishev in [4] where conservativity between these theories with respect to boolean combinations of Σn+1–sentences was established, and closes a notable gap in our understanding of relationships between the standard fragments of arithmetic. 2. On Local Induction In this section we give a precise definition of the auxiliary schemes that will be central in our analysis of the class of p.t.c.f. of IΠ− 2. We work in the 3 language of first–order arithmetic L={0, S, +,·, <}and define the formula classes ∆0, Σnand Πnas usual. For a class Γ of formulas, IΓ is the theory axiomatized over Robinson’s Qby the induction scheme, Iϕ, restricted to formulas ϕ(x)∈Γ. If free variables other that xare not allowed, we write ϕ(x)∈Γ−and, accordingly, IΓ−denotes the theory axiomatized over Qby the axioms Iϕ, for ϕ(x)∈Γ−. The schemes we are interested in are local variants of the usual induction scheme in a sense that the conclusion of the induction principle is no longer assumed for every element in the universe but only for a certain subclass of the universe. More precisely, we define: Definition 1. For every n≥1,I(Σn,Kn)is the theory given by I∆0together with the scheme ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)) → → ∀x1, x2(δ(x1)∧δ(x2)→x1=x2)→ ∀x(δ(x)→ϕ(x)) where ϕ(x)∈Σnand δ(x)∈Σ− n. The natural inference rule associated to this scheme, denoted (Σn,Kn)–IR, is given by: ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)) ∀x1, x2(δ(x1)∧δ(x2)→x1=x2)→ ∀x(δ(x)→ϕ(x)) where δ(x)∈Σ− nand ϕ(x)∈Σn. Finally, if we restrict the scheme to ϕ(x)∈Σ− n, we obtain the parameter free counterpart of I(Σn,Kn), denoted I(Σ− n,Kn). Remark 1. Firstly, let us recall that, given a model A,Kn(A)denotes the set of elements of Athat are definable in Aby a formula δ(x)∈Σn. This explains why Knappears in our notation for these theories. Secondly, if A|=IΣ− n−1, then Kn(A)≺nA(i.e. Kn(A)is a Πn–elementary substructure of A). This property plays an important role in what follows and it is because of it that some of our results on I(Σn,Kn)are obtained over IΣ− n−1instead of over I∆0. A key fact is that I(Σ− n,Kn) provides an alternative formulation of IΠ− n for every n≥1: Lemma 1. Over IΣ− n−1,IΠ− n≡I(Σ− n,Kn). 4 Proof. (`): Suppose A|=IΠ− nand A|=ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)), with ϕ(x)∈Σ− n. Let δ(v)∈Σndefining some element in A, say a. Towards a contradiction, assume A6|=∀x(δ(x)→ϕ(x)). Then, A|=¬ϕ(a). Define θ(x) to be ∀v(δ(v)→ ¬ϕ(x−v)). Clearly, A|=θ(0) ∧ ∀x(θ(x)→θ(x+ 1)). By IΠ− n,A|=θ(a) and so A|=¬ϕ(0), which is a contradiction. (a): Suppose A|=I(Σ− n,Kn) and A|=ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)), with ϕ(x)∈Π− n. Assume A|=∃x¬ϕ(x). Since A|=IΣ− n−1,Kn(A)≺nAand there is a∈ Kn(A) such that A|=¬ϕ(a). Let δ(v) be a Σnformula defining the element aand let θ(x) be ∃v(δ(v)∧ ¬ϕ(v−x)). Clearly, A|=θ(0) ∧ ∀x(θ(x)→θ(x+1)). By I(Σ− n,Kn), A|=∀x(δ(x)→θ(x)) and so A|=θ(a). Thus A|=¬ϕ(0), which is a contradiction. Given a theory Tand an inference rule R, we denote by [T, R] the closure of Tunder first order logic and unnested applications of R. We denote by T+Rthe closure of Tunder first order logic and (nested) applications of R. Therefore, T+R=Sk∈ω[T, R]k, where [T, R]0=Tand [T, R]k+1 = [[T, R]k, R]. The first step in the analysis of IΠ− 2is a suitable reduction of I(Σ2,K2) to a fragment defined by the rule (Σ2,K2)–IR. Indeed, the following general result holds for each n≥1. Proposition 1. Let Tbe a Πn+2–axiomatizable theory. Then, T+I(Σn,Kn) is Πn+1–conservative over T+ (Σn,Kn)–IR. Very conveniently, this reduction can be carried out by the same tools used to derive the reduction of IΣ1to Σ1–IR (e.g. by adapting the cut–elimination argument used in [3] to derive a similar reduction for the Collection scheme). Alternatively, here we give a model–theoretic proof following the methods developed by J. Avigad in [1], who in turn builds on previous ideas of A. Visser (unpublished) and D. Zambella [14]. In [1] Avigad introduced the notion of a Herbrand saturated model and showed that this notion provides us with an unified method to prove ∀∃–conservation over universal theories. Here we consider a hierarchical version of that notion that yields an unified method to prove Πn+1–conservation over Πn+2–theories. Definition 2. We say that a model of a theory T,A, is a Σn+1–closed model of Tif for every model of T,B, A≺nB=⇒A≺n+1 B. 5 In words, Ais a Σn+1–closed model of Tif every Πn–formula that can be satisfied in a Πn–elementary extension of Awhich is a model of Tcan be already satisfied by an element of A. It is easy to show that Σn+1– closed models exist for every n. In fact, by a rather standard union of chain argument it follows that if Tis a Πn+2–axiomatizable theory, then every model of Tcan be Πn–elementary extended to a Σn+1–closed model of T. As a consequence, the following version of theorem 3.4 of [1] holds. Lemma 2. Suppose T2is Πn+2–axiomatizable. In order to prove that T1 is Πn+1–conservative over T2it is sufficient to show that every Σn+1–closed model of T2satisfies T1. Next lemma is an analog of theorem 3.3 of [1] and states the key property of Σn+1–closed models for proving conservation results. Lemma 3. Suppose Ais a Σn+1–closed model of T, ϕ(v)∈Πn+1 and a∈A. Then A|=ϕ(a) =⇒T`ψ(v, w)→ϕ(v), for some ψ(v, w)∈Πnsuch that A|=ψ(a, b)for some bin A. Proof. It follows from the Σn+1–closedness condition that T+DΠn(A)` ϕ(a), where DΠn(A) denotes the Πn–diagram of A, i.e. the set of all Πn– formulas (possibly with parameters) valid in A. Now the result follows by compactness. We are now in a position to give a proof of Proposition 1. Proof. Suppose that Ais a Σn+1–closed model of T+ (Σn,Kn)–IR and A|= ϕ(0, b)∧ ∀x(ϕ(x, b)→ϕ(x+ 1, b)), with ϕ(x, v)∈Σn. Consider a∈ Kn(A) and δ(x)∈Σndefining a. We must show that A|=ϕ(a, b). It follows from Lemma 3 that (T+ (Σn,Kn)–IR) `ψ(v, w)→ϕ(0, v)∧ ∀x(ϕ(x, v)→ϕ(x+ 1, v)), with ψ(v, w)∈Πnand A|=ψ(b, c) for some c∈A. Put θ(x, v, w)≡ ψ(v, w)→ϕ(x, v). Clearly, θ∈Σnand (T+ (Σn,Kn)–IR) proves the antecedent of the induction axiom for θand so A|=∀v, w, x (δ(x)→θ(x, v, w)). Thus θ(a, b, c) is valid in Aand hence so is ϕ(a, b). Combining Lemma 1 and Proposition 1, we get Corollary 1. IΠ− 2is Π3–conservative over IΣ− 1+ (Σ2,K2)–IR. 6 3. Local Induction and Restricted Iteration Next step in our analysis is to show that applications of (Σ2,K2)–IR correspond to (a restricted form of) the iteration operator. To this end, we shall consider extensions of Lobtained by adding a finite set of unary function symbols, F={f1, . . . , fn}, and a (finite or countable) set of new constant symbols, C. Through this section we consider a fixed set of constants, C, and we will denote by LFthe language L+{f1, . . . , fn}+C. If gis a new unary function symbol then LF,g will denote the language L{f1,...,fn,g}. Definition 3. Let f∈ F be a unary function symbol and let Tbe an LF– theory. We say that fis an iterable non decreasing function over Tif the theory Tproves: ∀x1, x2(x1≤x2→f(x1)≤f(x2)),and ∀x(x2< f(x)) Let ΣF 0= ΠF 0be the class of bounded formulas of LF. Classes ΣF n+1 and ΠF n+1 are defined as usual. The theory IΣF 0is the LF–theory axiomatized over I∆0by •The induction axiom Iϕfor each formula ϕ∈ΣF 0, and •Axioms for each f∈ F: ∀x1, x2(x1≤x2→f(x1)≤f(x2)), and ∀x(x2< f(x)) This is a basic theory to deal with the iteration of fand to guarantee the usual properties of the iteration of a nondecreasing function with a ΠF 0–definable graph. The basic facts provable in this theory were stated in [6]. Next result collects together the facts that we shall need in the present context. Proposition 2. For each f∈ F there exists a formula ITf(z, x, y)∈ΣF 0 such that the following formulas are theorems of IΣF 0: 1. ITf(z, x, y1)∧ITf(z, x, y2)→y1=y2. 2. (ITf(0, x, y)↔x=y)∧(ITf(1, x, y)↔f(x) = y). 3. ITf(z+ 1, x, y)↔ ∃y0≤y(ITf(z, x, y0)∧f(y0) = y). 4. ITf(z, x, y)→ ∀z0< z ∃y0< y ITf(z0, x, y0). 5. z≥1∧ITf(z, x, y)→x2< y ∧z≤y. 6. z≥1∧x1≤x2∧ITf(z, x1, y1)∧ITf(z, x2, y2)→y1≤y2. 7 7. ITf(z1, x, y0)∧ITf(z2, y0, y)→ITf(z1+z2, x, y). In what follows we use a more suggestive notation and write fz(x) = y instead of ITf(z, x, y). Definition 4. We say that f∈ F is a dominating function over Tif, for each term t(x)of LF, there exists k∈ωsuch that Tproves ∀x(t(x)≤fk(x+σ(t))) where σ(t) = c1+· · · +cmand c1, . . . , cmare all the constants occurring in t(x). Lemma 4. Let Tbe an extension of IΣF 0and let f∈ F be a (iterable nondecreasing) dominating function over T. Then, for each term t(x1, . . . , xm) of LFwhose variables are among x1, . . . , xm, there exists k∈ωsuch that T`t(x1, . . . , xm)< fk(x1+· · · +xm+σ(t)). Proof. We proceed by induction on terms of LF. The most interesting case occurs when t(x1, . . . , xm) is a sum (or a product) of two terms, say t1(x1, . . . , xm) + t1(x1, . . . , xm). By induction hypothesis, t1(~x)< fk(x1+· · · +xm+σ(t1)) and t2(~x)< fl(x1+· · · +xm+σ(t2)), for some k, l ∈ω. Without loss of generality we may assume k≥max(l, 2) (so, for every u,fk(u)≥k≥2.) Then, t(~x) = t1(~x) + t2(~x) < fk(x1+· · · +xm+σ(t1)) + fl(x1+· · · +xm+σ(t2)) ≤2fk(x1+· · · +xm+σ(t)) ≤(fk(x1+· · · +xm+σ(t)))2 < fk+1(x1+· · · +xm+σ(t)). The remaining cases are similar. Languages LFand the notion of a dominating function are tailored to deal with the situation described in the following lemma. Lemma 5. Let Γ = {θ1(x, y), . . . , θm(x, y)}be a finite set of ∆0–formulas with only two free variables. For each j= 1, . . . , m, let ¯ θj(x, y)denote the formula ∀u≤x∃v≤y θj(u, v). Let F={f1, . . . , fm, f}be a set of unary function symbols and let Tbe the LF–theory extending I∆0with the following additional axioms: 8 •For each j= 1, . . . , m, ∀x(fj(x) = y↔ ∃y0≤y(y0=µt. ¯ θj(x, t)∧y= (x+ 1)2+y0)). • ∀x(f(x) = (x+ 1)2+f1(x) + · · · +fm(x)). Then, Textends IΣF 0and fis a dominating function over T. Proof. It is straighforward to check that each h∈ F is an iterable nondecreasing function over T. In addition, by proposition V.1.3 of [8], Tproves ΣF 0–induction. Thus we only must show that fis a dominating function over T. This fact can be proved by induction on terms of LF. Again, the most interesting case occurs when t(x) is a product (or sum) of two terms, say t1(x)·t2(x). By induction hypothesis, t1(x)≤fk(x+σ(t1)) and t2(x)≤fl(x+σ(t2)), for some k≥max(l, 2) (so, for every u,fk(u)≥k≥2.) Then, t(x)≤(t1(x) + t2(x))2≤f(t1(x) + t2(x)) ≤f(fk(x+σ(t1)) + fl(x+σ(t2))) ≤f(2 ·fk(x+σ(t))) ≤f((fk(x+σ(t)))2)≤fk+2(x+σ(t)). The remaining cases are similar. As a final step in the analysis of (Σ2,K2)–IR and due to technical reasons, it will be convenient to denote the Σ2–definable elements by closed terms of an extended language. This motivates the introduction of the following local induction rules. Definition 5. For each set of formulas Γand each set of closed terms Λof LFwe consider the rules (where ϕ(x)∈Γand t∈Λ): (Γ,Λ)–IR :ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)) ϕ(t) (Γ,Λ)–IR0:∀x(ϕ(x)→ϕ(x+ 1)) ϕ(0) →ϕ(t) These rules were first considered and intensively studied in [6]. There we proved that a number of results on classical induction rules are also true for the local ones. In what follows, we state two of these results that will be needed in the present paper. For the rest of the section, we assume that 9 4. Provably Total Computable Functions of IΠ− 2 We are now in a position to give a proof that R(IΠ− 2) = PR. Firstly, we need a version of Theorem 2 in the language of first–order Arithmetic. Lemma 9. IΣ1extends I∆0+ (Σ2,K2)–IR. Proof. Let A|=IΣ1and ϕ(x)∈Σ2such that (•)I∆0+ (Σ2,K2)–IR `ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)). We must show that for every δ(u)∈Σ− 2, (?)A|=∀x1∀x2(δ(x1)∧δ(x2)→x1=x2)→ ∀x(δ(x)→ϕ(x)). By (•) there exist formulas ϕ1(x), . . . , ϕr(x)∈Σ2and δ1(x), . . . , δr(x)∈Σ− 2 such that I∆0plus the sentences αj:∀x1∀x2(δj(x1)∧δj(x2)→x1=x2)→ ∀x(δj(x)→ϕj(x)) (j= 1, . . . , r) proves ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)).More precisely, for each j≤r, I∆0+^ 1≤i<j αi`ϕj(0) ∧ ∀x(ϕj(x)→ϕj(x+ 1)), and I∆0+Vr i=1 αi`ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)). Let E={j: 1 ≤j≤r, A|=¬∃xδj(x)}and, for each j∈E, let θj(x, y)∈Π0such that ¬∃x δj(x) is equivalent to ∀x∃y θj(x, y). Let mbe the cardinal of Eand let F={f1, . . . , fm, f}be a set of new unary function symbols. From the set of Σ0formulas Γ = {θj(x, y) : j∈E}, we define a theory Tas in Lemma 5. Let L(A) denote the language obtained by adding to La constant symbol a, for each a∈A. Put T0=T+DΠ1(A), where DΠ1(A) is the Π1–diagram of A. Let Λ be the set of closed terms of L(A) containing only constants of the form afor a∈ K2(A). Then Ahas a natural expansion AFto the language LF∪ L(A) such that AF|=T0+IΣF 1. By Theorem 2, AF|=T0+ (ΣF 2,Λ)–IR. Given δ(x)∈Σ− 2, we distinguish several cases: If A|=¬∃x δ(x) then (?) obviously holds. On the other hand, if A|= ¬∀x1∀x2(δ(x1)∧δ(x2)→x1=x2), since this is a Σ2–sentence and T0extends DΠ1(A), T0` ¬∀x1∀x2(δ(x1)∧δ(x2)→x1=x2). So, T0` ∀x1∀x2(δ(x1)∧δ(x2)→x1=x2)→ ∀x(δ(x)→ϕ(x)). 16 In that way (?) holds again. We must deal with a last case: A|=∃!x δ(x). Then there exists d∈ K2(A) such that A|=δ(d) and d∈Λ. In order to verify (?) it is enough to show that T0+ (ΣF 2,Λ)–IR `ϕ(d). We prove, by induction on j, that for all j= 1, . . . , r,T0+ (ΣF 2,Λ)–IR ` αj.Let j≤r, and assume that T0+ (ΣF 2,Λ)–IR `V1≤i<j αi. Then (•)jT0+ (ΣF 2,Λ)–IR `ϕj(0) ∧ ∀x(ϕj(x)→ϕj(x+ 1)). If j∈Eor A|=¬∀x1∀x2(δj(x1)∧δj(x2)→x1=x2) then, reasoning as in previous cases, we conclude that T0`αj. If A|=∃!x δj(x), then there exists b∈ K2(A) such that A|=δj(b) and b∈Λ. Using (•)jwe obtain T0+ (ΣF 2,Λ)–IR `ϕj(b). Therefore, T0+ (ΣF 2,Λ)–IR ` ∃x(δj(x)∧ϕj(x)), and it follows that T0+ (ΣF 2,Λ)–IR `αj, as required. We have proved that T0+ (ΣF 2,Λ)–IR `Vr j=1 αjand so T0+ (ΣF 2,Λ)–IR `ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)). Thus, T0+ (ΣF 2,Λ)–IR `ϕ(d) and, as a consequence, (?) holds. Next theorem extends a previous conservation result obtained in [4] and, as a direct corollary, yields the characterization of the p.t.c.f. of IΠ− 2. Theorem 3. IΠ− 2is Π3–conservative over IΣ1. Proof. Let θbe a Π3sentence provable in IΠ− 2. Then I(Σ2,K2)`θby Lemma 1 and IΣ− 1+(Σ2,K2)–IR `θby Proposition 1. We need the following fact: Claim 2. IΣ− 1+ (Σ2,K2)–IR ≡IΣ− 1+ (I∆0+ (Σ2,K2)–IR). Proof of Claim: Each axiom of IΣ− 1is a Σ3sentence, so it is enough to prove that for every σ0(u)∈Π2, [I∆0,(Σ2,K2)–IR] + ∃u σ0(u) extends [I∆0+∃u σ0(u),(Σ2,K2)–IR]. Assume I∆0+∃u σ0(u)`ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)), where ϕ(x)∈Σ2, and let ψ(x, u)∈Σ2be σ0(u)→ϕ(x). Then, I∆0proves ψ(0, u)∧ ∀x(ψ(x, u)→ψ(x+ 1, u)) 17 and, therefore, [I∆0,(Σ2,K2)–IR] `Uδ→ ∀x(δ(x)→ψ(x, u)), where δ(x)∈ Σ− 2and Uδdenotes the sentence ∀x1∀x2(δ(x1)∧δ(x2)→x1=x2).Then [I∆0,(Σ2,K2)–IR] also proves ∃u σ0(u)→(Uδ→ ∀x(δ(x)→ϕ(x))) and so [I∆0,(Σ2,K2)–IR] + ∃u σ0(u)`Uδ→ ∀x(δ(x)→ϕ(x)), as required. It follows from Claim and Lemma 9 that IΣ1implies IΣ− 1+ (Σ2,K2)–IR and, therefore, IΣ1`θ. Corollary 3. The class of provably total computable functions of IΠ− 2is the class of primitive recursive functions. 5. Relativization and Concluding Remarks It is natural to ask ourselves whether Theorem 3 is also true for IΠ− n+1 and IΣnfor an arbitrary n≥1. We have already seen that the reduction of IΠ− n+1 to IΣ− n+(Σn+1,Kn+1)–IR works for all nand it is immediate to check that the claim in the proof of Theorem 3 can be generalized too. Thus, the key point is to prove that Lemma 9 also holds for n > 1, i.e. to prove that IΣnimplies IΣn−1+(Σn+1,Kn+1)–IR for all n≥1. Our proof of Lemma 9 for n= 1 leans upon Theorem 2 reducing (ΣF 2,Λ)–IR to IΣF 1. Interestingly, the result for n > 1 can also be derived from Theorem 2 by using some standard relativization techniques. Building on previous work of Kaye [9], in [7] it is shown that, for each n≥1, there is a Πn–formula y=Kn(x) satisfying that (a) IΣn≡I∆0+∀x∃!y(y=Kn(x)), (b) y=Kn(x) is iterable and non decreasing over IΣn, and (c) initial segments of A|=IΣnclosed under function y=Kn(x) are Πn– elementary substructures of A. Using functions Knone can reformulate IΣnas a ΠF 1–theory in an extended language L ∪ {g1, . . . , gn}so that Σn+mformulas of Lcorrespond to ΣF mformulas of the extended language (a similar treatment of relativization was also developed by Z. Ratajczyk in [11] via the notion of a conditionally absolute formula.) Lemma 10. Let n≥1and let F={g1, . . . , gn}. There is a ΠF 1–theory Tn satisfying that 18 1. Tnextends IΣn, 2. every model of IΣnhas a (canonical) extension to a model of Tn, 3. every ΣF mformula is equivalent in Tnto a Σn+m–formula of L, and 4. every Σn+mformula is equivalent in Tnto a ΣF m–formula. Proof. (Sketch) n= 1: Put T1≡IΣF 0+ (y=g1(x)→y=K1(x)). Conditions (1), (2) and (3) are easy to verify, for we know that allowing monotone functions instead of only variables as the bounds in ΣF 0formulas does not increase the strength of ΣF 0–induction (see, e.g. proposition V.1.3 of [8]). As for (4), since IΣ1contains the strong collection scheme for Π0– formulas ∀z∃u∀x≤z(∃y ϕ(x, y)→ ∃y≤u ϕ(x, y)), by a Parikh–like argument (available thanks to condiction (c) above) it follows that for each θ(~x, y)∈Π0there is some k∈ωsuch that IΣ1` ∃y θ(~x, y)↔ ∃y≤Kk 1(x1+. . . +xp)θ(~x, y), and the result follows. n→n+ 1: Let y=K0 n+1(x) denote a ΠF 1–formula equivalent in Tnto y= Kn+1(x) and put Tn+1 ≡Tn+ (y=gn+1(x)→y=K0 n+1(x)). Equipped with this result, it is not hard to check that everything in the proof of Lemma 9 relativizes. Indeed, let n≥2 and suppose Ais a model of IΣnand ϕ(x) is in Σn+1. As in Lemma 9 let δ1(x), . . . , δr(x) be the Σ− n+1–formulas occurring in a proof of ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)) in IΣn−1+ (Σn+1,Kn+1)–IR. Let E={j: 1 ≤j≤r, A|=¬∃xδj(x)}and let F={f1, . . . , fm, g1, . . . , gn−1, f}, where mis the cardinal of E. For each j∈E, let θ0 j(x, y)∈ΠF 0such that ¬∃x δj(x) is equivalent in Tn−1to ∀x∃y θj(x, y). From this set of ΣF 0formulas define a ΠF 1–theory Textending Tn−1as in Lemma 5. Finally, put T0≡T+DΠg 1(A), where DΠg 1(A) is the Π1–diagram of Ain the language of Tn−1, and take Λ = Kn+1(A). Then, A|=T0+IΣF 1. So, applying Theorem 2 and reasoning as in Lemma 9 we get A|=IΣn−1+ (Σn+1,Kn+1)–IR, as desired. Thus, we have Theorem 4. For every n≥1,IΠ− n+1 is Πn+2–conservative over IΣn. 19 A straightforward consequence of this result is a characterization of the class of p.t.c.f. of IΠ− n+1 in terms of the extended Grzegorczyk Hierarchy {Eα:α < ε0}, see [12] for precise definitions. Corollary 4. For every n≥1,R(IΠ− n+1) = R(IΣn) = Eωn, where ω0= 1, ωn+1 =ωωn. An important ingredient in this analysis of the class of Πn+2–consequences of IΠ− n+1 is the study of the closure a weak theory, such as IΣ− n(or even I∆0), under (Σn+1,Kn+1)–IR. This analysis can be extended to stronger base theories providing us with similar conservation results for theories of the form T+IΠ− n+1, where Tis a Πn+2–axiomatizable extension IΣn. In the following proposition we obtain this kind of conservation results when Tis closed under Σn+1–collection rule: Σn+1–CR : ∀x∃y ϕ(x, y) ∀u∃v∀x≤u∃y≤v ϕ(x, y) for ϕ(x, y)∈Σn+1. Proposition 4. Let Tbe a Πn+2–axiomatizable extension of IΣn, closed under Σn+1–CR. Then: 1. T+IΠ− n+1 is Πn+2–conservative over [T, Σn+1–IR] 2. T+IΠ− n+1 is Πn+1–conservative over T+ Πn+1–IR. Proof. These results were proved for n= 0 in [6]. The proof for n≥1 is very similar, modulo relativization. Here we discuss the proof for n= 1. (1) First of all, let us recall that, over IΣ1,IΠ− 2≡I(Σ− 2,K2) and that, by Proposition 1, T+I(Σ2,K2) is Π3–conservative over T+ (Σ2,K2)–IR. So it is enough to show that [T, Σ2–IR] extends this last theory. But observe that (•)T+ (Σ2,K2)–IR ≡[T, (Σ2,K2)–IR]. This can be obtained from Lemma 6, by using the relativization device that we have developed (see the proof of lemma 3.7 in [6] for details). By (•), [T, Σ2–IR] obviously extends T+ (Σ2,K2)–IR and the result follows. (2) By part (1) it suffices to show that [T, Σ2–IR] is Π2–conservative over T+ Π2–IR. By proposition 2.1 of [2], [T, Σ2–IR] is equivalent to [T, Π2–IR0] and it is straightforward to show (using Lemma 3) that every Σ2–closed model of T+ Π2–IR is a model of [T, Π2–IR0]. By Lemma 2 it follows that [T, Π2–IR0] is Π2–conservative over T+ Π2–IR, as required. 20 The interest of Proposition 4 is twofold. On the one hand, part (1) provides a generalization of a similar result obtained in [10]: Theorem 5 (Kaye–Paris–Dimitracopoulos). IΠ− 1is Π2–conservative over I∆0+ exp (≡[I∆0,Σ1–IR]). We can think of this result as a counterpart of Theorem 4 for IΠ− 1. However, a generalization of Theorem 5 for every n≥1 must take into consideration two different scenarios, since I∆0≡I∆− 0, but IΣnis a proper extension of IΣ− n. Together Proposition 4 and Theorem 4 show that both generalizations are correct. For T=IΣn, Proposition 4 shows that Theorem 5 also holds for every n≥1 (essentially, this result was obtained by Kaye in [9]): Corollary 5. IΣn+IΠ− n+1 is Πn+2–conservative over [IΣn,Σn+1–IR]. In turn, Theorem 4 shows that this corollary also holds for IΣ− n, since for every n≥1, IΣn≡[IΣ− n,Σn+1–IR] and, obviously IΠ− n+1 extends IΣ− n. On the other hand, Proposition 4 reduces the question about the class of p.t.c.f. of IΣ1+IΠ− 2to the study of the closure of IΣ1under Π2–IR. In a similar vein, by combining parts (1) and (2), we obtain that, for every k≥1, [IΣ1,Σ2–IR]k+1 is Π2–conservative over [IΣ1,Σ2–IR]k+ Π2–IR. These reductions suggest that local induction can be a useful tool in obtaining new proofs of some of the already known characterizations of classes of p.t.c.f. in terms of the extended Grzegorczyk hierarchy; for instance, R(IΣ1+IΠ− 2) (studied by Beklemishev in [4]), R([IΣ1,Σ2–IR]k) or R(IΣ2) and, more generally, R(IΣn+IΠ− n+1) and R(IΣn). This points out natural extensions of the results and methods we have introduced in this paper. Acknowledgement This work was partially supported by grants MTM2008–06435 and MTM2011– 26840 of Ministerio de Ciencia e Innovaci´on, Spain. Cofinanced with FEDER funds, EU. References [1] Avigad, J. Saturated models of universal theories. Annals of Pure and Applied Logic, 118 (2002) 219–234. 21 [2] Beklemishev, L.D. Induction rules, reflection principles and provably recursive functions. Annals of Pure and Applied Logic, 85 (1997) 193– 242. [3] Beklemishev, L.D. A proof–theoretic analysis of collection. Archive for Mathematical Logic, 37 (1998) 275–296. [4] Beklemishev, L.D. Parameter free induction and provably total computable functions. Theoretical Computer Science, 224 (1999) 13-33. [5] Buss, S. The Witness Function Method and Provably Recursive Functions of Peano Arithmetic, in: D. Westertahl, D. Prawitz, B. Skyrms (Eds.), Proceedings of the 9th. International Congress on Logic, Methodology and Philosophy of Science, Elsevier, North–Holland, Amsterdam, (1994) 29–68. [6] Cord´on–Franco, A.; Fern´andez–Margarit, A.; Lara–Mart´ın, F. F. On conservation results for parameter–free Πn–induction. In Studies in Weak Arithmetics, Patrick C´egielski (editor). CSLI Publications, Stanford, California (2010) 49–97. [7] Fern´andez–Margarit, A.; Lara–Mart´ın, F.F. Induction, Minimization and Collection for ∆n+1(T)–formulas. Archive for Mathematical Logic, 43 (2004) 505–542. [8] H´ajek, P.; Pudl´ak, P. Metamathematics of First–Order Arithmetic. Perspectives in Mathematical Logic, Springer Verlag, 1993. [9] Kaye, R. Diophantine and Parameter–free Induction. Ph.D. University of Manchester, 1987. [10] Kaye, R.; Paris, J; Dimitracopoulos, C. On parameter free induction schemas. The Journal of Symbolic Logic, 53 (1988) 1082–1097. [11] Ratajczyk, Z. Functions provably total in I−Σn. Fundamenta Mathematicae, 132 (1989) 81–95. [12] Rose, H. E. Subrecursion. Functions and hierarchies. Oxford Logic Guides 9. Clarendon Press, Oxford, 1984. [13] Sieg, W. Herbrand Analyses. Archive for Mathematical Logic, 30 (1991) 409–441. 22 [14] Zambella, D. Notes on polynomial bounded arithmetic. Journal of Symbolic Logic, 61 (1996) 942–966. 23