Local Induction and Provably Total Computable Functions: A Case Study

Local Induction and Provably Total Computable Functions: A Case Study Andr´es Cord´on–Franco and F. F´elix Lara–Mart´ın Departamento Ciencias de la Computaci´on e Inteligencia Artificial, Facultad de Matem´aticas. Universidad de Sevilla, C/ Tarfia, s/n, 41012 Sevilla, Spain {acordon,fflara}@us.es 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 (p.t.c.f.) of IΠ− 2are, precisely, the primitive recursive ones. In this work we give a new proof of this fact through an analysis of the p.t.c.f. of certain local versions of induction principles closely related to IΠ− 2. This analysis is essentially based on the equivalence between local induction rules and restricted forms of iteration. 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. 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:IN k→IN is 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: 1. ϕdefines the graph of fin the standard model of Arithmetic IN; and 2. T∀x ∃!yϕ(x, y). Observe that condition 1. amounts to the computability of f, whereas condition 2. yields an implicit measure of the complexity of f attending to the logical principles needed to prove that a Σ1–definition of f defines a total function. 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Σ1 equals 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 [9], 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Σ1is Σ3– conservative over IΣ− 1[8], 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 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)=PRwill 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 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Π− 2is Π2(in fact, Π3) conservative over the corresponding 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. Our analysis also yields a new conservation theorem for fragments of Peano Arithmetic, which is of independent interest. Namely, we prove that IΠ− 2is Π3– conservative over IΣ1. This improves on a previous result by Beklemishev in [4], where conservativity between these theories with respect to boolean combinations of Σ2–sentences was established. We close this section by giving a precise definition of the auxiliary scheme that will be central in our analysis of the class of p.t.c.f. of IΠ− 2. Let L={0,S,+,·,<}denote the language of first order Arithmetic. If Γis a set of formulas of L,thenIΓ 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)∈Γ−. Definition 1. I(Σ2,K2)is the theory given by IΣ− 1together with the scheme ϕ(0) ∧∀x(ϕ(x)→ϕ(x+1))→ →∀x1,x 2(δ(x1)∧δ(x2)→x1=x2)→∀x(δ(x)→ϕ(x)) where ϕ(x)∈Σ2and δ(x)∈Σ− 2. The natural inference rule associated to this scheme, denoted (Σ2,K2)–IR, is given by: ϕ(0) ∧∀x(ϕ(x)→ϕ(x+1)) ∀x1,x 2(δ(x1)∧δ(x2)→x1=x2)→∀x(δ(x)→ϕ(x)) where δ(x)∈Σ− 2and ϕ(x)∈Σ2. Finally, if we restrict the scheme to ϕ(x)∈ Σ− 2, we obtain the parameter free counterpart of I(Σ2,K2),denotedI(Σ− 2,K2). Remark 1. Firstly, let us recall that, given a model A,K2(A) denotes the set of elements of Athat are definable in Aby a formula δ(x)∈Σ2. This explains why K2appears in our notation for these theories. Secondly, if A|=IΣ− 1,then K2(A)≺2A(i.e., K2(A)isaΠ2–elementary substructure of A). This property plays an important role in what follows and it is because of it that I(Σ2,K2)is axiomatized over IΣ− 1instead of over a weaker system (such as Qor IΔ0). A key fact is that I(Σ− 2,K2) provides an alternative formulation of IΠ− 2: Lemma 2. IΠ− 2≡I(Σ− 2,K2). Proof. We only prove that I(Σ− 2,K2) extends IΠ− 2. The converse is similar. Let A|=I(Σ− 2,K2)andϕ(x)∈Π− 2such that A|=ϕ(0) ∧∀x(ϕ(x)→ϕ(x+ 1)). Assume A|=∃x¬ϕ(x). Since A|=IΣ− 1,K2(A)≺2Aand there is a∈K 2(A) such that A|=¬ϕ(a). Let δ(v)beaΣ2formula defining the element aand let θ(x)be∃v(δ(v)∧¬ϕ(v−x)). Clearly, A|=θ(0) ∧∀x(θ(x)→θ(x+ 1)). By I(Σ− 2,K2), A|=θ(a)andsoA|=¬ϕ(0), which is a contradiction. Given a theory Tand an inference rule R,wedenoteby[T,R] the closure of T under first order logic and unnested applications of R.WedenotebyT+Rthe closure of Tunder first order logic and (nested) applications of R. Therefore, T+R=k∈ω[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)toa fragment defined by the rule (Σ2,K2)–IR. Indeed, we have: Proposition 3. I(Σ2,K2)is Π3–conservative over IΣ− 1+(Σ2,K2)–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, in [6], lemma 3.6, we gave a model–theoretic proof of this result using the notion of a Σn+1–closed model, following the methods introduced by Avigad in [1]. 2 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,...,f n}, and a (finite or countable) set of new constant symbols, C. Through this section we consider a fixed set of constants, C, and we shall denote by LF the language L+{f1,...,f n}+C.Ifgis a new unary function symbol then LF,g will denote the language L{f1,...,fn,g}. Definition 4. Let f∈Fa unary function symbol and Tan LF–theory. We say that fis an iterable non decreasing function over Tif the theory Tproves: ∀x1,x 2(x1≤x2→f(x1)≤f(x2)),and ∀x(x2<f(x)) Let Σ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 Qby –The induction axiom Iϕfor each formula ϕ∈ΣF 0,and –Axioms for each f∈F: ∀x1,x 2(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 5. For each f∈F there exists a formula ITf(z,x,y)∈ΣF 0such 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<yIT f(z0,x,y 0). 5. z≥1∧ITf(z,x,y)→x2<y∧z≤y. 6. z≥1∧x1≤x2∧ITf(z,x1,y 1)∧ITf(z,x2,y 2)→y1≤y2. 7. ITf(z1,x,y 0)∧ITf(z2,y 0,y)→ITf(z1+z2,x,y). In what follows we use a more suggestive notation and write fz(x)=yinstead of ITf(z,x,y). Definition 6. We say that f∈F is a dominating function over Tif, for any term t(x)of LF,thereexistsk∈ωsuch that Tproves ∀x(t(x)≤fk(x+σ(t))) where σ(t)=c1+···+cmand c1,...,c mare all the constants occurring in t(x). Lemma 7. Let Tbe an extension of IΣF 0and let f∈Fa (iterable nondecreasing) dominating function over T. Then, for each term t(x1,...,x m)of LF whose variables are among x1,...,x m,thereexistsk∈ωsuch that Tt(x1,...,x m)<f k(x1+···+xm+σ(t)). Remark 2. Languages LFand the notion of a dominating function are tailored to deal with the following situation. Assume Γ={θ1,...,θ m}is a finite set of Σ0–formulas with only two free variables, say xand y,andforeachj=1,...,m, ¯ θj(x, y) denotes the formula ∀u≤x∃v≤yθ j(u, v). Let F={f1,...,f m,f}be a set of unary function symbols and let Tbe the extension of IΣF 0with the following additional axioms: –For each j=1,...,m,∀x(fj(x)=y↔∃y0≤y(¯ θj(x, y0)∧y=(x+1)2+y0). –∀x(f(x)=(x+1) 2+f1(x)+···+fm(x)). Then, every h∈Fis an iterable nondecreasing function over Tand fis a dominating function over T. This last fact can be proved by induction on terms. The most interesting case occurs when t(x) is a product of two terms, 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)) and we conclude that t(x)≤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 8. For each set of formulas Γand each set of closed terms Λ0of LFwe consider the rules (where ϕ(x)∈Γand t∈Λ0): (Γ, Λ0)–IR :ϕ(0) ∧∀x(ϕ(x)→ϕ(x+1)) ϕ(t) (Γ, Λ0)–IR0:∀x(ϕ(x)→ϕ(x+1)) ϕ(0) →ϕ(t) Definition 9. We say that Λ0is exponentially closed over Tif for every t, s ∈ Λ0there exists t∈Λ0such that [T,(ΣF 1,Λ 0)–IR]∃y≤t(st=y). These rules were intensively studied in [6], where the following results were obtained. From now on, we assume that Tis a fixed extension of IΣF 0obtained by adding a set of ΠF 1sentences, and Λ0denotes the set of all closed terms of a sublanguage of LFextending Land containing the set of constants C(and so Λ0is closed under sum and product). Remark 3. Let us note that under these assumptions Tsatisfies a natural version of Parikh’s theorem (see [7], chapter 5, theorem 1.4). This fact will be used extensively without further comments. In addition, we assume that there is f∈L Fa dominating function over Tand Λ0is exponentially closed over T. Then, we have (see lemma 4.8, lemma 4.10 and theorem 4.14 of [6]): Proposition 10. T+(ΠF 2,Λ 0)–IR ≡T+{∀x∃y(ft(x)=y): t∈Λ0}. Theorem 11. T+(ΠF 2,Λ 0)–IR0is ΠF 2–conservative over T+(ΠF 2,Λ 0)–IR. Here we extend our work in [6] and obtain a new theorem on these local induction systems that will be crucial to derive our main result. The ideas involved are similar to the ones used in [6] to obtain Proposition 10 and Theorem 11. Theorem 12. T+IΣF 1extends T+(ΣF 2,Λ 0)–IR. Proof. The arguments used in [2], proposition 2.1, can be easily adapted to yield that for every k∈ω,[T,(ΣF 2,Λ 0)–IR]k≡[T,(ΠF 2,Λ 0)–IR0]k.So it is enough to prove that for every k∈ω,T+IΣF 1extends [T,(ΠF 2,Λ 0)–IR0]k. We proceed by induction on k∈ω: Case k= 0 is trivial; so, let us assume that T+IΣF 1extends [T,(ΠF 2,Λ 0)–IR0]k. Let t∈Λ0and ϕ(u, v)∈ΠF 2such that (†)[T,(ΠF 2,Λ 0)–IR]k∀u(ϕ(u, v)→ϕ(u+1,v)). We must prove that T+IΣF 1ϕ(0,v)→ϕ(t, v). Without loss of generality, we can assume that ϕ(u, v)≡∀x∃yϕ 0(u, x, y, v), with ϕ0(u, x, y, v)∈ΣF 0.Letgbe a new unary function symbol and Tgthe extension of T+IΣF,g 0obtained by adding the sentences: ∀x1,x 2(x1≤x2→g(x1)≤g(x2)),∀x(x2<g(x)) and ∀x(f(x)≤g(x)). Thus, gis a dominating (iterable nondecreasing) function over Tg.By(†), it follows that [Tg,(ΠF,g 2,Λ 0)–IR]kϕg,whereϕgis the following sentence: ∀u(∀x∃y≤g(x+u+v)ϕ0(u, x, y, v)→∀x∃yϕ 0(u+1,x,y,v)). Claim. There is a closed term τ0∈Λ0such that Tg+∀x∃y(gτ0(x)=y)proves ∀u(∀x∃y≤g(x+u+v)ϕ0(u, x, y, v)→∀x∃y≤gτ0(u+x+v)ϕ0(u+1,x,y,v)) Proof of Claim: We distinguish two cases: Case 1:k=0.ThenTgϕg. Hence, by Parikh’s theorem, there exists a term s(u, x, v)ofLF,g such that Tg∀u(∀x∃y≤g(x+u+v)ϕ0(u, x, y, v)→∀x∃y≤s(u, x, v)ϕ0(u+1,x,y,v)) By Lemma 7, there is m∈ωsuch that Tgs(u, x, v)<g m(u+x+v+σ(s)). By induction on zit can be proved that Tggu(x+z)=y1∧gu+z(x)=y2→y1≤y2 and, thus, if τ0=m+σ(s)thenτ0∈Λ0and the result follows. Case 2:k≥1. Since [Tg,(ΠF,g 2,Λ 0)–IR]kϕgand ϕgis a ΠF,g 2–formula, by Theorem 11, Tg+(ΠF,g 2,Λ 0)–IR also proves ϕg. It follows from Proposition 10 that there exist t1,...,t n∈Λ0such that Tg+{∀x∃y(gtj(x)=y): j=1,...,n}ϕg. Let r=t1+···+tn. Then, by part (4) of Proposition 5, Tg+∀x∃y(gr(x)=y) extends Tg+{gtjis total : j=1,...,n}.Lethbe a new unary function symbol and let Thbe the extension of Tgobtained by adding to Tgthe axiom ∀x(gr(x)=h(x)). Then Thϕgand This conservative over Tg. By Proposition 5, his an iterable nondecreasing function over Thand Th ∀x(g(x)≤h(x)). Therefore, his a dominating function over Thand Thextends IΣF,g,h 0. By Parikh’s theorem, there is a term s(u, x, v)ofLF,g,h such that Th∀u(∀x∃y≤g(x+u+v)ϕ0(u, x, y, v)→∀x∃y≤s(u, x, v)ϕ0(u+1,x,y,v)) and, by Lemma 7, there is m∈ωsuch that Ths(u, x, v)<h m(u+x+v+σ(s)). Recall that Thhu(x+z)=y1∧hu+z(x)=y2→y1≤y2and, thus, if σ0=m+σ(s)thenσ0∈Λ0and Th+∀x∃y(hσ0(x)=y)proves ∀u(∀x∃y≤g(x+u+v)ϕ0(u, x, y, v)→∀x∃y≤hτ0(u+x+v)ϕ0(u+1,x,y,v)) Using part (7) of Proposition 5, we can prove, by ΣF,g,h 0–induction, that Thhz(x)=y↔gr·z(x)=y As a consequence, Th+∀x∃y(hσ0(x)=y)proves ∀u(∀x∃y≤g(x+u+v)ϕ0(u, x, y, v)→∀x∃y≤gr·σ0(u+x+v)ϕ0(u+1,x,y,v)) Hence, putting τ0=r·σ0∈Λ0, the result follows concluding the proof of Claim. Let A|=T+IΣF 1and c∈Asuch that A|=ϕ(0,c). We shall show that A|=ϕ(t, c). Let ψ(x, y, c)∈ΣF 0the formula ∀z≤x∃w≤y(ϕ0(0,z,w,c)∧y=w+f(x)). Then A|=∀x∃yψ(x, y, c)andtheformulaψ(x, y, c)∧∀z<y¬ψ(x, z, c) defines a total nondecreasing function H:A→A. There is a ΣF 0formula, that we denote by Hz(x)=y, defining the iteration of Hand, since A|=IΣF 1,wehave A|=∀x∀z∃y(Hz(x)=y). Let θ(u, v) be the following ΠF 1formula: u>t∨∀x∀y1Hτu 0(x+u+v)=y1→∃y≤y1ϕ0(u, x, y, v). Since A|=∀x∃y(H(x)=y), by definition of θ(u, v)wehaveA|=θ(0,v). Let us show that A|=∀u(θ(u, v)→θ(u+1,v)). Pick a, b ∈Asuch that A|=a≤t∧θ(a, b). Then, the formula Hτa 0(x)=y defines a total nondecreasing function in Aand we can use it to get an expansion of Ato a model Agof Tgsuch that Ag|=∀x∃y≤g(x+a+b)ϕ0(a, x, y, b).By part (7) of Proposition 5, we can prove by ΣF,g 0–induction on zthat Ag|=∀z≤τ0[gz(x+a+b)=Hτa 0·z(x+a+b)] In particular, Ag|=∀x(gτ0(x+a+b)=Hτa 0·τ0(x+a+b)) and, as a consequence, Ag|=Tg+∀x∃y(gτ0(x)=y). Hence, by the Claim, we conclude that Ag|= ∀x∃y≤gτ0(x+a+b)ϕ0(a+1,x,y,b) and, therefore, A|=θ(a+1,b). We have shown that A|=θ(0,v)∧∀u(θ(u, v)→θ(u+1,v)), and we know that A|=IΠF 1(because IΣF 1≡IΠF 1), so, A|=∀uθ(u, b). In particular, since A|=θ(t, v)→∀x∃y≤Hτt 0(t+x+v)ϕ0(t, x, y, v), we conclude A|=ϕ(t, v). 3MainResult We are now ready to obtain the main results. Firstly, we need a version of Theorem 12 in the language of first–order Arithmetic. Lemma 13. 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+r 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)∈Π0 such that ¬∃xδ j(x) is equivalent to ∀x∃yθ j(x, y). Let mthe cardinal of Eand let F={f1,...,f m,f}a set of new unary function symbols. From the set of Σ0formulas Γ={θj(x, y): j∈E}, we define a theory Tas in Remark 2. Let L(A) denote the language obtained by adding to La constant symbol a,for each a∈A.PutT=T+DΠ1(A), where DΠ1(A)istheΠ1–diagram of A.Let Λ0be the set of closed terms of L(A) containing only constants of the form a for a∈K 2(A). Then Ahas a natural expansion AFto the language LF∪L(A) such that AF|=T+IΣF 1. By Proposition 12, AF|=T+(ΣF 2,Λ 0)–IR. Given δ(x)∈Σ− 2, we can 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 Textends DΠ1(A), we have that T¬∀x1∀x2(δ(x1)∧δ(x2)→x1=x2). So, T∀x1∀x2(δ(x1)∧δ(x2)→x1=x2)→∀x(δ(x)→ϕ(x)). In that way () holds again. We must deal with a last case: A|=∃!xδ(x). Then there exists d∈K 2(A) such that A|=δ(d)andd∈Λ0.Inorderto verify () it is enough to show that T+(ΣF 2,Λ 0)–IR ϕ(d). We prove, by induction on j, that for all j=1,...,r,T+(ΣF 2,Λ 0)–IR αj. Let j≤r, and assume that T+(ΣF 2,Λ 0)–IR 1≤i<j αi.Then (•)jT+(ΣF 2,Λ 0)–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 Tαj.IfA|=∃!xδ j(x), then there exists b∈K 2(A) such that A|=δj(b)andb∈Λ0.Using(•)jwe get T+(ΣF 2,Λ 0)–IR  ϕj(b). As a consequence, T+(ΣF 2,Λ 0)–IR ∃x(δ(x)∧ϕj(x)), and it follows that T+(ΣF 2,Λ 0)–IR αj, as required. We have proved that T+(ΣF 2,Λ 0)–IR r j=1 αj; hence T+(ΣF 2,Λ 0)–IR ϕ(0) ∧∀x(ϕ(x)→ϕ(x+1)) It follows that T+(ΣF 2,Λ 0)–IR ϕ(d) and, as a consequence, ()holds. Our last 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 14. IΠ− 2is Π3–conservative over IΣ1. Proof. Let θbe a Π3sentence provable in IΠ− 2.ThenI(Σ2,K2)θby Lemma 2 and IΣ− 1+(Σ2,K2)–IR θby Proposition 3. We need the following fact: