Provably Total Primitive Recursive Functions: Theories with Induction

Provably Total Primitive Recursive Functions: Theories with Induction Andr´es Cord´on-Franco, Alejandro Fern´andez-Margarit, and F. F´elix Lara-Mart´ın Dpto. Ciencias de la Computaci´on e Inteligencia Artificial. Facultad de Matem´aticas. Universidad de Sevilla C/ Tarfia, s/n. Sevilla, 41012, (Spain) {acordon,fflara}@us.es Abstract. A natural example of a function algebra is R(T), the class of provably total computable functions (p.t.c.f.) of a theory Tin the language of first order Arithmetic. In this paper a simple characterization of that kind of function algebras is obtained. This provides a useful tool for studying the class of primitive recursive functions in R(T). We prove that this is the class of p.t.c.f. of the theory axiomatized by the induction scheme restricted to (parameter free) ∆1(T)–formulas (i.e. Σ1–formulas which are equivalent in Tto Π1–formulas). Moreover, if Tis a sound theory and proves that exponentiation is a total function, we characterize the class of primitive recursive functions in R(T) as a function algebra described in terms of bounded recursion (and composition). Extensions of this result are related to open problems on complexity classes. We also discuss an application to the problem on the equivalence between (parameter free) Σ1–collection and (uniform) ∆1–induction schemes in Arithmetic. The proofs lean upon axiomatization and conservativeness properties of the scheme of ∆1(T)–induction and its parameter free version. 1 Introduction A function algebra is a family of functions that can be described as the smallest class of functions that contains some initial functions and is closed under certain operators. Classical examples of function algebras include the class of primitive recursive functions, PR, classes En,(n ≥ 1), in the Grzegorczyk hierarchy and the class of Kalm´ar elementary functions, E (see [6, 13]). Another important example is given by R(T), the class of provably total computable functions (p.t.c.f.) of a theory T in the language of first order Arithmetic. The class R(T) can be used to obtain independence results for T and to separate it from other theories. On the other hand, if a function algebra, C, is the class of p.t.c.f. of a theory, T, then proof–theoretic and model–theoretic properties of T can be used to establish results on C. This increases the methods available in the study of function algebras by adding to them techniques from Proof Theory and Model Theory. As surveyed in [6], function algebras provide machine–independent characterizations of many complexity classes and offer an alternative view of important open problems in Complexity Theory. In this way, classes of p.t.c.f. constitute a link among Complexity Theory, Proof Theory and Model Theory that has been exploited in the work on Bounded Arithmetic (see [12]). In this paper we present a new example of the fruitful interactions among fragments of Arithmetic, function algebras and computational complexity. Given a function algebra, C, we introduce the algebra ECdefined as the smallest class containing the basic functions (zero, successor and projections) and closed under composition and C–bounded recursion. We study the relationship between Cand ECwhen Cis the class of p.t.c.f. of a theory T.IfC=R(T) then –(Theorem 4) C∩PR⊆E C. Moreover, if Cis closed under bounded minimization, ECis the closure of C∩PRunder composition and bounded recursion. –(Theorem 5) Assume that Cis closed under bounded minimization. Then C∩PR=ECif and only if there exists a theory Tsuch that EC=R(T). For the proof of these results the concept of a ∆0–generated function algebra is introduced. A function algebra, C,is∆0–generated if (it contains Grzegorcyk’s class M2and) each function in Ccan be obtained as a composition of two functions in Cwith ∆0-definable graph. We prove (see Theorem 1) that a function algebra is ∆0–generated if and only if it is the class R(T) for some theory T (extending I∆0). If C⊆PRis closed under bounded minimization, then Theorem 5 states that C=ECif and only if ECis ∆0–generated. This fact has interesting applications to complexity classes as Fph (computable functions in the Polynomial Time Hierarchy, that is, ∞ i=1 2p iin S. Buss’ terminology, see [10]) and Flth (computable functions in the Linear Time Hierarchy, see [6]). Both classes are contained in PR and are ∆0–generated and closed under bounded minimization: –Flth =M2=R(I∆0) (see [6, 16]), and –Fph =R(I∆0+Ω1) (see [10]), where I∆0+Ω1is the theory introduced by A. Wilkie and J. Paris in [17]. But EFlth =E2=Flinspace (R.W. Ritchie, see [6]) and EFph =Fpspace (D.B. Thompson, see [6]). Therefore, by Theorem 5 it follows that: 1. If Fpspace is ∆0–generated then Fpspace =Fph. 2. If Flinspace is ∆0–generated then Flinspace =Flth. Or, equivalently, E2=M2if and only if E2is ∆0–generated. These facts suggest that a deeper knowledge of structural properties of ∆0– generated function algebras (specially, construction of non ∆0–generated function algebras) could be relevant in the study of complexity classes. They also raise a natural question: if C=R(T) and ECis ∆0–generated, is there a natural theory Tsuch that R(T)=EC? We obtain an answer to this question from the study of induction schemes for ∆1–formulas. Let I∆1(T)−be the theory axiomatized by induction scheme restricted to parameter free ∆1(T)–formulas. –(Theorem 2) R(I∆1(T)−)=C∩PR. So, from Theorem 5 we get that, if Cis closed under bounded minimization and ECis ∆0–generated, then EC=R(I∆1(T)−). Next step is to find conditions ensuring ECis ∆0–generated. Classes ECare a generalization of Grzegorcyzk’s classes Enand it is well–known that if exponential function is in En, then bounded recursion can be reduced to bounded minimization (see [6, 13]). But bounded minimization has a straightforward formulation in the language of first order Arithmetic and as a consequence (for n≥3) Enis ∆0–generated. The key ingredients in the proof of this fact are exponential function (which allows for coding of sequences of arbitrary length) and Σ1–collection principle (as a suitable formulation of the combinatorial principles involved). These arguments lead to a natural condition for ECto be a ∆0–generated function algebra and relate the study of ECto the problem on the equivalence between the schemes of Σ1–collection and ∆1–induction in Arithmetic (see [7]). In [3, 5], L. Beklemishev obtains Π2–axiomatized theories that are not closed under Σ1–collection rule or ∆1–induction rule. He proposes classes of p.t.c.f. as a tool to separate the fragments I∆1and BΣ1. Recently (see [15]) T. Slaman has proved that I∆1+exp is equivalent to BΣ1+exp (where exp is aΠ2–sentence expressing that exponentiation defines a total function with ∆0 definable graph (see [10])). So, Beklemishev’s approach must fail. Nevertheless, as we shall show, classes of p.t.c.f. could be used to obtain positive results on fragments of Arithmetic. Motivated by Beklemishev’s work in [3, 4, 5], we study the classes of p.t.c.f. of the theories I∆1(T) and L∆1(T) introduced in [9], and their relationship with the uniform counterpart of Slaman’s result. Theorem 5 holds for Cclosed under bounded minimization. We prove that if Theorem 5 also holds under the (apparently weaker) following hypothesis: (IC)C=R(T) and Textends I∆1(T), then a (weak) uniform counterpart of Slaman’s result can be obtained, namely, theories BΣ− 1+exp and UI∆1+exp are equivalent, modulo Π1–true sentences (see Theorem 7). Last equivalence can be also obtained from Slaman’s theorem and Σ3–conservativeness between I∆1+exp and UI∆1+exp (see corollary 6 in [5]). However, we present an independent approach stressing the role of function algebras via classes of p.t.c.f. Our main tools for the proofs are axiomatization and conservativeness results for I∆n+1(T) and Herbrand analyses, essentially along the lines presented by W. Sieg in [14]; however, we work in a model–theoretic framework, following J. Avigad’s work in [1]. 2 Fragments of Arithmetic and Function Algebras Through this paper we deal with classes of p.t.c.f. of a number of theories. We are mainly interested in characterizations of these classes as function algebras. So, first of all, we introduce the theories and classes of functions we are concerned with. These theories are axiomatized by axiom schemes expressing classical principles in Arithmetic as induction, minimization and collection. Let L={0,1,<,+,·} be the language of first order Arithmetic. The induction and minimization axioms for a formula ϕ(x,v) with respect to xare, respectively, Iϕ,x(v)≡ϕ(0,v)∧∀x[ϕ(x,v)→ϕ(x+1,v)] →∀xϕ(x,v), Lϕ,x(v)≡∃xϕ(x,v)→∃x(ϕ(x,v)∧∀z<x¬ϕ(z,v)). The collection axiom for a formula ϕ(x, y,v) with respect to x, y is Bϕ,x,y(z,v)≡∀x≤z∃yϕ(x, y,v)→∃u∀x≤z∃y≤uϕ(x, y, v). As usual, we write Iϕinstead of Iϕ,x and similarly we use Lϕand Bϕ. All theories considered in this paper are extensions of P−a finite set of Π1 formulas whose models are the nonnegative part of a discretely ordered commutative ring (see [11]). Other theories are defined by restricting the schemes just introduced to formulas in the classes Σnor Πnin the Arithmetical Hierarchy. If Γis a class of formulas of L, then IΓ=P−+{Iϕ:ϕ∈Γ}. The theory LΓis similarly defined using Lϕinstead of Iϕ. For collection, BΓ=I∆0+{Bϕ:ϕ∈Γ}, where ∆0denotes the class of bounded formulas of L(see [10, 11]). Induction schemes for ∆n+1–formulas will be also considered, I∆n+1 is the theory given by: P−+{∀x(ϕ(x,v)↔ψ(x,v)) →Iϕ(v): ϕ(x,v)∈Σn+1,ψ(x,v)∈Πn+1}. If parameters, v, are not allowed, then we obtain the theory I∆− n+1. The uniform version of induction scheme, UI∆n+1, was introduced by R. Kaye. It is defined by considering the scheme ∀v ∀x(ϕ(x,v)↔ψ(x,v)) →∀v Iϕ(v). This theory is also studied by Beklemishev in [5], where it is denoted by sI∆1. Definition. Let Tbe a theory in the language L. We say that f:ωk→ωis a provably total computable function of Tif there exists a formula ϕ(x, y)∈Σ1 such that 1. T∀x ∃!yϕ(x, y). 2. For all a1,...,a k,b∈ω, f(a)=b⇐⇒ N |=ϕ(a, b). Where Ndenotes the standard model of Arithmetic whose universe is the set of natural numbers, ω. In such a case, we say that ϕ(x, y) defines fin T. This definition is sensitive to changes in the language of the theory. If Tis a theory in a language Lextending L, then R(T) will denote the class obtained by considering Σ1(L)–formulas instead of Σ1–formulas. The class R(T) has turned out to be a natural object, its closure properties (under certain operators) reflecting axiom schemes (or inference rules) provable in T. Thus, closure under primitive recursion corresponds to Σ1–induction and bounded minimization to Σ1–collection (see [2]). In particular, R(IΣ1)=PR and R(I∆0+exp)=E. It is easy to check that if Φ⊆ThΠ1(N) and Tis a sound theory (that is, N|=T) then R(T)=R(T+Φ) (see [14]). The class R(T) is determined by ThΠ2(T) (the set of Π2–sentences provable in T). The converse also holds modulo Π1–true sentences. Proposition 1. Let T1and T2be Π2–axiomatized sound extensions of I∆0. The following conditions are equivalent: 1. R(T1)=R(T2). 2. T1+ThΠ1(N)⇐⇒ T2+ThΠ1(N). Proof. We only prove (1)=⇒(2). By symmetry, it is enough to show that T1+ThΠ1(N)=⇒T2. Let θ(x, y)bea∆0–formula such that T2∀x∃yθ(x, y). Let θ(x, y) be the formula θ(x, y)∧∀z<y¬θ(x, z). Since T2=⇒I∆0,T2 ∀x∃!yθ (x, y). Let fbe the computable function defined by θin N. Then, f∈R(T2); so, by (1),f∈R(T1). Hence, there is ϕ(x, y)∈Σ1defining fin T1. Thus, N|=ϕ(x, y)↔θ(x, y).In particular, N|=∀x, y (ϕ(x, y)→θ(x, y)); so, since this last formula is a Π1sentence, T1+ThΠ1(N)∀x∃yθ(x, y).  Functions with a ∆0–definable graph will play a prominent role throughout this work. Let us introduce the following notation. We denote by ∆0 0the class of sets ∆0definable in the standard model. The graph of a function fis denoted by Gr(f)={(a, b)∈ωk+1 :f(a)=b}.IfCis a class of functions, then C∗denotes the class of subsets of ωkwhose characteristic functions are in C. Finally, given f,g :ωk→ω, we write f≤gto mean that for each a ∈ωk,f(a)≤g(a). One of the aims of this work is to obtain descriptions of R(T) as a function algebra generated by means of some operators from a small set of basic functions. The considered classes of basic functions will always contain the set B={S, O}∪{Πn i:1≤i≤n} where S, O :ω→ωare given by S(a)=a+ 1 and O(a)=0,andΠn i:ωn→ω, by Πn i(a1,...,a n)=ai. As operators, beside composition, we consider: Bounded minimization,µ≤:Ifg:ωm+1 →ω, then f=µ≤(g) is the function f:ωm+1 →ωdefined by f(a1,...,a m,b)=min({z:g(a, z)=0}),if ∃z≤b(g(a, z) = 0); 0,otherwise. Bounded recursion,BR: A function f:ωn+1 →ωis defined from g:ωn→ω, h:ωn+2 →ωand C:ωn+1 →ωby bounded recursion, if f≤Cand f(x, 0) = g(x); f(x, y +1)=h(x, y, f(x, y)). In this case we write, f=BRC(g,h) and we shall say that fis defined by C–bounded recursion from gand h. Let Fbe a class containing B. In this paper, C(F) will denote the closure of F under composition and E(F) the closure of Funder composition and bounded recursion. We also consider the following slight (but crucial) modification of closure under bounded recursion. Definition. EFis the smallest class of functions containing Band closed under composition and F–bounded recursion; that is, closed under C–bounded recursion for every C∈F. Let us observe that EF⊆PRand if F⊆E F, then C(F)⊆E F⊆E(F). Grzegorczyk’s classes, En, can be described in the form EF. For instance, let P0,P1and P2be, respectively, the classes of functions C(B), C(B∪{+}) and C(B∪{+,×}), then, for j=0,1,2, it holds that EPj=Ej(see [13]). The basic function algebra in this paper will be Grzegorczyk’s class M2: the closure of B∪{+,×} under composition and µ≤(see [6, 13]). As we shall see (Proposition 3), M2is the class R(I∆0) and, therefore, all function algebras considered in this paper contain it. This motivates the following definition. Definition. An F–algebra is a family, C, of computable functions containing B and closed under composition. We shall say that Cis rudimentary if M2⊆C. A pairing function is available in M2. Let J:ω2→ωbe Cantor’s function: J(a, b)=(a+b)(a+b+1) 2+a. Its lateral inverses K,Lare given by K(a)=(µz)≤a(∃y≤a(J(z,y)=a)) and L(a)=(µz)≤a(∃x≤a(J(x, z)=a)). Then J, K, L ∈M 2. We shall write x, y=J(x, y) and (z)0=K(z), (z)1=L(z). Basic properties of M2are summed up in next proposition (see [6] or [13]). Proposition 2. 1. ∆0 0=M2 ∗. 2. For each f:ωk→ω, the following conditions are equivalent: (a) f∈M 2. (b) Gr(f)∈∆0 0and there exists a term tof Lsuch that f≤t. As a consequence a characterization of R(I∆0) can be obtained. A proof– theoretic proof of this result was obtained by G. Takeuti (see [16]). Proposition 3. M2=R(I∆0). Hence, for every extension, T,ofI∆0the class R(T) is a rudimentary F– algebra. Now we introduce a necessary and sufficient condition under which a rudimentary F–algebra is the class of p.t.c.f. of some theory. The following results seem to be folklore and have appeared more or less explicitly in the literature (see proposition 4.1 in [2] and previous remarks in that paper). However, Theorem 1 below does not seem to be known. As it was remarked in the Introduction, it provides interesting insights on open problems in Complexity Theory. Lemma 1. Let Cbe a rudimentary F–algebra and f:ωk→ωsuch that Gr(f)∈∆0 0. If there exists g∈Csuch that f≤g, then f∈C. Proof. Let h:ωk+1 →ωgiven by h(a, b)=(µz)≤b[f(a)=z]. Since Gr(f)∈∆0 0, then Gr(h)∈∆0 0. By Proposition 2–(2), h∈M 2⊆C. Let g∈Csuch that f≤g. Then f(a)=h(a, g(a)). Since Cis closed under composition, f∈C. Lemma 2. Let Tbe an extension of I∆0. Then for each f∈R(T)there exists g∈R(T)such that Gr(g)∈∆0 0and f=K◦g. Proof. For each f∈R(T) and ϕ(x, y, z)∈∆0such that ∃zϕ(x, y, z) defines f in T, let ψ(x, v)∈∆0be the formula ∃y,z ≤v[y,z=v∧ϕ(x, y, z)∧∀z<z¬ϕ(x, y, z)]. Then T∀x ∃!yψ(x, y). Let gbe the function defined in Nby ψ(x, v). Then g∈R(T), Gr(g)∈∆0 0and f(a)=K(g(a)).  The above lemma motivates the following definition. Definition. Let Cbe a rudimentary F–algebra. We say that Cis a ∆0–generated F–algebra if for each f∈Cthere exist g1,g 2∈C 0such that f=g1◦g2. The following result shows that ∆0–generated F–algebras correspond to classes of p.t.c.f. of extensions of I∆0. Theorem 1. The following conditions are equivalent: 1. Cis a ∆0–generated F–algebra. 2. There exists a (sound) L–theory, T, extending I∆0such that R(T)=C. Proof. (2)=⇒(1): It follows from Proposition 3 and Lemma 2. (1)=⇒(2): For each f∈C 0={h∈C:Gr(h)∈∆0 0}, let θf(x, y)bea∆0– formula defining fin N. Let Γ={∀x∃yθ f(x, y):f∈C 0,f :ω→ω}. Next claim is a slight generalization of proposition 4.2 in [2] and it can also be proved along the lines sketched there. Claim:R(I∆0+Γ)=C(M2∪C 0). Thus, R(I∆0+Γ)=C(M2∪C0)=C, last equality since Cis ∆0– generated.  The aim of this section is to characterize the class of primitive recursive functions in R(T), where Tis an extension of I∆0, as the class of p.t.c.f. of a suitable theory. To this end, we consider the class of ∆n+1(T)–formulas: ∆n+1(T)={ϕ(x,v)∈Σn+1 : there exists ψ(x,v)∈Πn+1,Tϕ↔ψ}. When the schemes of induction and minimization are restricted to these classes of formulas we obtain the theories I∆n+1(T) and L∆n+1(T) introduced in [9]. There the following version of the collection scheme is also considered B∗∆n+1(T)=I∆0+{Bϕ,x,y(z,v): ϕ∈Πn,∃yϕ(x, y,v)∈∆n+1(T)}. Let us state here some basic properties of these theories, for details and proofs see [9]. If ϕ∈Σn+1 and ψ∈Πn+1 then ϕ↔ψis a Πn+2–formula. Therefore, –If ThΠn+2 (T)=ThΠn+2 (T) then I∆n+1(T)⇐⇒ I∆n+1(T). 3 Axiomatizing ∆n+1(T)–Induction A similar result holds for minimization and collection. The following basic properties will be used without explicit mention. –L∆n+1(T)=⇒I∆n+1(T) and B∗∆n+1(T)=⇒IΣn. –If Tis an extension of IΣnthen L∆n+1(T)=⇒B∗∆n+1(T). As noticed in [9], last property follows by an argument that mimics the proof of Gandy’s Theorem, L∆1=⇒BΣ1, given in [10], lemma I.2.17. A variation of that argument, considering also lemma I.2.16 in [10], gives us that Lemma 3. ThΠn+2 (T)+L∆n+1(T)⇐⇒ ThΠn+2 (T)+B∗∆n+1(T). The following notion, introduced in [9], has turned out to be useful for the study of ∆n+1(T)–induction. Definition. We say that Thas ∆n+1–induction if T=⇒I∆n+1(T). Theories I∆n+1(T) and L∆n+1(T) are Πn+3–axiomatizable. But adding to them ThΠn+2 (T), their quantifier complexity is reduced to Πn+2. Lemma 4. ThΠn+2 (T)+I∆n+1(T)and ThΠn+2 (T)+L∆n+1(T)are Πn+2– axiomatizable. In this section we shall obtain a useful axiomatization of I∆n+1(T) in terms of IΣn+1 and ThΠn+2 (T). To this end we introduce the disjunction of two theories, which corresponds to intersection between classes of p.t.c.f. If T1and T2are theories in the language L, then T1∨T2denotes the theory axiomatized by the set of formulas {ϕ1∨ϕ2:ϕ1∈T1and ϕ2∈T2}. Lemma 5. If T1,T2=⇒I∆0then R(T1∨T2)=R(T1)∩R(T2). Proof. Since T1,T2=⇒T1∨T2, it holds that R(T1∨T2)⊆R(T1)∩R(T2). Conversely, if f∈R(T1)∩R(T2), then there exist ψ1(x, y, z),ψ 2(x, y, z)∈ ∆0such that ∃zψ i(x, y, z) defines fin Ti. Let θ0(x, u)∈∆0the formula (ψ1(x, (u)0,(u)1)∨ψ2(x, (u)0,(u)1)) and let θ(x, y) be the formula ∃z[θ0(x, y,z)∧∀w<y,z¬θ0(x, w)] . Then θ(x, y) defines fin T1∨T2. So, f∈R(T1∨T2).  Next proposition is theorem 2.2 in [8]. Now it can be rephrased as follows. Proposition 4. If A|=ThΠn+2 (T)and A|=I∆n+1(T), then A|=IΣn+1. Hence, I∆n+1(T)=⇒IΣn+1 ∨ThΠn+2 (T). Moreover, if Thas ∆n+1–induction then I∆n+1(T)⇐⇒ IΣn+1 ∨ThΠn+2 (T). From this proposition, using Lemma 5, a first result on R(T)∩PR is obtained for theories with ∆1–induction. Corollary 1. 1. PR∩R(T) ⊆R(I∆1(T)). 2. If Thas ∆1–induction then PR∩R(T)=R(I∆1(T)). By Lemma 5, R(T)∩PRis always a ∆0–generated F–algebra. To get a natural theory Tsuch that R(T)=R(T)∩PR without assuming that T has ∆1–induction, we consider parameter free versions of I∆n+1(T) and IΣn+1, denoted by I∆n+1(T)−and IΣ− n+1, respectively. Theorem 2. For each sound theory, T,R(I∆1(T)−)=R(T)∩PR. Proof. By a similar argument to that of theorem 2.2 in [8], it is shown that: I∆n+1(T)−=⇒IΣ− n+1 ∨ThΠn+2 (T). Since PR =R(IΣ− 1), by Lemma 5, PR∩R(T)=R(IΣ− 1∨T)⊆R(I∆1(T)−). Let us prove R(I∆1(T)−)⊆R(T)∩PR. Obviously, R(I∆1(T)−)⊆PR. Now, let us observe that I∆− 1is Σ2–axiomatizable and, therefore, T+ThΠ1(N)=⇒T+I∆− 1=⇒T+I∆1(T)−=⇒I∆1(T)−. So, by Proposition 1, R(I∆1(T)−)⊆R(T+ThΠ1(N)) = R(T).  In this section we characterize R(T)∩PRin terms of bounded recursion. Our main tool will be a version of the well–known system PRA (Primitive Recursive Arithmetic). Our analysis of this theory follows the lines sketched in [1]. Definition. Let Cbe a rudimentary F–algebra. The theory C–BRA,C–Bounded Recursive Arithmetic, is given by: –Language: LC pr =i∈ωLi, where •L0=Lplus a function symbol Bffor each basic function, f∈B. •Lj+1 =Ljplus a function symbol, ftfor each term of Lj, and a function symbol ft1,t2,g for each function g∈Cand terms t1(x), t2(x, y, z)ofLj such that the function defined from t1and t2by primitive recursion is bounded by g,i.e.,h≤g, where h:ωn+1 →ωis the function given by h(x, 0) = t1(x),h(x, y +1)=t2(x, y, h(x, y)). –Axioms: (1) P−. (2) BS(x)=x+1,B Πn i(x1,...,x n)=xi,B O(x)=0. (3) ft(x)=t(x). (4) ft1,t2,g(x, 0) = t1(x),ft1,t2,g(x, y +1)=t2(x, y, ft1,t2,g(x, y)). (5) Open Induction: The induction scheme for open formulas of LC pr. It is routine to check that C–BRA satisfies the following properties stated for PRA in [1]. 4C–Bounded Recursive Arithmetic: C–BRA