Local Induc ion and P o ably To al Compu able
Func ions: A Case S udy
And ´es Co d´on–F anco and F. F´elix La a–Ma ´ın
Depa amen o Ciencias de la Compu aci´on e In eligencia A i icial, Facul ad de
Ma em´a icas. Uni e sidad de Se illa, C/ Ta ia, s/n, 41012 Se illa, Spain
{aco don, la a}@us.es
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. An-
swe ing a ques ion o R. Kaye, L. Beklemishe showed ha he p o ably
o al compu able unc ions (p. .c. .) 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 he p. .c. . o ce ain local e sions o induc ion p inciples
closely ela ed o IΠ−
2. This analysis is essen ially based on he equi a-
lence be ween local induc ion ules and es ic ed o ms o i e a ion. 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 .
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 :IN
k→IN is 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 :
1. ϕde ines he g aph o in he s anda d model o A i hme ic IN; and
2. T∀x ∃!yϕ(x, y).
Obse e ha condi ion 1. amoun s o he compu abili y o , whe eas condi ion
2. yields an implici measu e o he complexi y o a ending o he logical
p inciples needed o p o e ha a Σ1–de ini ion o de ines a o al unc ion. 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Σ1 equals 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 [9], S. Buss’ wi nessing me hod [5]
o , in gene al, p oo – heo e ic echniques using Cu elimina ion heo em. How-
e 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Σ1is Σ3–
conse a i e o e IΣ−
1[8], 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 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)=PRwill 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 imi 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 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Π−
2is Π2(in ac , Π3)
conse a i e o e he co esponding in e ence ule e sion (Σ2,K2)–IR. Then,
we show ha applica ions o (Σ2,K2)–IR co espond 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.
Ou analysis also yields a new conse a ion heo em o agmen s o Peano
A i hme ic, which is o independen in e es . Namely, we p o e ha IΠ−
2is Π3–
conse a i e o e IΣ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 combina-
ions o Σ2–sen ences was es ablished.
We close his sec ion by gi ing a p ecise de ini ion o he auxilia y scheme
ha will be cen al in ou analysis o he class o p. .c. . o IΠ−
2.
Le L={0,S,+,·,<}deno e he language o i s o de A i hme ic. I Γis
a se o o mulas o L, henIΓ 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)∈Γ−.
De ini ion 1. I(Σ2,K2)is he heo y gi en by IΣ−
1 oge he wi h he scheme
ϕ(0) ∧∀x(ϕ(x)→ϕ(x+1))→
→∀x1,x
2(δ(x1)∧δ(x2)→x1=x2)→∀x(δ(x)→ϕ(x))
whe e ϕ(x)∈Σ2and δ(x)∈Σ−
2. The na u al in e ence ule associa ed o his
scheme, deno ed (Σ2,K2)–IR, is gi en by:
ϕ(0) ∧∀x(ϕ(x)→ϕ(x+1))
∀x1,x
2(δ(x1)∧δ(x2)→x1=x2)→∀x(δ(x)→ϕ(x))
whe e δ(x)∈Σ−
2and ϕ(x)∈Σ2. Finally, i we es ic he scheme o ϕ(x)∈
Σ−
2, we ob ain he pa ame e ee coun e pa o I(Σ2,K2),deno edI(Σ−
2,K2).
Rema k 1. Fi s ly, le us ecall ha , gi en a model A,K2(A) deno es he se
o elemen s o A ha a e de inable in Aby a o mula δ(x)∈Σ2. This explains
why K2appea s in ou no a ion o hese heo ies. Secondly, i A|=IΣ−
1, hen
K2(A)≺2A(i.e., K2(A)isaΠ2–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 I(Σ2,K2)is
axioma ized o e IΣ−
1ins ead o o e a weake sys em (such as Qo IΔ0).
A key ac is ha I(Σ−
2,K2) p o ides an al e na i e o mula ion o IΠ−
2:
Lemma 2. IΠ−
2≡I(Σ−
2,K2).
P oo . We only p o e ha I(Σ−
2,K2) ex ends IΠ−
2. The con e se is simila . Le
A|=I(Σ−
2,K2)andϕ(x)∈Π−
2such ha A|=ϕ(0) ∧∀x(ϕ(x)→ϕ(x+ 1)).
Assume A|=∃x¬ϕ(x). Since A|=IΣ−
1,K2(A)≺2Aand he e is a∈K
2(A)
such ha A|=¬ϕ(a). Le δ( )beaΣ2 o mula de ining he elemen aand le
θ(x)be∃ (δ( )∧¬ϕ( −x)). Clea ly, A|=θ(0) ∧∀x(θ(x)→θ(x+ 1)). By
I(Σ−
2,K2), A|=θ(a)andsoA|=¬ϕ(0), which is a con adic ion.
Gi en a heo y Tand an in e ence ule R,wedeno eby[T,R] he closu e o T
unde i s o de logic and unnes ed applica ions o R.Wedeno ebyT+R he
closu e o Tunde i s o de logic and (nes ed) applica ions o R. The e o e,
T+R=k∈ω[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) oa
agmen de ined by he ule (Σ2,K2)–IR. Indeed, we ha e:
P oposi ion 3. I(Σ2,K2)is Π3–conse a i e o e IΣ−
1+(Σ2,K2)–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, in [6], lemma 3.6, we ga e a model– heo e ic p oo o his esul
using he no ion o a Σn+1–closed model, ollowing he me hods in oduced by
A igad in [1].
2 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 shall 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 4. Le ∈Fa una y unc ion symbol and Tan 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,x
2(x1≤x2→ (x1)≤ (x2)),and ∀x(x2< (x))
Le Σ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 Qby
–The induc ion axiom Iϕ o each o mula ϕ∈ΣF
0,and
–Axioms o each ∈F:
∀x1,x
2(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 5. Fo each ∈F he e exis s a o mula IT (z,x,y)∈ΣF
0such
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<yIT
(z0,x,y
0).
5. z≥1∧IT (z,x,y)→x2<y∧z≤y.
6. z≥1∧x1≤x2∧IT (z,x1,y
1)∧IT (z,x2,y
2)→y1≤y2.
7. IT (z1,x,y
0)∧IT (z2,y
0,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)=yins ead
o IT (z,x,y).
De ini ion 6. We say ha ∈F is a domina ing unc ion o e Ti , o any
e m (x)o LF, he eexis sk∈ωsuch ha Tp o es
∀x( (x)≤ k(x+σ( )))
whe e σ( )=c1+···+cmand c1,...,c
ma e all he cons an s occu ing in (x).
Lemma 7. Le Tbe an ex ension o IΣF
0and le ∈Fa (i e able nonde-
c easing) domina ing unc ion o e T. Then, o each e m (x1,...,x
m)o LF
whose a iables a e among x1,...,x
m, he eexis sk∈ωsuch ha
T (x1,...,x
m)<
k(x1+···+xm+σ( )).
Rema k 2. Languages LFand he no ion o a domina ing unc ion a e ailo ed
o deal wi h he ollowing si ua ion. Assume Γ={θ1,...,θ
m}is a ini e se o
Σ0– o mulas wi h only wo ee a iables, say xand y,and o eachj=1,...,m,
¯
θj(x, y) deno es 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 ex ension o IΣF
0wi h he
ollowing addi ional axioms:
–Fo each j=1,...,m,∀x( j(x)=y↔∃y0≤y(¯
θj(x, y0)∧y=(x+1)2+y0).
–∀x( (x)=(x+1)
2+ 1(x)+···+ m(x)).
Then, e e y h∈Fis an i e able nondec easing unc ion o e Tand is a
domina ing unc ion o e T. This las ac can be p o ed by induc ion on e ms.
The mos in e es ing case occu s when (x) is a p oduc o wo e ms, 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+σ( ))
and we conclude ha (x)≤ 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 8. Fo each se o o mulas Γand each se o closed e ms Λ0o
LFwe conside he ules (whe e ϕ(x)∈Γand ∈Λ0):
(Γ, Λ0)–IR :ϕ(0) ∧∀x(ϕ(x)→ϕ(x+1))
ϕ( )
(Γ, Λ0)–IR0:∀x(ϕ(x)→ϕ(x+1))
ϕ(0) →ϕ( )
De ini ion 9. We say ha Λ0is exponen ially closed o e Ti o e e y , s ∈
Λ0 he e exis s ∈Λ0such ha [T,(ΣF
1,Λ
0)–IR]∃y≤ (s =y).

These ules we e in ensi ely s udied in [6], whe e he ollowing esul s we e
ob ained. F om now on, we assume ha Tis a ixed ex ension o IΣF
0ob ained
by adding a se o ΠF
1sen ences, and Λ0deno es he se o all closed e ms o
a sublanguage o LFex ending Land con aining he se o cons an s C(and so
Λ0is closed unde sum and p oduc ).
Rema k 3. Le us no e ha unde hese assump ions Tsa is ies a na u al e sion
o Pa ikh’s heo em (see [7], chap e 5, heo em 1.4). This ac will be used
ex ensi ely wi hou u he commen s.
In addi ion, we assume ha he e is ∈L
Fa domina ing unc ion o e Tand
Λ0is exponen ially closed o e T. Then, we ha e (see lemma 4.8, lemma 4.10
and heo em 4.14 o [6]):
P oposi ion 10. T+(ΠF
2,Λ
0)–IR ≡T+{∀x∃y( (x)=y): ∈Λ0}.
Theo em 11. T+(ΠF
2,Λ
0)–IR0is ΠF
2–conse a i e o e T+(ΠF
2,Λ
0)–IR.
He e we ex end ou wo k in [6] and ob ain a new heo em on hese local induc ion
sys ems ha will be c ucial o de i e ou main esul . The ideas in ol ed a e
simila o he ones used in [6] o ob ain P oposi ion 10 and Theo em 11.
Theo em 12. T+IΣF
1ex ends T+(ΣF
2,Λ
0)–IR.
P oo . The a gumen s used in [2], p oposi ion 2.1, can be easily adap ed o yield
ha o e e y k∈ω,[T,(ΣF
2,Λ
0)–IR]k≡[T,(ΠF
2,Λ
0)–IR0]k.So i is enough o
p o e ha o e e y k∈ω,T+IΣF
1ex ends [T,(ΠF
2,Λ
0)–IR0]k. We p oceed
by induc ion on k∈ω:
Case k= 0 is i ial; so, le us assume ha T+IΣF
1ex ends [T,(ΠF
2,Λ
0)–IR0]k.
Le ∈Λ0and ϕ(u, )∈ΠF
2such ha
(†)[T,(ΠF
2,Λ
0)–IR]k∀u(ϕ(u, )→ϕ(u+1, )).
We mus p o e ha T+IΣF
1ϕ(0, )→ϕ( , ).
Wi hou loss o gene ali y, we can assume ha ϕ(u, )≡∀x∃yϕ
0(u, x, y, ),
wi h ϕ0(u, x, y, )∈ΣF
0.Le gbe a new una y unc ion symbol and Tg he
ex ension o T+IΣF,g
0ob ained by adding he sen ences:
∀x1,x
2(x1≤x2→g(x1)≤g(x2)),∀x(x2<g(x)) and ∀x( (x)≤g(x)).
Thus, gis a domina ing (i e able nondec easing) unc ion o e Tg.By(†), i
ollows ha [Tg,(ΠF,g
2,Λ
0)–IR]kϕg,whe eϕgis he ollowing sen ence:
∀u(∀x∃y≤g(x+u+ )ϕ0(u, x, y, )→∀x∃yϕ
0(u+1,x,y, )).
Claim. The e is a closed e m τ0∈Λ0such ha Tg+∀x∃y(gτ0(x)=y)p o es
∀u(∀x∃y≤g(x+u+ )ϕ0(u, x, y, )→∀x∃y≤gτ0(u+x+ )ϕ0(u+1,x,y, ))
P oo o Claim: We dis inguish wo cases:
Case 1:k=0.ThenTgϕg. Hence, by Pa ikh’s heo em, he e exis s a e m
s(u, x, )o LF,g such ha
Tg∀u(∀x∃y≤g(x+u+ )ϕ0(u, x, y, )→∀x∃y≤s(u, x, )ϕ0(u+1,x,y, ))
By Lemma 7, he e is m∈ωsuch ha Tgs(u, x, )<g
m(u+x+ +σ(s)).
By induc ion on zi can be p o ed ha
Tggu(x+z)=y1∧gu+z(x)=y2→y1≤y2
and, hus, i τ0=m+σ(s) henτ0∈Λ0and he esul ollows.
Case 2:k≥1. Since [Tg,(ΠF,g
2,Λ
0)–IR]kϕgand ϕgis a ΠF,g
2– o mula, by
Theo em 11, Tg+(ΠF,g
2,Λ
0)–IR also p o es ϕg. I ollows om P oposi ion 10
ha he e exis 1,...,
n∈Λ0such ha
Tg+{∀x∃y(g j(x)=y): j=1,...,n}ϕg.
Le = 1+···+ n. Then, by pa (4) o P oposi ion 5, Tg+∀x∃y(g (x)=y)
ex ends Tg+{g jis o al : j=1,...,n}.Le hbe a new una y unc ion
symbol and le Thbe he ex ension o Tgob ained by adding o Tg he axiom
∀x(g (x)=h(x)). Then Thϕgand This conse a i e o e Tg.
By P oposi ion 5, his an i e able nondec easing unc ion o e Thand Th
∀x(g(x)≤h(x)). The e o e, his a domina ing unc ion o e Thand Thex ends
IΣF,g,h
0. By Pa ikh’s heo em, he e is a e m s(u, x, )o LF,g,h such ha
Th∀u(∀x∃y≤g(x+u+ )ϕ0(u, x, y, )→∀x∃y≤s(u, x, )ϕ0(u+1,x,y, ))
and, by Lemma 7, he e is m∈ωsuch ha Ths(u, x, )<h
m(u+x+ +σ(s)).
Recall ha Thhu(x+z)=y1∧hu+z(x)=y2→y1≤y2and, hus, i
σ0=m+σ(s) henσ0∈Λ0and Th+∀x∃y(hσ0(x)=y)p o es
∀u(∀x∃y≤g(x+u+ )ϕ0(u, x, y, )→∀x∃y≤hτ0(u+x+ )ϕ0(u+1,x,y, ))
Using pa (7) o P oposi ion 5, we can p o e, by ΣF,g,h
0–induc ion, ha
Thhz(x)=y↔g ·z(x)=y
As a consequence, Th+∀x∃y(hσ0(x)=y)p o es
∀u(∀x∃y≤g(x+u+ )ϕ0(u, x, y, )→∀x∃y≤g ·σ0(u+x+ )ϕ0(u+1,x,y, ))
Hence, pu ing τ0= ·σ0∈Λ0, he esul ollows concluding he p oo o Claim.
Le A|=T+IΣF
1and c∈Asuch ha A|=ϕ(0,c). We shall show ha
A|=ϕ( , c). Le ψ(x, y, c)∈ΣF
0 he o mula
∀z≤x∃w≤y(ϕ0(0,z,w,c)∧y=w+ (x)).
Then A|=∀x∃yψ(x, y, c)and he o mulaψ(x, y, c)∧∀z<y¬ψ(x, z, c) de ines a
o al nondec easing unc ion H:A→A. The e is a ΣF
0 o mula, ha we deno e
by Hz(x)=y, de ining he i e a ion o Hand, since A|=IΣF
1,weha e
A|=∀x∀z∃y(Hz(x)=y).
Le θ(u, ) be he ollowing ΠF
1 o mula:
u> ∨∀x∀y1Hτu
0(x+u+ )=y1→∃y≤y1ϕ0(u, x, y, ).
Since A|=∀x∃y(H(x)=y), by de ini ion o θ(u, )weha eA|=θ(0, ). Le us
show ha A|=∀u(θ(u, )→θ(u+1, )).
Pick a, b ∈Asuch ha A|=a≤ ∧θ(a, b). Then, he o mula Hτa
0(x)=y
de ines a o al nondec easing unc ion in Aand we can use i o ge an expansion
o A o a model Ago Tgsuch ha Ag|=∀x∃y≤g(x+a+b)ϕ0(a, x, y, b).By
pa (7) o P oposi ion 5, we can p o e by ΣF,g
0–induc ion on z ha
Ag|=∀z≤τ0[gz(x+a+b)=Hτa
0·z(x+a+b)]
In pa icula , Ag|=∀x(gτ0(x+a+b)=Hτa
0·τ0(x+a+b)) and, as a consequence,
Ag|=Tg+∀x∃y(gτ0(x)=y). Hence, by he Claim, we conclude ha Ag|=
∀x∃y≤gτ0(x+a+b)ϕ0(a+1,x,y,b) and, he e o e, A|=θ(a+1,b).
We ha e shown ha A|=θ(0, )∧∀u(θ(u, )→θ(u+1, )), and we know
ha A|=IΠF
1(because IΣF
1≡IΠF
1), so, A|=∀uθ(u, b). In pa icula , since
A|=θ( , )→∀x∃y≤Hτ
0( +x+ )ϕ0( , x, y, ),
we conclude A|=ϕ( , ).
3MainResul
We a e now eady o ob ain he main esul s. Fi s ly, we need a e sion o
Theo em 12 in he language o i s –o de A i hme ic.
Lemma 13. 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+
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)∈Π0
such ha ¬∃xδ
j(x) is equi alen o ∀x∃yθ
j(x, y). Le m he ca dinal o Eand
le F={ 1,...,
m, }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 Rema k 2.
Le L(A) deno e he language ob ained by adding o La cons an symbol a, o
each a∈A.Pu T=T+DΠ1(A), whe e DΠ1(A)is heΠ1–diag am o A.Le
Λ0be he se o closed e ms o L(A) con aining only cons an s o he o m a
o a∈K
2(A). Then Ahas a na u al expansion AF o he language LF∪L(A)
such ha AF|=T+IΣF
1. By P oposi ion 12, AF|=T+(ΣF
2,Λ
0)–IR. Gi en
δ(x)∈Σ−
2, we can 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 Tex ends
DΠ1(A), we ha e ha T¬∀x1∀x2(δ(x1)∧δ(x2)→x1=x2). So,
T∀x1∀x2(δ(x1)∧δ(x2)→x1=x2)→∀x(δ(x)→ϕ(x)).
In ha way () holds again. We mus deal wi h a las case: A|=∃!xδ(x).
Then he e exis s d∈K
2(A) such ha A|=δ(d)andd∈Λ0.Ino de o
e i y () i is enough o show ha T+(ΣF
2,Λ
0)–IR ϕ(d).
We p o e, by induc ion on j, ha o all j=1,..., ,T+(ΣF
2,Λ
0)–IR αj.
Le j≤ , and assume ha T+(ΣF
2,Λ
0)–IR 1≤i<j αi.Then
(•)jT+(ΣF
2,Λ
0)–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 Tαj.I A|=∃!xδ
j(x), hen he e exis s
b∈K
2(A) such ha A|=δj(b)andb∈Λ0.Using(•)jwe ge T+(ΣF
2,Λ
0)–IR 
ϕj(b). As a consequence, T+(ΣF
2,Λ
0)–IR ∃x(δ(x)∧ϕj(x)), and i ollows
ha T+(ΣF
2,Λ
0)–IR αj, as equi ed.
We ha e p o ed ha T+(ΣF
2,Λ
0)–IR 
j=1 αj; hence
T+(ΣF
2,Λ
0)–IR ϕ(0) ∧∀x(ϕ(x)→ϕ(x+1))
I ollows ha T+(ΣF
2,Λ
0)–IR ϕ(d) and, as a consequence, ()holds.
Ou las 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 14. IΠ−
2is Π3–conse a i e o e IΣ1.
P oo . Le θbe a Π3sen ence p o able in IΠ−
2.ThenI(Σ2,K2)θby
Lemma 2 and IΣ−
1+(Σ2,K2)–IR θby P oposi ion 3. We need he
ollowing ac :