Local induction and provably total computable functions

Local Induc ion and P o ably To al Compu able Func ions And ´es Co d´on–F anco, F. F´elix La a–Ma ´ın Dep o. Ciencias de la Compu aci´on e In eligencia A i icial, Uni e si y o Se ille C/ Ta ia, s/n, 41012 Se illa (Spain) Abs ac Le IΠ− 2deno e he agmen o Peano A i hme ic ob ained by es ic ing he induc ion scheme o pa ame e ee Π2 o mulas. Answe ing a ques ion o R. Kaye, L. Beklemishe showed ha he p o ably o al compu able unc ions o IΠ− 2a e, p ecisely, he p imi i e ecu si e ones. In his wo k we gi e a new p oo o his ac h ough an analysis o ce ain local a ian s o induc ion p inciples closely ela ed o IΠ− 2. In his way, we ob ain a mo e di ec answe o Kaye’s ques ion, a oiding he me ama hema ical machine y ( e lec ion p inciples, p o abili y logic,...) needed o Beklemishe ’s o iginal p oo . Ou me hods a e model– heo e ic and allow o a gene al s udy o IΠ− n+1 o all n≥0. In pa icula , we de i e a new conse a ion esul o hese heo ies, namely ha IΠ− n+1 is Πn+2–conse a i e o e IΣn o each n≥1. Keywo ds: Fi s o de A i hme ic, conse a ion esul s, pa ame e ee induc ion, p imi i e ecu si e unc ions. 2000 MSC: 03F30, 03D20 1. In oduc ion An impo an no ion in s udying he compu a ional con en o a agmen o A i hme ic is ha o i s p o ably o al compu able unc ions. A numbe – heo e ic compu able unc ion :Nk→Nis said o be a p o ably o al compu able unc ion (p. .c. .) o a heo y T, w i en ∈ R(T), i he e is a Σ1 o mula ϕ(~x, y) such ha : Email add esses: [email p o ec ed] (And ´es Co d´on–F anco), [email p o ec ed] (F. F´elix La a–Ma ´ın) P ep in submi ed o Annals o Pu e and Applied Logic Feb ua y 17, 2014 1. ϕde ines he g aph o in he s anda d model o A i hme ic N; and 2. T` ∀~x ∃!y ϕ(~x, y). Since i was in oduced by G. K eisel in he 1950s his no ion has been widely s udied, and nice ecu sion– heo e ic and compu a ional complexi y cha ac e iza ions o he se s R(T) ha e been ob ained o a good numbe o heo ies T. Fo ins ance, by a classical esul due independen ly o G. Min s, C. Pa sons and G. Takeu i, he class o p. .c. . o he scheme o induc ion o Σ1– o mulas IΣ1equals o he class o he p imi i e ecu si e unc ions PR. Indeed, all classes R(IΣn), n≥1, can be cha ac e ized in e ms o he Fas G owing Hie a chy up o he o dinal ε0. As o weak agmen s below IΣ1, hei p. .c. . ha e been cha ac e ized in e ms o sub ecu si e ope a o s (bounded ecu sion, bounded minimiza ion, ...) as well as in e ms o compu a ional complexi y classes. In ac , hei classes o p. .c. . ha e been in ensi ely in es iga ed in connec ion wi h impo an open p oblems in Complexi y Theo y, mainly in he con ex o Bounded A i hme ic. In spi e o he wide ange o he heo ies conside ed, a numbe o uni o m me hods o cha ac e izing he p. .c. . o an a i hme ic heo y a e a ailable. E.g. He b and analyses as de eloped by W. Sieg in [13], S. Buss’ wi nessing me hod [5] o , in gene al, p oo – heo e ic echniques using Cu elimina ion heo em. Howe e , o some pa icula agmen s o Peano A i hme ic none o hese s anda d me hods seems o be applicable. O special in e es is he case o he scheme o pa ame e ee Π2–induc ion, IΠ− 2, gi en by he induc ion scheme Iϕ:ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)) → ∀x ϕ(x), es ic ed o ϕ(x)∈Π− 2(as usual, we w i e ϕ(x)∈Γ− o mean ha ϕis in Γ and con ains no o he ee a iables han x). Since IΣ− 1⊆IΠ− 2and IΣ1 is Σ3–conse a i e o e IΣ− 1[10], i ollows ha e e y p imi i e ecu si e unc ion is p o ably o al in IΠ− 2; and R. Kaye asked whe he he p. .c. . o IΠ− 2a e exac ly he p imi i e ecu si e ones. This ques ion emained elusi e un il [4], whe e L. Beklemishe ga e a posi i e answe using modal p o abili y logic echniques. Al hough qui e elegan , Beklemishe ’s answe only p o ides an indi ec solu ion. Fi s ly, he e o mula ed IΠ− 2in e ms o local e lec ion p inciples ( e lec ion p inciples in A i hme ic a e axiom schemes exp essing he s a emen ha “i a o mula ϕis p o able in a heo y T hen ϕis alid”). Secondly, he de i ed he esul as an applica ion o a 2 conse a ion heo em o local e lec ion p inciples whose p oo leans upon p ope ies o G¨odel–L¨ob p o abili y logic GL. In his wo k we ob ain a mo e di ec answe o Kaye’s ques ion, a oiding he me ama hema ical machine y needed o Beklemishe ’s p oo . In ac , ou p oo ha R(IΠ− 2) = PR will ollow he lines o s anda d a gumen s o cha ac e izing classes R(T). Le us conside , o ins ance, a p oo ha R(IΣ1) = PR. Such a p oo ypically p oceeds in wo s eps. •S ep 1: IΣ1is Π2–conse a i e o e he in e ence ule e sion o he p inciple o Σ1–induc ion Σ1–IR. So, R(IΣ1) = R(Σ1–IR). •S ep 2: Applica ions o Σ1–IR co espond o applica ions o he p im- i i e ecu sion ope a o . The main obs acle o apply his a gumen o IΠ− 2is ha he e is no simple, di ec a gumen o educe IΠ− 2 o an in e ence ule e sion o i . He e we sol e his p oblem by showing ha IΠ− 2is equi alen o I(Σ− 2,K2), a ce ain local e sion o he pa ame e ee Σ2–induc ion scheme whe e he elemen s x o which he induc ion axiom claims ϕ(x) o hold a e es ic ed o be Σ2– de inable elemen s. Equipped wi h his esul , i is easy o ob ain ha IΠ− 2 is Π2(in ac , Π3) conse a i e o e he co esponding local in e ence ule e sion (Σ2,K2)–IR. Then, we show ha applica ions o (Σ2,K2)–IR co e- spond o ( es ic ed o ms) o he i e a ion ope a o and hus all unc ions in R(IΠ− 2) a e p imi i e ecu si e. Local induc ion schemes and local induc ion ules play a c ucial ole in ou me hods. In e es ingly, hese local subsys ems can be applied in con- side able gene ali y o s udy agmen s o a i hme ic. Ac ually, in his wo k we also make use o hese ideas o de elop a gene al s udy o he heo ies IΠ− n+1 o all n≥1. As a esul , we a e able o gi e new p oo s o some well–known esul s on hese agmen s as well as o ob ain a no el conse - a ion esul . Namely, we p o e ha IΠ− n+1 is Πn+2–conse a i e o e IΣn o all n≥1. This imp o es on a p e ious esul by Beklemishe in [4] whe e conse a i i y be ween hese heo ies wi h espec o boolean combi- na ions o Σn+1–sen ences was es ablished, and closes a no able gap in ou unde s anding o ela ionships be ween he s anda d agmen s o a i hme ic. 2. On Local Induc ion In his sec ion we gi e a p ecise de ini ion o he auxilia y schemes ha will be cen al in ou analysis o he class o p. .c. . o IΠ− 2. We wo k in he 3 language o i s –o de a i hme ic L={0, S, +,·, <}and de ine he o mula classes ∆0, Σnand Πnas usual. Fo a class Γ o o mulas, IΓ is he heo y axioma ized o e Robinson’s Qby he induc ion scheme, Iϕ, es ic ed o o mulas ϕ(x)∈Γ. I ee a iables o he ha xa e no allowed, we w i e ϕ(x)∈Γ−and, acco dingly, IΓ−deno es he heo y axioma ized o e Qby he axioms Iϕ, o ϕ(x)∈Γ−. The schemes we a e in e es ed in a e local a ian s o he usual induc ion scheme in a sense ha he conclusion o he induc ion p inciple is no longe assumed o e e y elemen in he uni e se bu only o a ce ain subclass o he uni e se. Mo e p ecisely, we de ine: De ini ion 1. Fo e e y n≥1,I(Σn,Kn)is he heo y gi en by I∆0 oge he wi h he scheme ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)) → → ∀x1, x2(δ(x1)∧δ(x2)→x1=x2)→ ∀x(δ(x)→ϕ(x)) whe e ϕ(x)∈Σnand δ(x)∈Σ− n. The na u al in e ence ule associa ed o his scheme, deno ed (Σn,Kn)–IR, is gi en by: ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)) ∀x1, x2(δ(x1)∧δ(x2)→x1=x2)→ ∀x(δ(x)→ϕ(x)) whe e δ(x)∈Σ− nand ϕ(x)∈Σn. Finally, i we es ic he scheme o ϕ(x)∈Σ− n, we ob ain he pa ame e ee coun e pa o I(Σn,Kn), deno ed I(Σ− n,Kn). Rema k 1. Fi s ly, le us ecall ha , gi en a model A,Kn(A)deno es he se o elemen s o A ha a e de inable in Aby a o mula δ(x)∈Σn. This explains why Knappea s in ou no a ion o hese heo ies. Secondly, i A|=IΣ− n−1, hen Kn(A)≺nA(i.e. Kn(A)is a Πn–elemen a y subs uc u e o A). This p ope y plays an impo an ole in wha ollows and i is because o i ha some o ou esul s on I(Σn,Kn)a e ob ained o e IΣ− n−1ins ead o o e I∆0. A key ac is ha I(Σ− n,Kn) p o ides an al e na i e o mula ion o IΠ− n o e e y n≥1: Lemma 1. O e IΣ− n−1,IΠ− n≡I(Σ− n,Kn). 4 P oo . (`): Suppose A|=IΠ− nand A|=ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)), wi h ϕ(x)∈Σ− n. Le δ( )∈Σnde ining some elemen in A, say a. Towa ds a con adic ion, assume A6|=∀x(δ(x)→ϕ(x)). Then, A|=¬ϕ(a). De ine θ(x) o be ∀ (δ( )→ ¬ϕ(x− )). Clea ly, A|=θ(0) ∧ ∀x(θ(x)→θ(x+ 1)). By IΠ− n,A|=θ(a) and so A|=¬ϕ(0), which is a con adic ion. (a): Suppose A|=I(Σ− n,Kn) and A|=ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)), wi h ϕ(x)∈Π− n. Assume A|=∃x¬ϕ(x). Since A|=IΣ− n−1,Kn(A)≺nAand he e is a∈ Kn(A) such ha A|=¬ϕ(a). Le δ( ) be a Σn o mula de ining he elemen aand le θ(x) be ∃ (δ( )∧ ¬ϕ( −x)). Clea ly, A|=θ(0) ∧ ∀x(θ(x)→θ(x+1)). By I(Σ− n,Kn), A|=∀x(δ(x)→θ(x)) and so A|=θ(a). Thus A|=¬ϕ(0), which is a con adic ion. Gi en a heo y Tand an in e ence ule R, we deno e by [T, R] he closu e o Tunde i s o de logic and unnes ed applica ions o R. We deno e by T+R he closu e o Tunde i s o de logic and (nes ed) applica ions o R. The e o e, T+R=Sk∈ω[T, R]k, whe e [T, R]0=Tand [T, R]k+1 = [[T, R]k, R]. The i s s ep in he analysis o IΠ− 2is a sui able educ ion o I(Σ2,K2) o a agmen de ined by he ule (Σ2,K2)–IR. Indeed, he ollowing gene al esul holds o each n≥1. P oposi ion 1. Le Tbe a Πn+2–axioma izable heo y. Then, T+I(Σn,Kn) is Πn+1–conse a i e o e T+ (Σn,Kn)–IR. Ve y con enien ly, his educ ion can be ca ied ou by he same ools used o de i e he educ ion o IΣ1 o Σ1–IR (e.g. by adap ing he cu –elimina ion a gumen used in [3] o de i e a simila educ ion o he Collec ion scheme). Al e na i ely, he e we gi e a model– heo e ic p oo ollowing he me hods de eloped by J. A igad in [1], who in u n builds on p e ious ideas o A. Visse (unpublished) and D. Zambella [14]. In [1] A igad in oduced he no ion o a He b and sa u a ed model and showed ha his no ion p o ides us wi h an uni ied me hod o p o e ∀∃–conse a ion o e uni e sal heo ies. He e we conside a hie a chical e sion o ha no ion ha yields an uni ied me hod o p o e Πn+1–conse a ion o e Πn+2– heo ies. De ini ion 2. We say ha a model o a heo y T,A, is a Σn+1–closed model o Ti o e e y model o T,B, A≺nB=⇒A≺n+1 B. 5 In wo ds, Ais a Σn+1–closed model o Ti e e y Πn– o mula ha can be sa is ied in a Πn–elemen a y ex ension o Awhich is a model o Tcan be al eady sa is ied by an elemen o A. I is easy o show ha Σn+1– closed models exis o e e y n. In ac , by a a he s anda d union o chain a gumen i ollows ha i Tis a Πn+2–axioma izable heo y, hen e e y model o Tcan be Πn–elemen a y ex ended o a Σn+1–closed model o T. As a consequence, he ollowing e sion o heo em 3.4 o [1] holds. Lemma 2. Suppose T2is Πn+2–axioma izable. In o de o p o e ha T1 is Πn+1–conse a i e o e T2i is su icien o show ha e e y Σn+1–closed model o T2sa is ies T1. Nex lemma is an analog o heo em 3.3 o [1] and s a es he key p ope y o Σn+1–closed models o p o ing conse a ion esul s. Lemma 3. Suppose Ais a Σn+1–closed model o T, ϕ( )∈Πn+1 and a∈A. Then A|=ϕ(a) =⇒T`ψ( , w)→ϕ( ), o some ψ( , w)∈Πnsuch ha A|=ψ(a, b) o some bin A. P oo . I ollows om he Σn+1–closedness condi ion ha T+DΠn(A)` ϕ(a), whe e DΠn(A) deno es he Πn–diag am o A, i.e. he se o all Πn– o mulas (possibly wi h pa ame e s) alid in A. Now he esul ollows by compac ness. We a e now in a posi ion o gi e a p oo o P oposi ion 1. P oo . Suppose ha Ais a Σn+1–closed model o T+ (Σn,Kn)–IR and A|= ϕ(0, b)∧ ∀x(ϕ(x, b)→ϕ(x+ 1, b)), wi h ϕ(x, )∈Σn. Conside a∈ Kn(A) and δ(x)∈Σnde ining a. We mus show ha A|=ϕ(a, b). I ollows om Lemma 3 ha (T+ (Σn,Kn)–IR) `ψ( , w)→ϕ(0, )∧ ∀x(ϕ(x, )→ϕ(x+ 1, )), wi h ψ( , w)∈Πnand A|=ψ(b, c) o some c∈A. Pu θ(x, , w)≡ ψ( , w)→ϕ(x, ). Clea ly, θ∈Σnand (T+ (Σn,Kn)–IR) p o es he an- eceden o he induc ion axiom o θand so A|=∀ , w, x (δ(x)→θ(x, , w)). Thus θ(a, b, c) is alid in Aand hence so is ϕ(a, b). Combining Lemma 1 and P oposi ion 1, we ge Co olla y 1. IΠ− 2is Π3–conse a i e o e IΣ− 1+ (Σ2,K2)–IR. 6 3. Local Induc ion and Res ic ed I e a ion Nex s ep in ou analysis is o show ha applica ions o (Σ2,K2)–IR co espond o (a es ic ed o m o ) he i e a ion ope a o . To his end, we shall conside ex ensions o Lob ained by adding a ini e se o una y unc ion symbols, F={ 1, . . . , n}, and a ( ini e o coun able) se o new cons an symbols, C. Th ough his sec ion we conside a ixed se o cons an s, C, and we will deno e by LF he language L+{ 1, . . . , n}+C. I gis a new una y unc ion symbol hen LF,g will deno e he language L{ 1,..., n,g}. De ini ion 3. Le ∈ F be a una y unc ion symbol and le Tbe an LF– heo y. We say ha is an i e able non dec easing unc ion o e Ti he heo y Tp o es: ∀x1, x2(x1≤x2→ (x1)≤ (x2)),and ∀x(x2< (x)) Le ΣF 0= ΠF 0be he class o bounded o mulas o LF. Classes ΣF n+1 and ΠF n+1 a e de ined as usual. The heo y IΣF 0is he LF– heo y axioma ized o e I∆0by •The induc ion axiom Iϕ o each o mula ϕ∈ΣF 0, and •Axioms o each ∈ F: ∀x1, x2(x1≤x2→ (x1)≤ (x2)), and ∀x(x2< (x)) This is a basic heo y o deal wi h he i e a ion o and o gua an- ee he usual p ope ies o he i e a ion o a nondec easing unc ion wi h a ΠF 0–de inable g aph. The basic ac s p o able in his heo y we e s a ed in [6]. Nex esul collec s oge he he ac s ha we shall need in he p esen con ex . P oposi ion 2. Fo each ∈ F he e exis s a o mula IT (z, x, y)∈ΣF 0 such ha he ollowing o mulas a e heo ems o IΣF 0: 1. IT (z, x, y1)∧IT (z, x, y2)→y1=y2. 2. (IT (0, x, y)↔x=y)∧(IT (1, x, y)↔ (x) = y). 3. IT (z+ 1, x, y)↔ ∃y0≤y(IT (z, x, y0)∧ (y0) = y). 4. IT (z, x, y)→ ∀z0< z ∃y0< y IT (z0, x, y0). 5. z≥1∧IT (z, x, y)→x2< y ∧z≤y. 6. z≥1∧x1≤x2∧IT (z, x1, y1)∧IT (z, x2, y2)→y1≤y2. 7 7. IT (z1, x, y0)∧IT (z2, y0, y)→IT (z1+z2, x, y). In wha ollows we use a mo e sugges i e no a ion and w i e z(x) = y ins ead o IT (z, x, y). De ini ion 4. We say ha ∈ F is a domina ing unc ion o e Ti , o each e m (x)o LF, he e exis s k∈ωsuch ha Tp o es ∀x( (x)≤ k(x+σ( ))) whe e σ( ) = c1+· · · +cmand c1, . . . , cma e all he cons an s occu ing in (x). Lemma 4. Le Tbe an ex ension o IΣF 0and le ∈ F be a (i e able non- dec easing) domina ing unc ion o e T. Then, o each e m (x1, . . . , xm) o LFwhose a iables a e among x1, . . . , xm, he e exis s k∈ωsuch ha T` (x1, . . . , xm)< k(x1+· · · +xm+σ( )). P oo . We p oceed by induc ion on e ms o LF. The mos in e es ing case occu s when (x1, . . . , xm) is a sum (o a p oduc ) o wo e ms, say 1(x1, . . . , xm) + 1(x1, . . . , xm). By induc ion hypo hesis, 1(~x)< k(x1+· · · +xm+σ( 1)) and 2(~x)< l(x1+· · · +xm+σ( 2)), o some k, l ∈ω. Wi hou loss o gene ali y we may assume k≥max(l, 2) (so, o e e y u, k(u)≥k≥2.) Then, (~x) = 1(~x) + 2(~x) < k(x1+· · · +xm+σ( 1)) + l(x1+· · · +xm+σ( 2)) ≤2 k(x1+· · · +xm+σ( )) ≤( k(x1+· · · +xm+σ( )))2 < k+1(x1+· · · +xm+σ( )). The emaining cases a e simila . Languages LFand he no ion o a domina ing unc ion a e ailo ed o deal wi h he si ua ion desc ibed in he ollowing lemma. Lemma 5. Le Γ = {θ1(x, y), . . . , θm(x, y)}be a ini e se o ∆0– o mulas wi h only wo ee a iables. Fo each j= 1, . . . , m, le ¯ θj(x, y)deno e he o mula ∀u≤x∃ ≤y θj(u, ). Le F={ 1, . . . , m, }be a se o una y unc ion symbols and le Tbe he LF– heo y ex ending I∆0wi h he ollowing addi ional axioms: 8 •Fo each j= 1, . . . , m, ∀x( j(x) = y↔ ∃y0≤y(y0=µ . ¯ θj(x, )∧y= (x+ 1)2+y0)). • ∀x( (x) = (x+ 1)2+ 1(x) + · · · + m(x)). Then, Tex ends IΣF 0and is a domina ing unc ion o e T. P oo . I is s aigh o wa d o check ha each h∈ F is an i e able nonde- c easing unc ion o e T. In addi ion, by p oposi ion V.1.3 o [8], Tp o es ΣF 0–induc ion. Thus we only mus show ha is a domina ing unc ion o e T. This ac can be p o ed by induc ion on e ms o LF. Again, he mos in e es ing case occu s when (x) is a p oduc (o sum) o wo e ms, say 1(x)· 2(x). By induc ion hypo hesis, 1(x)≤ k(x+σ( 1)) and 2(x)≤ l(x+σ( 2)), o some k≥max(l, 2) (so, o e e y u, k(u)≥k≥2.) Then, (x)≤( 1(x) + 2(x))2≤ ( 1(x) + 2(x)) ≤ ( k(x+σ( 1)) + l(x+σ( 2))) ≤ (2 · k(x+σ( ))) ≤ (( k(x+σ( )))2)≤ k+2(x+σ( )). The emaining cases a e simila . As a inal s ep in he analysis o (Σ2,K2)–IR and due o echnical easons, i will be con enien o deno e he Σ2–de inable elemen s by closed e ms o an ex ended language. This mo i a es he in oduc ion o he ollowing local induc ion ules. De ini ion 5. Fo each se o o mulas Γand each se o closed e ms Λo LFwe conside he ules (whe e ϕ(x)∈Γand ∈Λ): (Γ,Λ)–IR :ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)) ϕ( ) (Γ,Λ)–IR0:∀x(ϕ(x)→ϕ(x+ 1)) ϕ(0) →ϕ( ) These ules we e i s conside ed and in ensi ely s udied in [6]. The e we p o ed ha a numbe o esul s on classical induc ion ules a e also ue o he local ones. In wha ollows, we s a e wo o hese esul s ha will be needed in he p esen pape . Fo he es o he sec ion, we assume ha 9 4. P o ably To al Compu able Func ions o IΠ− 2 We a e now in a posi ion o gi e a p oo ha R(IΠ− 2) = PR. Fi s ly, we need a e sion o Theo em 2 in he language o i s –o de A i hme ic. Lemma 9. IΣ1ex ends I∆0+ (Σ2,K2)–IR. P oo . Le A|=IΣ1and ϕ(x)∈Σ2such ha (•)I∆0+ (Σ2,K2)–IR `ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)). We mus show ha o e e y δ(u)∈Σ− 2, (?)A|=∀x1∀x2(δ(x1)∧δ(x2)→x1=x2)→ ∀x(δ(x)→ϕ(x)). By (•) he e exis o mulas ϕ1(x), . . . , ϕ (x)∈Σ2and δ1(x), . . . , δ (x)∈Σ− 2 such ha I∆0plus he sen ences αj:∀x1∀x2(δj(x1)∧δj(x2)→x1=x2)→ ∀x(δj(x)→ϕj(x)) (j= 1, . . . , ) p o es ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)).Mo e p ecisely, o each j≤ , I∆0+^ 1≤i<j αi`ϕj(0) ∧ ∀x(ϕj(x)→ϕj(x+ 1)), and I∆0+V i=1 αi`ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)). Le E={j: 1 ≤j≤ , A|=¬∃xδj(x)}and, o each j∈E, le θj(x, y)∈Π0such ha ¬∃x δj(x) is equi alen o ∀x∃y θj(x, y). Le mbe he ca dinal o Eand le F={ 1, . . . , m, }be a se o new una y unc ion symbols. F om he se o Σ0 o mulas Γ = {θj(x, y) : j∈E}, we de ine a heo y Tas in Lemma 5. Le L(A) deno e he language ob ained by adding o La cons an symbol a, o each a∈A. Pu T0=T+DΠ1(A), whe e DΠ1(A) is he Π1–diag am o A. Le Λ be he se o closed e ms o L(A) con aining only cons an s o he o m a o a∈ K2(A). Then Ahas a na u al expansion AF o he language LF∪ L(A) such ha AF|=T0+IΣF 1. By Theo em 2, AF|=T0+ (ΣF 2,Λ)–IR. Gi en δ(x)∈Σ− 2, we dis inguish se e al cases: I A|=¬∃x δ(x) hen (?) ob iously holds. On he o he hand, i A|= ¬∀x1∀x2(δ(x1)∧δ(x2)→x1=x2), since his is a Σ2–sen ence and T0ex ends DΠ1(A), T0` ¬∀x1∀x2(δ(x1)∧δ(x2)→x1=x2). So, T0` ∀x1∀x2(δ(x1)∧δ(x2)→x1=x2)→ ∀x(δ(x)→ϕ(x)). 16 In ha way (?) holds again. We mus deal wi h a las case: A|=∃!x δ(x). Then he e exis s d∈ K2(A) such ha A|=δ(d) and d∈Λ. In o de o e i y (?) i is enough o show ha T0+ (ΣF 2,Λ)–IR `ϕ(d). We p o e, by induc ion on j, ha o all j= 1, . . . , ,T0+ (ΣF 2,Λ)–IR ` αj.Le j≤ , and assume ha T0+ (ΣF 2,Λ)–IR `V1≤i<j αi. Then (•)jT0+ (ΣF 2,Λ)–IR `ϕj(0) ∧ ∀x(ϕj(x)→ϕj(x+ 1)). I j∈Eo A|=¬∀x1∀x2(δj(x1)∧δj(x2)→x1=x2) hen, easoning as in p e ious cases, we conclude ha T0`αj. I A|=∃!x δj(x), hen he e exis s b∈ K2(A) such ha A|=δj(b) and b∈Λ. Using (•)jwe ob ain T0+ (ΣF 2,Λ)–IR `ϕj(b). The e o e, T0+ (ΣF 2,Λ)–IR ` ∃x(δj(x)∧ϕj(x)), and i ollows ha T0+ (ΣF 2,Λ)–IR `αj, as equi ed. We ha e p o ed ha T0+ (ΣF 2,Λ)–IR `V j=1 αjand so T0+ (ΣF 2,Λ)–IR `ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)). Thus, T0+ (ΣF 2,Λ)–IR `ϕ(d) and, as a consequence, (?) holds. Nex heo em ex ends a p e ious conse a ion esul ob ained in [4] and, as a di ec co olla y, yields he cha ac e iza ion o he p. .c. . o IΠ− 2. Theo em 3. IΠ− 2is Π3–conse a i e o e IΣ1. P oo . Le θbe a Π3sen ence p o able in IΠ− 2. Then I(Σ2,K2)`θby Lemma 1 and IΣ− 1+(Σ2,K2)–IR `θby P oposi ion 1. We need he ollowing ac : Claim 2. IΣ− 1+ (Σ2,K2)–IR ≡IΣ− 1+ (I∆0+ (Σ2,K2)–IR). P oo o Claim: Each axiom o IΣ− 1is a Σ3sen ence, so i is enough o p o e ha o e e y σ0(u)∈Π2, [I∆0,(Σ2,K2)–IR] + ∃u σ0(u) ex ends [I∆0+∃u σ0(u),(Σ2,K2)–IR]. Assume I∆0+∃u σ0(u)`ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)), whe e ϕ(x)∈Σ2, and le ψ(x, u)∈Σ2be σ0(u)→ϕ(x). Then, I∆0p o es ψ(0, u)∧ ∀x(ψ(x, u)→ψ(x+ 1, u)) 17 and, he e o e, [I∆0,(Σ2,K2)–IR] `Uδ→ ∀x(δ(x)→ψ(x, u)), whe e δ(x)∈ Σ− 2and Uδdeno es he sen ence ∀x1∀x2(δ(x1)∧δ(x2)→x1=x2).Then [I∆0,(Σ2,K2)–IR] also p o es ∃u σ0(u)→(Uδ→ ∀x(δ(x)→ϕ(x))) and so [I∆0,(Σ2,K2)–IR] + ∃u σ0(u)`Uδ→ ∀x(δ(x)→ϕ(x)), as equi ed. I ollows om Claim and Lemma 9 ha IΣ1implies IΣ− 1+ (Σ2,K2)–IR and, he e o e, IΣ1`θ. Co olla y 3. The class o p o ably o al compu able unc ions o IΠ− 2is he class o p imi i e ecu si e unc ions. 5. Rela i iza ion and Concluding Rema ks I is na u al o ask ou sel es whe he Theo em 3 is also ue o IΠ− n+1 and IΣn o an a bi a y n≥1. We ha e al eady seen ha he educ ion o IΠ− n+1 o IΣ− n+(Σn+1,Kn+1)–IR wo ks o all nand i is immedia e o check ha he claim in he p oo o Theo em 3 can be gene alized oo. Thus, he key poin is o p o e ha Lemma 9 also holds o n > 1, i.e. o p o e ha IΣnimplies IΣn−1+(Σn+1,Kn+1)–IR o all n≥1. Ou p oo o Lemma 9 o n= 1 leans upon Theo em 2 educing (ΣF 2,Λ)–IR o IΣF 1. In e es ingly, he esul o n > 1 can also be de i ed om Theo em 2 by using some s anda d ela i iza ion echniques. Building on p e ious wo k o Kaye [9], in [7] i is shown ha , o each n≥1, he e is a Πn– o mula y=Kn(x) sa is ying ha (a) IΣn≡I∆0+∀x∃!y(y=Kn(x)), (b) y=Kn(x) is i e able and non dec easing o e IΣn, and (c) ini ial segmen s o A|=IΣnclosed unde unc ion y=Kn(x) a e Πn– elemen a y subs uc u es o A. Using unc ions Knone can e o mula e IΣnas a ΠF 1– heo y in an ex- ended language L ∪ {g1, . . . , gn}so ha Σn+m o mulas o Lco espond o ΣF m o mulas o he ex ended language (a simila ea men o ela i iza ion was also de eloped by Z. Ra ajczyk in [11] ia he no ion o a condi ionally absolu e o mula.) Lemma 10. Le n≥1and le F={g1, . . . , gn}. The e is a ΠF 1– heo y Tn sa is ying ha 18 1. Tnex ends IΣn, 2. e e y model o IΣnhas a (canonical) ex ension o a model o Tn, 3. e e y ΣF m o mula is equi alen in Tn o a Σn+m– o mula o L, and 4. e e y Σn+m o mula is equi alen in Tn o a ΣF m– o mula. P oo . (Ske ch) n= 1: Pu T1≡IΣF 0+ (y=g1(x)→y=K1(x)). Condi ions (1), (2) and (3) a e easy o e i y, o we know ha allowing mono one unc ions ins ead o only a iables as he bounds in ΣF 0 o mulas does no inc ease he s eng h o ΣF 0–induc ion (see, e.g. p oposi ion V.1.3 o [8]). As o (4), since IΣ1con ains he s ong collec ion scheme o Π0– o mulas ∀z∃u∀x≤z(∃y ϕ(x, y)→ ∃y≤u ϕ(x, y)), by a Pa ikh–like a gumen (a ailable hanks o condic ion (c) abo e) i ol- lows ha o each θ(~x, y)∈Π0 he e is some k∈ωsuch ha IΣ1` ∃y θ(~x, y)↔ ∃y≤Kk 1(x1+. . . +xp)θ(~x, y), and he esul ollows. n→n+ 1: Le y=K0 n+1(x) deno e a ΠF 1– o mula equi alen in Tn o y= Kn+1(x) and pu Tn+1 ≡Tn+ (y=gn+1(x)→y=K0 n+1(x)). Equipped wi h his esul , i is no ha d o check ha e e y hing in he p oo o Lemma 9 ela i izes. Indeed, le n≥2 and suppose Ais a model o IΣnand ϕ(x) is in Σn+1. As in Lemma 9 le δ1(x), . . . , δ (x) be he Σ− n+1– o mulas occu ing in a p oo o ϕ(0) ∧ ∀x(ϕ(x)→ϕ(x+ 1)) in IΣn−1+ (Σn+1,Kn+1)–IR. Le E={j: 1 ≤j≤ , A|=¬∃xδj(x)}and le F={ 1, . . . , m, g1, . . . , gn−1, }, whe e mis he ca dinal o E. Fo each j∈E, le θ0 j(x, y)∈ΠF 0such ha ¬∃x δj(x) is equi alen in Tn−1 o ∀x∃y θj(x, y). F om his se o ΣF 0 o mulas de ine a ΠF 1– heo y Tex ending Tn−1as in Lemma 5. Finally, pu T0≡T+DΠg 1(A), whe e DΠg 1(A) is he Π1–diag am o Ain he language o Tn−1, and ake Λ = Kn+1(A). Then, A|=T0+IΣF 1. So, applying Theo em 2 and easoning as in Lemma 9 we ge A|=IΣn−1+ (Σn+1,Kn+1)–IR, as desi ed. Thus, we ha e Theo em 4. Fo e e y n≥1,IΠ− n+1 is Πn+2–conse a i e o e IΣn. 19 A s aigh o wa d consequence o his esul is a cha ac e iza ion o he class o p. .c. . o IΠ− n+1 in e ms o he ex ended G zego czyk Hie a chy {Eα:α < ε0}, see [12] o p ecise de ini ions. Co olla y 4. Fo e e y n≥1,R(IΠ− n+1) = R(IΣn) = Eωn, whe e ω0= 1, ωn+1 =ωωn. An impo an ing edien in his analysis o he class o Πn+2–consequences o IΠ− n+1 is he s udy o he closu e a weak heo y, such as IΣ− n(o e en I∆0), unde (Σn+1,Kn+1)–IR. This analysis can be ex ended o s onge base heo ies p o iding us wi h simila conse a ion esul s o heo ies o he o m T+IΠ− n+1, whe e Tis a Πn+2–axioma izable ex ension IΣn. In he ollowing p oposi ion we ob ain his kind o conse a ion esul s when Tis closed unde Σn+1–collec ion ule: Σn+1–CR : ∀x∃y ϕ(x, y) ∀u∃ ∀x≤u∃y≤ ϕ(x, y) o ϕ(x, y)∈Σn+1. P oposi ion 4. Le Tbe a Πn+2–axioma izable ex ension o IΣn, closed unde Σn+1–CR. Then: 1. T+IΠ− n+1 is Πn+2–conse a i e o e [T, Σn+1–IR] 2. T+IΠ− n+1 is Πn+1–conse a i e o e T+ Πn+1–IR. P oo . These esul s we e p o ed o n= 0 in [6]. The p oo o n≥1 is e y simila , modulo ela i iza ion. He e we discuss he p oo o n= 1. (1) Fi s o all, le us ecall ha , o e IΣ1,IΠ− 2≡I(Σ− 2,K2) and ha , by P oposi ion 1, T+I(Σ2,K2) is Π3–conse a i e o e T+ (Σ2,K2)–IR. So i is enough o show ha [T, Σ2–IR] ex ends his las heo y. Bu obse e ha (•)T+ (Σ2,K2)–IR ≡[T, (Σ2,K2)–IR]. This can be ob ained om Lemma 6, by using he ela i iza ion de ice ha we ha e de eloped (see he p oo o lemma 3.7 in [6] o de ails). By (•), [T, Σ2–IR] ob iously ex ends T+ (Σ2,K2)–IR and he esul ollows. (2) By pa (1) i su ices o show ha [T, Σ2–IR] is Π2–conse a i e o e T+ Π2–IR. By p oposi ion 2.1 o [2], [T, Σ2–IR] is equi alen o [T, Π2–IR0] and i is s aigh o wa d o show (using Lemma 3) ha e e y Σ2–closed model o T+ Π2–IR is a model o [T, Π2–IR0]. By Lemma 2 i ollows ha [T, Π2–IR0] is Π2–conse a i e o e T+ Π2–IR, as equi ed. 20 The in e es o P oposi ion 4 is wo old. On he one hand, pa (1) p o ides a gene aliza ion o a simila esul ob ained in [10]: Theo em 5 (Kaye–Pa is–Dimi acopoulos). IΠ− 1is Π2–conse a i e o e I∆0+ exp (≡[I∆0,Σ1–IR]). We can hink o his esul as a coun e pa o Theo em 4 o IΠ− 1. How- e e , a gene aliza ion o Theo em 5 o e e y n≥1 mus ake in o conside a- ion wo di e en scena ios, since I∆0≡I∆− 0, bu IΣnis a p ope ex ension o IΣ− n. Toge he P oposi ion 4 and Theo em 4 show ha bo h gene aliza- ions a e co ec . Fo T=IΣn, P oposi ion 4 shows ha Theo em 5 also holds o e e y n≥1 (essen ially, his esul was ob ained by Kaye in [9]): Co olla y 5. IΣn+IΠ− n+1 is Πn+2–conse a i e o e [IΣn,Σn+1–IR]. In u n, Theo em 4 shows ha his co olla y also holds o IΣ− n, since o e e y n≥1, IΣn≡[IΣ− n,Σn+1–IR] and, ob iously IΠ− n+1 ex ends IΣ− n. On he o he hand, P oposi ion 4 educes he ques ion abou he class o p. .c. . o IΣ1+IΠ− 2 o he s udy o he closu e o IΣ1unde Π2–IR. In a simila ein, by combining pa s (1) and (2), we ob ain ha , o e e y k≥1, [IΣ1,Σ2–IR]k+1 is Π2–conse a i e o e [IΣ1,Σ2–IR]k+ Π2–IR. These educ ions sugges ha local induc ion can be a use ul ool in ob aining new p oo s o some o he al eady known cha ac e iza ions o classes o p. .c. . in e ms o he ex ended G zego czyk hie a chy; o ins ance, R(IΣ1+IΠ− 2) (s udied by Beklemishe in [4]), R([IΣ1,Σ2–IR]k) o R(IΣ2) and, mo e gen- e ally, R(IΣn+IΠ− n+1) and R(IΣn). This poin s ou na u al ex ensions o he esul s and me hods we ha e in oduced in his pape . Acknowledgemen This wo k was pa ially suppo ed by g an s MTM2008–06435 and MTM2011– 26840 o Minis e io de Ciencia e Inno aci´on, Spain. Co inanced wi h FEDER unds, EU. Re e ences [1] A igad, J. Sa u a ed models o uni e sal heo ies. Annals o Pu e and Applied Logic, 118 (2002) 219–234. 21 [2] Beklemishe , L.D. Induc ion ules, e lec ion p inciples and p o ably ecu si e unc ions. Annals o Pu e and Applied Logic, 85 (1997) 193– 242. [3] Beklemishe , L.D. A p oo – heo e ic analysis o collec ion. A chi e o Ma hema ical Logic, 37 (1998) 275–296. [4] Beklemishe , L.D. Pa ame e ee induc ion and p o ably o al com- pu able unc ions. Theo e ical Compu e Science, 224 (1999) 13-33. [5] Buss, S. The Wi ness Func ion Me hod and P o ably Recu si e Func- ions o Peano A i hme ic, in: D. Wes e ahl, D. P awi z, B. Sky ms (Eds.), P oceedings o he 9 h. In e na ional Cong ess on Logic, Me hod- ology and Philosophy o Science, Else ie , No h–Holland, Ams e dam, (1994) 29–68. [6] Co d´on–F anco, A.; Fe n´andez–Ma ga i , A.; La a–Ma ´ın, F. F. On conse a ion esul s o pa ame e – ee Πn–induc ion. In S udies in Weak A i hme ics, Pa ick C´egielski (edi o ). CSLI Publica ions, S an- o d, Cali o nia (2010) 49–97. [7] Fe n´andez–Ma ga i , A.; La a–Ma ´ın, F.F. Induc ion, Minimiza ion and Collec ion o ∆n+1(T)– o mulas. A chi e o Ma hema ical Logic, 43 (2004) 505–542. [8] H´ajek, P.; Pudl´ak, P. Me ama hema ics o Fi s –O de A i hme ic. Pe - spec i es in Ma hema ical Logic, Sp inge Ve lag, 1993. [9] Kaye, R. Diophan ine and Pa ame e – ee Induc ion. Ph.D. Uni e si y o Manches e , 1987. [10] Kaye, R.; Pa is, J; Dimi acopoulos, C. On pa ame e ee induc ion schemas. The Jou nal o Symbolic Logic, 53 (1988) 1082–1097. [11] Ra ajczyk, Z. Func ions p o ably o al in I−Σn. Fundamen a Ma he- ma icae, 132 (1989) 81–95. [12] Rose, H. E. Sub ecu sion. Func ions and hie a chies. Ox o d Logic Guides 9. Cla endon P ess, Ox o d, 1984. [13] Sieg, W. He b and Analyses. A chi e o Ma hema ical Logic, 30 (1991) 409–441. 22 [14] Zambella, D. No es on polynomial bounded a i hme ic. Jou nal o Sym- bolic Logic, 61 (1996) 942–966. 23