Fragments of Arithmetic and true sentences

FRAGMENTS OF ARITHMETIC AND TRUE SENTENCES A. Cord´on–Franco, A. Fern´andez–Margarit, and F.F. Lara–Mart´ın Dpto. Ciencias de la Computaci´on e Inteligencia Artificial Facultad de Matem´aticas. Universidad de Sevilla C/ Tarfia, s/n, 41012 Sevilla (Spain) {acordon,afmargarit,fflara}@us.es Abstract. By a theorem of R. Kaye, J. Paris and C. Dimitracopoulos, the class of the Πn+1–sentences true in the standard model is the only (up to deductive equivalence) consistent Πn+1–theory which extends the scheme of induction for parameter free Πn+1–formulas. Motivated by this result, we present a systematic study of extensions of bounded quantifier complexity of fragments of first–order Peano Arithmetic. Here, we improve that result and show that this property describes a general phenomenon valid for parameter free schemes. As a consequence, we obtain results on the quantifier complexity, (non)finite axiomatizability and relative strength of schemes for ∆n+1–formulas. 1. Introduction In this paper we shall deal with parameter free fragments of Arithmetic, that is, those subsystems of first–order Peano Arithmetic obtained by restricting some axiom scheme (induction, minimization and collection) to a class of formulas without parameters. A central paper on this topic is [15], where R. Kaye, J. Paris and C. Dimitracopoulos introduced parameter free fragments for Σnand Πnformulas and proved their basic properties. This work was further developed by Kaye [13], Z. Adamowicz and T. Bigorajska [1, 5], L. Beklemishev [3, 4], and others, pointing out tight relationships among parameter free schemes, classification of provably total recursive functions and subsystems of Arithmetic described in terms of inference rules or reflection principles. All these works provide evidence that the behaviour of parameter free fragments is very different from their parameter counterparts. The aim of this paper is to investigate one of those differences: the existence of extensions with small quantifier complexity. In [19] A. Wilkie proved that the scheme of induction for parameter free universal formulas I∀− 1does not have a universal axiomatization but does have a universal extension: Th∀1(N) (the theory of the ∀1–sentences true in the standard model of Arithmetic). To establish this result it is shown that Th∀1(N) is the only (up to deductive equivalence) consistent ∀1–theory which extends I∀− 1and Wilkie asked if the same was true for I∀− n+1 and Th∀n+1 (N) for n≥1. In his thesis [13] Kaye gave a positive answer to Wilkie’s Partially supported by the Andalusian Government, grant TIC–137. 1 question. By Kaye’s analysis of Matiyaseviˇc’s theorem on the diophantine representation of recursively enumerable predicates, it follows that, for n≥1, Matiyaseviˇc’s theorem is provable both in Th∀n+1 (N) and in I∀− n+1. So, for n≥1, Th∀n+1 (N) and ThΠn+1 (N) are deductively equivalent and I∀− n+1 is equivalent to the parameter free Πn+1–induction scheme IΠ− n+1. Then Wilkie’s question is answered by proving that ThΠn+1 (N) is the only (up to deductive equivalence) consistent Πn+1–theory which implies IΠ− n+1. The fragment IΠ− n+1 is Σn+2–axiomatized but not Πn+2. Therefore, for each n,IΠ− n+1 has consistent extensions of quantifier complexity less than Σn+2 (the one given by its natural formulation), but necessarily of big descriptive complexity (such extensions correspond to Π0 n+1–complete sets). Our purpose is to show that this result is not a particular property of IΠ− n+1, but actually a general phenomenon valid for parameter free schemes. More concretely, we deal with the following problem: Given a fragment of Arithmetic, T, •determine the least level Γ in the classical Σn/ΠnArithmetic Hierarchy such that there exists some consistent and Γ–axiomatized theory which extends T, •in the case that Thas consistent extensions of quantifier complexity less than that of its axiomatization, determine the descriptive complexity of such extensions. In order to describe in a simple way the results obtained in this work, we introduce the following measures for the complexity of extensions of T(where ThΠm(T) denotes the class of the Πm–sentences provable in T): (1) (Syntactical complexity) We say that Thas Γ–extensions if there is some consistent and Γ–axiomatized theory which implies T. (2) (Descriptive complexity) Let k, m ≥1. Assume that Thas Πk–extensions. (a) We say that Tis of type k→mif for each Πk–extension of T,T0, it holds that ThΠm(T0) = ThΠm(N). (b) We say that Tis of type kw −→ mif for each Πk–extension of T,T0, it holds that ThΠm(N) is recursive in ThΠm(T0). Notice that we can reformulate Kaye–Paris–Dimitracopoulos’ result on IΠ− n+1 by saying that this theory is of type n+ 1 →n+ 1. Our main motivation for a systematic analysis of properties of extensions of fragments of Arithmetic is to use these properties in order to obtain (usual) results on fragments of Arithmetic such as quantifier complexity, (non)finite axiomatizability or relative strength. For instance, let us observe that for a theory Tto be of type k→mis a strong way of saying Tis not finitely axiomatized. Moreover, the investigation of these properties of fragments of Arithmetic naturally leads to new conditions to solve some open problems in this area. In [10] some previous work in this direction was developed in connection with (the parameter free version of) Paris–Friedman’s problem on the equivalence between the schemes of induction and minimization for ∆n+1–formulas. The present paper can be considered to be an extension of [10]. We improve some results and give partial answers to some open problems there. Besides we simplify some proofs, especially 2 for results on ∆n+1–induction scheme, both for its parameter free version, I∆− n+1, and for its uniform version, UI∆n+1 (see section 2 for a detailed formulation of these fragments). Proofs given in [10] for determining the quantifier complexity and (non)finite axiomatizability of theories I∆− n+1,UI∆n+1 make use of the Arithmetized Completeness Theorem. On the other hand, as remarked by the anonymous referee, some results obtained in this paper can be also proved using reflection principles (see [3, 4, 16, 20]). Here we offer alternative proofs which employ a basic technique in the study of fragments of Arithmetic; namely, the construction of submodels using definable elements. To close this section we describe and briefly discuss the main results obtained in this paper. In section 3 we refine basic results on models constructed using definable elements. In section 4 we use those results to develop a systematic study of the syntactical and descriptive complexity of extensions of fragments. Diagrams in Theorem 1.1 summarize our main results on extensions of fragments (let us remark that Wndenotes the class of formulas {ϕ∨θ:ϕ∈Σn, θ ∈Πn}and ∪ndenotes the class Σn∪Πn). Theorem 1.1. •(Syntactical complexity): Theories IΣn+1,BΣn+1 I∆n+1 IΣ− n+1,BΣ− n+1 UI∆n+1 IΠ− n+1 L∆− n+1,I∆− n+1 Quantifier complexity Πn+3 Wn+2 Σn+2 Γ–extensions Πn+3 but not(1)Σn+3 Πn+2 but not(2)Σn+2 Πn+1 but not(1)Σn+1 (1) n= 0, for BΣ1,I∆1,L∆− 1and I∆− 1, extensions consistent with exp, (2) n= 0, for BΣ− 1and UI∆1, sound extensions. •(Descriptive complexity): Theories IΣ− n+1 BΣ− n+1 +exp IΠ− n+1 L∆− n+1 +exp I∆− n+1 +exp L∆− 1 I∆− 1 type n+ 2 →n+ 2 n+ 2 w −→ n+ 2 n+ 2 →n+ 1 1 w −→ 1 Previous theorem shows that parameter free fragments do have extensions of quantifier complexity less than that of their axiomatizations (but, necessarily, of big descriptive complexity), while fragments with parameters do not. This divergent behaviour between schemes with and without parameters can be explained from the study of fragments for ∆n+1(N)–formulas (that is, the class of the Σn+1–formulas equivalent in the standard model to some Πn+1–formula). For instance, induction for ∆n+1(N)–formulas, I∆n+1(N), and its parameter free version, I∆n+1(N)−, have extensions of less syntactical complexity but of big descriptive complexity. But fragments IΣ− n+1 and I∆n+1(N)−are equivalent, while IΣn+1 is strictly stronger than I∆n+1(N) (for more on ∆n+1(N)–schemes, see [7]). Notice that, for n≥1, all the results on the syntactical complexity of extensions are best possible. For n= 0, it remains to find out if the additional conditions 3 (1) and (2) can be omitted. As will be noticed in section 4 (see Corollary 4.5 and remarks following Questions 3 and 4), this question is related to an open problem raised by Wilkie and Paris [21] asking if every model of bounded induction which is not closed under exponentiation is a model of the Σ1–collection scheme. Results on descriptive complexity are also best possible for n≥1 (except for the collection scheme). Optimal results for n= 0 would also yield a solution to Wilkie–Paris’ Problem. Finally, in section 5, from the results in Theorem 1.1, we obtain the following properties on the schemes of induction and minimization for ∆n+1–formulas. Theorem 1.2. (1) I∆− n+1 and L∆− n+1 are Σn+2–axiomatized, but not Πn+2. (2) UI∆n+1 is Wn+2–axiomatized, but not ∪n+2. (3) I∆− n+1,L∆− n+1 and UI∆n+1 are not finitely axiomatized. (4) I∆n+1 is strictly stronger than UI∆n+1 and UI∆n+1 is strictly stronger than I∆− n+1. (5) There is no recursively enumerable set of true Πn+2–sentences which implies I∆− n+1. Some parts of Theorem 1.2 were previously established by Beklemishev [4] by means of proof–theoretical methods. Nevertheless, part 5 above answers problem 4 posed in [4]. Through this paper we also raise some questions which allow one to obtain stronger forms of some of the proved results and we point out relationships between these questions and other open problems in the field of Fragments of Arithmetic. 2. Preliminaries In this section we state some notation and results on fragments of Arithmetics that will be used through this paper (for general notation and references see [12, 14]). We work in the usual language of first order Arithmetic, L={0,1,+,·, <}. We denote by Nthe standard model for L, that is, the model with domain consisting of the set of natural numbers, ω, where the nonlogical symbols have the usual interpretation. For T,T0theories, we shall write: T=⇒T0, if Tis an extension of T0;T⇐⇒ T0, if Tand T0are deductively equivalent; and T|=⇒T0, if Tis a proper extension of T0. If N |=T, we say that Tis a sound theory. We denote by hx1, x2i=yCantor’s pairing function and by (y)0=xand (y)1=xits lateral inverse functions; that is, h(y)0,(y)1i=y. By xy=zwe denote a bounded formula which defines, in the standard model, the exponential function; and exp is the Π2 sentence ∀x∀y∃z(xy=z), see [12] for details. We recall the usual formulations of the fragments considered in this paper. The induction and minimization axioms for a formula ϕ(x,~v) of Lare, respectively, Iϕ(v)≡ϕ(0,~v)∧ ∀x[ϕ(x,~v)→ϕ(x+ 1,~v)] → ∀x ϕ(x,~v), Lϕ(v)≡ ∃x ϕ(x,~v)→ ∃x(ϕ(x,~v)∧ ∀y < x ¬ϕ(y,~v)). 4 The collection axiom for a formula ϕ(x, y,~v) of Lis Bϕ(z, v)≡ ∀x≤z∃y ϕ(x, y,~v)→ ∃u∀x≤z∃y≤u ϕ(x, y, ~v). Let Γ be a class of formulas of L. The fragments of induction, minimization and collection for Γ–formulas are, respectively, the following theories: IΓ = P−+{Iϕ: ϕ∈Γ},LΓ = P−+{Lϕ:ϕ∈Γ}and BΓ = I∆0+{Bϕ:ϕ∈Γ}; where P− denotes a finite set of Π1axioms for the nonnegative part of a commutative discretely ordered ring and ∆0is the class of the bounded formulas of L. Now we consider parameter free fragments. We shall write ϕ(x1, . . . , xn)∈Γ−if ϕ∈Γ and x1, . . . , xnare all variables which occur free in ϕ. Then IΓ−and LΓ−are defined as before but restricting the corresponding scheme to formulas ϕ(x)∈Γ−. We consider two versions of the parameter free collection scheme: BsΓ−is the fragment given by I∆0+{Bϕ:ϕ(x, y)∈Γ−}and BΓ−is I∆0together with the scheme ∀x∃y ϕ(x, y)→ ∀z∃u∀x≤z∃y≤u ϕ(x, y), for all ϕ(x, y)∈Γ−. Fragment BsΓ−was first considered in the proof of Proposition 1.7 in [15]. There it is proved that IΣ− n+1 |=⇒BsΣ− n+1 =⇒BΣ− n+1 and it is posed as an open problem if both formulations of the parameter free collection scheme are equivalent. Problem 1.BΣ− n+1 =⇒BsΣ− n+1? We need to consider this (apparently) strong formulation mainly due to the following result. Lemma 2.1. Let ϕ(x)∈Σ− n+1. Then ∀x≤z ϕ(x)∈Σ− n+1 in BsΣ− n+1. Fragments for ∆n+1–formulas are obtained as follows. The theory I∆n+1 is P− together with {∀x(ϕ(x, v)↔θ(x, v)) →Iϕ(v) : ϕ∈Σn+1, θ ∈Πn+1}. If parameters in formulas ϕ(x) and θ(x) are not allowed, then we obtain I∆− n+1. Moreover, Kaye [13] introduced an intermediate case: parameters are allowed but they are uniformly distributed. Namely, UI∆n+1 is P−together with {∀~v ∀x(ϕ(x,~v)↔θ(x,~v)) → ∀~v Iϕ(v) : ϕ∈Σn+1, θ ∈Πn+1}. Similarly, theories L∆n+1,L∆− n+1 and UL∆n+1 are defined. For the basic results on the considered fragments we refer the reader to [12, 13, 15]. Nevertheless, we emphasize some properties on ∆n+1–schemes. The relationships between ∆n+1–induction and ∆n+1–minimization schemes are not completely determined. In a preprint (about 1985) H. Friedman claimed L∆n+1 and I∆n+1 to be equivalent; but in [6] that equivalence appears as an open problem credited to J. Paris. 5 •(Paris–Friedman’s Conjecture)I∆n+1 ⇐⇒ L∆n+1. The usual argument for the equivalence of IΣn+1 and LΠn+1 allows one to show that the ∆n+1–minimization scheme implies the ∆n+1–induction scheme (for each one of the considered versions), but this argument does not work to prove the converse. Even so, recently T. Slaman [18] has obtained a partial answer to this problem. Theorem 2.2. (Slaman’s Theorem) I∆n+1 +exp ⇐⇒ BΣn+1 +exp. It is well known that L∆n+1 ⇐⇒ BΣn+1 (it holds that UL∆n+1 ⇐⇒ BΣ− n+1 as well) and, for n≥1, I∆n+1 =⇒IΣn=⇒exp; so, by Slaman’s Theorem, it follows that, for n≥1, I∆n+1 and L∆n+1 are indeed equivalent. However, the case n= 0 is still an open problem. Problem 2.I∆1=⇒L∆1? This seems to be a hard question since the proof of Slaman’s Theorem heavily depends on the use of the exponential function to handle a (suitable) coding of sequences. Besides it is related to the following open question raised by Wilkie and Paris [21]. Problem 3.I∆0+¬exp =⇒BΣ1? Problem 3 in turn is related to a central open question in the field of Fragments of Arithmetic, the End Extension Problem asking if every countable model of BΣ1has a proper end extension to a model of I∆0. In [21] it is shown that one of Problem 3 or the End Extension Problem must fail. We also have the following result. Corollary 2.3. Suppose that Problem 3 has an affirmative answer, that is, I∆0+ ¬exp =⇒BΣ1. Then: (1) I∆1⇐⇒ L∆1. (2) I∆0is finitely axiomatized if and only if BΣ1is finitely axiomatized. Proof. (1): By Slaman’s Theorem and the hypothesis, it follows that both I∆1+exp and I∆1+¬exp are extensions of L∆1. So, I∆1=⇒L∆1. (2): Assume that there is a sentence ϕaxiomatizing I∆0. Let θbe a sentence axiomatizing BΣ1+exp. Then, it holds that BΣ1⇐⇒ (ϕ∧ ¬exp)∨θ; so BΣ1is finitely axiomatized. The proof of the converse is similar. ¤ Slaman’s proof also depends on the presence of parameters in the ∆n+1–schemes; so, it does not provide a direct answer to uniform and parameter free versions of ParisFriedman’s Conjecture. Nonetheless, from Slaman’s Theorem and a theorem due to Beklemishev [4] stating that I∆1+exp is Σ3–conservative over UI∆1+exp, we can deduce a partial answer to the Uniform Conjecture for n= 0. In [4] the author claims to be routine to prove the analog of the previous conservativeness result for 6 schemes I∆n+1,UI∆n+1 for n≥1. In [9] we have obtained an independent modeltheoretic proof of that fact: for all n∈ω,I∆n+1 is a Σn+3–conservative extension of UI∆n+1. So, it holds Theorem 2.4. UI∆n+1 +exp ⇐⇒ UL∆n+1 +exp. Therefore, it only remains to answer parameter free Paris–Friedman’s Conjecture and its uniform version for n= 0: Problem 4. (1) I∆− n+1 =⇒L∆− n+1? (2) UI∆− 1=⇒UL∆− 1? Obviously, Theorem 2.4 reduces, for n≥1, the study of the fragment UI∆n+1 to BΣ− n+1. Nevertheless, in this paper we shall provide altenative proofs of some properties of UI∆n+1 that do not use Theorem 2.4, and also work for n= 0 without using exponential, see Lemma 3.4, Proposition 4.18 and Theorem 5.3. Finally, we recall some results on structures constructed using definable elements. Let Abe a model and p∈A. Then Kn(A, p) is the submodel of Awith domain {a∈ A:ais Σn–definable in (A, p)}and In(A, p) is the initial segment of Adetermined by Kn(A, p), that is, {b∈A: there is a∈ Kn(A, p) such that b≤a}. If parameter pis not used, we shall write Kn(A) and In(A), respectively. Proposition 2.5. ([15, 17]) Let A|=IΣnand p∈A. (1) Kn+1(A, p)≺n+1 Aand Kn+1(A, p)|=IΣn. Furthermore, if parameter pis not used, A|=IΣ− nsuffices. (2) Kn+1(A, p)≺n+1 In+1(A, p)≺nA. (3) If In+1(A, p)6=A, then In+1(A, p)|=BΣn+1. (4) If A|=BΣn+1, then In+1(A, p)|=ThΠn+2 (A). It is well known that submodels constructed using Σn+1–definable elements provide examples of models in which the Σn+1–induction or the Σn+1–collection scheme fails. Theorem 2.6. (Paris–Kirby, [17]) Let A|=IΣn+1 and p∈Anonstandard. Then Kn+1(A, p)6|=BΣn+1 and In+1(A, p)6|=IΣn+1. In [15] it is proved that if parameter pis not used, then Kn+1(A)|=BΣn+1 if and only if Kn+1(A)|=BΣ− n+1, and In+1(A)|=IΣn+1 if and only if In+1(A)|=IΠ− n+1; thus Theorem 2.6 is strengthened as follows. Theorem 2.7. ([15]) Let A|=IΣn+1 such that Kn+1(A)is nonstandard. Then Kn+1(A)6|=BΣ− n+1 and In+1(A)6|=IΠ− n+1. 7 Notice that previous theorem is no longer true when an arbitrary parameter pis allowed. To see this, let us consider A|=IΣn+1 +ThΠn+2 (N) and p∈Anonstandard. Then Kn+1(A, p) and In+1(A, p) are models of ThΠn+2 (N); and, consequently, both structures satisfy IΣ− n+1. 3. Σn+1–definable elements The main tool for the study of fragments of Arithmetic developed in this paper is the construction of submodels using definable elements. It will be important to establish the usual properties of these structures under sufficiently general conditions. Concretely, the aim of this section is to refine Theorems 2.6 and 2.7 in two ways: (a) weakening the main hypothesis on A,A|=IΣn+1; and (b) characterizing parameters p∈Asuch that Kn+1(A, p)6|=BΣ− n+1. To this end, following ideas in [10, 15], we consider classes of Πn+1–definable and Πn+1–minimal elements. (–) We say that a∈Ais Πk–definable in (A, p) if there exists ϕ(x, v)∈Πksuch that A|=ϕ(a, p)∧ ∀x(ϕ(x, p)→x=a). (–) We say that a∈Ais Πk–minimal in (A, p) if there exists ϕ(x, v)∈Πksuch that A|=ϕ(a, p)∧ ∀x < a ¬ϕ(x, p), that is, A|=a= (µx) (ϕ(x, p)). We shall denote by Dk(A, p) and Mk(A, p), respectively, the classes of Πk–definable and Πk–minimal elements in (A, p). If no parameters are used, we shall write Dk(A) and Mk(A). If A|=BΣk+1 then Dk(A, p) and Mk(A, p) are domains of substructures of A, but they are not, in general, models of very weak fragments of Arithmetic. In fact, if they are nonstandard, then they are not closed under Cantor’s lateral inverse functions; so, they are not models of Open induction. Our starting point is the study of the distribution of definable elements. We write A ⊆eBif Ais an initial segment of B, and A ⊆cBif Ais a cofinal subclass of B. Proposition 3.1. Let A|=IΣn+1 and p∈A. Then Kn+1(A, p)eDn+1(A, p)⊆cMn+1(A, p)⊆cKn+2(A, p). Furthermore, if parameter pis not used, A|=IΣ− n+1 suffices. Proof. (Kn+1(A, p)⊆eDn+1(A, p)): Let a∈ Kn+1(A, p) and ϕ(x, v)∈Σn+1 a formula defining ain (A, p). Then ∀z(ϕ(z, v)→x=z) is a Πn+1 formula that defines a in (A, p); so, a∈ Dn+1(A, p). Let b∈ Dn+1(A, p) such that b≤aand ψ(x, v)∈Πn+1 a formula defining bin (A, p). Let δ(x, v) be the formula ∃z(ϕ(z, v)∧ ∀y≤z(ψ(y, v)→y=x)). 8 Then δ(x, v)∈Σn+1 in BΣn+1 and, as b≤a,A|=δ(b, p)∧ ∀x(δ(x, p)→x=b). So, b∈ Kn+1(A, p). (Dn+1(A, p)⊆cMn+1(A, p)): The proof of this part essentially appears in the proof of Proposition 1.13 in [15]. Let a∈ Dn+1(A, p) and ϕ(x, v)∈Πn+1 a formula defining ain (A, p). Then A|=a= (µx)(ϕ(x, p)); so, a∈ Mn+1(A, p). Now let b∈ Mn+1(A, p) and ψ(x, y, v)∈Σnsuch that A|=b= (µx)(∀y ψ(x, y, p)). Since A|=BΣn+1, A|=∀y ψ(b, y, p)∧ ∃u∀x < b ∃y≤u¬ψ(x, y, p). So, as A|=LΠn(⇐⇒ IΣn), there exists c∈Asuch that A|=c= (µu)(∀x < b ∃y≤u¬ψ(x, y, p)); that is, cis the maximum of the function ¬ψ(x, y, p) when x < b. Let d=hb, ciand let θ(u, v) be the formula ∀y ψ((u)0, y, v)∧ ∀x < (u)0∃y≤(u)1¬ψ(x, y, v)∧ ∃x < (u)0∀y < (u)1ψ(x, y, v). Since θ(u, v)∈Πn+1 in BΣn+1 and A|=θ(d, p)∧ ∀u(θ(u, p)→u=d), d∈ Dn+1(A, p). Hence, as b= (d)0≤d, this proves that Dn+1(A, p) is cofinal in Mn+1(A, p). (Mn+1(A, p)⊆cKn+2(A, p)): Let a∈ Mn+1(A, p), ϕ(x, v)∈Πn+1 such that A|= a= (µx)(ϕ(x, p)) and θ(x, v)≡ϕ(x, v)∧ ∀z < x ¬ϕ(z, v). Then θ(x, v)∈Σn+2 in BΣn+1 and A|=θ(a, p)∧ ∀x(θ(x, p)→x=a). So, a∈ Kn+2(A, p). Now let a∈ Kn+2(A, p) and ϕ(x, y, v)∈Πn+1 such that ∃y ϕ(x, y, v) defines ain (A, p). So, A|=∃u ϕ((u)0,(u)1, p). Since A|=LΠn+1, there exists b∈Asuch that A|=b= (µu)(ϕ((u)0,(u)1, p)). So, b∈ Mn+1(A, p). Since a= (b)0< b,Mn+1(A, p) is cofinal in Kn+2(A, p). ¤ Nota 3.2. (1) Notice that the hypothesis A|=IΣn+1 is only needed to establish that Mn+1(A, p) is cofinal in Kn+2(A, p). For the rest of the proof of Proposition 3.1, A|=BΣn+1 (or, A|=BsΣ− n+1 if parameter pis not used) suffices. (2) The proof of the last inclusion in the previous proposition also shows that if A|=I∆0and p∈A, then M0(A, p) is cofinal in K1(A, p). (3) It is well known that Σn+1–definable elements are not cofinal in nonstandard models of IΣn+1. Hence, by Proposition 3.1, it follows that in every model of IΣ− n+1 containing nonstandard Σn+2–definable elements there exists a Πn+1– definable element which is not Σn+1–definable. Even more; it is easy to check that for every model of IΣn+1 containing nonstandard Σn+1–definable elements all the inclusions in Proposition 3.1 are proper. 9 If m1< m2, then I∆0`(x+ 2)m1<(x+ 2)m2; so, by compactness, there exists A|=T0. Let dbe a new constant and T1=ED(A) + {a < d:a∈A}(where ED(A) is the elementary diagram of A). By compactness, there exists B|=T1. Then Bis a proper elementary extension of A. Let Cbe the substructure of Bwith domain {b∈B: there exists m∈ωsuch that B|=b < (c+ 2)m}. Since Cis an initial segment in Bclosed under function (x+ 2)2=y, then it follows that Bis a proper Σ0–elementary end extension of C. Hence, C|=T+BΣ1. So, C|=∀x∃y ϕ(x, y). Let b∈Csuch that C|=ϕ(c, b). Since ϕ(x, y)∈Σ1,B|=ϕ(c, b). Let m∈ωsuch that b≤(c+ 2)m. Since A≺B,A|=∃y≤(c+ 2)mϕ(c, y). Contradiction, since A|=T0. (2): Since Tis a Σ2–axiomatized theory, there exists θ(u)∈Π− 1such that T` ∃u θ(u) and BΣ1+∃u θ(u)` ∀x∃y ϕ(x, y). Assume that for every m∈ω,T+I∆06` ∃z∀x[z < x → ∃y≤(x+ 2)mϕ(x, y)]. Let c,dbe new constants and T0=I∆0+θ(d) + d<c+{∀y≤(c+ 2)m¬ϕ(c, y) : m∈ω}. By compactness, there is A|=T0. Let Band Cas in the proof of part (1). Since C|=∃u θ(u), reasoning as before we get the desired contradiction. ¤ Theorem 4.8. (1) I∆0+exp and IΣ− 1do not have Σ2–extensions. (2) BsΣ− 1,BΣ− 1and UI∆1do not have Π1–extensions; so, they do not have sound Σ2–extensions. Proof. (1): Assume that I∆0+exp has a Σ2–extension, Tsay. Then, by Proposition 4.7, there exists m∈ωsuch that T` ∃z∀x > z (2x≤(x+ 2)m). Which gives the desired contradiction. (2): Since every Π1–extension of P−is a sound theory, it is enough to show that ThΠ1(N) does not imply UI∆1. By Lemma 4.2, there exists A|=IΣ1+ThΠ1(N) such that A6|=ThΠ2(N). So, by Corollary 3.3, there exists p∈ M1(A) nonstandard. Since K1(A, p)≺1A,K1(A, p)|=ThΠ1(N) + exp. Towards a contradiction, assume that K1(A, p)|=UI∆1. By the Claim in the proof of Theorem 3.5–(3), K2(K1(A, p)) = K1(A, p), so by Lemma 3.4–(2.b), K1(A, p)|=I∆1+exp. By Theorem 2.2, K1(A, p)|=BΣ1+exp, which contradicts Theorem 3.5. ¤ Notice that part (1) of the above theorem follows from a result of Wilkie and Paris stating that I∆0+exp proves uniform Π2–reflection principle for I∆0with respect to tableau provability (see [20]). Part (2) is essentially proved by Beklemishev in [4] (see the proof of corollary 4 there). Nota 4.9.In [11] it is shown that, for each n≥1, there is a Πn–formula, y=Kn(x), which satisfies the corresponding hierarchical versions of those properties of the formula y= (x+ 2)2necessary for the proof of Proposition 4.7, namely: (a) IΣn` ∀x∃!y(y=Kn(x)); and 16 (b) initial segments of B|=IΣnclosed under function y=Kn(x) are Σn– elementary substructures of B. Moreover, in [8] for each n≥1 it is presented a Πn–formula, y=Kz n(x), which expresses the iteration of the function y=Kn(x) and it is established that (see section 3 in [8] for details): (c) IΣn`z1< z2→Kz1 n(x)<Kz2 n(x); and IΣn` ∀x∃!y(y=Km n(x)), for all m∈ω. Therefore, by repeating the arguments in the proof of Proposition 4.7, we obtain the following generalization of that result. Let us denote by y=K0(x) the ∆0–formula y= (x+ 2)2. Proposition Let Tbe a theory and ϕ(x, y)∈Σn+1 such that T+BΣn+1 ` ∀x∃y ϕ(x, y). 1. If Tis Πn+1–axiomatized, there is m∈ωsuch that T+IΣn` ∀x∃y≤Km n(x)ϕ(x, y). 2. If Tis Σn+2–axiomatized, there is m∈ωsuch that T+IΣn` ∃z∀x[z < x → ∃y≤Km n(x)ϕ(x, y)]. In [8] it is also proved that IΣ− n+1 ` ∀x∃y(y=Kx+1 n(x+2)). Hence, an argument similar to that of part (1) of Theorem 4.8 shows that there is no class of Σn+2– sentences, Γ, such that BΣn+1 + Γ is a consistent extension of IΣ− n+1. This fact can be also obtained from the results of [3]. There it is shown (see theorem 1) that IΣ− n+1 proves uniform Πn+2–reflection principle for IΣn. Since BΣn+1 is a Πn+2–conservative extension of IΣn,IΣ− n+1 also proves Πn+2–reflection principle for BΣn+1 and, as a consequence, there is no class of Σn+2–sentences, Γ, such that BΣn+1 + Γ is a consistent extension of IΣ− n+1. (C) Extensions of IΠ− n+1, L∆− n+1 and I∆− n+1 All these theories are Σn+2–axiomatized; so, as they are sound, we have ThΠn+1 (N) =⇒IΠ− n+1 =⇒L∆− n+1 =⇒I∆− n+1. Let us now consider the existence of Σn+1–extensions. Theorem 4.10. (1) IΠ− n+1,L∆− n+1 and I∆− n+1 have Πn+1–extensions, and, for n≥1, they do not have Σn+1–extensions. (2) IΠ− 1does not have Σ1–extensions. (3) I∆− 1and L∆− 1do not have Σ1–extensions consistent with exp. Proof. (1): The results follow from Theorem 4.6 for n > 1 and from Theorem 4.8 for n= 1, since all these fragments imply IΣ− n. (2): Assume that there exists a Σ1–extension of IΠ− 1,Tsay. By Lemma 4.2, there exists A|=Tsuch that A6|=ThΠ1(N) and, therefore, K1(A) is nonstandard. Since 17 K1(A)≺1Aand Tis a Σ1–axiomatized theory, K1(A)|=T; so, K1(A)|=IΠ− 1. Then, from the fact that all elements of K1(A) are Σ1–definable, we deduce that K1(A)|=IΠ1(⇐⇒ IΣ1). In particular, K1(A)|=BΣ1+exp. Which contradicts Theorem 3.5. (3): Assume that there is a Σ1–extension of I∆− 1consistent with exp,Tsay. By Lemma 4.2, there exists A|=T+exp such that A6|=ThΠ1(N); so, K1(A) is nonstandard. Since Tis Σ1–axiomatized and K1(A)≺1A,K1(A)|=T+exp; so, K1(A)|=I∆− 1+exp. Which contradicts Theorem 3.5. ¤ 4.2. Descriptive complexity. (A) Πn+2–extensions of IΠ− n+1, L∆− n+1 and I∆− n+1 As we have noticed before, in [15] Kaye–Paris–Dimitracopoulos proved that for any Πn+1–extension of IΠ− n+1,T, it holds that T⇐⇒ ThΠn+1 (N). Here we extend that result to any Πn+2–extension. We also answer (partially) Problem 5.5 in [10]. Lemma 4.11. Let Tbe a Πn+2–extension of I∆− n+1 such that for every A|=T, Kn+1(A)|=exp. Then ThΠn+1 (T) = ThΠn+1 (N). Proof. Assume that ThΠn+1 (T)6=ThΠn+1 (N). By Lemma 4.1, Tdoes not extend ThΠn+1 (N); so, there is A|=Tsuch that A6|=ThΠn+1 (N) and, therefore, Kn+1(A) is nonstandard. Since Tis Πn+2–axiomatized and Kn+1(A)≺n+1 A,Kn+1(A)|=T. Hence, Kn+1(A)|=I∆− n+1 +exp. Which contradicts Theorem 3.5. ¤ Theorem 4.12. (1) L∆− n+1 +exp and I∆− n+1 +exp are of type n+ 2 →n+ 1. (2) IΠ− n+1 is of type n+ 2 →n+ 1. Proof. (1): Immediate from Lemma 4.11. (2): Let Tbe a Πn+2–extension of IΠ− n+1 and A|=T. Then Kn+1(A)|=T; so, Kn+1(A)|=IΠ− n+1. Since all elements of Kn+1(A) are Σn+1–definable, Kn+1(A)|= IΠn+1; so, Kn+1(A)|=exp. Hence, the result follows from Lemma 4.11. ¤ The above result is best possible for IΠ− n+1 and, when n≥1, also for L∆− n+1 and I∆− n+1. However, it remains to eliminate the exponential function in the case n= 0. Question 3.Are L∆− 1and I∆− 1of type 2 →1, or 1 →1? Notice that this question is related to Problem 3. In fact, if Problem 3 has an affirmative answer, then, by Corollary 4.5, L∆− 1has recursively axiomatized ∪1– extensions; so, neither L∆− 1nor I∆− 1is of type 2 →1. Nevertheless, we prove a weak version of previous question. Proposition 4.13. L∆− 1and I∆− 1are of type 1w −→ 1. 18 Proof. Let Tbe a Π1–extension of I∆− 1. Then Tis sound; so, T+exp is a consistent Π2–extension of I∆− 1+exp. By Theorem 4.12, ThΠ1(T+exp) = ThΠ1(N). This gives that ThΠ1(N) is recursively enumerable in ThΠ1(T+exp); so, also in ThΠ1(T). Hence, by Lemma 4.1, ThΠ1(N) is recursive in ThΠ1(T). So, I∆− 1(and, consequently, also L∆− 1) is of type 1 w −→ 1, as required. ¤ (B) Πn+2–extensions of IΣ− n+1, BsΣ− n+1, BΣ− n+1 and UI∆n+1 Since ThΠn+2 (N) =⇒IΣ− n+1 =⇒BsΣ− n+1 +exp =⇒BΣ− n+1 +exp =⇒UI∆n+1 + exp =⇒I∆− n+1 +exp, then, by Theorem 4.12, we have the following result. Proposition 4.14. IΣ− n+1,BsΣ− n+1 +exp,BΣ− n+1 +exp and UI∆n+1 +exp are of type n+ 2 →n+ 1. Now we shall improve this result: we shall see that IΣ− n+1 is of type n+ 2 →n+ 2 and a weaker version for BΣ− n+1 +exp and UI∆n+1 +exp, namely, these theories are of type n+ 2 w −→ n+ 2. Lemma 4.15. Let Tbe Πn+2–axiomatized and ϕaΣn+2–sentence such that IΣ− n+1+ T+ϕis consistent. (1) If T+ϕ=⇒BΣ− n+1, then IΣ− n+1 +T+ϕ⇐⇒ ThΠn+2 (N). (2) If IΣn+IΠ− n+1 +T+ϕ=⇒BΣ− n+1, then IΣ− n+1 +T+ϕ⇐⇒ ThΠn+2 (N). Proof. Even though it is enough to prove part 2, we shall prove both parts. Let θ(x) be a Π− n+1 formula such that ϕ≡ ∃x θ(x). (=⇒): Assume that there is A|=IΣ− n+1 +T+ϕsuch that A6|=ThΠn+2 (N). Since A|=LΠ− n+1(⇐⇒ IΣ− n+1), there exists a∈ Mn+1(A) such that A|=a= (µx)(θ(x)). (1): By Corollary 3.3, there exists b∈ Mn+1(A) nonstandard. Take p=ha, bi. Since Kn+1(A, p)|=T+ϕ, by hypothesis, Kn+1(A, p)|=BΣ− n+1. Which contradicts Theorem 3.5 since p∈ Mn+1(A). (2): By Corollary 3.7, there exists b∈ Dn+1(A) nonstandard such that Kn+1(A, a, b)|= IΠ− n+1. Let p=ha, bi. Then Kn+1(A, p)|=IΣn+IΠ− n+1 +T+ϕ; so, by hypothesis, Kn+1(A, p)|=BΣ− n+1. Which contradicts Theorem 3.5 since p∈ Mn+1(A). (⇐=): It is enough to prove that T+ϕis a sound theory. Let Abe a model of IΣ− n+1 +T+ϕ. By part =⇒, it holds that A|=ThΠn+2 (N); hence, N ≺n+2 A. So, N |=T+ϕ.¤ Theorem 4.16. (1) IΣ− n+1 is of type n+ 2 →n+ 2. (2) BΣ− n+1+exp (and, consequently, also BsΣ− n+1+exp) is of type n+2 w −→ n+2. Proof. (1): Immediate from Lemma 4.15. (2): Let Tbe a Πn+2–extension of BΣ− n+1 +exp. Then T=⇒L∆− n+1 +exp. By Theorem 4.12, ThΠn+1 (T) = ThΠn+1 (N) and N |=T; so, IΣ− n+1 +Tis consistent. 19 By Lemma 4.15, ThΠn+2 (IΣ− n+1 +T) = ThΠn+2 (N). Then ThΠn+2 (N) is recursively enumerable in ThΠn+2 (T). Hence, by Lemma 4.1, ThΠn+2 (N) is recursive in ThΠn+2 (T). ¤ Our result on descriptive complexity of extensions of IΣ− n+1 is best possible; however, the following questions are left unanswered for the collection scheme. Question 4. (1) Is BΣ− n+1 +exp of type n+ 2 →n+ 2? (2) Is BΣ− 1of type 2 →2, or 2 w −→ 2, or 2 →1, or 2 w −→ 1? Part (2) is connected with Problem 3. Note that by Corollary 4.5, if Problem 3 has an affirmative answer, then BΣ− 1has recursively axiomatized ∪1-extensions; so, it is not of type 2 w −→ 1. We shall see now that part (1) is related to the existence of nonstandard Πn+1–definable elements in models of BΣn+1. Proposition 4.17. If Question 1 has an affirmative answer, then BΣ− n+1 +exp is of type n+ 2 →n+ 2. Proof. Let Tbe a Πn+2–extension of BΣ− n+1+exp. Let us see that T=⇒ThΠn+2 (N). Since BΣn+1 is a Σn+3–conservative extension of BΣ− n+1 (see Theorem 2.4 in [15]), it suffices to prove that T+BΣn+1 =⇒ThΠn+2 (N). Assume that there exists A|=T+BΣn+1 such that A6|=ThΠn+2 (N). By the hypothesis, there is p∈ Dn+1(A) nonstandard. Since Tis Πn+2–axiomatized, Kn+1(A, p)|=T; so, Kn+1(A, p)|=BΣ− n+1 +exp. Which contradicts Theorem 3.5. ¤ For the uniform ∆n+1–induction scheme, we have obtained that UI∆n+1 +exp is of type n+ 2 →n+ 1 from the fact that this fragment is an extension of I∆− n+1 +exp. Since UI∆n+1 +exp and BΣ− n+1 +exp are equivalent (see Theorem 2.4), it is immediate that UI∆n+1 +exp is of type n+ 2 w −→ n+ 2. However, by Lemma 3.4–(2.b), we can apply the same reasoning as in Lemma 4.15 and Theorem 4.16 to show, independently of the equivalence between UI∆n+1 +exp and BΣ− n+1 +exp, that Proposition 4.18. UI∆n+1 +exp is of type n+ 2 w −→ n+ 2. 5. On ∆n+1–schemes In this section, we make use of results in the previous section in order to determine quantifier complexity, (non)finite axiomatizability and relative strength of the fragments studied in this work. We focus on fragments for ∆n+1–formulas and the scheme BsΣ− n+1 since the properties of these theories are not well known. First we state general conditions for a theory Tto establish its axiomatization properties. 20 Lemma 5.1. If ThΠn+2 (N) =⇒T=⇒I∆− n+1, then Tis not finitely axiomatized. Proof. Assume Tis finitely axiomatized. Then there exists ϕ∈ThΠn+2 (N) such that ϕ=⇒Tand hence ϕ+exp =⇒I∆− n+1 +exp. Since I∆− n+1 +exp is of type n+ 2→n+1 (Theorem 4.12), it holds that ϕ+exp =⇒ThΠn+1 (N). Contradiction. ¤ Lemma 5.2. Let Tbe a theory consistent with exp. (1) If Tis Σn+1–definable and extends I∆− n+1, then Tis not Πn+2–axiomatized. (2) If Tis a sound Σn+2–definable extension of UI∆n+1, then Tis not ∪n+2– axiomatized. Proof. (1): Assume Tis Πn+2–axiomatized. Then T+exp is a Πn+2–extension of I∆− n+1 +exp and hence, by Theorem 4.12, it follows that T+exp =⇒ThΠn+1 (N). Which is impossible since Tis Σn+1–definable. (2): Assume that T⇐⇒ T1+T2where T1is Σn+2–axiomatized and T2is Πn+2– axiomatized. Since T1is sound, ThΠn+1 (N) =⇒T1. Let T3=T+IΣn+1 + ThΠn+1 (N). Since T3is consistent and Σn+2–definable, T3×=⇒ThΠn+2 (N); so, there exists A|=T3such that A6|=ThΠn+2 (N). By Corollary 3.3, there exists p∈ Mn+1(A) nonstandard. Then Kn+1(A, p)|=ThΠn+1 (N) + T2and; hence, Kn+1(A, p)|=UI∆n+1 +exp. By the Claim in the proof of Theorem 3.5–(3), Kn+2(Kn+1(A, p)) = Kn+1(A, p), so by Lemma 3.4–(2.b), Kn+1(A, p)|=I∆n+1. By Theorem 2.2, Kn+1(A, p)|=BΣn+1 +exp. Which contradicts Theorem 3.5. ¤ Now we apply both lemmas to obtain the basic information on the quantifier complexity of the considered ∆n+1–schemes and fragment BsΣ− n+1. First, let us observe that all these fragments are recursively axiomatized and, consequently, Σ1– definable. Theorem 5.3. (1) L∆− n+1,I∆− n+1,UI∆n+1 and BsΣ− n+1 are not finitely axiomatized. (2) L∆− n+1 and I∆− n+1 are not Πn+2–axiomatized. (3) BsΣ− n+1 and UI∆n+1 are not ∪n+2–axiomatized. Finally, from the obtained results, we can deduce the following properties on the relative strength of the considered fragments. Theorem 5.4. (1) I∆n+1 |=⇒UI∆n+1 |=⇒I∆− n+1 |=⇒IΣn. (2) L∆− n+1 does not imply UI∆n+1, and UL∆n+1 does not imply I∆n+1. (3) (Answer to problem 4 in [4]) There is no recursively enumerable set of true Πn+2–sentences which extends I∆− n+1. In particular, I∆0+exp does not extend I∆− 1. 21 Proof. By Theorem 5.3–(2) and the fact that IΣnis Πn+2–axiomatized, it follows that IΣndoes not imply I∆− n+1. By Lemma 5.2–(3) and the fact that I∆− n+1 and L∆− n+1 are Σn+2–axiomatized, it follows that neither I∆− n+1 nor L∆− n+1 implies UI∆n+1. By Theorem 4.4, it follows that I∆n+1 +exp does not have Σn+3– extensions; so, neither UI∆n+1 nor UL∆n+1 implies I∆n+1 since UI∆n+1 and UL∆n+1 are Wn+2–axiomatized. Finally, observe that part (3) follows by the fact that I∆− n+1 +exp is of type n+ 2 →n+ 1. ¤ Concerning to the scheme BsΣ− n+1 the following question on its quantifier complexity remains unanswered. Question 5.Is BsΣ− n+1 aWn+2–axiomatized theory? Using the same reasoning as for its parameter counterpart, it is easy to check that BsΣ− n+1 is a Πn+3–axiomatized theory. However, we do not even know if it is a Σn+3–axiomatized theory. In fact, we have the following result. Proposition 5.5. The following conditions are equivalent. (1) BΣ− n+1 ⇐⇒ BsΣ− n+1. (2) BsΣ− n+1 is Wn+2–axiomatized. (3) BsΣ− n+1 is Σn+3–axiomatized. Proof. Since BΣ− n+1 is Wn+2–axiomatized, (1) =⇒(2) is immediate. The implication (2) =⇒(3) is trivial and (3) =⇒(1) follows from the fact that BΣn+1 is Σn+3– conservative over BΣ− n+1.¤ References [1] Adamovicz, Z.; Bigorajska, T. Functions provably total in I−Σ1. Fundamenta Mathematicae, 132:189–194, 1989. [2] Beklemishev, L.D. Induction rules, reflection principles and provably recursive functions. Annals of Pure and Applied Logic, 85(3):193–242, 1997. [3] Beklemishev, L.D. Parameter free induction and provably total computable functions. Theoretical Computer Science, 224(1–2):13–33, 1999. [4] Beklemishev, L.D. On the induction schema for decidable predicates. The Journal of Symbolic Logic, 68(1):17–34, 2003. [5] Bigorajska, T. On Σ1–definable functions provably total in IΠ− 1. Mathematical Logic Quartely, 41:135–137, 1995. [6] Clote, P; Kraj´ıˇcek, J. Open Problems. In Arithmetic, Proof Theory and Computational Complexity, 1–19. Oxford Logic Guides, 23. Oxford University Press, Oxford, 1993. [7] Cord´on Franco, A. Extensiones de Fragmentos de la Aritm´etica. Ph.D. Thesis. Universidad de Sevilla, 2003. [8] Cord´on Franco, A; Fern´andez Margarit, A.; Lara Mart´ın, F.F. On the quantifier complexity of ∆n+1(T)–induction. Archive for Mathematical Logic, 43(3):371–398, 2004. [9] Cord´on Franco, A; Fern´andez Margarit, A.; Lara Mart´ın, F.F. Fragments of Arithmetic on ∆n+1–formulas. Preprint, Sevilla, December 2004. 22 [10] Fern´andez Margarit, A.; Lara Mart´ın, F.F. Some Results on L∆− n+1. Mathematical Logic Quarterly, 47(4):503–512, 2001. [11] Fern´andez Margarit, A.; Lara Mart´ın, F.F. Induction, Minimization and Collection for ∆n+1(T)–formulas. Archive for Mathematical Logic, 43(4):505–541, 2004. [12] H´ajek, P.; Pudl´ak, P. Metamathematics of First–Order Arithmetic. Perspectives in Mathematical Logic, Springer Verlag, 1993. [13] Kaye, R. Diophantine and Parameter–free Induction. Ph.D. Thesis. University of Manchester, 1987. [14] Kaye, R. Models of Peano Arithmetic. Oxford Logic Guides, 15. Clarendon Press. Oxford, 1991. [15] Kaye, R.; Paris, J; Dimitracopoulos, C. On parameter free induction schemas. The Journal of Symbolic Logic, 53(4):1082–1097, 1988. [16] Leivant, D. The optimality of induction as an axiomatization of arithmetic. The Journal of Symbolic Logic. 48(1):182–184, 1983. [17] Paris, J.; Kirby, L. Σn–collection schemas in arithmetic. Logic Colloquium’77, 199–209. North Holland, 1978. [18] Slaman, T. Σn–Bounding and ∆n–induction. Proceedings of the American Mathematical Society, 132(8):2449–2456, 2004. [19] Wilkie, A. Some Results and Problems on Weak Systems of Arithmetic. Logic Colloquium’77, 285–296. North Holland, 1978. [20] Wilkie, A; Paris, J. On the scheme of induction for bounded arithmetic formulas. Annals of Pure and Applied Logic, 35(3):261–302, 1987. [21] Wilkie, A; Paris, J. On the existence of end extensions of models of bounded induction. Logic, Methodology and Philosophy of Science VIII, 143–161. North–Holland, Amsterdam 1989. 23