scieee Science in your language
[en] (orig)

On axiom schemes for T-provably Δ1 formulas

Abstract

This paper investigates the status of the fragments of Peano Arithmetic obtained by restricting induction, collection and least number axiom schemes to formulas which are Δ1 provably in an arithmetic theory T. In particular, we determine the provably total computable functions of this kind of theories. As an application, we obtain a reduction of the problem whether IΔ0+¬exp implies BΣ1 to a purely recursion-theoretic question.

Read accessible full text

On axiom schemes for T-provably Δ1 formulas

Author: Cordón Franco, Andrés; Fernández Margarit, Alejandro; Lara Martín, Francisco Félix
Publisher: Springer
Year: 2014
DOI: 10.1007/s00153-014-0368-9
Source: https://idus.us.es/bitstreams/08fdac7e-fdd6-482f-94c9-cebe821a1d27/download
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Σ1IΣ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 Texp.
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 SBΔ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Σ1ThΠ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Σ1ThΠ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Σ1ThΠ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Σ1ThΠ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,0x=0
sg( (x−1,z)), 01≤x≤w
1,0x>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,cand 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)∨Tand ¬θ≡∃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 =CEC=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)