On axiom schemes o T-p o ably Δ1 o mulas
A. Co dón-F anco · A. Fe nández-Ma ga i ·
F. F. La a-Ma ín
Abs ac This pape in es iga es he s a us o he agmen s o Peano A i hme ic
ob ained by es ic ing induc ion, collec ion and leas numbe axiom schemes o o -
mulas which a e Δ1 p o ably in an a i hme ic heo y T . In pa icula , we de e mine
he p o ably o al compu able unc ions o his kind o heo ies. As an applica ion,
we ob ain a educ ion o he p oblem whe he I Δ0 +¬exp implies BΣ1 o a pu ely
ecu sion- heo e ic ques ion.
Keywo ds F agmen s o Peano A i hme ic · Δ1 o mulas ·
P o ably o al compu able unc ions
Ma hema ics Subjec Classi ica ion 03F30 · 03D20
1 In oduc ion
Among he subsys ems o i s o de Peano A i hme ic (PA), agmen s o Δ1- o -
mulas a e no comple ely unde s ood ye . A well-known p oblem posed by Pa is [6]
asks whe he , o e he heo y o bounded induc ion I Δ0, he induc ion p inciple o
Δn- o mulas I Δn and he collec ion p inciple o Σn- o mulas BΣn a e equi alen .
By a esul o R. Gandy (unpublished, see [12]), BΣn is equi alen o he leas
numbe p inciple o Δn- o mulas LΔn. Hence, Pa is’ ques ion can be e o mula ed
as asking whe he I Δn and LΔn a e equi alen . In 2004 Slaman [21] ob ained a
pa ial answe
o he p oblem. He p o ed IΔnand BΣn o be equi alen o e IΔ0+exp, whe e exp
is he axiom asse ing he o ali y o he exponen ial unc ion. Since IΔ2p o es exp,
his answe ed he p oblem comple ely o each n≥2. As o he case n=1, building
on Slaman’s wo k Thapen [23] showed ha BΣ1is p o able om IΔ1plus a e y
weak o m o exponen ia ion: “ o all x,xyexis s o some ysuch ha x<p(y)”,
whe e pcan be any p imi i e ecu si e unc ion. (An al e na i e p oo o his esul
was gi en in [20]). Howe e , he p oblem o p o ing o disp o ing he equi alence
o e IΔ0 o n=1 is s ill pending.
Mo i a ed by his ques ion, we ini ia ed in [11] and [7] he s udy o agmen s o
PA o o mulas ha a e Δ1p o ably in an ex e nal heo y T. Mo e p ecisely, le Tbe
an ex ension o IΔ0in he language o a i hme ic. The heo y IΔ1(T)is axioma ized
o e Robinson’s Qby he axiom scheme
(Iϕ)ϕ(0, )∧∀x(ϕ(x, )→ϕ(x+1, )) →∀xϕ(x, ),
whe e ϕ(x, )∈Δ1(T), i.e., ϕ(x, )∈Σ1and he e is some ψ(x, )∈Π1such ha
T∀x, (ϕ(x, )↔ψ(x, )). The heo y LΔ1(T)is Q oge he wi h
(Lϕ)∃xϕ(x, )→∃x(ϕ(x, )∧∀y<x¬ϕ(y, )),
whe e ϕ(x, )∈Δ1(T). The heo y BΔ1(T)consis s o IΔ0plus
(Bϕ)∀x∃yϕ(x,y, )→∀z∃u∀x≤z∃y≤uϕ(x,y, ),
whe e ϕ(x,y, )∈Σ1and T∀x∃yϕ(x,y, )(so ∃yϕ(x,y, )∈Δ1(T)).
A a ian o Pa is’ p oblem hen a ises: Fo which heo ies T does he equi alence
IΔ1(T)≡LΔ1(T)hold?
Besides his o iginal mo i a ion, Δ1(T)-schemes ha e u ned ou o be in e es ing
subsys ems o PA in hei own igh . On he one hand, Δ1(T) o mulas appea na u-
ally in he s udy o agmen s o PA, ema kably in connec ion wi h he compu able
unc ions p o ably o al in T. In ac , as we shall show in his pape , Δ1(T)-schemes
exhibi a nice compu a ional beha io : i is possible o gi e nea cha ac e iza ions o
hei p o ably o al unc ions by means o some sub ecu si e ope a o s. On he o he
hand, Δ1(T)-schemes a e closely ela ed o heo ies o a i hme ic desc ibed in e ms
o in e ence ules. In ac , T+IΔ1(T)coincides wi h he closu e o Tunde unnes ed
applica ions o he Δ1-induc ion ule [T,Δ
1-IR]. E en mo e, IΔ1(T)p ecisely iso-
la es he amoun o induc ion axioms added o Tby unnes ed applica ions o Δ1-IR.
Simila ema ks apply o LΔ1(T)and BΔ1(T)conside ing he Δ1-minimiza ion ule
Δ1-LR and he Σ1-collec ion ule Σ1-CR, espec i ely.
In his wo k we go a s ep u he and show ha , as a ma e o ac , Δ1(T)-schemes
can be ully cha ac e ized as he in e sec ion be ween a “classic” scheme o Σ1- o -
mulas and an in e ence ule heo y. Mo e p ecisely, le ThΓ(T)deno e he se o all
Γ-consequences o a heo y T. Then, o each sen ence ϕwe ha e
IΔ1(T)ϕi , and only i , bo h IΣ1ϕand [ThΠ2(T), Δ1-IR]ϕ;
LΔ1(T)ϕi , and only i , bo h IΣ1ϕand [ThΠ2(T), Δ1-LR]ϕ;
BΔ1(T)ϕi , and only i , bo h BΣ1ϕand [ThΠ2(T), Σ1-CR]ϕ.
Thus, he s udy o Δ1(T)-schemes can be educed o in es iga ing how he p op-
e ies o wo heo ies a e ans e ed o he heo y gi en by he in e sec ion o hei
heo ems. Using his me hodology we shall ob ain a comple e desc ip ion o he p oo -
heo e ic and compu a ional p ope ies o Δ1(T)-schemes.
No ably:
•We show ha Slaman’s heo em ans e s o he p esen con ex and p o e ha
IΔ1(T)and LΔ1(T)a e equi alen o e e y Tex ending IΔ0+exp.
•In s udying pa ame e ee Δ1(T)-schemes we in oduce pa ame e ee Δ1- ules
Δ−
1-IR and Δ−
1-LR ( o ou bes knowledge, conside ed he e o he i s ime) and
ob ain a conse a ion esul , which is o independen in e es . Namely, i T⊆Π2
hen [T,Δ
1-IR]and [T,Δ
1-LR]a e conse a i e o e hei pa ame e ee coun-
e pa s wi h espec o Σ2-sen ences.
•We de e mine he p o ably o al compu able unc ions (p. .c. .) o IΔ1(T)and o
LΔ1(T) o an a bi a y Tex ending IΔ0. We show ha he p. .c. .’s o LΔ1(T)
a e, p ecisely, he closu e unde composi ion and he bounded minimiza ion ope -
a o o he p. .c. .’s o Twhich a e p imi i e ecu si e. Fo IΔ1(T)we ob ain
a simila esul in e ms o he sea ch ope a o in oduced in [5]. In addi ion,
in p esence o exp we gi e al e na i e and pa icula ly nea cha ac e iza ions by
means o a sui ably modi ied e sion o he bounded ecu sion ope a o , ha we
call C-bounded ecu sion.
•We ob ain a educ ion o he well-known p oblem whe he IΔ0+¬exp implies
BΣ1( o sho , he NE P oblem) aised by Wilkie and Pa is [24] o a pu ely ecu -
sion- heo e ic ques ion. Namely, BΣ1is no p o able om IΔ0+¬exp i he e
is some elemen a y unc ion wi h a Δ0-de inable g aph such ha he unc ion
x→ maxi∈[0,x] (i)canno be ob ained by composi ion om and udimen a y
unc ions.
The ou line o he pape is as ollows. Sec ions 1and 2a e in oduc o y. Sec ion 3
con ains he p oo o he cha ac e iza ion heo em o Δ1(T)-schemes and se e al
applica ions. (In pa icula , we sol e a numbe o ques ions le o e om [11] and
[7]). In Sec . 4we in es iga e pa ame e ee Δ1(T)-schemes and pa ame e ee Δ1-
in e ence ules. Finally, Sec . 5is de o ed o de e mining he p. .c. .’s o IΔ1(T)and
o LΔ1(T)and con ains he abo e-men ioned educ ion o he NE P oblem.
2 P elimina ies
We assume amilia i y wi h basic no ions and esul s conce ning agmen s o Pea-
no A i hme ic (all ele an in o ma ion can be ound in [12]). We wo k in he usual
i s -o de language o a i hme ic L={0,1,+,·,≤}. We deno e by N he s anda d
model o a i hme ic and say ha a heo y Tis sound i all i s axioms a e ue in N.As
usual, he o mulas o La e classi ied in he Σn/Πnhie a chy, Δ0deno es he class o
bounded o mulas, i.e., o mulas wi h bounded quan i ie s only, and B(Σn)deno es
he class o boolean combina ions o Σn- o mulas. Fo Γ=Σno Πn,IΓdeno es
Qplus he scheme o induc ion o Γ- o mulas, LΓdeno es Qplus minimiza ion o
Γ- o mulas, and BΓdeno es IΔ0plus collec ion o Γ- o mulas. F agmen s IΔn
and LΔna e gi en by Q oge he wi h
(ϕ(x, )↔ψ(x, )) →Iϕ(x, );(ϕ(x, )↔ψ(x, )) →Lϕ(x, ),
whe e ϕ∈Σnand ψ∈Πn. Recall om [14] ha EΓ−deno es he pa ame e ee
e sion o he heo y EΓ. We also w i e ϕ(x)∈Γ− o mean ha ϕ(x)is in Γand
con ains no o he ee a iables han he ones shown. We will be conce ned wi h he-
o ies desc ibed in e ms o in e ence ules oo. The Γ-induc ion ule, Γ-IR, and he
Γ-collec ion ule, Γ-CR, a e gi en by
ϕ(0, )∧∀x(ϕ(x, )→ϕ(x+1, ))
∀xϕ(x, );∀x∃yϕ(x,y, )
∀z∃u∀x≤z∃y≤uϕ(x,y, ),
whe e ϕ∈Γ. Simila ly, Δn-IR and Δn-LR a e gi en by
ϕ(x, )↔ψ(x, )
Iϕ(x, )
;ϕ(x, )↔ψ(x, )
Lϕ(x, )
,
wi h ϕ∈Σnand ψ∈Πn. Following [3], gi en an in e ence ule Rand a heo y
T,T+Rdeno es he closu e o Tunde Rand i s o de logic; while [T,R]deno es
he closu e o Tunde non-nes ed applica ions o Rand i s o de logic. A ule R1is
educible o R2i [T,R1]⊆[T,R2] o e e y heo y Tex ending IΔ0; wo ulesR1
and R2a e cong uen i hey a e mu ually educible o each o he .
In he p esen pape by an a bi a y a i hme ic heo y Twe mean any ex en-
sion o IΔ0in he language L. In pa icula , Can o ’s pai ing unc ion x,y=
(x+y+1)·(x+y)
2+xand p ojec ions y=(x)0and y=(x)1will be a ailable in all
ou heo ies.
Finally, i Aand Ba e L-s uc u es we w i e A≺ΓB o mean ha AisaΓ-
elemen a y subs uc u e o B, i.e., o all ϕ(x)∈Γand a∈A,A| ϕ(a)i , and
only i , B| ϕ(a). We deno e by Kn(A,p) he submodel o Aconsis ing o elemen s
which a e Σn-de inable (possibly wi h a pa ame e p). Submodels o Σn-de inable
elemen s a e na u al examples o Σn-elemen a y subs uc u es. In addi ion, since [16]
and [17] i has been known ha hey p o ide examples o a i hme ic s uc u es whe e
Σn-collec ion ails. In [9] we ob ained he ollowing s eng hening o hese old esul s.
P oposi ion 1 ([9], Theo em 3.6)
1. I A| IΔ0and p ∈Ais nons anda d, K1(A,p)| BΣ1+exp.
2. I A| IΔ0and K1(A)is nons anda d, K1(A)| LΔ−
1+exp.
3. I A| BΣ1and p ∈Ais nons anda d and Π1-minimal (i.e., p is he leas
elemen sa is ying some Π1- o mula), hen K1(A,p)| BΣ−
1+exp.
3 Models o Δ1(T)-schemes
Le T be a ixed bu a bi a y ex ension o I Δ0. In his sec ion we p o e ou cha ac e -
iza ion heo em o Δ1(T )-schemes and ob ain hei basic p oo - heo e ic
p ope ies.
Al hough we shall concen a e on he case n=1, ou esul s easily gene alize o
Δn(T)-schemes o an a bi a y n≥1. Fi s , ecall om [11] ha
Lemma 1 1. LΔ1(T)IΔ1(T).
2. LΔ1(T)BΔ1(T).
3. ThΠ2(T)+BΔ1(T)LΔ1(T).
The p oo s a e easy adap a ions o he p oo s ha LΣ1IΣ1and LΔ1≡BΣ1(see
e.g., [12]). In pa icula , i ollows ha o e T,LΔ1(T)and BΔ1(T)a e deduc i ely
equi alen , which is a e o mula ion o he ac ha Δ1-LR and Σ1-CR a e cong uen
ules.
Tu ning o he cha ac e iza ion heo em, we will e o mula e he heo ems o a
Δ1(T)-scheme as he in e sec ion o he heo ems o o he wo heo ies. O , equi a-
len ly, we will e o mula e he class o models o a Δ1(T)-scheme as he union o he
models o o he wo heo ies. This mo i a es he ollowing de ini ion.
De ini ion 1 Le Sand Tbe L- heo ies and le Ax(S)and Ax(T)be he se s o hei
non-logical axioms. Then S∨Tis he heo y whose non-logical axioms a e he se o
sen ences {ϕ∨θ:ϕ∈Ax(S)and θ∈Ax(T)}.
Lemma 2 A| S∨T i and only i ei he A| So A| T. Hence, o each
ϕ, S∨Tϕi and only i bo h S ϕand T ϕ.
We a e now eady o s a e ou esul .
Theo em 1 (T ans e heo em)
1. IΔ1(T)ThΠ2(T)∨IΣ1.
2. LΔ1(T)ThΠ2(T)∨IΣ1.
3. BΔ1(T)ThΠ2(T)∨BΣ1.
P oo We only w i e he p oo o pa 1. The emaining cases a e analogous. Suppose
A| IΔ1(T)and A| ThΠ2(T). To see ha A| IΣ1conside ϕ(x, ) ∈Σ1.
Since A| ThΠ2(T), he e a e θ(w) ∈Σ1and b∈Asuch ha T∀wθ(w)and
A| ¬ θ(b). Pu δ(x, ,w) ≡ϕ(x, )∨θ(w). Clea ly, Tp o es ∀ , w, xδ(x, ,w)
and so δ(x, ,w) ∈Δ1(T). Hence, o all a∈A,A| Iδ(x,a,b)by IΔ1(T).Bu
A| ϕ(x,a)↔δ(x,a,b)since A| ¬ θ(b). Thus, Iϕ(x,a)is ue in A.
F om Lemma 2and Theo em 1i ollows ha
Co olla y 1 (Cha ac e iza ion heo em)
1. IΔ1(T)≡[ThΠ2(T), Δ1-IR]∨IΣ1.
2. LΔ1(T)≡[ThΠ2(T), Σ1-CR]∨IΣ1.
3. BΔ1(T)≡[ThΠ2(T), Σ1-CR]∨BΣ1.
As a i s applica ion, we ob ain a pa ial solu ion o he a ian o Pa is’ p oblem
o Δ1(T)-schemes. Since Co olla y 1associa es IΔ1(T)and LΔ1(T) o he same
classic scheme IΣ1, i will su ice o show ha Δ1-IR and Σ1-CR a e cong uen ules.
P oposi ion 2 Suppose T exp. Then [T,Δ
1-IR]≡[T,Σ
1-CR].
P oo Since Σ1-CR and Δ1-LR a e cong uen ules, i is clea ha [T,Σ
1-CR]implies
[T,Δ
1-IR]. The con e se will ollow by adap ing Slaman’s p oo ha IΔ1+exp
BΣ1(see Theo em 2.1 o [21]). Suppose A| Tand [T,Σ
1-CR] ails in A. No e ha
Σ1-CR is educible o i s pa ame e ee e sion Σ−
1-CR which in u n is educible o
Π−
0-CR. Hence, he e is θ(x,y)∈Π−
0such ha
•T∀x∃yθ(x,y);
•Bθ ails in Aand so A| ∀ u∃x≤a∀y≤u¬θ(x,y) o some a∈A.
Le δ(z)deno e he Π1- o mula ∀u∃x≤z∀y≤u¬θ(x,y). Slaman’s p oo shows
us how o p oduce a ailu e o IΔ1 om a ailu e o BΣ1. Inspec ion o ha p oo
gi es us ha he e a e ϕ(x,z)∈Σ1and ψ(x,z)∈Π1such ha
•T∀z(δ(z)→∀x(ϕ(x,z)↔ψ(x,z))
•Iϕ(x,a) ails in A.
S ill we canno conclude, as ϕ(x,z)need no be in Δ1(T). Howe e , i su ices o
modi y ϕ(x,z)a bi o p oduce a ailu e o [T,Δ
1-IR]. To ha end, w i e δ(z)as
∀yδ(z,y), ϕ(x,z)as ∃yϕ(x,y,z), and ψ(x,z)as ∀yψ(x,y,z), wi h δ,ϕ,ψ∈
Δ0. Then, we ha e
T∀x,z∃y[¬δ(z,y)∨¬ψ(x,y,z)∨ϕ(x,y,z)].
W i e θ(x,y,z) o he Δ0- o mula in squa e b acke s abo e and conside
ϕ(x,z)≡∃y(y=μ .θ(x, ,z)∧ϕ(x,y,z))
ψ(x,z)≡∀y(y=μ .θ(x, ,z)→ϕ(x,y,z))
I is clea ha T∀x,z(ϕ(x,z)↔ψ(x,z)). In addi ion, i is easy o see ha
Tδ(z)→(ϕ(x,z)↔ϕ(x,z)) and so Iϕ(x,a) ails in Asince A| δ(a). The e-
o e, A| [ T,Δ
1-IR].
Theo em 2 Suppose T exp. Then IΔ1(T)≡LΔ1(T).
P oo Suppose A| IΔ1(T).I A| ThΠ2(T) hen A| BΔ1(T)by P oposi-
ion 2and so A| LΔ1(T)by Lemma 1.I A| ThΠ2(T) hen Asa is ies IΣ1by
Theo em 1.
Rema k 1 1. In [11] he au ho s p o ed he equi alence IΔ1(T)≡LΔ1(T)p o-
ided Tis an ex ension o IΔ0closed unde Σ1-CR, and asked whe he his
condi ion is also necessa y o ha equi alence (see pa 3 o P oblem 7.1 in
[11]). Theo em 2answe s in he nega i e ha ques ion.
2. I ollows om Theo em 1 ha IΔ1(T)ThΠ2(T)whene e ThΠ2(T)⊆IΣ1.
This answe s in he nega i e P oblem 7.1 in [7], whe e he au ho s asked whe he
a heo y Tsa is ying ha IΔ1(T)ThΠ2(T)mus be closed unde Δ1-IR.
3. I ollows om Lemma 1and Theo em 2 ha IΔ1(T)BΔ1(T)i Texp.
Bu , in gene al, BΔ1(T)does no imply IΔ1(T)( o example, i T=IΔ0+exp
hen IΔ1(T)exp whe eas BΔ1(T)⊆BΣ1). This di e s om he classic case
whe e BΔ1(≡BΣ1)IΔ1.
A second applica ion o he T ans e Theo em is an unboundedness esul o
Δ1(T)-schemes. The so-called K eisel–Lé y unboundedness heo ems [15] a e esul s
s a ing ha a ce ain agmen o a i hme ic has no ex ensions o bounded quan i ie
complexi y o a ce ain kind. He e we ob ain he ollowing a ian o his amily o
esul s.
P oposi ion 3 (Unboundedness) Suppose S ⊆Σ3.
1. I S IΔ1(T) hen S ThΠ2(T).
2. I S exp and S BΔ1(T) hen S ThΠ2(T).
P oo We only p o e pa 2. The p oo o pa 1 is simila . Towa ds a con adic-
ion, assume SBΔ1(T)+exp and Sdoes no imply ThΠ2(T).Le θbe a Π2
sen ence such ha Tθand S θ. I ollows om Theo em 1 o BΔ1(T) ha
S+¬θBΣ1+exp. Since BΣ1+exp is ini ely axioma izable, he e is a sin-
gle Σ3sen ence ϕsuch ha ϕ+¬θis a consis en ex ension o BΣ1+exp.Le
Abe a nons anda d model o ϕ+¬θ. Pu ϕ≡∃xϕ(x)and ¬θ≡∃xθ(x), wi h
ϕ(x)∈Π2and θ(x)∈Π1, and pick a,b,c∈Asuch ha ais nons anda d and
A| ϕ(b)∧θ(c). Finally conside d=a,b,c. Then, he submodel o de inable
elemen s K1(A,d)also sa is ies ϕ(b)∧θ(c)since K1(A,d)≺Σ1A. So, K1(A,d)
is a model o BΣ1+exp, which con adic s P oposi ion 1.
Since he sen ence exp essing ha a Σ1 o mula is equi alen o a Π1 o mula has
complexi y Π2, i is clea ha Δ1(T)-schemes only depend on he Π2- heo ems o T.
Somewha su p isingly, i ollows om he Unboundedness esul s ha we can also
eco e he Π2- heo ems o T om he co esponding Δ1(T)-schemes, no ma e s
how s ong Tmigh be.
P oposi ion 4
1. Suppose S and T a e closed unde Δ1-IR. Then, IΔ1(S)≡IΔ1(T)i and only
i ThΠ2(S)=ThΠ2(T).
2. Suppose S and T a e closed unde Σ1-CR and p o e exp. Then, BΔ1(S)≡
BΔ1(T)i and only i ThΠ2(S)=ThΠ2(T).
P oo We only w i e he p oo o pa 2. Assume BΔ1(S)BΔ1(T). Since Sis
closed unde Σ1-CR,ThΠ2(S)implies BΔ1(S). So, ThΠ2(S)implies BΔ1(T)and
hen ThΠ2(T)⊆ThΠ2(S)by P oposi ion 3. The opposi e di ec ion ollows by sym-
me y.
As an immedia e consequence, we ob ain ha
Theo em 3 (Hie a chy heo em)
1. IΔ0≡IΔ1(IΔ0)IΔ1(IΣ1)IΔ1(IΣ2)IΔ1(IΣ3)··· ⊆ IΣ1
2. IΔ0≡BΔ1(IΔ0)BΔ1(IΣ1)BΔ1(IΣ2)BΔ1(IΣ3)··· ⊆ BΣ1
Using a modi ied e sion o he model- heo e ic no ion o an en elope, Theo em 6.6
in [11] gi es ano he p oo ha IΔ1(IΣn), n≥0 o m a hie a chy. In con as , a
hie a chy heo em o BΔ1(IΣn), n≥0, was le o e (see P oblem 7.5 in [11]).
Theo em 3answe s ha ques ion as well as p o ides a much simple p oo o he
hie a chy heo em o he induc ion case.
We close his sec ion by showing how o use he Unboundedness heo em o de e -
mine he usual p oo - heo e ic p ope ies o Δ1(T)-schemes. Ra he han being sys-
ema ic, we p e e o illus a e his me hodology wi h a ew salien examples.
P oposi ion 5 (Quan i ie complexi y)
1. I IΣ1ThΠ2(T), hen IΔ1(T)is Π2-axioma izable. I IΣ1 ThΠ2(T), hen
IΔ1(T)is Π3and no Σ3-axioma izable.
2. I IΔ0+exp ThΠ2(T), hen BΔ1(T)is Π3and no Σ3-axioma izable.
P oo No e ha he na u al axioma iza ions o IΔ1(T)and BΔ1(T)a e o quan i ie
complexi y Π3.
(1) On he one hand, i IΣ1ThΠ2(T) hen i ollows om Theo em 1 ha
IΔ1(T)ThΠ2(T). Hence IΔ1(T)is equi alen o [ThΠ2(T), Δ1-IR]and his
las heo y is Π2-axioma izable. On he o he hand, i IΔ1(T)we e o be Σ3-
axioma izable hen i would ollow om P oposi ion 3 ha IΔ1(T)ThΠ2(T)
and so IΣ1ThΠ2(T) oo.
(2) I BΔ1(T)we e o be Σ3-axioma izable hen i would ollow om P oposi ion 3
ha BΔ1(T)+exp ThΠ2(T)and hence IΔ0+exp ThΠ2(T) oo, o
BΣ1+exp is well-known o be Π2-conse a i e o e IΔ0+exp.
No ice ha i ollows om P oposi ion 5 ha IΔ1(T)is Π2-axioma izable i , and
only i , IΣ1ThΠ2(T). This se les he mo i a ing ques ion o [7]: unde which
condi ions is IΔ1(T)aΠ2-axioma izable heo y?
P oposi ion 6 (Fini e axioma izabili y)
1. IΔ1(T)is ini ely axioma izable i and only i so is [ThΠ2(T), Δ1-IR].
2. Suppose T exp. I BΔ1(T)is ini ely axioma izable, so is [ThΠ2(T), Σ1-CR].
3. So, i T is a consis en ex ension o IΣ1, nei he IΔ1(T)no BΔ1(T)is ini ely
axioma izable.
P oo (1) By Co olla y 1we ha e IΔ1(T)≡[ThΠ2(T), Δ1-IR]∨IΣ1. So, i
[ThΠ2(T), Δ1-IR]has a ini e axioma iza ion hen he second heo y in he p e-
ious equi alence p o ides a ini e axioma iza ion o IΔ1(T). Fo he opposi e
di ec ion, assume ha IΔ1(T)is ini ely axioma izable. Then he e is a single
Π2-sen ence, ϕ, such ha ThΠ2(T)+IΔ1(T)ϕIΔ1(T). Bu i ollows
om P oposi ion 3 ha ϕThΠ2(T)and hence ϕ≡[ThΠ2(T), Δ1-IR].
(2) Reason as in he second pa o he p oo o pa 1.
(3) Assume Tis consis en and implies IΣ1. Then, ThΠ2(T)is closed unde Δ1-IR
and Σ1-CR and is known o be no ini ely axioma izable ( o a p oo see, e.g.,
Theo em 5.3 o [7]).
Rema k 2 (The heo y BΔ1(I Δ0 +exp) and he NE P oblem) In con as o he induc-
ion case, P oposi ion 3 o BΔ1(T ) has only been ob ained o Σ3-ex ensions p o ing
exp. As a consequence, his addi ional assump ion has also appea ed in he subsequen
esul s on BΔ1(T). Elimina ing his use o exp is appa en ly qui e di icul , o i is
ela ed o he well-known open p oblem whe he IΔ0plus he nega ion o exp implies
BΣ1( o sho , he NE P oblem) aised by Wilkie and Pa is in [24]. Ac ually, we ha e
Lemma 3 The ollowing a e equi alen .
1. IΔ0+¬exp BΣ1.
2. BΔ1(IΔ0+exp)≡IΔ0.
P oo (1⇒2) By pa 1, IΔ0+¬exp BΔ1(IΔ0+exp).Bu IΔ0+exp also implies
BΔ1(IΔ0+exp)since IΔ0+exp is closed unde Σ1-CR and hence pa 2 ollows.
(2⇒1) No e ha BΔ1(IΔ0+exp)+¬exp BΣ1by Theo em 1.
Hence, elimina ing exp in P oposi ion 3would gi e ha IΔ0is s ic ly weake han
BΔ1(IΔ0+exp), hus se ling he NE P oblem. (A ecen discussion on he di icul y
and signi icance o his p oblem can be ound in [1]).
4 Pa ame e - ee Δ1(T)-schemes
This sec ion in es iga es he e ec o disallowing pa ame e s in Δ1(T)-schemes and
in Δ1-in e ence ules. Recall ha IΔ1(T)−,LΔ1(T)−and BΔ1(T)−deno e he
pa ame e ee e sions o he co esponding heo ies. Simila ly, we de ine
Δ−
1-IR :∀x(ϕ(x)↔ψ(x))
Iϕ(x)
;Δ−
1-LR :∀x(ϕ(x)↔ψ(x))
Lϕ(x)
,
whe e ϕ(x)∈Σ−
1and ψ(x)∈Π−
1. We ha e no in oduced he in e ence ule
associa ed o BΔ1(T)−, o Σ1-CR is educible o i s pa ame e ee coun e pa . In
con as , Δ1-IR and Δ1-LR a e no longe educible o hei pa ame e ee e sions.
To see ha , ecall om [13] ha UIΔ1deno es a a ian o he Δ1-induc ion scheme
whe e pa ame e s a e dis ibu ed uni o mly. Namely, UIΔ1is Q oge he wi h
∀ ∀x(ϕ(x, )↔ψ(x, )) →∀ Iϕ(x, ),
whe e ϕ∈Σ1and ψ∈Π1. Since IΔ−
1does no imply UIΔ1(see e.g., Theo-
em 1.2 in [9]), he e a e ϕ(x, )∈Σ1and ψ(x, )∈Π1sa is ying ha T=
IΔ−
1+∀ ∀x(ϕ(x, )↔ψ(x, )) does no p o e ∀ Iϕ(x, ). Thus, such a heo y T
is closed unde Δ−
1-IR and, howe e , does no imply [T,Δ
1-IR]. A simila ema k
applies o Δ1-LR conside ing ULΔ1≡BΣ−
1.
Rega ding Δ1(T)-schemes, i ollows om ou esul s on quan i ie complexi y
in Sec . 3 ha disallowing pa ame e s also makes a di e ence. Le us see ha o
he induc ion case. Fi s , obse e ha IΔ1(T)−has quan i ie complexi y B(Σ2),
i.e., boolean combina ions o Σ2-sen ences. Second, by P oposi ion 5,IΔ1(T)is no
Σ3-axioma izable whene e IΣ1 ThΠ2(T). Thus, IΔ1(T)−is s ic ly weake han
IΔ1(T)i ThΠ2(T)IΣ1. Simila ema ks apply o he collec ion and minimiza ion
cases.
Ou s a ing poin is a T ans e Theo em o hese heo ies.
P oo I ollows om Lemma 2 ha i ϕ(x,y)and ψ(x,y)a e Σ1-de ini ions o in
Tand in S, espec i ely, hen ϕ(x,y)∨ψ(x,y)is a Σ1-de ini ion o in T∨S.
By a well-known esul due independen ly o G. Min s, C. Pa sons and G. Takeu i,
R(IΣ1)equals o he class o p imi i e ecu si e unc ions PR. In iew o Co ol-
la y 1, i only emains o de e mine he p. .c. .’s o [T,Σ
1-CR]and [T,Δ
1-IR] o T
a sound Π2-ex ension o IΔ0. In bo h cases ou esul s will be, mo e o less, di ec
consequences o p e ious wo k by Beklemishe . In ac , in Co olla y 5.6 o [3]i is
shown ha i Tex ends IΔ0+exp, hen R([T,Σ
1-CR])coincides wi h he closu e o
R(T)unde he bounded ecu sion ope a o BR o , equi alen ly, unde he bounded
minimiza ion ope a o M. He e we gi e a a ian o ha esul in e ms o he maxi-
mum ope a o Max. The p oo is simila o ha o Co olla y 5.6 o [3] and we omi
i .
De ini ion 2 (Bounded Min and Max ope a o s) Assume :Nk+1→N. Then
M( )deno es he unc ion gi en by M( )(x,z)=μi≤x.[ (i,z)=0]i such an i
exis s, o x+1 o he wise; and Max( )deno es he unc ion gi en by Max( )(x,z)=
max({ (i,z):0≤i≤x}).
P oposi ion 9 Suppose ha T is a sound Π2- heo y ex ending IΔ0. Then,
R([T,Σ
1-CR])=[R(T), Max]=M(R(T)).
As o he Δ1-IR case, Beklemishe in oduced in [5] a new ecu si e ope a o
called sea chope a o and showed ha i co esponds o Δ1-IR. Gi en :N→N, he
unc ion de ined by he sea ch ope a o (S) om is S( )(a,b)=μz.J( ,a,b,z),
whe e J( ,a,b,z)s ands o
∃x,u, ≤zz=x,u,
∧[(a≤x<b∧(u)0=0∧( )0= 0∧ (x)=u∧ (x+1)= )
∨(x=a∧(u)0= 0∧ =0∧ (a)=u)
∨(x=b∧( )0=0∧u=0∧ (b)= )]
In wo ds, ei he one inds x ∈[a, b) such ha ( (x))0 = 0 and ( (x + 1))0 = 0, o
one es ablishes ha ( (a))0 = 0o ( (b))0 = 0. Then one ou pu s such an x as he
i s coo dina e o a wi ness z ha x is as equi ed (see [5] o de ails). I is impo an
o no e ha in [5] i is assumed ha , by de ini ion, he sea ch ope a o can only be
applied o una y unc ions wi h Δ0-de inable g aph. Res ic ing he ope a o o una y
unc ions is unessen ial bu he es ic ion o unc ions wi h bounded g aph is c ucial.
He e, o make his es ic ion explici , we p e e o keep he sea ch ope a o applicable
o any una y unc ion and hen in oduce he ollowing no a ions. Le R0(T ) deno e
he class o hose p. .c. .’s o T wi h a Δ0-de ini ion in T . No e ha , in gene al, R0(T )
is no closed unde composi ion and ha R(T ) = C(R0(T )). In addi ion,
Lemma 7 R0(T ) coincides wi h he class o he unc ions in R(T ) whose g aph is
Δ0-de inable in he s anda d model.
P oo One inclusion is ob ious. Fo he o he , le ϕ(x, y) ∈ Σ1 be a de ini ion o
a unc ion in T and le θ(x, y) ∈ Δ0 de ining he g aph o in N. Then N |
∀x∀y(ϕ(x,y)→θ(x,y)) and so he e is a ue Π1-sen ence, say ∀zδ(z)wi h δ∈Δ0,
sa is ying ha T+∀zδ(z)∀x∃yθ(x,y). I is easy o see ha he Δ0- o mula
¬δ(y)∨θ(x,y)is a de ini ion o in T.
Le [F,S]wdeno e he smalles se o unc ions con aining F, closed unde composi-
ion, and sa is ying ha S( )belongs o he se whene e ∈F. No e ha [F,S]wis
con ained in, bu could be weake han, [F,S]i Fis no closed unde composi ion.
Using his e minology, Theo em 3in [5] can be es a ed as ollows ( ha esul is
p o ed in [5] o e IΔ0+exp bu his is unessen ial).
P oposi ion 10 Suppose ha T is a sound Π2- heo y ex ending IΔ0. Then,
R([T,Δ
1-IR])=[R0(T), S]w.
The abo e cha ac e iza ion is no as nea as he one ob ained o Σ1-CR. I would
be nice o show R([T,Δ
1-IR])=[R(T), S], i.e., wi h he sea ch ope a o being
applied o any compu able unc ion a he han only o unc ions wi h a bounded
g aph. Howe e , one should ake in o accoun he ollowing ac .
Lemma 8 1. [C,M]⊆[C,S] o each unc ion algeb a Ccon aining M2.
2. Assume ha R([T,Δ
1-IR])=[R(T), S] o e e y sound Π2- heo y T ex ending
IΔ0. Then BΣ−
1is p o able om ThΠ1(N)+IΔ1. (Whe he such a p oo exis s
is s ill open).
P oo (1) Pick :Nk+1→Nin C(C). Roughly speaking, in o de o ob ain he
leas i≤xsuch ha (i,z)=0, i su ices o apply he sea ch ope a o on he
in e al [0,x+2] o he unc ion ha akes he alues
0,0,sg( (0,z)), 0,··· ,sg( (x,z)), 0,1,0,
whe e sg deno es Kleene’s signum unc ion, which sa is ies sg(0)=1 and
sg(x)=0i x= 0. Mo e o mally, de ine :Nk+2→N o be
(x,z,w)=⎧
⎨
⎩
0,0x=0
sg( (x−1,z)), 01≤x≤w
1,0x>w
Then, ∈C(C)as M2⊆C, and i ollows om he de ini ion o he sea ch
ope a o ha M( )(x,z)=(S( )(0,x+2,z,x+1))0, whe e by abuse o
no a ion we also w i e S( ) o deno e he sea ch ope a o applied o a unc ion
wi h pa ame e s. I only emains o elimina e he use o pa ame e s z,w in .
This can be achie ed by pu ing oge he pieces o as ollows. (This idea has
been aken om he p oo o Lemma 14 in [5] bu we need o modi y he coding
me hod because we wo k o e M2 a he han o e he class o elemen a y unc-
ions). Fo simplici y, we i s encode z,w in o a single pa ame e by pu ing
(x, )= (x,( )
0,...,( )
k). Now conside
g(x)= ((x)0,((x)0+(x)1)0).
I ollows om he de ini ion o he pai ing unc ion ha gon he in e al
[0, , x,0, , x + x] akes he alues (0, ),..., (x, ). I we pu
h(x, ) =0, , x and w i e S(g)(h(x, ),h(x, ) +x)as a,b,c, hen
we ha e S( )(0,x, ) =a−h(x, ),b,cand S( )(0,x,z,w)=
S( )(0,x,z,w). So, he la e unc ion is in [C,S], as equi ed.
(2) Suppose A| ThΠ1(N)+IΔ1and conside T o be he se o all Π2-sen ences
ue in A. Then Tis a sound Π2-ex ension o IΔ0closed unde Δ1-IR and
hence R(T)is closed unde he sea ch ope a o by he assump ion. I ollows
om pa 1 ha R(T)is also closed unde bounded minimiza ion. So R(T)=
R([T,Σ
1-CR])by P oposi ion 9and Tex ends [T,Σ
1-CR]by Lemma 5. Thus,
A| BΣ−
1as equi ed.
Ha ing jus i ied he in oduc ion o he unc ion algeb a [F,S]w,wea enowina
posi ion o ob ain he main heo em o his sec ion.
Theo em 6 Le T be a sound ex ension o IΔ0.
1. R(IΔ1(T)−)=PR ∩R(T).
2. R(IΔ1(T)) =PR ∩[R0(T), S]w=[PR∩R0(T), S]w.
3. R(LΔ1(T)) =PR ∩[R(T), Max]=[PR∩R(T), Max].
P oo W i e T o ThΠ2(T).
(1) I ollows om Co olla y 2and Lemma 6 ha R(IΔ1(T)−)equals o PR ∩
R([T,Δ
−
1-IR]).Bu T+ThΠ1(N)implies [T,Δ
−
1-IR]and R(T)=R([T,
Δ−
1-IR]), o adding ue Π1-sen ences o a sound heo y does no inc ease he
co esponding class o p o ably o al unc ions.
(2) Fi s , i ollows om Co olla y 1, Lemma 6and P oposi ion 10 ha R(IΔ1(T)) =
PR∩[R0(T), S]w. Second, no ice ha
Claim IΔ1(T)is Π2-conse a i e o e IΔ1(IΣ1∨T).
Suppose ha IΔ1(T)p o es θ, wi h θ∈Π2. Then bo h IΣ1and [T,Δ
1-IR]
p o e θ oo. Towa ds a con adic ion, assume IΔ1(IΣ1∨T) θ. Since IΣ1
θ, i ollows om Theo em 1 ha [ThΠ2(IΣ1)∨T,Δ
1-IR]+¬θis consis en .
Pu S=ThΠ2(IΣ1)∨Tand ¬θ≡∃zδ(z), wi h δ∈Π1, and suppose ha
S+¬θ∀x(ϕ(x, )↔ψ(x, )), wi h ϕ∈Σ1,ψ∈Π1. Then Sp o es ∀z(δ(z)→
∀x(ϕ(x, ) ↔ψ(x, ))) and easoning as in he p oo o P oposi ion 2, we ge ha
[S,Δ
1-IR]+¬θ∀ Iϕ(x, ). As a esul , [S,Δ
1-IR]+¬θimplies [S+¬θ,Δ1-IR]
and hence he la e heo y is consis en as well. Bu we ha e
S+¬θ≡(ThΠ2(IΣ1)+¬θ)∨(T+¬θ) ≡(T+¬θ)
since θis a Π2- heo em o IΣ1. We ha e hus ob ained ha [T,Δ
1-IR]+¬θis
consis en , which is a con adic ion. This comple es he p oo o he Claim.
I hen ollows ha
R(IΔ1(T)) =R(IΔ1(IΣ1∨T)) =PR ∩R([ThΠ2(IΣ1)∨T,Δ
1-IR])
=[R0(ThΠ2(IΣ1)∨T), S]w
=[PR ∩R0(T), S]w
(Fo he las equali y no e ha each p imi i e ecu si e unc ion whose g aph is Δ0-
de inable in Nhas a Δ0-de ini ion in IΣ1by Lemma 7).
(3) The p oo is simila o ha o pa 2.
In wha ollows we show ha in p esence o exp,R(IΔ1(T)) and R(LΔ1(T))
can also be desc ibed in pu ely ecu sion- heo e ic e ms. We in oduce a sui ably
modi ied e sion o he bounded ecu sion ope a o , called C-bounded ecu sion, and
p o e ha i Tis a sound ex ension o IΔ0+exp hen R(LΔ1(T)) coincides wi h
he closu e o he basic unc ions unde composi ion and R(T)-bounded ecu sion.
(A p elimina y e sion o his esul appea ed in [8]).
De ini ion 3 (C-bounded ecu sion) A unc ion :Nk+1→Nis de ined om
g:Nk→N,h:Nk+2→Nand C:Nk+1→Nby C-bounded ecu sion, w i en
=BRC(g,h),i ≤Cand
(x,0)=g(x); (x,y+1)=h(x,y, (x,y)),
i.e., is de ined om gand hby p imi i e ecu sion and is bounded by C.Gi ena
unc ion class C,ECis he smalles se o unc ions con aining he basic unc ions ( he
cons an ze o, p ojec ions, and he successo unc ion) and closed unde composi ion
and C-bounded ecu sion, ha is, C-bounded ecu sion o e e y C∈C.
We use he no a ion ECin analogy wi h he well-known G zego czyk hie a chy Ei,i≥
0, de ined in e ms o usual bounded ecu sion (see e.g., [19]). One can a ach o ECa
i s -o de heo y in an ex ended language, deno ed C-BRA, so ha EC=R(C-BRA).
The de ini ion o C-BRAis inspi ed by he well-known sys em PRA o he p imi i e
ecu si e unc ions.
De ini ion 4 Suppose ha Ccon ains M2and is closed unde composi ion. The heo y
C-BRA,C-Bounded Recu si e A i hme ic, is gi en by:
Language: LC=i∈ωLi, whe e
•L0=Lplus a unc ion symbol B o each basic unc ion.
•Lj+1=Ljplus a unc ion symbol o each e m o Lj, and a unc ion
symbol 1, 2 o each pai o e ms 1(x), 2(x,y,z)o Ljsuch ha he unc ion
de ined in he s anda d model om 1and 2by p imi i e ecu sion is bounded
by some unc ion C∈C.
Axioms: ( he uni e sal closu e o )
(1)Robinson’s Q.
(2)BS(x)=x+1,BΠn
i(x1,...,xn)=xi,BO(x)=0.
(3) (x)= (x).
(4) 1, 2(x,0)= 1(x), 1, 2(x,z,y+1)= 2(x,y, 1, 2(x,y)).
(5)Open Induc ion: The induc ion scheme o open o mulas o LC.
Obse e ha C-BRA is a heo y only in an abs ac model- heo e ic sense (i.e., a se o
sen ences in a i s o de language) bu , in gene al, i is no e en e ec i ely axioma-
ized. We shall use his heo y as a echnical ool in o de o p o e ha C∩PR ⊆EC
in P oposi ion 11. Le us also no e ha bounds (i.e., he unc ions om C) a e no
included in he axioma iza ions o he ecu si e schemes (pa (4) o he de ini ion)
and, so, C-BRA canno p o e any hing abou hem. This is na u al because, in gene al,
Cis no con ained in EC: o ins ance, conside he case when Ccon ains some non
p imi i e ecu si e unc ions, o , al e na i ely, see Rema k 4below.
I is ou ine o check ha C-BRA sa is ies he ollowing p ope ies, which a e well-
known o PRA:
•in C-BRA e e y bounded o mula is equi alen o an open one;
•C-BRA suppo s de ini ion by cases;
•C-BRA admi s a pu ely uni e sal axioma iza ion.
As a consequence, a s anda d applica ion o He b and’s heo em gi es us ha R(C −
BRA) = EC
. Equipped wi h his esul , we a e able o show ha
P oposi ion 11 Suppose ha C = R(T ) o T some sound ex ension o I Δ0. Then
C ∩ PR ⊆ EC
.
P oo Since R(C-BRA) = EC and C ∩ PR ⊆ R(I Δ1(T )) by Theo em 6,i is
su icien o p o e ha
Claim I Δ1(T ) is Π2-conse a i e o e C-BRA.
To his end, we ollow J. A igad’s p oo ha I Σ1 is Π2-conse a i e o e PRA
gi en in [2]. The key ing edien is ha o an ∃2-closed model (o He b and sa u a ed
model in A igad’s e minology). We say ha A is an ∃2-closed i , o e e y s uc u e
B, A ≺∀1 B implies A ≺∃2 B. By a union o chain a gumen e e y model o a
uni e sal heo y U can be ∀1-elemen a y ex ended o a new model o U which is ∃2-
closed. Thus, i e e y ∃2-closed model o a uni e sal heo y U is a model o a heo y
W , hen W is ∀2-conse a i e o e U ( his is Theo em 3.4 o [2]).
Tu ning back o he p oo o he Claim, i su ices o show ha e e y ∃2-closed model
o C−BRA sa is ies I Δ1(T ), o each Π2- o mula is equi alen in C−BRA o a ∀2- o -
mula. Suppose ha A is an ∃2-closed model o C − BRA.Le ϕ(x, y, ), ψ(x, y, ) ∈
Δ0 wi h T ∃y ϕ(x, y, ) ↔∀y ψ(x, y, ). We may assume I Δ0 ϕ(x, y1, ) ∧
ϕ(x, y2, ) → y1 = y2, o he wise conside ϕ(x, y, )∧∀y < y ¬ϕ(x, y, ) ins ead.
Since T ∀x, ∃y (ϕ(x, y, ) ∨¬ψ(x, y, )) and T is sound, y = μ .(ϕ(x, , ) ∨
¬ψ(x, , )) de ines a p. . .c. o T ,sayC. Then,
(†) N | ϕ(x, y, ) → y = C(x, ).
Le a ∈ A and le ϕ0(x, y, ) be an open o mula equi alen in C-BRA o ϕ.Wemus
show ha he induc ion axiom o ∃y ϕ0(x, y, a) is ue in A. To ha end, assume
A | ∃y ϕ0(0, y, a) ∧∀x (∃y ϕ0(x, y, a) →∃y ϕ0(x + 1, y, a)). In pa icula , A |
∀x, y ∃y (ϕ0(x, y, a) → ϕ0(x +1, y, a)). Since his las o mula has quan i ie com-
plexi y ∀2, i is p o able om he uni e sal diag am o A by he closedness condi ion
o A. Thus, applying He b and’s heo em and using ha C − BRA suppo s de ini ion
by cases, we ob ain ha he e a e b, c ∈ A and a e m o LC
, (x, y, ,w), sa is ying
ha
A | ϕ0(0, c, a) ∧∀x, y (ϕ0(x, y, a) → ϕ0(x + 1, (x, y, a, b), a)).
Le hdeno e he unc ion de ined in he s anda d model by
h(x,y,z, ,w)= (x,z, ,w) i ϕ0(x+1, (x,z, ,w), );
0 o he wise
Clea ly h∈EC.Le be he unc ion de ined by p imi i e ecu sion as ollows:
(0,y, ,w)=y, (x+1,y, ,w)=h(x,y, (x,y, ,w), ,w).
By (†) (x,y, ,w)≤C(x,y, ,w)=y+C(x, ).So ∈EC, since i is de ined by
C-bounded ecu sion and C∈C.Le be he unc ion symbol o LCco esponding
o . Then Asa is ies ha
ϕ0(0, (0,c,a,b), a)∧∀x(ϕ0(x, (x,c,a,b), a)→ϕ0(x+1, (x+1,c,a,b), a)).
Since Ais a model o open induc ion, A| ∀ xϕ0(x, (x,c,a,b), a)and hence A|
∀x∃yϕ0(x,y,a), as equi ed.
Rema k 4 I is wo h no ing ha he assump ion ha Cis he class o p. .c. .’s o a
heo y Tcanno be d opped in P oposi ion 11. Fo example, pu C=C(M2∪{ChA}),
whe e ChAis he cha ac e is ic unc ion o a p imi i e ecu si e se Awhich is no
in he second le el o he G zego czyk hie a chy E2.Fi s ,Ccanno be w i en as
R(T) o any heo y Tin he language o a i hme ic, o we ha e R(T)=C(R0(T))
whe eas closing unde composi ion he unc ions in Cwi h a Δ0-de inable g aph only
gi es us M2. Second, C∩PR =CEC=E2.
Theo em 7 Le T be a sound ex ension o IΔ0+exp and le C=R(T). Then,
R(IΔ1(T)) =R(LΔ1(T)) =EC.
P oo I ollows om P oposi ion 11 ha C∩PR ⊆ECand i ollows om Theo-
em 6 ha R(LΔ1(T)) =[C∩PR,Max]=M(C∩PR). Bu i is easy o see ha
ECis closed unde bounded minimiza ion. Thus, R(LΔ1(T)) ⊆EC. Fo he opposi e
inclusion, no e ha
Claim EC=EC∩PR.
We eason by induc ion on he de ini ion o ∈EC. The c i ical s ep is he de ini ion
by C-bounded ecu sion. Suppose =BRC(g,h)wi h C∈C. Since i sel is p im-
i i e ecu si e, he e a e C1∈PR and C2∈Cwi h Δ0-de inable g aphs such ha
≤C1,C2.Le θ1(x,y)∈Δ0be a de ini ion o C1in IΣ1and le θ2(x,y)∈Δ0be
a de ini ion o C2in T. Then y=μ .(θ
1(x, )∨θ2(x, )) de ines a p. .c. . o T∨IΣ1,
say C3. No e ha C3∈C∩PRand =BRC3(g,h), which p o es he claim.
Thus EC=EC∩PR ⊆BR(C∩PR)=M(C∩PR)=R(LΔ1(T)), whe e in he las
bu one equali y BR deno es he usual bounded ecu sion ope a o and we use ha in
p esence o exp, bounded ecu sion can be educed o bounded minimiza ion.
Exponen ia ion is used in wo di e en ways in Theo em 7abo e. On he one hand,
exp is needed o p o e IΔ1(T)and LΔ1(T) o be equi alen and hus sha e he same
p. .c. .’s. On he o he hand, exp is needed o educe bounded ecu sion o bounded
minimiza ion in he p oo ha EC⊆R(LΔ1(T)). Elimina ing his second use o exp
seems o be a ha d p oblem, o i is ela ed o impo an p oblems in Complexi y
Theo y. In ac , i T=IΔ0 hen R(LΔ1(T)) =M2and EC=E2. Thus i Theo-
em 7holds o T=IΔ0 hen he Linea Time Hie a chy coincides wi h LinSpace.
Likewise, i Theo em 7holds o T=IΔ0+Ω1, whe e Ω1exp esses “x|x|is o al”,
hen he Polynomial Time Hie a chy equals o PolySpace.
In he same spi i , we close his sec ion wi h a educ ion o he NE P oblem (see
Rema k 2) o a pu ely ecu sion- heo e ic ques ion. Recall ha E3deno es he hi d
le el o he G zego czyk hie a chy, which is well-known o coincide wi h he se o
Kalmá ’s elemen a y unc ions.
P oposi ion 12 The ollowing a e equi alen .
1. ThΠ1(N)+¬exp BΣ−
1.
2. Fo each ∈E3wi haΔ0-de inable g aph, C(M2∪{ })isclosedunde bounded
minimiza ion.
P oo (1⇒2): Le ∈ E3 whose g aph is de inable by a Δ0- o mula, say θ(x, y),
and pu T = ThΠ1 (N) +∀x ∃y θ(x, y). I ollows om Lemmas 4 and 5 ha R(T ) =
C(M2 ∪{ }). Now obse e ha i ollows om condi ion 1 ha
Claim T is closed unde Σ1-CR.
On he one hand, since R(T ) ⊆ E3 = R(I Δ0 + exp), i ollows om he p oo o
Lemma 5 ha T is included in ThΠ1 (N) + exp. Bu he la e heo y is closed unde
Σ1-CR and hence T exp implies T Σ1-CR. On he o he hand, T exp is an
ex ension o BΣ1
− by
+
condi ion 1 and
+
so T +¬exp implies T + Σ1-CR
+¬
oo. As a
esul , T implies T + Σ1-CR, as equi ed.
Thus C(M2 ∪{ }) is closed unde bounded minimiza ion by P oposi ion 9.
(2⇒1): Obse e ha i ollows om condi ion 2 ha
Claim ThΠ1 (N) implies BΔ1(I Δ0 + exp)−.
To see his, assume ha I Δ0 + exp ∀x ∃y ϕ(x, y), wi h ϕ(x, y) ∈ Σ1
−. Pu
ϕ(x, y) ≡∃z ϕ0(x, y, z), wi h ϕ0 ∈ Δ0, and de ine θ(x, y) o be he Δ0- o mula
y = μ .ϕ0(x,( )0,( )1). Then θ(x, y) de ines a compu able unc ion ∈ E3 since
I Δ0 + exp ∀x ∃y θ(x, y). By condi ion 2, Max( ) ∈ C(M2 ∪{ }) = R(I Δ0 +
∀x ∃y θ(x, y)). No e ha ∀x ≤ z ∃y ≤ u θ(x, y) ∧∃x ≤ z θ(x, u) is a Δ0- o mula
de ining Max( ) in he s anda d model. Hence easoning as in he p oo o Lemma 5
we ob ain ha ThΠ1 (N) +∀x ∃y θ(x, y) p o es ∀z ∃u ∀x ≤ z ∃y ≤ u θ(x, y) and so
ThΠ1 (N) Bϕ(x,y), as equi ed.
Thus ThΠ1
(N)+¬exp implies BΔ1(I Δ0 +exp)−+¬exp which in u n implies BΣ1
−
by Theo em 4.
Co olla y 5 Assume ha he e exis s some ∈ E3 wi h a Δ0-de inable g aph such
ha Max( ) ∈ C(M2 ∪{ }). Then I Δ0 +¬exp does no imply BΣ1.
In e es ingly, Lemma 6.1 o [4] shows how o cons uc a unc ion ∈E4wi h
an elemen a y g aph such ha Max( )∈ C(E3∪{ }). The cons uc ion uses Tu ing
machines equipped wi h an in e nal clock. Al hough i is a om ob ious how o
adap ha cons uc ion o ob ain a unc ion sa is ying he assump ions o Co olla y 5,
his app oach gi es us some new ideas o a ack he NE P oblem and o ob ain, a leas ,
a condi ional nega i e answe unde some complexi y- heo e ic assump ion.
Acknowledgmen s Wo k pa ially suppo ed by g an MTM2008-06435, Minis e io de Ciencia e Inno-
ación, Spain and FEDER unds (EU).
Re e ences
1. Adamowicz, Z., Kołodziejczyk, L.A., Pa is, J.B.: T u h de ini ions wi hou exponen ia ion and he Σ1
collec ion scheme. J. Symb. Logic 77, 649–655 (2012)
2. A igad, J.: Sa u a ed models o uni e sal heo ies. Ann. Pu e Appl. Logic 118, 219–234 (2002)
3. Beklemishe , L.D.: Induc ion ules, e lec ion p inciples, and p o ably ecu si e unc ions. Ann. Pu e
Appl. Logic 85, 193–242 (1997)
4. Beklemishe , L.D.: A p oo - heo e ic analysis o collec ion. A ch. Ma h. Logic 37, 275–296 (1998)
5. Beklemishe , L.D.: On he induc ion scheme o decidable p edica es. J. Symb. Logic 68, 17–34 (2003)
6. Clo e, P., K ajíˇcek, J. : Open p oblems. In: Clo e, P., K ajíˇcek, J. (eds.) A i hme ic, P oo Theo y, and
Compu a ional Complexi y, pp. 1–19. Ox o d Uni e si y P ess, Ox o d (1993)
7. Co dón-F anco, A., Fe nández-Ma ga i , A., La a-Ma ín, F.F.: On he quan i ie complexi y o
Δn+1(T)-induc ion. A ch. Ma h. Logic 43, 371–398 (2004)
8. Co dón-F anco, A., Fe nández-Ma ga i , A., La a-Ma ín, F.F.: P o ably o al p imi i e ecu si e unc-
ions: heo ies wi h induc ion. In: Ma cinkowski, J., Ta lecki, A. (eds.) Compu e Science Logic, 18 h
In e na ional Wo kshop, CSL 2004, Ka pacz, Poland, Sep 20–24, 2004, P oceedings, pp. 355–369,
Lec u e No es in Compu . Sci. 3210, Sp inge , Be lin, Heidelbe g (2004)
9. Co dón-F anco, A., Fe nández-Ma ga i , A., La a-Ma ín, F.F.: F agmen s o A i hme ic and ue sen-
ences. MLQ Ma h. Log. Q. 51, 313–328 (2005)
10. Co dón-F anco, A., Fe nández-Ma ga i , A., La a-Ma ín, F.F.: A no e on pa ame e ee Π1-induc ion
and es ic ed exponen ia ion. MLQ Ma h. Log. Q. 57, 444–455 (2011)
11. Fe nández-Ma ga i , A., La a-Ma ín, F.F.: Induc ion, minimiza ion and collec ion o Δn+1(T)- o -
mulas. A ch. Ma h. Logic 43, 505–541 (2004)
12. Hájek, P., Pudlák, P.: Me ama hema ics o Fi s -O de A i hme ic. Sp inge , Be lin, Heidelbe g (1993)
13. Kaye, R.: Diophan ine and pa ame e - ee induc ion. Ph.D. hesis, Uni e si y o Manches e (1987)
14. Kaye, R., Pa is, J., Dimi acopoulos, C.: On pa ame e ee induc ion schemas. J. Symb. Logic 53, 1082–
1097 (1988)
15. K eisel, H., Lé y, A.: Re lec ion p inciples and hei use o es ablising he complexi y o axioma ic
sys ems. A ch. Ma h. Logik G undlag. 14, 97–142 (1968)
16. Lessan, H.: Models o A i hme ic. Ph.D. hesis, Uni e si y o Manches e (1978)
17. Pa is, J.B., Ki by, L. : Σn-Collec ion schemas in a i hme ic. In: Macin y e, A., Pacholski, L., Pa is,
J. (eds.) Logic Colloquium 77, S udies in Logic and he Founda ions o Ma hema ics 96., pp. 285–296.
No h-Holland, Ams e dam (1978)
18. Pa sons, C.: On n-quan i ie induc ion. J. Symb. Logic 37, 466–482 (1972)
19. Rose, H.E.: Sub ecu sion: Func ions and Hie a chies. Cla endon P ess, Ox o d (1984)
20. Si oko skich, A., Dimi acopoulos, C.: On a p oblem o J. Pa is. J. Log. Compu . 17, 1099–1107 (2007)
21. Slaman, T.: Σn-bounding and Δn-induc ion. P oc. Am. Ma h. Soc. 132, 2449–2456 (2004)
22. Takeu i, G.: G zego cyk’s hie a chy and IepΣ1. J. Symb. Logic 59, 1274–1284 (1994)
23. Thapen, N.: A no e on Δ1induc ion and Σ1collec ion. Fund. Ma h. 186, 79–84 (2005)
24. Wilkie, A.J., Pa is, J.B.: On he exis ence o end-ex ensions o models o bounded induc ion. In: Fens-
ad, J.E., F olo , I.T., Hilpinen, R. (eds.) Logic, Me hodology, and Philosophy o Science VIII, Moscow,
1987, pp. 143–161. No h-Holland, Ams e dam (1989)