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