On axiom schemes for T-provably Δ1 formulas
Abstract
This paper investigates the status of the fragments of Peano Arithmetic obtained by restricting induction, collection and least number axiom schemes to formulas which are Δ1 provably in an arithmetic theory T. In particular, we determine the provably total computable functions of this kind of theories. As an application, we obtain a reduction of the problem whether IΔ0+¬exp implies BΣ1 to a purely recursion-theoretic question.
Full text
On axiom schemes for T-provably Δ1 formulas A. Cordón-Franco · A. Fernández-Margarit · F. F. Lara-Martín Abstract This paper investigates the status of the fragments of Peano Arithmetic obtained by restricting induction, collection and least number axiom schemes to formulas which are Δ1 provably in an arithmetic theory T . In particular, we determine the provably total computable functions of this kind of theories. As an application, we obtain a reduction of the problem whether I Δ0 +¬exp implies BΣ1 to a purely recursion-theoretic question. Keywords Fragments of Peano Arithmetic · Δ1 formulas · Provably total computable functions Mathematics Subject Classification 03F30 · 03D20 1 Introduction Among the subsystems of first order Peano Arithmetic (PA), fragments for Δ1-formulas are not completely understood yet. A well-known problem posed by Paris [6] asks whether, over the theory of bounded induction I Δ0, the induction principle for Δn-formulas I Δn and the collection principle for Σn-formulas BΣn are equivalent. By a result of R. Gandy (unpublished, see [12]), BΣn is equivalent to the least number principle for Δn-formulas LΔn. Hence, Paris’ question can be reformulated as asking whether I Δn and LΔn are equivalent. In 2004 Slaman [21] obtained a partial answer
to the problem. He proved IΔnand BΣnto be equivalent over IΔ0+exp, where exp is the axiom asserting the totality of the exponential function. Since IΔ2proves exp, this answered the problem completely for each n≥2. As to the case n=1, building on Slaman’s work Thapen [23] showed that BΣ1is provable from IΔ1plus a very weak form of exponentiation: “for all x,xyexists for some ysuch that x<p(y)”, where pcan be any primitive recursive function. (An alternative proof of this result was given in [20]). However, the problem of proving or disproving the equivalence over IΔ0for n=1 is still pending. Motivated by this question, we initiated in [11] and [7] the study of fragments of PA for formulas that are Δ1provably in an external theory T. More precisely, let Tbe an extension of IΔ0in the language of arithmetic. The theory IΔ1(T)is axiomatized over Robinson’s Qby the axiom scheme (Iϕ)ϕ(0,v)∧∀x(ϕ(x,v)→ϕ(x+1,v)) →∀xϕ(x,v), where ϕ(x,v)∈Δ1(T), i.e., ϕ(x,v)∈Σ1and there is some ψ(x,v)∈Π1such that T∀x,v(ϕ(x,v)↔ψ(x,v)). The theory LΔ1(T)is Qtogether with (Lϕ)∃xϕ(x,v)→∃x(ϕ(x,v)∧∀y<x¬ϕ(y,v)), where ϕ(x,v)∈Δ1(T). The theory BΔ1(T)consists of IΔ0plus (Bϕ)∀x∃yϕ(x,y,v)→∀z∃u∀x≤z∃y≤uϕ(x,y,v), where ϕ(x,y,v)∈Σ1and T∀x∃yϕ(x,y,v)(so ∃yϕ(x,y,v)∈Δ1(T)). A variant of Paris’ problem then arises: For which theories T does the equivalence IΔ1(T)≡LΔ1(T)hold? Besides this original motivation, Δ1(T)-schemes have turned out to be interesting subsystems of PA in their own right. On the one hand, Δ1(T)formulas appear naturally in the study of fragments of PA, remarkably in connection with the computable functions provably total in T. In fact, as we shall show in this paper, Δ1(T)-schemes exhibit a nice computational behavior: it is possible to give neat characterizations of their provably total functions by means of some subrecursive operators. On the other hand, Δ1(T)-schemes are closely related to theories of arithmetic described in terms of inference rules. In fact, T+IΔ1(T)coincides with the closure of Tunder unnested applications of the Δ1-induction rule [T,Δ 1-IR]. Even more, IΔ1(T)precisely isolates the amount of induction axioms added to Tby unnested applications of Δ1-IR. Similar remarks apply to LΔ1(T)and BΔ1(T)considering the Δ1-minimization rule Δ1-LR and the Σ1-collection rule Σ1-CR, respectively. In this work we go a step further and show that, as a matter of fact, Δ1(T)-schemes can be fully characterized as the intersection between a “classic” scheme for Σ1-formulas and an inference rule theory. More precisely, let ThΓ(T)denote the set of all Γ-consequences of a theory T. Then, for each sentence ϕwe have IΔ1(T)ϕif, and only if, both IΣ1ϕand [ThΠ2(T), Δ1-IR]ϕ; LΔ1(T)ϕif, and only if, both IΣ1ϕand [ThΠ2(T), Δ1-LR]ϕ;
BΔ1(T)ϕif, and only if, both BΣ1ϕand [ThΠ2(T), Σ1-CR]ϕ. Thus, the study of Δ1(T)-schemes can be reduced to investigating how the properties of two theories are transferred to the theory given by the intersection of their theorems. Using this methodology we shall obtain a complete description of the prooftheoretic and computational properties of Δ1(T)-schemes. Notably: •We show that Slaman’s theorem transfers to the present context and prove that IΔ1(T)and LΔ1(T)are equivalent for every Textending IΔ0+exp. •In studying parameter free Δ1(T)-schemes we introduce parameter free Δ1-rules Δ− 1-IR and Δ− 1-LR (to our best knowledge, considered here for the first time) and obtain a conservation result, which is of independent interest. Namely, if T⊆Π2 then [T,Δ 1-IR]and [T,Δ 1-LR]are conservative over their parameter free counterparts with respect to Σ2-sentences. •We determine the provably total computable functions (p.t.c.f.) of IΔ1(T)and of LΔ1(T)for an arbitrary Textending IΔ0. We show that the p.t.c.f.’s of LΔ1(T) are, precisely, the closure under composition and the bounded minimization operator of the p.t.c.f.’s of Twhich are primitive recursive. For IΔ1(T)we obtain a similar result in terms of the search operator introduced in [5]. In addition, in presence of exp we give alternative and particularly neat characterizations by means of a suitably modified version of the bounded recursion operator, that we call C-bounded recursion. •We obtain a reduction of the well-known problem whether IΔ0+¬exp implies BΣ1(for short, the NE Problem) raised by Wilkie and Paris [24] to a purely recursion-theoretic question. Namely, BΣ1is not provable from IΔ0+¬exp if there is some elementary function fwith a Δ0-definable graph such that the function x→ maxi∈[0,x]f(i)cannot be obtained by composition from fand rudimentary functions. The outline of the paper is as follows. Sections 1and 2are introductory. Section 3 contains the proof of the characterization theorem for Δ1(T)-schemes and several applications. (In particular, we solve a number of questions left over from [11] and [7]). In Sect. 4we investigate parameter free Δ1(T)-schemes and parameter free Δ1inference rules. Finally, Sect. 5is devoted to determining the p.t.c.f.’s of IΔ1(T)and of LΔ1(T)and contains the above-mentioned reduction for the NE Problem. 2 Preliminaries We assume familiarity with basic notions and results concerning fragments of Peano Arithmetic (all relevant information can be found in [12]). We work in the usual first-order language of arithmetic L={0,1,+,·,≤}. We denote by Nthe standard model of arithmetic and say that a theory Tis sound if all its axioms are true in N.As usual, the formulas of Lare classified in the Σn/Πnhierarchy, Δ0denotes the class of bounded formulas, i.e., formulas with bounded quantifiers only, and B(Σn)denotes the class of boolean combinations of Σn-formulas. For Γ=Σnor Πn,IΓdenotes Qplus the scheme of induction for Γ-formulas, LΓdenotes Qplus minimization for
Γ-formulas, and BΓdenotes IΔ0plus collection for Γ-formulas. Fragments IΔn and LΔnare given by Qtogether with (ϕ(x,v)↔ψ(x,v)) →Iϕ(x,v);(ϕ(x,v)↔ψ(x,v)) →Lϕ(x,v), where ϕ∈Σnand ψ∈Πn. Recall from [14] that EΓ−denotes the parameter free version of the theory EΓ. We also write ϕ(x)∈Γ−to mean that ϕ(x)is in Γand contains no other free variables than the ones shown. We will be concerned with theories described in terms of inference rules too. The Γ-induction rule, Γ-IR, and the Γ-collection rule, Γ-CR, are given by ϕ(0,v)∧∀x(ϕ(x,v)→ϕ(x+1,v)) ∀xϕ(x,v);∀x∃yϕ(x,y,v) ∀z∃u∀x≤z∃y≤uϕ(x,y,v), where ϕ∈Γ. Similarly, Δn-IR and Δn-LR are given by ϕ(x,v)↔ψ(x,v) Iϕ(x,v) ;ϕ(x,v)↔ψ(x,v) Lϕ(x,v) , with ϕ∈Σnand ψ∈Πn. Following [3], given an inference rule Rand a theory T,T+Rdenotes the closure of Tunder Rand first order logic; while [T,R]denotes the closure of Tunder non-nested applications of Rand first order logic. A rule R1is reducible to R2if [T,R1]⊆[T,R2]for every theory Textending IΔ0;tworulesR1 and R2are congruent if they are mutually reducible to each other. In the present paper by an arbitrary arithmetic theory Twe mean any extension of IΔ0in the language L. In particular, Cantor’s pairing function x,y= (x+y+1)·(x+y) 2+xand projections y=(x)0and y=(x)1will be available in all our theories. Finally, if Aand Bare L-structures we write A≺ΓBto mean that AisaΓelementary substructure of B, i.e., for all ϕ(x)∈Γand a∈A,A| ϕ(a)if, and only if, B| ϕ(a). We denote by Kn(A,p)the submodel of Aconsisting of elements which are Σn-definable (possibly with a parameter p). Submodels of Σn-definable elements are natural examples of Σn-elementary substructures. In addition, since [16] and [17] it has been known that they provide examples of arithmetic structures where Σn-collection fails. In [9] we obtained the following strengthening of these old results. Proposition 1 ([9], Theorem 3.6) 1. If A| IΔ0and p ∈Ais nonstandard, K1(A,p)| BΣ1+exp. 2. If A| IΔ0and K1(A)is nonstandard, K1(A)| LΔ− 1+exp. 3. If A| BΣ1and p ∈Ais nonstandard and Π1-minimal (i.e., p is the least element satisfying some Π1-formula), then K1(A,p)| BΣ− 1+exp. 3 Models of Δ1(T)-schemes Let T be a fixed but arbitrary extension of I Δ0. In this section we prove our characterization theorem for Δ1(T )-schemes and obtain their basic proof-theoretic properties.
Although we shall concentrate on the case n=1, our results easily generalize to Δn(T)-schemes for an arbitrary n≥1. First, recall from [11] that Lemma 1 1. LΔ1(T)IΔ1(T). 2. LΔ1(T)BΔ1(T). 3. ThΠ2(T)+BΔ1(T)LΔ1(T). The proofs are easy adaptations of the proofs that LΣ1IΣ1and LΔ1≡BΣ1(see e.g., [12]). In particular, it follows that over T,LΔ1(T)and BΔ1(T)are deductively equivalent, which is a reformulation of the fact that Δ1-LR and Σ1-CR are congruent rules. Turning to the characterization theorem, we will reformulate the theorems of a Δ1(T)-scheme as the intersection of the theorems of other two theories. Or, equivalently, we will reformulate the class of models of a Δ1(T)-scheme as the union of the models of other two theories. This motivates the following definition. Definition 1 Let Sand Tbe L-theories and let Ax(S)and Ax(T)be the sets of their non-logical axioms. Then S∨Tis the theory whose non-logical axioms are the set of sentences {ϕ∨θ:ϕ∈Ax(S)and θ∈Ax(T)}. Lemma 2 A| S∨T if and only if either A| SorA| T. Hence, for each ϕ, S∨Tϕif and only if both S ϕand T ϕ. We are now ready to state our result. Theorem 1 (Transfer theorem) 1. IΔ1(T)ThΠ2(T)∨IΣ1. 2. LΔ1(T)ThΠ2(T)∨IΣ1. 3. BΔ1(T)ThΠ2(T)∨BΣ1. Proof We only write the proof of part 1. The remaining cases are analogous. Suppose A| IΔ1(T)and A| ThΠ2(T). To see that A| IΣ1consider ϕ(x,v) ∈Σ1. Since A| ThΠ2(T), there are θ(w) ∈Σ1and b∈Asuch that T∀wθ(w)and A| ¬ θ(b). Put δ(x,v,w) ≡ϕ(x,v)∨θ(w). Clearly, Tproves ∀v, w, xδ(x,v,w) and so δ(x,v,w) ∈Δ1(T). Hence, for all a∈A,A| Iδ(x,a,b)by IΔ1(T).But A| ϕ(x,a)↔δ(x,a,b)since A| ¬ θ(b). Thus, Iϕ(x,a)is true in A. From Lemma 2and Theorem 1it follows that Corollary 1 (Characterization theorem) 1. IΔ1(T)≡[ThΠ2(T), Δ1-IR]∨IΣ1. 2. LΔ1(T)≡[ThΠ2(T), Σ1-CR]∨IΣ1. 3. BΔ1(T)≡[ThΠ2(T), Σ1-CR]∨BΣ1. As a first application, we obtain a partial solution to the variant of Paris’ problem for Δ1(T)-schemes. Since Corollary 1associates IΔ1(T)and LΔ1(T)to the same classic scheme IΣ1, it will suffice to show that Δ1-IR and Σ1-CR are congruent rules. Proposition 2 Suppose T exp. Then [T,Δ 1-IR]≡[T,Σ 1-CR].
Proof Since Σ1-CR and Δ1-LR are congruent rules, it is clear that [T,Σ 1-CR]implies [T,Δ 1-IR]. The converse will follow by adapting Slaman’s proof that IΔ1+exp BΣ1(see Theorem 2.1 of [21]). Suppose A| Tand [T,Σ 1-CR]fails in A. Note that Σ1-CR is reducible to its parameter free version Σ− 1-CR which in turn is reducible to Π− 0-CR. Hence, there is θ(x,y)∈Π− 0such that •T∀x∃yθ(x,y); •Bθfails in Aand so A| ∀ u∃x≤a∀y≤u¬θ(x,y)for some a∈A. Let δ(z)denote the Π1-formula ∀u∃x≤z∀y≤u¬θ(x,y). Slaman’s proof shows us how to produce a failure of IΔ1from a failure of BΣ1. Inspection of that proof gives us that there are ϕ(x,z)∈Σ1and ψ(x,z)∈Π1such that •T∀z(δ(z)→∀x(ϕ(x,z)↔ψ(x,z)) •Iϕ(x,a)fails in A. Still we cannot conclude, as ϕ(x,z)need not be in Δ1(T). However, it suffices to modify ϕ(x,z)a bit to produce a failure of [T,Δ 1-IR]. To that end, write δ(z)as ∀yδ(z,y), ϕ(x,z)as ∃yϕ(x,y,z), and ψ(x,z)as ∀yψ(x,y,z), with δ,ϕ,ψ∈ Δ0. Then, we have T∀x,z∃y[¬δ(z,y)∨¬ψ(x,y,z)∨ϕ(x,y,z)]. Write θ(x,y,z)for the Δ0-formula in square brackets above and consider ϕ(x,z)≡∃y(y=μt.θ(x,t,z)∧ϕ(x,y,z)) ψ(x,z)≡∀y(y=μt.θ(x,t,z)→ϕ(x,y,z)) It is clear that T∀x,z(ϕ(x,z)↔ψ(x,z)). In addition, it is easy to see that Tδ(z)→(ϕ(x,z)↔ϕ(x,z)) and so Iϕ(x,a)fails in Asince A| δ(a). Therefore, A| [ T,Δ 1-IR]. Theorem 2 Suppose T exp. Then IΔ1(T)≡LΔ1(T). Proof Suppose A| IΔ1(T).IfA| ThΠ2(T)then A| BΔ1(T)by Proposition 2and so A| LΔ1(T)by Lemma 1.IfA| ThΠ2(T)then Asatisfies IΣ1by Theorem 1. Remark 1 1. In [11] the authors proved the equivalence IΔ1(T)≡LΔ1(T)provided Tis an extension of IΔ0closed under Σ1-CR, and asked whether this condition is also necessary for that equivalence (see part 3 of Problem 7.1 in [11]). Theorem 2answers in the negative that question. 2. It follows from Theorem 1that IΔ1(T)ThΠ2(T)whenever ThΠ2(T)⊆IΣ1. This answers in the negative Problem 7.1 in [7], where the authors asked whether a theory Tsatisfying that IΔ1(T)ThΠ2(T)must be closed under Δ1-IR. 3. It follows from Lemma 1and Theorem 2that IΔ1(T)BΔ1(T)if Texp. But, in general, BΔ1(T)does not imply IΔ1(T)(for example, if T=IΔ0+exp then IΔ1(T)exp whereas BΔ1(T)⊆BΣ1). This differs from the classic case where BΔ1(≡BΣ1)IΔ1.
A second application of the Transfer Theorem is an unboundedness result for Δ1(T)-schemes. The so-called Kreisel–Lévy unboundedness theorems [15] are results stating that a certain fragment of arithmetic has no extensions of bounded quantifier complexity of a certain kind. Here we obtain the following variant of this family of results. Proposition 3 (Unboundedness) Suppose S ⊆Σ3. 1. If S IΔ1(T)then S ThΠ2(T). 2. If S exp and S BΔ1(T)then S ThΠ2(T). Proof We only prove part 2. The proof of part 1 is similar. Towards a contradiction, assume SBΔ1(T)+exp and Sdoes not imply ThΠ2(T).Letθbe a Π2 sentence such that Tθand S θ. It follows from Theorem 1for BΔ1(T)that S+¬θBΣ1+exp. Since BΣ1+exp is finitely axiomatizable, there is a single Σ3sentence ϕsuch that ϕ+¬θis a consistent extension of BΣ1+exp.Let Abe a nonstandard model of ϕ+¬θ. Put ϕ≡∃xϕ(x)and ¬θ≡∃xθ(x), with ϕ(x)∈Π2and θ(x)∈Π1, and pick a,b,c∈Asuch that ais nonstandard and A| ϕ(b)∧θ(c). Finally consider d=a,b,c. Then, the submodel of definable elements K1(A,d)also satisfies ϕ(b)∧θ(c)since K1(A,d)≺Σ1A. So, K1(A,d) is a model of BΣ1+exp, which contradicts Proposition 1. Since the sentence expressing that a Σ1formula is equivalent to a Π1formula has complexity Π2, it is clear that Δ1(T)-schemes only depend on the Π2-theorems of T. Somewhat surprisingly, it follows from the Unboundedness results that we can also recover the Π2-theorems of Tfrom the corresponding Δ1(T)-schemes, no matters how strong Tmight be. Proposition 4 1. Suppose S and T are closed under Δ1-IR. Then, IΔ1(S)≡IΔ1(T)if and only if ThΠ2(S)=ThΠ2(T). 2. Suppose S and T are closed under Σ1-CR and prove exp. Then, BΔ1(S)≡ BΔ1(T)if and only if ThΠ2(S)=ThΠ2(T). Proof We only write the proof of part 2. Assume BΔ1(S)BΔ1(T). Since Sis closed under Σ1-CR,ThΠ2(S)implies BΔ1(S). So, ThΠ2(S)implies BΔ1(T)and then ThΠ2(T)⊆ThΠ2(S)by Proposition 3. The opposite direction follows by symmetry. As an immediate consequence, we obtain that Theorem 3 (Hierarchy theorem) 1. IΔ0≡IΔ1(IΔ0)IΔ1(IΣ1)IΔ1(IΣ2)IΔ1(IΣ3)··· ⊆ IΣ1 2. IΔ0≡BΔ1(IΔ0)BΔ1(IΣ1)BΔ1(IΣ2)BΔ1(IΣ3)··· ⊆ BΣ1 Using a modified version of the model-theoretic notion of an envelope, Theorem 6.6 in [11] gives another proof that IΔ1(IΣn), n≥0 form a hierarchy. In contrast, a hierarchy theorem for BΔ1(IΣn), n≥0, was left over (see Problem 7.5 in [11]).
Theorem 3answers that question as well as provides a much simpler proof of the hierarchy theorem for the induction case. We close this section by showing how to use the Unboundedness theorem to determine the usual proof-theoretic properties of Δ1(T)-schemes. Rather than being systematic, we prefer to illustrate this methodology with a few salient examples. Proposition 5 (Quantifier complexity) 1. If IΣ1ThΠ2(T), then IΔ1(T)is Π2-axiomatizable. If IΣ1 ThΠ2(T), then IΔ1(T)is Π3and not Σ3-axiomatizable. 2. If IΔ0+exp ThΠ2(T), then BΔ1(T)is Π3and not Σ3-axiomatizable. Proof Note that the natural axiomatizations of IΔ1(T)and BΔ1(T)are of quantifier complexity Π3. (1) On the one hand, if IΣ1ThΠ2(T)then it follows from Theorem 1that IΔ1(T)ThΠ2(T). Hence IΔ1(T)is equivalent to [ThΠ2(T), Δ1-IR]and this last theory is Π2-axiomatizable. On the other hand, if IΔ1(T)were to be Σ3axiomatizable then it would follow from Proposition 3that IΔ1(T)ThΠ2(T) and so IΣ1ThΠ2(T)too. (2) If BΔ1(T)were to be Σ3-axiomatizable then it would follow from Proposition 3 that BΔ1(T)+exp ThΠ2(T)and hence IΔ0+exp ThΠ2(T)too, for BΣ1+exp is well-known to be Π2-conservative over IΔ0+exp. Notice that it follows from Proposition 5that IΔ1(T)is Π2-axiomatizable if, and only if, IΣ1ThΠ2(T). This settles the motivating question of [7]: under which conditions is IΔ1(T)aΠ2-axiomatizable theory? Proposition 6 (Finite axiomatizability) 1. IΔ1(T)is finitely axiomatizable if and only if so is [ThΠ2(T), Δ1-IR]. 2. Suppose T exp. If BΔ1(T)is finitely axiomatizable, so is [ThΠ2(T), Σ1-CR]. 3. So, if T is a consistent extension of IΣ1, neither IΔ1(T)nor BΔ1(T)is finitely axiomatizable. Proof (1) By Corollary 1we have IΔ1(T)≡[ThΠ2(T), Δ1-IR]∨IΣ1. So, if [ThΠ2(T), Δ1-IR]has a finite axiomatization then the second theory in the previous equivalence provides a finite axiomatization of IΔ1(T). For the opposite direction, assume that IΔ1(T)is finitely axiomatizable. Then there is a single Π2-sentence, ϕ, such that ThΠ2(T)+IΔ1(T)ϕIΔ1(T). But it follows from Proposition 3that ϕThΠ2(T)and hence ϕ≡[ThΠ2(T), Δ1-IR]. (2) Reason as in the second part of the proof of part 1. (3) Assume Tis consistent and implies IΣ1. Then, ThΠ2(T)is closed under Δ1-IR and Σ1-CR and is known to be not finitely axiomatizable (for a proof see, e.g., Theorem 5.3 of [7]). Remark 2 (The theory BΔ1(I Δ0 +exp) and the NE Problem) In contrast to the induction case, Proposition 3 for BΔ1(T ) has only been obtained for Σ3-extensions proving exp. As a consequence, this additional assumption has also appeared in the subsequent
results on BΔ1(T). Eliminating this use of exp is apparently quite difficult, for it is related to the well-known open problem whether IΔ0plus the negation of exp implies BΣ1(for short, the NE Problem) raised by Wilkie and Paris in [24]. Actually, we have Lemma 3 The following are equivalent. 1. IΔ0+¬exp BΣ1. 2. BΔ1(IΔ0+exp)≡IΔ0. Proof (1⇒2) By part 1, IΔ0+¬exp BΔ1(IΔ0+exp).ButIΔ0+exp also implies BΔ1(IΔ0+exp)since IΔ0+exp is closed under Σ1-CR and hence part 2 follows. (2⇒1) Note that BΔ1(IΔ0+exp)+¬exp BΣ1by Theorem 1. Hence, eliminating exp in Proposition 3would give that IΔ0is strictly weaker than BΔ1(IΔ0+exp), thus settling the NE Problem. (A recent discussion on the difficulty and significance of this problem can be found in [1]). 4 Parameter-free Δ1(T)-schemes This section investigates the effect of disallowing parameters in Δ1(T)-schemes and in Δ1-inference rules. Recall that IΔ1(T)−,LΔ1(T)−and BΔ1(T)−denote the parameter free versions of the corresponding theories. Similarly, we define Δ− 1-IR :∀x(ϕ(x)↔ψ(x)) Iϕ(x) ;Δ− 1-LR :∀x(ϕ(x)↔ψ(x)) Lϕ(x) , where ϕ(x)∈Σ− 1and ψ(x)∈Π− 1. We have not introduced the inference rule associated to BΔ1(T)−,forΣ1-CR is reducible to its parameter free counterpart. In contrast, Δ1-IR and Δ1-LR are no longer reducible to their parameter free versions. To see that, recall from [13] that UIΔ1denotes a variant of the Δ1-induction scheme where parameters are distributed uniformly. Namely, UIΔ1is Qtogether with ∀v∀x(ϕ(x,v)↔ψ(x,v)) →∀vIϕ(x,v), where ϕ∈Σ1and ψ∈Π1. Since IΔ− 1does not imply UIΔ1(see e.g., Theorem 1.2 in [9]), there are ϕ(x,v)∈Σ1and ψ(x,v)∈Π1satisfying that T= IΔ− 1+∀v∀x(ϕ(x,v)↔ψ(x,v)) does not prove ∀vIϕ(x,v). Thus, such a theory T is closed under Δ− 1-IR and, however, does not imply [T,Δ 1-IR]. A similar remark applies to Δ1-LR considering ULΔ1≡BΣ− 1. Regarding Δ1(T)-schemes, it follows from our results on quantifier complexity in Sect. 3that disallowing parameters also makes a difference. Let us see that for the induction case. First, observe that IΔ1(T)−has quantifier complexity B(Σ2), i.e., boolean combinations of Σ2-sentences. Second, by Proposition 5,IΔ1(T)is not Σ3-axiomatizable whenever IΣ1 ThΠ2(T). Thus, IΔ1(T)−is strictly weaker than IΔ1(T)if ThΠ2(T)IΣ1. Similar remarks apply to the collection and minimization cases. Our starting point is a Transfer Theorem for these theories.
Proof It follows from Lemma 2that if ϕ(x,y)and ψ(x,y)are Σ1-definitions of fin Tand in S, respectively, then ϕ(x,y)∨ψ(x,y)is a Σ1-definition of fin T∨S. By a well-known result due independently to G. Mints, C. Parsons and G. Takeuti, R(IΣ1)equals to the class of primitive recursive functions PR. In view of Corollary 1, it only remains to determine the p.t.c.f.’s of [T,Σ 1-CR]and [T,Δ 1-IR]for T a sound Π2-extension of IΔ0. In both cases our results will be, more or less, direct consequences of previous work by Beklemishev. In fact, in Corollary 5.6 of [3]itis shown that if Textends IΔ0+exp, then R([T,Σ 1-CR])coincides with the closure of R(T)under the bounded recursion operator BR or, equivalently, under the bounded minimization operator M. Here we give a variant of that result in terms of the maximum operator Max. The proof is similar to that of Corollary 5.6 of [3] and we omit it. Definition 2 (Bounded Min and Max operators) Assume f:Nk+1→N. Then M(f)denotes the function given by M(f)(x,z)=μi≤x.[f(i,z)=0]if such an i exists, or x+1 otherwise; and Max(f)denotes the function given by Max(f)(x,z)= max({f(i,z):0≤i≤x}). Proposition 9 Suppose that T is a sound Π2-theory extending IΔ0. Then, R([T,Σ 1-CR])=[R(T), Max]=M(R(T)). As for the Δ1-IR case, Beklemishev introduced in [5] a new recursive operator called searchoperator and showed that it corresponds to Δ1-IR. Given f:N→N,the function defined by the search operator (S) from fis S(f)(a,b)=μz.J(f,a,b,z), where J(f,a,b,z)stands for ∃x,u,v ≤zz=x,u,v ∧[(a≤x<b∧(u)0=0∧(v)0= 0∧f(x)=u∧f(x+1)=v) ∨(x=a∧(u)0= 0∧v=0∧f(a)=u) ∨(x=b∧(v)0=0∧u=0∧f(b)=v)] In words, either one finds x ∈[a, b) such that ( f (x))0 = 0 and ( f (x + 1))0 = 0, or one establishes that ( f (a))0 = 0or( f (b))0 = 0. Then one outputs such an x as the first coordinate of a witness z that x is as required (see [5] for details). It is important to note that in [5] it is assumed that, by definition, the search operator can only be applied to unary functions with Δ0-definable graph. Restricting the operator to unary functions is unessential but the restriction to functions with bounded graph is crucial. Here, to make this restriction explicit, we prefer to keep the search operator applicable to any unary function and then introduce the following notations. Let R0(T ) denote the class of those p.t.c.f.’s of T with a Δ0-definition in T . Note that, in general, R0(T ) is not closed under composition and that R(T ) = C(R0(T )). In addition, Lemma 7 R0(T ) coincides with the class of the functions in R(T ) whose graph is Δ0-definable in the standard model. Proof One inclusion is obvious. For the other, let ϕ(x, y) ∈ Σ1 be a definition of a function f in T and let θ(x, y) ∈ Δ0 defining the graph of f in N. Then N |
∀x∀y(ϕ(x,y)→θ(x,y)) and so there is a true Π1-sentence, say ∀zδ(z)with δ∈Δ0, satisfying that T+∀zδ(z)∀x∃yθ(x,y). It is easy to see that the Δ0-formula ¬δ(y)∨θ(x,y)is a definition of fin T. Let [F,S]wdenote the smallest set of functions containing F, closed under composition, and satisfying that S(f)belongs to the set whenever f∈F. Note that [F,S]wis contained in, but could be weaker than, [F,S]if Fis not closed under composition. Using this terminology, Theorem 3in [5] can be restated as follows (that result is proved in [5] over IΔ0+exp but this is unessential). Proposition 10 Suppose that T is a sound Π2-theory extending IΔ0. Then, R([T,Δ 1-IR])=[R0(T), S]w. The above characterization is not as neat as the one obtained for Σ1-CR. It would be nicer to show R([T,Δ 1-IR])=[R(T), S], i.e., with the search operator being applied to any computable function rather than only to functions with a bounded graph. However, one should take into account the following fact. Lemma 8 1. [C,M]⊆[C,S]for each function algebra Ccontaining M2. 2. Assume that R([T,Δ 1-IR])=[R(T), S]for every sound Π2-theory T extending IΔ0. Then BΣ− 1is provable from ThΠ1(N)+IΔ1. (Whether such a proof exists is still open). Proof (1) Pick f:Nk+1→Nin C(C). Roughly speaking, in order to obtain the least i≤xsuch that f(i,z)=0, it suffices to apply the search operator on the interval [0,x+2]to the function that takes the values 0,0,sg(f(0,z)), 0,··· ,sg(f(x,z)), 0,1,0, where sg denotes Kleene’s signum function, which satisfies sg(0)=1 and sg(x)=0ifx= 0. More formally, define f:Nk+2→Nto be f(x,z,w)=⎧ ⎨ ⎩ 0,0x=0 sg(f(x−1,z)), 01≤x≤w 1,0x>w Then, f∈C(C)as M2⊆C, and it follows from the definition of the search operator that M(f)(x,z)=(S(f)(0,x+2,z,x+1))0, where by abuse of notation we also write S(f)to denote the search operator applied to a function with parameters. It only remains to eliminate the use of parameters z,w in f. This can be achieved by putting together pieces of fas follows. (This idea has been taken from the proof of Lemma 14 in [5] but we need to modify the coding method because we work over M2rather than over the class of elementary functions). For simplicity, we first encode z,w into a single parameter vby putting f(x,v)=f(x,(v) 0,...,(v) k). Now consider g(x)=f((x)0,((x)0+(x)1)0). It follows from the definition of the pairing function that gon the interval [0,v, x,0,v, x + x]takes the values f(0,v),..., f(x,v). If we put
h(x,v) =0,v, x and write S(g)(h(x,v),h(x,v) +x)as a,b,c, then we have S(f)(0,x,v) =a−h(x,v),b,cand S(f)(0,x,z,w)= S(f)(0,x,z,w). So, the latter function is in [C,S], as required. (2) Suppose A| ThΠ1(N)+IΔ1and consider Tto be the set of all Π2-sentences true in A. Then Tis a sound Π2-extension of IΔ0closed under Δ1-IR and hence R(T)is closed under the search operator by the assumption. It follows from part 1 that R(T)is also closed under bounded minimization. So R(T)= R([T,Σ 1-CR])by Proposition 9and Textends [T,Σ 1-CR]by Lemma 5. Thus, A| BΣ− 1as required. Having justified the introduction of the function algebra [F,S]w,wearenowina position to obtain the main theorem of this section. Theorem 6 Let T be a sound extension of IΔ0. 1. R(IΔ1(T)−)=PR ∩R(T). 2. R(IΔ1(T)) =PR ∩[R0(T), S]w=[PR∩R0(T), S]w. 3. R(LΔ1(T)) =PR ∩[R(T), Max]=[PR∩R(T), Max]. Proof Write Tfor ThΠ2(T). (1) It follows from Corollary 2and Lemma 6that R(IΔ1(T)−)equals to PR ∩ R([T,Δ − 1-IR]).ButT+ThΠ1(N)implies [T,Δ − 1-IR]and R(T)=R([T, Δ− 1-IR]), for adding true Π1-sentences to a sound theory does not increase the corresponding class of provably total functions. (2) First, it follows from Corollary 1, Lemma 6and Proposition 10 that R(IΔ1(T)) = PR∩[R0(T), S]w. Second, notice that Claim IΔ1(T)is Π2-conservative over IΔ1(IΣ1∨T). Suppose that IΔ1(T)proves θ, with θ∈Π2. Then both IΣ1and [T,Δ 1-IR] prove θtoo. Towards a contradiction, assume IΔ1(IΣ1∨T) θ. Since IΣ1 θ, it follows from Theorem 1that [ThΠ2(IΣ1)∨T,Δ 1-IR]+¬θis consistent. Put S=ThΠ2(IΣ1)∨Tand ¬θ≡∃zδ(z), with δ∈Π1, and suppose that S+¬θ∀x(ϕ(x,v)↔ψ(x,v)), with ϕ∈Σ1,ψ∈Π1. Then Sproves ∀z(δ(z)→ ∀x(ϕ(x,v) ↔ψ(x, v))) and reasoning as in the proof of Proposition 2, we get that [S,Δ 1-IR]+¬θ∀vIϕ(x,v). As a result, [S,Δ 1-IR]+¬θimplies [S+¬θ,Δ1-IR] and hence the latter theory is consistent as well. But we have S+¬θ≡(ThΠ2(IΣ1)+¬θ)∨(T+¬θ) ≡(T+¬θ) since θis a Π2-theorem of IΣ1. We have thus obtained that [T,Δ 1-IR]+¬θis consistent, which is a contradiction. This completes the proof of the Claim. It then follows that R(IΔ1(T)) =R(IΔ1(IΣ1∨T)) =PR ∩R([ThΠ2(IΣ1)∨T,Δ 1-IR]) =[R0(ThΠ2(IΣ1)∨T), S]w =[PR ∩R0(T), S]w (For the last equality note that each primitive recursive function whose graph is Δ0definable in Nhas a Δ0-definition in IΣ1by Lemma 7). (3) The proof is similar to that of part 2.
In what follows we show that in presence of exp,R(IΔ1(T)) and R(LΔ1(T)) can also be described in purely recursion-theoretic terms. We introduce a suitably modified version of the bounded recursion operator, called C-bounded recursion, and prove that if Tis a sound extension of IΔ0+exp then R(LΔ1(T)) coincides with the closure of the basic functions under composition and R(T)-bounded recursion. (A preliminary version of this result appeared in [8]). Definition 3 (C-bounded recursion) A function f:Nk+1→Nis defined from g:Nk→N,h:Nk+2→Nand C:Nk+1→Nby C-bounded recursion, written f=BRC(g,h),if f≤Cand f(x,0)=g(x);f(x,y+1)=h(x,y,f(x,y)), i.e., fis defined from gand hby primitive recursion and fis bounded by C.Givena function class C,ECis the smallest set of functions containing the basic functions (the constant zero, projections, and the successor function) and closed under composition and C-bounded recursion, that is, C-bounded recursion for every C∈C. We use the notation ECin analogy with the well-known Grzegorczyk hierarchy Ei,i≥ 0, defined in terms of usual bounded recursion (see e.g., [19]). One can attach to ECa first-order theory in an extended language, denoted C-BRA, so that EC=R(C-BRA). The definition of C-BRAis inspired by the well-known system PRAfor the primitive recursive functions. Definition 4 Suppose that Ccontains M2and is closed under composition. The theory C-BRA,C-Bounded Recursive Arithmetic, is given by: Language: LC=i∈ωLi, where •L0=Lplus a function symbol Bffor each basic function. •Lj+1=Ljplus a function symbol ftfor each term tof Lj, and a function symbol ft1,t2for each pair of terms t1(x), t2(x,y,z)of Ljsuch that the function defined in the standard model from t1and t2by primitive recursion is bounded by some function C∈C. Axioms: (the universal closure of) (1)Robinson’s Q. (2)BS(x)=x+1,BΠn i(x1,...,xn)=xi,BO(x)=0. (3)ft(x)=t(x). (4)ft1,t2(x,0)=t1(x), ft1,t2(x,z,y+1)=t2(x,y,ft1,t2(x,y)). (5)Open Induction: The induction scheme for open formulas of LC. Observe that C-BRA is a theory only in an abstract model-theoretic sense (i.e., a set of sentences in a first order language) but, in general, it is not even effectively axiomatized. We shall use this theory as a technical tool in order to prove that C∩PR ⊆EC in Proposition 11. Let us also note that bounds (i.e., the functions from C) are not included in the axiomatizations of the recursive schemes (part (4) of the definition) and, so, C-BRA cannot prove anything about them. This is natural because, in general,
Cis not contained in EC: for instance, consider the case when Ccontains some non primitive recursive functions, or, alternatively, see Remark 4below. It is routine to check that C-BRA satisfies the following properties, which are wellknown for PRA: •in C-BRA every bounded formula is equivalent to an open one; •C-BRA supports definition by cases; •C-BRA admits a purely universal axiomatization. As a consequence, a standard application of Herbrand’s theorem gives us that R(C − BRA) = EC . Equipped with this result, we are able to show that Proposition 11 Suppose that C = R(T ) for T some sound extension of I Δ0. Then C ∩ PR ⊆ EC . Proof Since R(C-BRA) = EC and C ∩ PR ⊆ R(I Δ1(T )) by Theorem 6,itis sufficient to prove that Claim I Δ1(T ) is Π2-conservative over C-BRA. To this end, we follow J. Avigad’s proof that I Σ1 is Π2-conservative over PRA given in [2]. The key ingredient is that of an ∃2-closed model (or Herbrand saturated model in Avigad’s terminology). We say that A is an ∃2-closed if, for every structure B, A ≺∀1 B implies A ≺∃2 B. By a union of chain argument every model of a universal theory U can be ∀1-elementary extended to a new model of U which is ∃2closed. Thus, if every ∃2-closed model of a universal theory U is a model of a theory W , then W is ∀2-conservative over U (this is Theorem 3.4 of [2]). Turning back to the proof of the Claim, it suffices to show that every ∃2-closed model of C−BRA satisfies I Δ1(T ), for each Π2-formula is equivalent in C−BRA to a ∀2-formula. Suppose that A is an ∃2-closed model of C − BRA.Let ϕ(x, y,v), ψ(x, y,v) ∈ Δ0 with T ∃y ϕ(x, y,v) ↔∀y ψ(x, y,v). We may assume I Δ0 ϕ(x, y1,v) ∧ ϕ(x, y2,v) → y1 = y2, otherwise consider ϕ(x, y,v)∧∀y < y ¬ϕ(x, y,v) instead. Since T ∀x,v ∃y (ϕ(x, y,v) ∨¬ψ(x, y,v)) and T is sound, y = μt.(ϕ(x, t,v) ∨ ¬ψ(x, t,v)) defines a p.t.f.c. of T ,sayC. Then, (†) N | ϕ(x, y,v) → y = C(x,v). Let a ∈ A and let ϕ0(x, y,v) be an open formula equivalent in C-BRA to ϕ.Wemust show that the induction axiom for ∃y ϕ0(x, y, a) is true in A. To that end, assume A | ∃y ϕ0(0, y, a) ∧∀x (∃y ϕ0(x, y, a) →∃y ϕ0(x + 1, y, a)). In particular, A | ∀x, y ∃y (ϕ0(x, y, a) → ϕ0(x +1, y, a)). Since this last formula has quantifier complexity ∀2, it is provable from the universal diagram of A by the closedness condition for A. Thus, applying Herbrand’s theorem and using that C − BRA supports definition by cases, we obtain that there are b, c ∈ A and a term of LC , t(x, y,v,w), satisfying that A | ϕ0(0, c, a) ∧∀x, y (ϕ0(x, y, a) → ϕ0(x + 1, t(x, y, a, b), a)).
Let hdenote the function defined in the standard model by h(x,y,z,v,w)=t(x,z,v,w) if ϕ0(x+1,t(x,z,v,w),v); 0 otherwise Clearly h∈EC.Let fbe the function defined by primitive recursion as follows: f(0,y,v,w)=y,f(x+1,y,v,w)=h(x,y,f(x,y,v,w),v,w). By (†)f(x,y,v,w)≤C(x,y,v,w)=y+C(x,v).So f∈EC, since it is defined by C-bounded recursion and C∈C.Letfbe the function symbol of LCcorresponding to f. Then Asatisfies that ϕ0(0,f(0,c,a,b), a)∧∀x(ϕ0(x,f(x,c,a,b), a)→ϕ0(x+1,f(x+1,c,a,b), a)). Since Ais a model of open induction, A| ∀ xϕ0(x,f(x,c,a,b), a)and hence A| ∀x∃yϕ0(x,y,a), as required. Remark 4 It is worth noting that the assumption that Cis the class of p.t.c.f.’s of a theory Tcannot be dropped in Proposition 11. For example, put C=C(M2∪{ChA}), where ChAis the characteristic function of a primitive recursive set Awhich is not in the second level of the Grzegorczyk hierarchy E2.First,Ccannot be written as R(T)for any theory Tin the language of arithmetic, for we have R(T)=C(R0(T)) whereas closing under composition the functions in Cwith a Δ0-definable graph only gives us M2. Second, C∩PR =CEC=E2. Theorem 7 Let T be a sound extension of IΔ0+exp and let C=R(T). Then, R(IΔ1(T)) =R(LΔ1(T)) =EC. Proof It follows from Proposition 11 that C∩PR ⊆ECand it follows from Theorem 6that R(LΔ1(T)) =[C∩PR,Max]=M(C∩PR). But it is easy to see that ECis closed under bounded minimization. Thus, R(LΔ1(T)) ⊆EC. For the opposite inclusion, note that Claim EC=EC∩PR. We reason by induction on the definition of f∈EC. The critical step is the definition by C-bounded recursion. Suppose f=BRC(g,h)with C∈C. Since fitself is primitive recursive, there are C1∈PR and C2∈Cwith Δ0-definable graphs such that f≤C1,C2.Letθ1(x,y)∈Δ0be a definition of C1in IΣ1and let θ2(x,y)∈Δ0be a definition of C2in T. Then y=μt.(θ 1(x,t)∨θ2(x,t)) defines a p.t.c.f. of T∨IΣ1, say C3. Note that C3∈C∩PRand f=BRC3(g,h), which proves the claim. Thus EC=EC∩PR ⊆BR(C∩PR)=M(C∩PR)=R(LΔ1(T)), where in the last but one equality BR denotes the usual bounded recursion operator and we use that in presence of exp, bounded recursion can be reduced to bounded minimization.
Exponentiation is used in two different ways in Theorem 7above. On the one hand, exp is needed to prove IΔ1(T)and LΔ1(T)to be equivalent and thus share the same p.t.c.f.’s. On the other hand, exp is needed to reduce bounded recursion to bounded minimization in the proof that EC⊆R(LΔ1(T)). Eliminating this second use of exp seems to be a hard problem, for it is related to important problems in Complexity Theory. In fact, if T=IΔ0then R(LΔ1(T)) =M2and EC=E2. Thus if Theorem 7holds for T=IΔ0then the Linear Time Hierarchy coincides with LinSpace. Likewise, if Theorem 7holds for T=IΔ0+Ω1, where Ω1expresses “x|x|is total”, then the Polynomial Time Hierarchy equals to PolySpace. In the same spirit, we close this section with a reduction of the NE Problem (see Remark 2) to a purely recursion-theoretic question. Recall that E3denotes the third level of the Grzegorczyk hierarchy, which is well-known to coincide with the set of Kalmár’s elementary functions. Proposition 12 The following are equivalent. 1. ThΠ1(N)+¬exp BΣ− 1. 2. Foreach f ∈E3withaΔ0-definable graph, C(M2∪{ f})isclosedunderbounded minimization. Proof (1⇒2): Let f ∈ E3 whose graph is definable by a Δ0-formula, say θ(x, y), and put T = ThΠ1 (N) +∀x ∃y θ(x, y). It follows from Lemmas 4 and 5 that R(T ) = C(M2 ∪{f }). Now observe that it follows from condition 1 that Claim T is closed under Σ1-CR. On the one hand, since R(T ) ⊆ E3 = R(I Δ0 + exp), it follows from the proof of Lemma 5 that T is included in ThΠ1 (N) + exp. But the latter theory is closed under Σ1-CR and hence T exp implies T Σ1-CR. On the other hand, T exp is an extension of BΣ1 − by + condition 1 and + so T +¬exp implies T + Σ1-CR +¬ too. As a result, T implies T + Σ1-CR, as required. Thus C(M2 ∪{f }) is closed under bounded minimization by Proposition 9. (2⇒1): Observe that it follows from condition 2 that Claim ThΠ1 (N) implies BΔ1(I Δ0 + exp)−. To see this, assume that I Δ0 + exp ∀x ∃y ϕ(x, y), with ϕ(x, y) ∈ Σ1 −. Put ϕ(x, y) ≡∃z ϕ0(x, y, z), with ϕ0 ∈ Δ0, and define θ(x, y) to be the Δ0-formula y = μt.ϕ0(x,(t)0,(t)1). Then θ(x, y) defines a computable function f ∈ E3 since I Δ0 + exp ∀x ∃y θ(x, y). By condition 2, Max( f ) ∈ C(M2 ∪{f }) = R(I Δ0 + ∀x ∃y θ(x, y)). Note that ∀x ≤ z ∃y ≤ u θ(x, y) ∧∃x ≤ z θ(x, u) is a Δ0-formula defining Max( f ) in the standard model. Hence reasoning as in the proof of Lemma 5 we obtain that ThΠ1 (N) +∀x ∃y θ(x, y) proves ∀z ∃u ∀x ≤ z ∃y ≤ u θ(x, y) and so ThΠ1 (N) Bϕ(x,y), as required. Thus ThΠ1 (N)+¬exp implies BΔ1(I Δ0 +exp)−+¬exp which in turn implies BΣ1 − by Theorem 4. Corollary 5 Assume that there exists some f ∈ E3 with a Δ0-definable graph such that Max( f ) ∈ C(M2 ∪{f }). Then I Δ0 +¬exp does not imply BΣ1.
Interestingly, Lemma 6.1 of [4] shows how to construct a function f∈E4with an elementary graph such that Max(f)∈ C(E3∪{f}). The construction uses Turing machines equipped with an internal clock. Although it is far from obvious how to adapt that construction to obtain a function satisfying the assumptions of Corollary 5, this approach gives us some new ideas to attack the NE Problem and to obtain, at least, a conditional negative answer under some complexity-theoretic assumption. Acknowledgments Work partially supported by grant MTM2008-06435, Ministerio de Ciencia e Innovación, Spain and FEDER funds (EU). References 1. Adamowicz, Z., Kołodziejczyk, L.A., Paris, J.B.: Truth definitions without exponentiation and the Σ1 collection scheme. J. Symb. Logic 77, 649–655 (2012) 2. Avigad, J.: Saturated models of universal theories. Ann. Pure Appl. Logic 118, 219–234 (2002) 3. Beklemishev, L.D.: Induction rules, reflection principles, and provably recursive functions. Ann. Pure Appl. Logic 85, 193–242 (1997) 4. Beklemishev, L.D.: A proof-theoretic analysis of collection. Arch. Math. Logic 37, 275–296 (1998) 5. Beklemishev, L.D.: On the induction scheme for decidable predicates. J. Symb. Logic 68, 17–34 (2003) 6. Clote, P., Krajíˇcek, J. : Open problems. In: Clote, P., Krajíˇcek, J. (eds.) Arithmetic, Proof Theory, and Computational Complexity, pp. 1–19. Oxford University Press, Oxford (1993) 7. Cordón-Franco, A., Fernández-Margarit, A., Lara-Martín, F.F.: On the quantifier complexity of Δn+1(T)-induction. Arch. Math. Logic 43, 371–398 (2004) 8. Cordón-Franco, A., Fernández-Margarit, A., Lara-Martín, F.F.: Provably total primitive recursive functions: theories with induction. In: Marcinkowski, J., Tarlecki, A. (eds.) Computer Science Logic, 18th International Workshop, CSL 2004, Karpacz, Poland, Sept 20–24, 2004, Proceedings, pp. 355–369, Lecture Notes in Comput. Sci. 3210, Springer, Berlin, Heidelberg (2004) 9. Cordón-Franco, A., Fernández-Margarit, A., Lara-Martín, F.F.: Fragments of Arithmetic and true sentences. MLQ Math. Log. Q. 51, 313–328 (2005) 10. Cordón-Franco, A., Fernández-Margarit, A., Lara-Martín, F.F.: A note on parameter free Π1-induction and restricted exponentiation. MLQ Math. Log. Q. 57, 444–455 (2011) 11. Fernández-Margarit, A., Lara-Martín, F.F.: Induction, minimization and collection for Δn+1(T)-formulas. Arch. Math. Logic 43, 505–541 (2004) 12. Hájek, P., Pudlák, P.: Metamathematics of First-Order Arithmetic. Springer, Berlin, Heidelberg (1993) 13. Kaye, R.: Diophantine and parameter-free induction. Ph.D. thesis, University of Manchester (1987) 14. Kaye, R., Paris, J., Dimitracopoulos, C.: On parameter free induction schemas. J. Symb. Logic 53, 1082– 1097 (1988) 15. Kreisel, H., Lévy, A.: Reflection principles and their use for establising the complexity of axiomatic systems. Arch. Math. Logik Grundlag. 14, 97–142 (1968) 16. Lessan, H.: Models of Arithmetic. Ph.D. thesis, University of Manchester (1978) 17. Paris, J.B., Kirby, L. : Σn-Collection schemas in arithmetic. In: Macintyre, A., Pacholski, L., Paris, J. (eds.) Logic Colloquium 77, Studies in Logic and the Foundations of Mathematics 96., pp. 285–296. North-Holland, Amsterdam (1978) 18. Parsons, C.: On n-quantifier induction. J. Symb. Logic 37, 466–482 (1972) 19. Rose, H.E.: Subrecursion: Functions and Hierarchies. Clarendon Press, Oxford (1984) 20. Sirokofskich, A., Dimitracopoulos, C.: On a problem of J. Paris. J. Log. Comput. 17, 1099–1107 (2007) 21. Slaman, T.: Σn-bounding and Δn-induction. Proc. Am. Math. Soc. 132, 2449–2456 (2004) 22. Takeuti, G.: Grzegorcyk’s hierarchy and IepΣ1. J. Symb. Logic 59, 1274–1284 (1994) 23. Thapen, N.: A note on Δ1induction and Σ1collection. Fund. Math. 186, 79–84 (2005) 24. Wilkie, A.J., Paris, J.B.: On the existence of end-extensions of models of bounded induction. In: Fenstad, J.E., Frolov, I.T., Hilpinen, R. (eds.) Logic, Methodology, and Philosophy of Science VIII, Moscow, 1987, pp. 143–161. North-Holland, Amsterdam (1989)