Induction, minimization and collection for Δ n+1 (T)–formulas

INDUCTION, MINIMIZATION AND COLLECTION FOR ∆n+1(T)–FORMULAS A. Fe n´andez–Ma ga i and F. F. La a–Ma ´ın Dep o. Ciencias de la Compu aci´on e I. A. Fac. de Ma em´a icas, Uni e sidad de Se illa C/Ta ia s/n, Se illa (Spain) la[email p o ec ed] Abs ac . Fo a heo y T, we s udy ela ionships among I∆n+1(T), L∆n+1(T) and B∗∆n+1(T). These heo ies a e ob ained es ic ing he schemes o induc ion, mini- miza ion and (a e sion o ) collec ion o ∆n+1(T) o mulas. We ob ain condi ions on T (Tis an ex ension o B∗∆n+1(T) o ∆n+1(T) is closed (in T) unde bounded quan i i- ca ion) unde which I∆n+1(T) and L∆n+1(T) a e equi alen . These condi ions depend on ThΠn+2 (T), he Πn+2–consequences o T. The i s con- di ion is connec ed wi h desc ip ions o ThΠn+2 (T) as IΣnplus a class o nondec easing o al Πn– unc ions, and he second one is ela ed wi h he equi alence be ween ∆n+1(T)– o mulas and bounded o mulas (o a language ex ending he language o A i hme ic). This las p ope y is closely ied o a gene al e sion o a well known heo em o R. Pa ikh. Using wha we call Πn–en elopes we gi e uni o m desc ip ions o he p e ious classes o nondec easing o al Πn– unc ions. Πn–en elopes a e a gene aliza ion o en elopes (see [10]) and a e closely ela ed o indica o s (see [12]). Finally, we s udy he hie a chy o heo ies I∆n+1(IΣm), m≥n, and p o e a hie a chy heo em. 1. In oduc ion This pape is de o ed o he s udy o wo main opics: he ela ionship be ween in- duc ion and minimiza ion, and he desc ip ion o he class o Πn+2 consequences o a heo y. The i s one is on F agmen s o A i hme ic ob ained es ic ing he schemes o in- duc ion, minimiza ion and collec ion o ∆n+1– o mulas. These schemes o Σnand Πn o mulas ha e been ho oughly s udied by J. Pa is, L. Ki by and o he s (see [17] o [12]). The pa ame e ee e sions o hose schemes ha e been s udied by R. Kaye, J. Pa is and C. Dimi acopoulos (see [11] and [14]). Howe e , he ela ionships be ween hose schemes o ∆n+1 o mulas a e no well known. Abou 1985, H. F iedman claimed ha L∆n+1 and I∆n+1 a e equi alen (see [10] pg. 398), bu in [6] ha equi alence appea s as an open p oblem (p oblem 34) and i is c edi ed o J. Pa is. He e ha equi alence will be called he Pa is–F iedman’s Conjec u e. In [19], T. Slaman p o es i o n≥1. Resea ch pa ially suppo ed by g an PB96–1345 (Spanish Go e nmen ). 1 In sec ions 2and 6, we s udy hose schemes es ic ed o ∆n+1(T) o mulas. I ϕ∈Σn+1 and ψ∈Πn+1 hen ϕ↔ψis a Πn+2 o mula. So, he second opic is ela ed o he i s one. In sec ions 3–5, we analyse he class o Πn+2 consequences o a heo y using a class o Πn– unc ions and ex ensions o he language o A i hme ic ela ed o ha class o unc ions. Now we p esen he main esul s ob ained on hese opics in his pape . Pa I: Induc ion and minimiza ion o ∆n+1(T) o mulas. In o de o ge a be e insigh on he Pa is–F iedman’s Conjec u e we conside he heo ies I∆n+1(T), L∆n+1(T) and B∗∆n+1(T), whe e ∆n+1(T) = {ϕ(x,~ )∈Σn+1 : he e exis s ψ(x,~ )∈Πn+1,T`ϕ↔ψ}. The idea is o change he seman ic pa o he axioms schemes on ∆n+1 o mulas by a syn ac ic condi ion: he equi alence be ween a Σn+1 o mula and a Πn+1 o mula is p o ed in a heo y. Thus we ob ain a ela i iza ion o Pa is–F iedman’s Conjec u e. We s udy he ollowing p oblem: (∗) Unde which condi ions on Tdoes L∆n+1(T)⇐⇒ I∆n+1(T) hold? We i s obse e ha =⇒always holds. In he o he way, le us no ice ha he usual p oo o IΣn+1 =⇒LΣn+1 leans upon he closu e o Σn+1 unde bounded quan i ica ion ( his p ope y is g an ed by he collec ion schemes, BΣn+1). In ac , he closu e unde bounded quan i ica ion o he class o ∆n+1– o mulas is he main obs acle in o de o adap he e e ed p oo o ob ain ha I∆n+1 =⇒L∆n+1. So, o answe p oblem (∗) he abo e e- ma ks sugges wo na u al p ope ies: Thas ∆n+1–collec ion ( ha is, T=⇒B∗∆n+1(T)), and Tis ∆n+1–closed ( ha is, ∆n+1(T) is closed in Tunde bounded quan i ica ion). We p o e ha i Tsa is ies one o he abo e condi ions hen L∆n+1(T)⇐⇒ I∆n+1(T), see heo em 1.4. We also s udy ela ionships among he abo e schemes, o dis inc heo ies. The ol- lowing heo em sums up he esul s ob ained. Theo em 1.1 (see 2.1, 2.10, 2.17, 2.18, 6.12, 6.13, 6.14).Fo all n∈ω IΣn⇐⇒ L∆n+1(IΣn)⇐⇒ I∆n+1(IΣn)⇐⇒ B∗∆n+1(IΣn) ⇑ ⇑ ⇑ BΣ− n+1,IΠ− n+1 I∆n+1,BΣn+1 ×⇐⇒ L∆n+1(IΣn+1)⇐⇒ I∆n+1(IΣn+1)|=⇒B∗∆n+1(IΣn+1) ⇑ ⇑ ⇑ . . . . . . . . . ⇑ ⇑ ⇑ IΣ− n+1 IΠ− n+1,BΣ− n+1 ×⇐= ×⇐⇒ L∆n+1(PA)⇐⇒ I∆n+1(PA)|=⇒B∗∆n+1(PA) ⇑ ⇑ ⇑ BΣn+1 IΠ− n+1 BΣ− n+1 ×⇐⇒ ⇐=| ×=⇒ L∆n+1(N)⇐⇒ I∆n+1(N)|=⇒B∗∆n+1(N) ⇑ ⇑ IΣn+1 |=⇒BΣn+1 (Some o hose ela ions o pa ame e ee schemes ollow om esul s in [9], see also [7] and [15]). 2 Pa II: Πn+2 consequences o a heo y. P ope ies conside ed in pa I (Thas ∆n+1–collec ion, Tis ∆n+1–closed and o he s ha we call ∆n+1–p ope ies) depend on ThΠn+2 (T), he class o Πn+2 consequences o T. He e we gi e cha ac e iza ions o hese p ope ies in a “ unc ional” way. The idea is o desc ibe ThΠn+2 (T) using IΣnand a class o Πn– unc ions. To his end we in oduce he concep s o Πn– unc ional class (which p o ides a cha ac e iza ion o he heo ies ha - ing ∆n+1–collec ion) and Πn–Pa ikh pai (which co esponds wi h ∆n+1–closed heo ies). Essen ially, a Πn– unc ional class is a se o nondec easing Πn– unc ions. The concep o Πn–Pa ikh pai is sugges ed by he ollowing well known esul . Theo em 1.2 (Pa ikh).Le ϕ(x, y)∈Σ1. I I∆0` ∀x∃y ϕ(x, y) hen he e exis s (x)∈ Te m(L)such ha I∆0` ∀x∃y≤ (x)ϕ(x, y). As a consequence o his esul (see 3.27) each ∆1(I∆0) o mula is equi alen (in I∆0) o a ∆0– o mula. So, ∆1(I∆0) is closed (in I∆0) unde bounded quan i ica ion. We gi e a gene al e sion o his ac . I Tis ∆n+1–closed, hen he e is a conse a i e ex ension o ThΠn+2 (T) (in a language ex ending he language o A i hme ic) in which each ∆n+1(T) o mula is equi alen o a bounded o mula. In pa icula , i Thas ∆n+1–collec ion hen a s ong Πn– unc ional class p o ides such an ex ension. One c u ial esul ha ela es he schemes o induc ion and collec ion is he F iedman– Pa is’ conse a i eness heo em (see [10] o [12]): Theo em 1.3. Fo all n∈ω,ThΠn+2 (IΣn) = ThΠn+2 (BΣn+1). He e we s udy a simila Πn+2–conse a i eness p ope y, closely ied o ∆n+1–collec ion: ThΠn+2 (T) = ThΠn+2 (T+BΣn+1). This p ope y plays a cen al ole in he s udy o Πn–en elopes ha will be de eloped in sec ion 5. Roughly speaking, a Πn–en elope is a Πn– unc ional class gi en in an uni o m way and gene alizes he concep o en elope (see [10]). In sec ion 6we use esul s o sec ions 4and 5 o sepa a e he agmen s I∆n+1(IΣm), m≥n(see heo em 1.1). The ollowing heo em sums up, o a consis en heo y, T, he ela ionships among he concep s in oduced. Theo em 1.4. (see 2.10, 2.11, 3.8, 3.11, 3.28, 4.18, 5.11, 5.21) Tis ∆n+1-PF Thas ∆n+1-min. Tis s ong Πn- unc . Thas Πn-s-en . ⇑ m m m3 Tis ∆n+1-closed ⇐=Thas ∆n+1-coll. ⇐⇒ Tis Πn- unc . ⇐⇒2 3Thas Πn-en . m m m1 Tis Πn–Pa ikh Thas ∆n+1-ind. Tis ∆n+1-closed Tis ΠB n+2-conse . Whe e: =⇒1holds i Tis Πn+2 axioma izable; ⇐=2holds i he Πn–en elope is gi en by aΠn o mula; and =⇒3holds i Tis ecu si ely axioma izable, and, o n= 0,T`exp. In o de o simpli y he s a emen o he abo e heo em we ha e used he e he ol- lowing no a ion: Thas Πn–en elope (Πn–s–en elope) means ha he e exis s a Πn– en elope (s ong Πn–en elope) o Tin IΣn; and Tis ΠB n+2–conse a i e i ThΠn+2 (T) = ThΠn+2 (T+BΣn+1). 3 The analysis o heo ies I∆n+1(T) and B∗∆n+1(T) ha we de elop in his pape is ela ed wi h he wo k o L. D. Beklemishe in [2], [3] and [4], on induc ion and collec ion as in e ence ules. Some esul s in hose pape s, p o ed he e using P oo Theo e ic echniques, a e simila o hose gi en he e o schemes on ∆n+1(T)– o mulas. Now we gi e a mo e p ecise desc ip ion o he ela ionship be ween Beklemishe ’s wo k and ou s. In he pape s ci ed abo e, Beklemishe s udy he schemes o induc ion and collec ion as in e ence ules. The induc ion ule o a o mula ϕ(x) is: ϕ(0),∀x(ϕ(x)→ϕ(x+ 1)) ∀x ϕ(x) I Γ is a class o o mulas, hen Γ–IR is he class o induc ion ules o each o mula in Γ. Gi en a heo y T, le T+ Σn+1–IR be he closu e o Tunde i s o de logic and applica ions o Σn+1–IR. We also deno e by [T,Σn+1–IR] he closu e o Tunde i s o de logic and unnes ed applica ions o Σn+1–IR; ha is, he ule o induc ion can be applied only i he hypo hesis o he ule a e heo ems o T(in i s o de logic). The ule o collec ion o a o mula ϕ(x, y) is: ∀x∃y ϕ(x, y) ∀z∃u∀x≤z∃y≤u ϕ(x, y) Theo ies T+ Σn+1–CR and [T,Σn+1–CR] a e de ined as o he induc ion ule. In [4] i is also conside ed he induc ion ule o ∆n+1 o mulas: o each ϕ(x)∈Σn+1 and ψ(x)∈Πn+1 ∆n+1–IR : ∀x(ϕ(x)↔ψ(x)) Iϕ,x As we shall see in 2.19, a heo y T(ex ension o I∆0) has ∆n+1–collec ion i and only i Tis closed unde Σn+1–CR ( ha is, [T,Σn+1–CR] ⇐⇒ T). Fo induc ion we ha e ha Thas ∆n+1–induc ion i and only i Tis closed unde ∆n+1–IR. Ou analysis o heo ies wi h ∆n+1–collec ion using Πn– unc ional classes is also e y simila ( o n= 0) o he one gi en by Beklemishe in [2] using wha he call mono one o mulas. In his way heo em 3.5 can be conside ed a gene aliza ion o heo em 5.4 o [2] (and i is linked wi h heo em 4.2 o [3]). Ne e heless, we mus obse e ha one o he aims o Beklemishe ’s wo k in [3] is o ob ain a p oo o F iedman–Pa is’ conse a i eness heo em. On he o he hand, ou analysis goes in a e e se di ec ion, since we ake ha esul as basic (due o i s easy model heo e ic p oo ) and ela e i wi h a cha ac e iza ion o Πn–en elopes using indica o s (Πn–IND p ope y, see heo em 5.6). The ela ionship o Σn+1–IR wi h he wo k de eloped he e is no so ob ious. Bu , as Beklemishe has no ed (pe sonal communica ion), I∆n+1(IΣn+1)⇐⇒ I∆0+ Σn+1–IR. This ac is closely ied o a conse a i eness heo em o Pa sons (see [18]) ThΠn+2 (IΣn+1)⇐⇒ I∆0+ Σn+1–IR. These esul s a e mo e deeply s udied in [8] in connec ion wi h axioma iza ion p ope ies o he heo ies I∆n+1(T). We conclude his sec ion wi h some basic esul s and no a ion ha we use h ough his pape . We wo k in he i s –o de language o A i hme ic, L={0,1,+,·, <}and N deno es he s anda d model o Lwhose uni e se is he se o he na u al numbe s, ω. As 4 usual, bounded quan i ie s a e deno ed by ∀x≤ ϕ(x) and ∃x≤ ϕ(x) (whe e xdoes no occu in ). ∆0= Σ0= Π0is he class o bounded o mulas and, o each n∈ω, Σn+1 ={∃~x ϕ(~x) : ϕ(~x)∈Πn}and Πn+1 ={∀~x ϕ(~x) : ϕ(~x)∈Σn}. Le ϕ(x,~ ) be a o mula o L. We shall deno e ϕ(x,~ )∧ ∀y < x ¬ϕ(y,~ ) by ϕµ,x(x,~ ). I A|=ϕµ,x(a,~ b) hen we w i e A|=a= (µx)[ϕ(x,~ b)]. I he e is no dange o misunde - s anding we omi he subsc ip xand he pa ame e s ~ and we shall w i e ϕµ(x). We deno e by P−a ini e se o Π1axioms such ha i A|=P− hen Ais he nonnega i e pa o a commu a i e disc e ely o de ed ing (see [12]). Le ϕ(x,~ ) be a o mula. The induc ion and he leas numbe p inciple axioms o ϕ(x,~ ) wi h espec o xa e, espec i ely, he ollowing o mulas Iϕ,x(~ )≡ϕ(0,~ )∧ ∀x[ϕ(x,~ )→ϕ(x+ 1,~ )] → ∀x ϕ(x,~ ), Lϕ,x(~ )≡ ∃x ϕ(x,~ )→ ∃x ϕµ,x(x,~ ). Le ϕ(x, y,~ ) be a o mula. The collec ion axiom and he s ong collec ion axiom o ϕ wi h espec o x, y a e, espec i ely, he o mulas Bϕ,x,y(z,~ )≡ ∀x≤z∃y ϕ(x, y,~ )→ ∃u∀x≤z∃y≤u ϕ(x, y,~ ), Sϕ,x,y(z,~ )≡ ∃u∀x≤z[∃y ϕ(x, y,~ )→ ∃y≤u ϕ(x, y,~ )]. As usual, we w i e Iϕins ead o Iϕ,x and simila ly we use Lϕ,Bϕand Sϕ. I Γ is a class o o mulas o L, hen IΓ = P−+{Iϕ:ϕ∈Γ}. The heo y LΓ is de ined simila ly using Lϕins ead o Iϕ. Fo collec ion, BΓ = I∆0+{Bϕ:ϕ∈Γ}and using Sϕins ead o Bϕ we ob ain SΓ. Peano A i hme ic is he heo y PA =P−+{Iϕ:ϕ o mula}. Now we conside schemes o pa ame e ee o mulas. Le Γ be a class o o mulas. We w i e ϕ(x1, . . . , xn)∈Γ−i ϕ∈Γ and x1, . . . , xna e all he a iables ha occu ee in ϕ. Then IΓ−=P−+{Iϕ,x :ϕ(x)∈Γ−}(simila ly o LΓ−) and BΓ−=I∆0+{B− ϕ,x,y : ϕ(x, y)∈Γ−}, whe e B− ϕ,x,y ≡ ∀x∃y ϕ(x, y)→ ∀z∃u∀x≤z∃y≤u ϕ(x, y). The pa ame e ee e sion o he s ong collec ion scheme o Σn o mulas is equi alen o SΣn. One o he basic unc ions used o desc ibe me ama hema ical p ope ies in he language o A i hme ic, such as u h p edica es, is he exponen ial unc ion. Le E(x, y, z) be a ∆0– o mula ha de ines in he s anda d model he exponen ial unc ion, I∆0p o es i s basic p ope ies and IΣ1p o es ha i is o al (see [10] o de ails). We shall usually w i e xy=zins ead o E(x, y, z) and shall deno e by exp he Π2sen ence ∀x∀y∃zE(x, y, z). We shall w i e: T=⇒T0, i Tis an ex ension o T0;T×=⇒T0, i Tis no an ex ension o T0;T×⇐⇒ T0, i T×=⇒T0and T0×=⇒T;T⇐⇒ T0, i Tand T0a e equi alen ; and T|=⇒T0, i Tis a p ope ex ension o T0. We ecall some de ini ions and esul s which a e impo an in he s udy o he abo e schemes. Le A|=P−,n∈ωand X⊆A. Then Kn(A, X) (i Xis he emp y se , we w i e Kn(A)) is he subs uc u e o Awhose uni e se is {b∈A:bis Σnde inable in (A, X)}. In(A, X) is he ini ial segmen o Ade e mined by Kn(A, X). I holds he ollowing esul s. Theo em 1.5. (1) Le A|=IΣnbe nons anda d. Then o all X⊆A (a) Kn+1(A, X)≺n+1 Aand Kn+1(A, X)|=IΣn. (b) Kn+1(A, X)≺c n+1 In+1(A, X)≺e nA. (⊂cand ⊂emean co inal and ini ial subs uc u e, espec i ely). 5 (c) I Kn+1(A, X)is no co inal in A hen In+1(A, X)|=BΣn+1. (2) Le A|=IΣn+1 be nons anda d such ha Kn+1(A)is nons anda d. Then Kn+1(A)6|= BΣ− n+1 and In+1(A)6|=IΣn+1. Finally, we in oduce he axiom schemes o ∆n+1 o mulas. I∆n+1 =P−+{∀x[ϕ(x,~ )↔ψ(x,~ )] →Iϕ,x(~ ) : ϕ∈Σn+1, ψ ∈Πn+1}. Using Lϕins ead o Iϕ, we ob ain L∆n+1. Pa ame e ee schemes, I∆− n+1 and L∆− n+1, a e de ined simila ly. Uni o m e sions o he abo e agmen s ha e been in oduced by R. Kaye (see [11]). UI∆n+1 is P− oge he wi h, o all ϕ∈Σn+1, ψ ∈Πn+1, ∀x∀~ [ϕ(x,~ )↔ψ(x,~ )] → ∀~ Iϕ,x(~ ). UL∆n+1 is de ined acco dingly using Lϕ. We in oduce a uni o m e sion o collec ion. UB∆n+1 is I∆0 oge he wi h, o all ϕ∈Πnand ψ∈Σn, ∀x∀~ [∃y ϕ(x, y,~ )↔ ∀w ψ(x, w,~ )] → ∀z∀~ Bϕ,x,y(z,~ ). Theo em 1.6. Fo all n∈ω,I∆− n+1 ×=⇒UL∆n+1 and IΠ− n+1 |=⇒L∆− n+1 =⇒I∆− n+1 ⇑ ⇑ UB∆n+1 ⇐⇒ BΣ− n+1 ⇐⇒ UL∆n+1 =⇒UI∆n+1 |=⇒IΣn ⇑ ⇑ ⇑ BΣn+1 ⇐⇒ L∆n+1 =⇒I∆n+1 Fo n≥1,L∆− n+1 ×=⇒UI∆n+1 and I∆− n+1 ×⇐⇒ IΣn, bu I∆− 1|=⇒I∆0. R.O. Gandy (see [10]) p o ed he equi alence be ween L∆n+1 and BΣn+1; and R. Kaye (see [11]) ob ained a simila esul o he uni o m e sions. See [9] o UI∆n+1 |=⇒IΣn, L∆− n+1 ×=⇒UI∆n+1 and I∆− n+1 ×=⇒UL∆n+1; [7] o I∆n+1 |=⇒UI∆n+1;2.14 o UB∆n+1 ⇐⇒ BΣ− n+1; and [4] o UI∆1|=⇒I∆− 1( he e UI∆1is deno ed by sI∆1). The abo e diag am con ains he ollowing open p oblems: (–): The Pa is–F iedman’s Conjec u e: L∆n+1 ⇐⇒ I∆n+1. (–): The Uni o m Pa is–F iedman’s Conjec u e: UL∆n+1 ⇐⇒ UI∆n+1. (–): The Pa ame e F ee Pa is–F iedman’s Conjec u e: L∆− n+1 ⇐⇒ I∆− n+1. Recen ly, T. Slaman (see [19]) has ob ained a pa ial answe . He has p o ed ha L∆n+1 +exp ⇐⇒ I∆n+1 +exp. On he o he hand, L. Beklemishe (see [4]) has p o ed ha I∆1+exp is a Σ3– conse a i e ex ension o UI∆1+exp; hence, UL∆1+exp ⇐⇒ UI∆1+exp. Beklem- ishe ’s esul seems o be easily ex ended o n≥1; so, only he case n= 0 seems o be open in he wo i s p oblems. Howe e , Slaman’s p oo es s on he equi alence be ween BΣn+1 and L∆n+1; he e o e i can no be adap ed o he pa ame e ee p oblem. 6 2. The heo ies I∆n+1(T),L∆n+1(T)and B∗∆n+1(T) Th ough his pape Twill deno e a consis en heo y in he i s –o de language o A i hme ic. Fo such a heo y we in oduce he classes o o mulas ∆n+1(T) = {ϕ(x,~ )∈Σn+1 : he e exis s ψ(x,~ )∈Πn+1,T`ϕ↔ψ}. When he schemes o induc ion and minimiza ion a e es ic ed o hese classes o o mulas we ob ain he heo ies I∆n+1(T) and L∆n+1(T). We also conside he ollowing e sion o he collec ion schemes B∗∆n+1(T) = I∆0+{Bϕ,x,y(z,~ ) : ϕ∈Πn,∃y ϕ(x, y,~ )∈∆n+1(T)}. Rema k 2.1.We shall begin wi h some basic p ope ies o he heo ies in oduced abo e. Fi s we obse e ha IΣn+1 =⇒I∆n+1(T) =⇒IΣn. I ϕ∈Σn+1 and ψ∈Πn+1 hen ϕ↔ψis a Πn+2– o mula. So, i ollows ha (a simila esul holds o minimiza ion and collec ion) Claim 2.2. I ThΠn+2 (T) = ThΠn+2 (T0) hen I∆n+1(T)⇐⇒ I∆n+1(T0). Le ∆∗ n+1(T) be he dual class o ∆n+1(T). Since he nega ion o a ∆n+1(T) o mula ( ha is, a ∆∗ n+1(T)– o mula) is equi alen (in T) o a ∆n+1(T)– o mula, as in he p oo o IΠn+1 ⇐⇒ IΣn+1 (see lemma 7.5 in [12]), we ge ha Claim 2.3. L∆n+1(T) =⇒I∆∗ n+1(T)⇐⇒ I∆n+1(T). Fo each ψ(x, y)∈Πn−1,∃y[ψ(x, y)∨(¬∃z ψ(x, z)∧y= 0)] ∈∆n+1(T). So, as in he p oo o BΣn+1 =⇒IΣn(see I.2.15 in [10]), we ob ain Claim 2.4. B∗∆n+1(T) =⇒IΣn. Hence, o n≥1,B∗∆n+1(T)|=⇒BΣn. Suppose ha Tis an ex ension o IΣn. Le ϕ∈Πnand ψ∈Σnsuch ha T` ∃y ϕ(x, y)↔ ∀y ψ(x, y). Le us conside he ollowing o mulas θ1(x, w)≡x≤w∧ ∃u[ϕµ,u(x, u)∧(∀z)x≤z≤w∃y≤u ϕ(z, y)], θ2(x, w)≡x≤w∧ ∀y ψ(x, y)∧ ∀u[ϕ(x, u)→(∀z)x≤z≤w∃y≤u ϕ(z, u)]. Then T`θ1(x, w)↔θ2(x, w) and θ1∈Σn+1 and θ2∈Πn+1 in Tand in L∆n+1(T). F om his, as in lemma I.2.17 in [10], we ob ain ha Claim 2.5. I Tis an ex ension o IΣn hen L∆n+1(T) =⇒B∗∆n+1(T). De ini ion 2.6. (∆n+1 p ope ies) We say ha (1) Tis ∆n+1–closed i ∆n+1(T)is closed in Tunde bounded quan i ie s. (2) Thas ∆n+1–collec ion i T=⇒B∗∆n+1(T). (3) Thas ∆n+1–minimiza ion i T=⇒L∆n+1(T). (4) Thas ∆n+1–induc ion i T=⇒I∆n+1(T). (5) Tis ∆n+1–PF i I∆n+1(T)⇐⇒ L∆n+1(T). 7 Rema k 2.7.Le us conside some examples o heo ies ha ing ∆n+1 p ope ies. Since BΣn+1 =⇒B∗∆n+1(T), we ge ha e e y heo y ex ending BΣn+1 has ∆n+1–collec ion. Now we imp o e his esul . Claim 2.8. I T=⇒BΣ− n+1 hen Thas ∆n+1–collec ion. P oo o Claim. Le ϕ(x, y, 1, . . . , m)∈Π− nand ψ(x, w,~ )∈Σ− nsuch ha T` ∃y ϕ(x, y,~ )↔ ∀w ψ(x, w,~ ). Le θ(x, y)∈Σ− n+1 be ϕ((x)0, y, (x)1, . . . , (x)m)∨[y= 0 ∧ ¬∀w ψ((x)0, w, (x)1, . . . , (x)m)]. Since T` ∀x∃y θ(x, y), T` ∀z∃u∀x≤z∃y≤u θ(x, y). Le A|=Tand a,~ b∈A such ha A|=∀x≤a∃y ϕ(x, y,~ b) and c=ha,~ bi. Then he e exis s d∈Asuch ha A|=∀x≤c∃y≤d θ(x, y). Since a≤c, hen A|=∀x≤a∃y≤d ϕ(x, y,~ b); hence, A|=Bϕ, as equi ed. ¤ The e exis heo ies, e.g. IΣn(see 2.17), ha ha e ∆n+1–collec ion and a e no ex en- sion o BΣ− n+1. Now we p esen a case in which bo h condi ions a e equi alen . Claim 2.9. I Tis comple e and has ∆n+1–collec ion hen T=⇒BΣ− n+1. P oo o Claim. Le A|=Tand θ(x, y)∈Σ− n+1 such ha A|=∀x∃y θ(x, y). Since T is comple e, T` ∀x∃y θ(x, y); so, ∃y θ(x, y)∈∆n+1(T). Since Thas ∆n+1–collec ion, A|=Bθ; hence, A|=∀z∃u∀x≤z∃y≤u θ(x, y). ¤ Nex esul was, ch onologically, he main eason o in oduce he heo y B∗∆n+1(T). This heo y became one o he main ools in his wo k once we came o he concep o Πn– unc ional heo y (see subsec ion 3.1). Theo em 2.10. (1) I Tis ∆n+1–closed hen Tis ∆n+1–PF. (2) I Thas ∆n+1–collec ion hen Tis ∆n+1–closed. P oo . ((1)): By 2.3, i is enough o see ha I∆n+1(T) =⇒L∆n+1(T). Suppose ha he e exis A|=I∆n+1(T) and ϕ(x)∈∆n+1(T) such ha A|=∃x ϕ(x)∧ ∀x¬ϕµ(x). Le θ(z)∈Πn+1 be ∀x≤z¬ϕ(x). We ha e ha A|=θ(0) ∧[θ(z)→θ(z+ 1)]. Since Tis ∆n+1–closed, θ(z)∈∆∗ n+1(T). By 2.3,A|=I∆∗ n+1(T); so, A|=∀x¬ϕ(x), a con adic ion. ((2)): Le ϕ(x, y)∈Πn,ψ(x, y)∈Σnsuch ha T` ∃y ϕ(x, y)↔ ∀y ψ(x, y). By he closu e p ope ies unde bounded quan i ica ion o BΣn, he e exis s θ(z)∈Σn+1 such ha BΣn`θ(z)↔ ∃u∀x≤z∃y≤u ϕ(x, y) ( o n= 0, we do no need BΣn). The ollowing equi alences hold in he gi en heo ies. ∀x≤z∀y ψ(x, y)↔ ∀x≤z∃y ϕ(x, y) [in T] ↔ ∃u∀x≤z∃y≤u ϕ(x, y) [in B∗∆n+1(T)] ↔θ(z) [in BΣn] Since Thas ∆n+1–collec ion, all he abo e equi alences hold in T. Then, as ∀x≤ z∀y ψ(x, y)∈Πn+1,θ(z)∈∆n+1(T). So, ∀x≤z∃y ϕ(x, y) is equi alen in T o a ∆n+1(T) o mula. ¤ 8 Rema k 2.11.Now we desc ibe o he s elemen a y ela ions among ∆n+1 p ope ies o a heo y. Claim 2.12. I Thas ∆n+1–collec ion hen Thas ∆n+1–induc ion. P oo o Claim. Suppose ha T` ∃y ϕ(x, y)↔ ∀y ψ(x, y), whe e ϕ(x, y)∈Πn,ψ(x, y)∈ Σn. Le θ(x, y)∈Πnbe ϕ(x, y)∨ ¬ψ(x, y). Since T` ∀x∃y θ(x, y), hen ∃y θ(x, y)∈ ∆n+1(T). Now he p oo con inues as in 2.4.¤ Claim 2.13. The ollowing condi ions a e equi alen (i) Thas ∆n+1–collec ion. (ii) Tis ∆n+1–closed and has ∆n+1–induc ion. (iii) Thas ∆n+1–minimiza ion. P oo o Claim. (i) =⇒(ii) is 2.10 and 2.12.(ii) =⇒(iii) ollows om 2.10–(1). ((iii) =⇒(i)): Suppose ha Thas ∆n+1–minimiza ion. Then T=⇒IΣn; so, by 2.5, L∆n+1(T) =⇒B∗∆n+1(T). Hence, T=⇒B∗∆n+1(T). ¤ Fo each model A,Th(A) has ∆n+1–collec ion i and only i A|=UB∆n+1 (o A|= BΣ− n+1, see 2.9); and Th(A) has ∆n+1–minimiza ion i only i A|=UL∆n+1. So, as a consequence o 2.13, we ob ain ha Claim 2.14. BΣ− n+1 ⇐⇒ UB∆n+1 ⇐⇒ UL∆n+1. Rema k 2.15 (ThΠn+2 (T)and ∆n+1 p ope ies).He e we shall see ha a heo y Thas a ∆n+1–p ope y i and only i ThΠn+2 (T) has ha p ope y. This is easily seen o ∆n+1–closed. Now we conside ∆n+1–induc ion. Claim 2.16. T=⇒I∆n+1(T)i and only i ThΠn+2 (T) =⇒I∆n+1(T). P oo o Claim. Le ϕ∈Σn+1 and ψ∈Πn+1 such ha T`ϕ↔ψ. Le Iϕ,ψ be ψ(0) ∧ ∀x[ϕ(x)→ψ(x+ 1)] → ∀x ψ(x). Then, ThΠn+2 (T)`Iϕ↔Iϕ,ψ. Suppose ha Thas ∆n+1–induc ion, hen T`Iϕ; hence, T`Iϕ,ψ. Since Iϕ,ψ ∈Πn+2,ThΠn+2 (T)`Iϕ,ψ; so, ThΠn+2 (T)`Iϕ, as equi ed. ¤ F om his, 2.13 and 2.10 we ge a simila esul o L∆n+1(T); and om 2.5, using again 2.13, also o B∗∆n+1(T). Claim 2.17. I ThΠn+2 (T) = ThΠn+2 (BΣn+1),Thas ∆n+1–collec ion. So, IΣn,I∆n+1 and UI∆n+1 ha e ∆n+1–collec ion. Rema k 2.18.Now we s udy ela ions be ween I∆n+1(T) and IΣn,BΣn+1 and BΣ− n+1. By 2.17,IΣnhas ∆n+1–collec ion; so, by 2.10 and 2.4, i ollows ha IΣn⇐⇒ I∆n+1(IΣn)⇐⇒ L∆n+1(IΣn)⇐⇒ B∗∆n+1(IΣn). F om his esul , 1.3 and 2.2 we ge ha IΣn⇐⇒ I∆n+1(BΣn+1)⇐⇒ L∆n+1(BΣn+1)⇐⇒ B∗∆n+1(BΣn+1). 9 Claim 3.23. Le ψ(~x, ~y)∈Π− nsuch ha T` ∀~x ∃~y ψ(~x, ~y). The e is a e m o L(G n(T)), (~x), such ha (IΣn+Funcn(T))G n(T)` ∀~x ∃~y ≤ (~x)ψ(~x, ~y). P oo o Claim. Le ψ0(u, ) be ∀~x ≤u∀~y ≤ ψc(u, , ~x, ~y), whe e ψc(u, , ~x, ~y) is as in 3.3. Then T` ∀u∃ ψ0(u, ). Le θ(u, )∈Π− nbe ψ0 (u, ), see 3.4, and le (~x) be he e m Gθ(Jk(x1, . . . , xk)) (whe e Jk(x1, . . . , xk) is a e m o L(G n(T)) associa ed o Can o ’s unc ion used in con ac ion o quan i ie s). Then (IΣn+ Funcn(T))G n(T)` ∀~x ∃~y ≤ (~x)ψ(~x, ~y). ¤ In wha ollows (Γ,Γ1) shall deno e a Πn–Pa ikh pai . Claim 3.24. (n≥1) Le ϕ(~x, ~y)∈Πn−1and ψ(~x, ~y)∈Σn−1. Then he e exis e ms o L(Γ), (~x), 0(~x), such ha (IΣn+ Γ1)Γ` ∃~y ϕ(~x, ~y)↔ ∃~y ≤ (~x)ϕ(~x, ~y), (IΣn+ Γ1)Γ` ∀~y ψ(~x, ~y)↔ ∀~y ≤ 0(~x)ψ(~x, ~y). P oo o Claim. Le ϕ1(~x, ~y)∈Πnbe he o mula ϕ(~x, ~y)∨(∀~z ¬ϕ(~x, ~z)∧~y = 0). Since IΣn+ Γ1` ∀~x ∃~y ϕ1(~x, ~y), by 3.20–(1), he e exis s a e m o L(Γ), (~x), such ha (IΣn+ Γ1)Γ` ∀~x ∃~y ≤ (~x)ϕ1(~x, ~y); hence, (IΣn+ Γ1)Γ` ∃~y ϕ(~x, ~y)↔ ∃~y ≤ (~x)ϕ(~x, ~y). Fo ψ∈Σn−1we ob ain he esul , om he abo e one, using ¬ψ.¤ Claim 3.25. Le ϕ(~x, ~y)∈∆Γ 0such ha (IΣn+ Γ1)Γ` ∀~x ∃~y ϕ(~x, ~y).The e is a e m (~x) o L(Γ) such ha (IΣn+ Γ1)Γ` ∀~x ∃~y ≤ (~x)ϕ(~x, ~y). P oo o Claim. By 3.20–(2), he e exis s ψ(~x, ~y, z)∈Πnsuch ha ∃z ψ(~x, ~y, z)∈∆n+1(IΣn+ Γ1) and (IΣn+ Γ1)Γ`ϕ(~x, ~y)↔ ∃z ψ(~x, ~y, z). Le (~x) be a e m o L(Γ) such ha (IΣn+ Γ1)Γ` ∀~x ∃~y, z ≤ (~x)ψ(~x, ~y, z). Then (IΣn+ Γ1)Γ` ∀~x ∃~y ≤ (~x)ϕ(~x, ~y). ¤ Claim 3.26. Le ϕ(~x)∈∆Γ 1((IΣn+ Γ1)Γ). Then he e exis s θ(~x)∈∆Γ 0such ha (IΣn+ Γ1)Γ`ϕ(~x)↔θ(~x). P oo o Claim. Assume (IΣn+ Γ1)Γ` ∃y ϕ0(~x, y)↔ ∀y ψ0(~x, y), whe e ϕ0(~x, y) and ψ0(~x, y) a e ∆Γ 0and ϕ(~x) is ∃y ϕ0(~x, y). Le δ(~x, y)∈∆Γ 0 he o mula ϕ0(~x, y)∨ ¬ ψ0(~x, y). Then (IΣn+ Γ1)Γ` ∀~x ∃y δ(~x, y); so, by 3.25, he e exis s a e m (~x) o L(Γ) such ha (IΣn+ Γ1)Γ` ∀~x ∃y≤ (~x)δ(~x, y). Hence, (IΣn+ Γ1)Γ`ϕ(~x)↔ ∃y≤ (~x)ϕ0(~x, y). ¤ Theo em 3.27. Le (Γ,Γ1)be a Πn–Pa ikh pai , ϕ(~x)∈∆n+1(IΣn+ Γ1). Then he e exis s θ(~x)∈∆Γ 0such ha (IΣn+ Γ1)Γ`ϕ(~x)↔θ(~x). P oo . Fo n= 0 he esul ollows om 3.26. Suppose ha n≥1. Le ϕ0(~x, ~y, ~z1, . . . , ~zn), ψ0(~x, ~y, ~z1, . . . , ~zn)∈∆0such ha (assume ne en) (–): ϕ(~x)≡ ∃~y ∀~z1∃~z2. . . ∃~znϕ0(~x, ~y, ~z1, ~z2, . . . , ~zn), (–): ψ(~x)≡ ∀~y ∃~z1∀~z2. . . ∀~znψ0(~x, ~y, ~z1, ~z2, . . . , ~zn), and (–): (IΣn+ Γ1)Γ`ϕ(~x)↔ψ(~x). 16 By 3.24, he e exis 1(~x, ~y), 2(~x, ~y, ~z1), . . . , n(~x, ~y, ~z1, . . . , ~zn−1) e ms o L(Γ) such ha he ollowing o mulas a e equi alen in (IΣn+ Γ1)Γ (–): ∀~z1∃~z2...∃~znϕ0(~x, ~y, ~z1, . . . , ~zn). (–): ∀~z1≤ 1(~x, ~y)∃~z2≤ 2(~x, ~y, ~z1). . . ∃~zn≤ n(~x, ~y, ~z1, . . . , ~zn−1)ϕ0. Le ϕ0(~x, ~y)∈∆Γ 0be he las o mula. Analogously, we ge ha he e exis 0 1(~x, ~y), 0 2(~x, ~y, ~z1), . . . , 0 n(~x, ~y, ~z1, . . . , ~zn−1) e ms o L(Γ) such ha he ollowing o mulas a e equi alen in (IΣn+ Γ1)Γ (–): ∃~z1∀~z2. . . ∀~znψ0(~x, ~y, ~z1, . . . , ~zn). (–): ∃~z1≤ 0 1(~x, ~y)∀~z2≤ 0 2(~x, ~y, ~z1). . . ∀~zn≤ 0 n(~x, ~y, ~z1, . . . , ~zn−1)ψ0. Le ψ0(~x, ~y)∈∆Γ 0be he las o mula. Then (IΣn+ Γ1)Γ` ∃~y ϕ0(~x, ~y)↔ ∀~y ψ0(~x, ~y). So, ∃~y ϕ0(~x, ~y)∈∆Γ 1((IΣn+Γ1)Γ) and, by 3.26, he e is θ(~x)∈∆Γ 0such ha (IΣn+Γ1)Γ` ∃~y ϕ0(~x, ~y)↔θ(~x); hence, (IΣn+ Γ1)Γ`ϕ(~x)↔θ(~x), as equi ed. ¤ Theo em 3.28. Le Tbe an ex ension o IΣn. Then Tis Πn–Pa ikh ⇐⇒ Tis ∆n+1–closed. P oo . (=⇒): Le ϕ(x,~ )∈∆n+1(T) and (~ )∈Te m(L). Le us see ha ∀x≤ (~ )ϕ(x,~ )∈∆n+1(T). Le (Γ,Γ1) be a Πn–Pa ikh pai o T. Then, using 3.27 and 3.20–(2), he e exis θ(x,~ )∈∆Γ 0and ψ(~ )∈∆n+1(T) such ha (IΣn+ Γ1)Γp o es ϕ(x,~ )↔θ(x,~ ) and ∀x≤ (~ )ϕ(x,~ )↔ψ(~ ). (⇐=): Le us p o e ha (G n(T),Funcn(T)) is a Πn–Pa ikh pai o T. By 3.23, we only need o p o e 3.20–(2). The p oo is by induc ion on he leng h o ∆Γ 0– o mulas. Le θ(~x)∈ ∆Γ 0, we only conside he case whe e θ(~x) is ∃y≤ (~x)θ0(~x, y). By induc ion hypo hesis he e exis s ψ0(~x, y)∈∆n+1(T) such ha (IΣn+ Funcn(T))G n(T)`ψ0(~x, y)↔θ0(~x, y). Then, by 3.2–(ii), he e exis s δ(~x, )∈∆n+1(IΣn+ Funcn(T)) such ha (IΣn+ Funcn(T))G n(T)` ∃ [δ(~x, )∧ ∃y≤ ψ0(~x, y)] ↔ ∃y≤ (~x)θ0(~x, y). As Tis ∆n+1–closed, he e exis s ψ(~x, )∈∆n+1(T) such ha T` ∃y≤ ψ0(~x, y)↔ψ(~x, ). Since ∃ [δ(~x, )∧ψ(~x, )] ∈∆n+1(T), his p o es he esul . ¤ 4. Ex ended Pa ikh’s Theo em In his sec ion, we shall see ha o some kind o Πn– unc ional class Γ he e exis s an ex ension o Lsuch ha each ∆n+1(IΣn+ Γ∗) o mula is equi alen o a bounded o mula o L(Γ). 4.1. ∆Γ 0 o mulas as ∆n+1 o mulas. Lemma 4.1. Le Γ⊆Πnand Γ1⊆Πn+2 such ha Func(Γ) ⊆Γ1and o all s(~x), (~x, y)∈Te m(L(Γ)) he e exis s s(~x)∈Te m(L(Γ)) such ha (BΣn+ Γ1)Γ`y≤s(~x)→ (~x, y)≤ s(~x). 17 (1) Le ϕ(~x)∈∆Γ 0. Then he e exis ψ(~x, z)∈Σn,θ(~x, z)∈Πnand (~x)∈Te m(L(Γ)) such ha (BΣn+ Γ1)Γ` ∀z≥ (~x) [ϕ(~x)↔ψ(~x, z)↔θ(~x, z)]. (2) Le ϕ(~x)∈∆Γ 0. Then he e exis s δ(~x)∈∆n+1(BΣn+Γ1)such ha (BΣn+Γ1)Γ` ϕ(~x)↔δ(~x). Fo n= 0,BΣ0can be eplaced by I∆0(collec ion is no needed). P oo . By induc ion on he leng h o ϕ(~x) as in lemma I.1.30 in [10]. ¤ Rema k 4.2.Le Γ be a Πn– unc ional class. We ha e he ollowing esul s. Claim 4.3. Fo e e y (~x, y), s(~x)∈Te m(L(Γ)) he e exis s a e m s(~x)such ha (I∆0+ Γ∗)Γ`y≤s(~x)→ (~x, y)≤ s(~x). So, lemma 4.1 holds o (BΣn+ Γ∗)Γand (Γ,Γ∗)sa is ies pa (2) o de ini ion 3.20. P oo o Claim. By 3.2–(i), he esul ollows aking s(~x) as (~x, s(~x)). ¤ Claim 4.4. (IΣn+ Γ∗)Γ=⇒I∆Γ∗ 0. P oo o Claim. Le ϕ(x)∈∆Γ 0and A|= (IΣn+ Γ∗)Γsuch ha A|=∃x ϕ(x). By 4.1– (1), he e exis ψ(x, z)∈Σnand (x) e m o L(Γ) such ha (BΣn+ Γ∗)Γ|=∀z≥ (x) [ϕ(x)↔ψ(x, z)]. Le a∈Asuch ha A|=ϕ(a) and le b= (a). Then A|=ψ(a, b). Since A|=LΣn, he e is c∈Asuch ha A|=c= (µx)[ψ(x, b)]. Since Γ is a Πn– unc ional class, by 3.2–(i) A|=c= (µx)[ϕ(x)]; hence, A|=Lϕ.¤ Rema k 4.5.He e we p o e ha Π0– unc ional classes p o ide examples o Π0–Pa ikh pai s. In he nex subsec ion we shall see ha o n≥1 his is also ue o some kind o Πn– unc ional classes. In wha ollows Γ shall deno e a Π0– unc ional class. As in 4.4, using 4.1–(1) o n= 0, we ge Claim 4.6. I∆Γ∗ 0⇐⇒ (I∆0+ Γ∗)Γ. Claim 4.7 (Pa ikh’s heo em).Le Γ0⊆ΠΓ 1. Fo each ϕ(~x, ~y)∈∆Γ 0such ha I∆Γ∗ 0+ Γ0` ∀~x ∃~y ϕ(~x, ~y) he e exis s a e m (~x)o L(Γ) such ha I∆Γ∗ 0+ Γ0` ∀~x ∃~y ≤ (~x)ϕ(~x, ~y). Claim 4.8. (Γ,Γ∗)is a Π0–Pa ikh pai . P oo o Claim. By 4.7, pa (1) o de ini ion 3.20 holds o (Γ,Γ∗). So, he esul ollows om 4.3.¤ 4.2. ∆n+1 o mulas as ∆Γ 0 o mulas. S ong Πn– unc ional classes. In o de o imp o e 4.1,4.4 and 4.6–4.8, we conside a special kind o Πn– unc ional classes. Le Γ be a Πn– unc ional class and A|=I∆0+ Γ∗. We shall also deno e by A he expansion o A o L(Γ) gi en by: o e e y a, b ∈Aand ϕ∈Γ A(Gϕ(a)) = b⇐⇒ A|=ϕ(a, b). 18 Le a1, . . . , ak∈A. The simple ini ial segmen o Ade e mined by a1, . . . , akis SΓ(A, a1, . . . , ak) = {b:b≤ (~a), (~x)∈Te m(L(Γ))}. Obse e ha i A|= (I∆0+ Γ∗)Γ hen SΓ(A,~a) is an L(Γ)–s uc u e. De ini ion 4.9. Le Γbe a Πn– unc ional class. We say ha Γis a s ong Πn– unc ional class i o e e y A|=I∆0+ Γ∗and e e y I i I⊂eAas L(Γ) s uc u es hen I≺e nAas L–s uc u es. Le us obse e ha e e y Π0– unc ional class is a s ong Π0– unc ional class. Mo eo e , i Γ is a s ong Πn– unc ional class and Γ0is a Πn– unc ional class such ha Γ ⊆Γ0, hen Γ0is a s ong Πn– unc ional class. Lemma 4.10. (n≥1) Le Γbe a s ong Πn– unc ional class. Then o e e y k < n, ThΠn+2 (BΣk+2 + Γ∗) = ThΠn+2 (IΣk+ Γ∗) = ThΠn+2 (I∆0+ Γ∗). P oo . Suppose ha BΣk+2 + Γ∗` ∀x∃y ϕ(x, y), whe e ϕ(x, y)∈Πnand IΣk+ Γ∗0 ∀x∃y ϕ(x, y). By compac eness, Tis consis en , whe e T= (IΣk+ Γ∗)Γ+∀y¬ϕ(c, y) + { (c)<d: (x) e m o L(Γ)}. Le A|=T,a=A(c) and B=SΓ(A, a). Since Γ is a Πn– unc ional class, B⊂eAas L(Γ)–s uc u es and, by he las g oup o axioms o T, i is p ope . Also, o all θ(x, y)∈Γ and b∈B he e exis s d∈Bsuch ha A|=θ(b, d). Since Γ is a s ong Πn– unc ional class and A|=I∆0+ Γ∗,B≺e nAas L–s uc u es. So, om A|=∀y¬ϕ(a, y) we ge ha B|=∀y¬ϕ(a, y). Since, B|=I∆0+ Γ∗; and, o k < n,B≺e k+1 A, hen B|=BΣk+2. So, B|=BΣk+2 + Γ∗and B|=∃y ϕ(a, y). Con adic ion. This p o es he i s iden i y. The second one ollows om he i s by induc ion on k < n.¤ Rema k 4.11.(S eng h o 4.4, 4.6, 3.7, 4.1) In wha ollows le Γ be a s ong Πn– unc ional class. Claim 4.12. (i) I∆Γ∗ 0⇐⇒ (IΣn+ Γ∗)Γ⇐⇒ (I∆0+ Γ∗)Γ. (ii) I∆0+ Γ∗⇐⇒ IΣn+ Γ∗. P oo o Claim. By 4.4, (IΣn+ Γ∗)Γ=⇒I∆Γ∗ 0=⇒(I∆0+ Γ∗)Γ. Le θ∈Σn. Then BΣn+1 `Iθ; so, by 4.10 ( o k=n−1), I∆0+ Γ∗`Iθ. This p o es (i). Pa (ii) ollows om (i).¤ By 4.12, we can ew i e 3.7 as ollows Claim 4.13. (i) ThΠn+2 (I∆0+ Γ∗) = ThΠn+2 (BΣn+1 + Γ∗). (ii) I∆0+ Γ∗=⇒I∆n+1(IΣn+ Γ∗) =⇒B∗∆n+1(IΣn+ Γ∗). Claim 4.14. (i) Le ϕ(~x)∈∆Γ 0. The e a e ψ(~x, z)∈Σn,θ(~x, z)∈Πnand (~x)such ha I∆Γ∗ 0` ∀z≥ (~x) [ϕ(~x)↔ψ(~x, z)↔θ(~x, z)]. (ii) Le ϕ(~x)∈∆Γ 0. Then he e exis s δ(~x)∈∆n+1(BΣn+ Γ∗)such ha I∆Γ∗ 0` ϕ(~x)↔δ(~x). 19 P oo o Claim. Fo n≥1, IΣn=⇒BΣn. So, (IΣn+ Γ∗)Γ=⇒(BΣn+ Γ∗)Γ. Then he esul ollows om 4.1 and 4.12.¤ Theo em 4.15 (Ex ended Pa ikh’s heo em (S eng h o 4.7)). Le Γbe a s ong Πn– unc ional class and Γ0⊆Πn+1 ∪ΠΓ 1. Fo each ϕ(x, y)∈Πn∪∆Γ 0 such ha (BΣn+1 + Γ0+ Γ∗)Γ` ∀x∃y ϕ(x, y) he e exis s a e m (x)o L(Γ) such ha I∆Γ∗ 0+ Γ0` ∀x∃y≤ (x)ϕ(x, y). P oo . Deny he p oposi ion’s conclusion. We p oceed as in 4.10. By compac eness he ollowing heo y is consis en (cand da e new cons an s) T=½I∆Γ∗ 0+ Γ0+{∀y≤ (c)¬ϕ(c, y) : (x) e m o L(Γ)} +{ (c)<d: (x) e m o L(Γ)} Le A|=T,a= (c) and B=SΓ(A, a). Since Γ is a Πn– unc ional class, B⊂eAas L(Γ)–s uc u es. Then B≺e nAas L–s uc u es. So, B|=∀y¬ϕ(a, y) and, since A|=IΣn and Ais a p ope ex ension o B(las se o axioms o T), B|= (BΣn+1 + Γ0+ Γ∗)Γ. Con adic ion. ¤ Co olla y 4.16. (S eng h o 4.8) I Γis a s ong Πn– unc ional class hen (Γ,Γ∗)is a Πn–Pa ikh pai . 4.3. Exis ence heo ems o s ong Πn– unc ional classes. Theo em 4.17. (n≥1) The e is a s ong Πn– unc ional class, Hn, such ha o all ϕ∈Hn,IΣn−1`IPF(ϕ)and IΣn⇐⇒ IΣn+H∗ n. P oo . Fo each θ( , y)∈Π− n−1le θ0(x, w) be he ollowing o mula        [¬∃ ≤x∃y θ( , y)∧w= 0] ∨ ∃w1, w2≤w   w=hw1, w2i ∧ w1≤x∧ ∀ ≤x[∃y θ( , y)→ ∃y≤w2θ( , y)] ∧ θµ,w2(w1, w2)∧ ∀ ≤x[θµ,w2( , w2)→ ≤w1] I is clea ha he e is θ∗(x, w)∈Πnsuch ha IΣn−1`θ0(x, w)↔θ∗(x, w). Le Hn= {θ∗(x, w) : θ( , y)∈Πn−1}. Le θ( , y)∈Πn−1. I holds ha IΣn−1`IPF(θ∗) and IΣn` ∀x∃w θ∗(x, w); so, Hnis a Πn– unc ional class and IΣn⇐⇒ IΣn+H∗ n. Le us obse e ha H1⊆H2⊆ · · · ⊆ Hn⊆. . . . Now, by induc ion on n≥1, we p o e ha Hn is a s ong Πn– unc ional class. Le A|=I∆0+H∗ nand I⊂eAsuch ha (∗) o all ϕ(x, w)∈Hn,a∈I he e is b∈Isuch ha A|=ϕ(a, b). By induc ion on n≥1, using Ta ski–Vaugh ’s es , we p o e ha I≺nA. (n= 1): Le us see ha I≺1A. Le θ( , y)∈Π0and a∈Isuch ha A|=∃y θ(a, y). Since θ∗(x, w)∈H1and A|=I∆0+H∗ 1, hen A|=∀x∃y θ∗(x, w). Since a∈I, by (∗), he e exis s d∈Isuch ha A|=θ∗(a, d). Since I∆0`θ0(x, w)↔θ∗(x, w), A|=θ0(a, d); so, he e exis s b∈Asuch ha b≤dand A|=θ(a, b). Since d∈Iand I⊂eA, hen b∈I, as equi ed. (n→n+ 1): Since A|=I∆0+H∗ nand, by induc ion hypo hesis, Hnis a s ong Πn– unc ional class, we ge ha A|=IΣn+H∗ n. Le θ(x, y)∈Πnand a∈Isuch ha 20 A|=∃y θ(a, y). Now as in he case n= 1, using ha A|=IΣn+H∗ n, we ob ain ha he e exis s b∈Isuch ha A|=θ(a, b). ¤ P oposi ion 4.18 (S eng h o 3.8).I Thas ∆n+1–collec ion, he e is a s ong Πn– unc ional class Γsuch ha ThΠn+2 (T) = ThΠn+2 (I∆0+ Γ∗). P oo . Suppose ha n≥1. By 3.8, he e is a Πn– unc ional class Γ1such ha Thn+2(T) = Thn+2(IΣn+ Γ∗ 1). Le Γ = Hn+ Γ1. Then, Γ is a s ong Πn– unc ional class; so, by 4.17 and 4.12,IΣn+ Γ∗ 1⇐⇒ I∆0+ Γ∗. Hence ThΠn+2 (T) = ThΠn+2 (IΣn+ Γ∗ 1) = ThΠn+2 (I∆0+ Γ∗). ¤ Lemma 4.19. Le T=⇒IΣn,A|=ThΠn+2 (T)and a∈A. I (Γ,Γ1)and (Γ0,Γ0 1)a e Πn–Pa ikh pai s o T hen SΓ(A, a) = SΓ0(A, a). P oo . Le b∈ SΓ(A, a). The e a e (x)∈Te m(L(Γ)) such ha b≤ (a) and ϕ(x, y)∈ ∆n+1(T) such ha (IΣn+ Γ1)Γ` (x) = y↔ϕ(x, y). Le s(x) be a e m o L(Γ0) such ha (IΣn+ Γ0 1)Γ0` ∀x∃y≤s(x)ϕ(x, y). So, b≤s(a); hence, b∈ SΓ0(A, a). ¤ Theo em 4.20. Le Tbe an ex ension o IΣnand (Γ,Γ1)aΠn–Pa ikh pai o T(so, T is ∆n+1–closed). The ollowing condi ions a e equi alen (1) Thas ∆n+1–collec ion. (2) (IΣn+ Γ1)Γ=⇒I∆Γ 0. (3) Fo each s(~ ), (~ , x)∈Te m(L(Γ)) he e exis s s(~ )∈Te m(L(Γ)) such ha (IΣn+ Γ1)Γ`x≤s(~ )→ (~ , x)≤ s(~ ). (4) ThΠn+2 (T) = ThΠn+2 (BΣn+1 + Γ1). (5) Fo e e y A|= (IΣn+ Γ1)Γand a∈A,SΓ(A, a)≺nAas L–s uc u es and SΓ(A, a)|=ThΠn+2 (T). P oo . F om 2.8 and 2.15, i ollows (4) =⇒(1). ((1) =⇒(5)): By 4.19 and 4.16 we may assume ha Γ is a s ong Πn– unc ional class o T(and ha Γ1= Γ∗). So, by 4.9,SΓ(A, a)≺nAas L–s uc u es. Le ϕ(x, y)∈Πnsuch ha T` ∀x∃y ϕ(x, y). Then he e exis s (x)∈Te m(L(Γ)) such ha (IΣn+ Γ∗)Γ` ∀x∃y≤ (x)ϕ(x, y). Le b∈ SΓ(A, a). Then, i holds ha he e exis c∈Aand s(x)∈Te m(L(Γ)) such ha A|=c≤ (b)∧ϕ(b, c)∧b≤s(a). Since Γ is Πn– unc ional, c≤ (b)≤ (s(a)); hence, c∈ SΓ(A, a). So, SΓ(A, a)|=∃y ϕ(b, y). ((5) =⇒(4)): Le ϕ(x, y)∈Πnsuch ha BΣn+1 + Γ1` ∀x∃y ϕ(x, y). Suppose ha IΣn+ Γ10∀x∃y ϕ(x, y). Le T0be he heo y (IΣn+ Γ1)Γ+∀y¬ϕ(c, y) + { (c)<d: (x)∈Te m(L(Γ))}. By compac eness, T0is consis en . Le A|=T0and a=A(c). Since SΓ(A, a)≺e nA as L–s uc u es and is p ope , SΓ(A, a)|=∀y¬ϕ(a, y) and SΓ(A, a)|=BΣn+1. Then, SΓ(A, a)|=BΣn+1 + Γ1. Con adic ion. ((1) =⇒(2)): Le ϕ(x)∈∆Γ 0. The e exis s ψ(x)∈∆n+1(T) such ha (IΣn+ Γ1)Γ` ϕ(x)↔ψ(x). Since Thas ∆n+1–induc ion, by 2.15,IΣn+Γ1has ∆n+1–induc ion; hence, IΣn+ Γ1`Iψ. So, (IΣn+ Γ1)Γ`Iϕ. 21 ((2) =⇒(1)): Le ϕ(x)∈∆n+1(T). By 3.27, he e exis s θ(x)∈∆Γ 0such ha (IΣn+ Γ1)Γ`θ(x)↔ϕ(x). Then, by (2),T`Iϕ; so, Thas ∆n+1–induc ion. Since Tis ∆n+1–closed, by 2.13,Thas ∆n+1–collec ion. ((1) =⇒(3)): Le s(~ ), (~ , x)∈Te m(L(Γ)). By 3.2 he e exis ϕ(~ , x), θ(~ , x, z)∈ ∆n+1(IΣn+ Γ1) such ha (IΣn+ Γ1)Γ`[s(~ ) = x↔ϕ(~ , x)] ∧[ (~ , x) = z↔θ(~ , x, z)]. Le Γ0be a s ong Πn– unc ional class o T. By 4.16, he e exis 0(~ , x) and s0(~ ) e ms o L(Γ0) and ψ(~ , z)∈∆n+1(T) such ha (IΣn+ Γ∗ 0)Γ0` ∀~ ∃x≤s0(~ )ϕ(~ , x)∧ ∀~ ∀x∃z≤ 0(~ , x)θ(~ , x, z). and (IΣn+ Γ∗ 0)Γ0` 0(~ , s0(~ )) = z↔ψ(~ , z). Then IΣn+ Γ∗ 0`ϕ(~ , x0)∧x≤x0∧θ(~ , x, z)→ ∃z0(ψ(~ , z0)∧z≤z0). Since ThΠn+2 (IΣn+ Γ∗ 0) = ThΠn+2 (T) = ThΠn+2 (IΣn+ Γ1), hen IΣn+ Γ1`ϕ(~ , x0)∧x≤x0∧θ(~ , x, z)→ ∃z0(ψ(~ , z0)∧z≤z0). Since T` ∀~ ∃z ψ(~ , z), he e exis s s(~ ) such ha (IΣn+ Γ1)Γ` ∀~ ∃z≤ s(~ )ψ(~ , z). So, (IΣn+ Γ1)Γ`x≤s(~ )→ (~ , x)≤ s(~ ), as equi ed. ((3) =⇒(1)): Le ϕ(x, y,~ )∈Π− nsuch ha ∃y ϕ(x, y,~ )∈∆n+1(T). Then he e exis θ(x,~ ), ϕ0(x, y,~ )∈∆Γ 0such ha (IΣn+ Γ1)Γ`[∃y ϕ(x, y,~ )↔θ(x,~ )] ∧[ϕ(x, y,~ )↔ϕ0(x, y,~ )]. Le ψ(x,~ , y)∈∆Γ 0be (θ(x,~ )∧ϕ0(x, y,~ )) ∨(¬θ(x,~ )∧y= 0). Then, by 3.25, he e exis s (x,~ )∈Te m(L(Γ)) such ha (IΣn+ Γ1)Γ` ∀x∀~ ∃y≤ (x,~ )ψ(x,~ , y). By (3), he e exis s 0(u,~ )∈Te m(L(Γ)) such ha (IΣn+ Γ1)Γ`x≤u→ (x,~ )≤ 0(u,~ ). So, (IΣn+ Γ1)Γ` ∀u∀~ [∀x≤u∃y ϕ(x, y,~ )→ ∃u0∀x≤u∃y≤u0ϕ(x, y,~ )]. Tha is, T`Bϕ,x,y. So, Thas ∆n+1–collec ion. ¤ 5. Πn–en elopes 5.1. Gene al p ope ies o Πn–en elopes. Ini ial segmen s. In his sec ion we in oduce he concep o Πn–en elope. This gene alizes he concep o en elope (see [10]) and is closely ela ed o indica o s (see [12]). Some esul s in his sec ion a e gene aliza ions o esul s on indica o s ha appea in chap e 14 o [12]. Howe e , Πn–en elopes will p o ide us wi h Πn– unc ional classes de ined uni o mely. This is why we include hese esul s he e. In pa icula , we will ob ain Πn–en elopes ha will be used in sec ion 6 o p o e he hie a chy heo em. Fo each o mula ϕ(u, x, y) le Γϕ={ϕ(k, x, y) : k∈ω}. De ini ion 5.1. Le ϕ(u, x, y)∈Σ− n+1. We say ha (1) ϕ(u, x, y)is a Πn–q–en elope o Tin T0i T`Γ∗ ϕ, and o all k∈ω,T0` ϕ(k+ 1, x, y)→ ∃z < y ϕ(k, x, z). 22 (2) ϕ(u, x, y)sa is ies Πn–ENV o Tand T0i o each ψ(x, y)∈Π− nsuch ha T` ∀x∃y ψ(x, y), he e exis s k∈ωsuch ha T0`ϕ(k, x, y)→ ∃z < y ψ(x, z). (3) ϕ(u, x, y)is a Πn–en elope o Tin T0i ϕ(u, x, y)is a Πn–q–en elope o Tin T0 and sa is ies Πn–ENV o Tand T0. Rema k 5.2.Now we shall gi e some basic p ope ies o en elopes. Le ϕ(u, x, y)∈Σn+1 a Πn–q–en elope o Tin T0. By con ac ion o quan i ie s, pa (2) o de ini ion 5.1 is also ue o ψ(x, y)∈Σ− n+1. We also ha e ha Claim 5.3. (i) I T=⇒T0 hen ThΠn+2 (T) = ThΠn+2 (T0+ Γ∗ ϕ). (ii) I ϕ∈Πnand T+IΣnis consis en hen Γϕis a Πn– unc ional class. De ini ion 5.4. Le ϕ(u, x, y)∈Σn+1. We say ha ϕ(u, x, y)sa is ies Πn–IND o Tand T0i o e e y A|=T0coun able, nons anda d and a, b ∈A, he ollowing condi ions a e equi alen : (IND-(i)): Fo all k∈ω,A|=∃y < b ϕ(k, a, y). (IND-(ii)): The e exis s I|=Tsuch ha I≺e nAand a < I< b. Rema k 5.5.Le ϕ(u, x, y)∈Σn+1 such ha T` ∀x∃y ϕ(k, x, y), o all k∈ω. Then o all heo y T0we ha e ha : IND-(ii) =⇒IND-(i). So, i ϕ(u, x, y) is a Πn–q–en elope, hen in o de o p o e ha ϕ(u, x, y) sa is ies Πn–IND i is enough o es ablish ha : IND-(i) =⇒IND-(ii). Now we shall s udy condi ions unde which i holds ha Πn–ENV is equi alen o Πn–IND. Le us no e, howe e , ha he p oo o pa ⇐= o nex heo em shows ha , i T0=⇒IΣn, hen e e y Πn–q–en elope o Tin T0sa is ying Πn–IND is a Πn–en elope. Theo em 5.6. (n≥1) Suppose ha T0=⇒IΣnand (i) Tis ecu si ely axioma izable, and (ii) ThΠn+2 (T) = ThΠn+2 (T+BΣn+1). Le ϕ(u, x, y)∈Σn+1 be a Πn–q–en elope o Tin T0. Then wi h espec o Tand T0 ϕ(u, x, y)sa is ies Πn–ENV ⇐⇒ ϕ(u, x, y)sa is ies Πn–IND. P oo . (⇐=): Le ψ(x, y)∈Π− nsuch ha T` ∀x∃y ψ(x, y) and suppose ha o all k∈ω, T00ϕ(k, x, y)→ ∃z < y ψ(x, z). Fo all k∈ωle Tk=T0+{∃y < dϕ(j, c, y)∧ ∀z < d¬ψ(c, z) : j < k}. Since, o all k∈ω,Tkis consis en , T∗=Sk∈ωTkis consis en . Le A∗|=Tcoun able nons anda d, A=A∗ |L,a=A∗(c) and b=A∗(d). Then A|=T0and o all k∈ω, A|=∃y < b ϕ(k, a, y). Since ϕsa is ies Πn–IND o Tand T0, he e exis s I|=Tsuch ha I≺e nAand a < I< b. So, he e exis s e∈Isuch ha I|=ψ(a, e); hence, e < b and A|=ψ(a, e). Bu A∗|=∀z < d¬ψ(c, z); hence, A|=∀z < b ¬ψ(a, z). So, A|=¬ψ(a, e), a con adic ion. (=⇒): By 5.5, i is enough o p o e IND-(i) =⇒IND-(ii). We ollow he p oo o heo em 11.7 in [12]. Le A|=T0coun able, nons anda d and a, b ∈Asuch ha A|= ∃y < b ϕ(k, a, y), o all k∈ω. Le 23 T0=T+BΣn+1 +{∀~z ψ(c, ~z) : ψ(x, ~z)∈Σn,A|=∀~z ≤b ψ(a, ~z)}. By (ii) i ollows ha T0is consis en . Since A|=IΣnand n≥1, he Σn– ype o a, b in A belongs o SSy(A) ( he s anda d sys em o A); hence, {p∀~z ψ(c, ~z)q:ψ∈Σn,A|=∀~z ≤ b ψ(a, ~z)} ∈ SSy(A). So, by (i),T0∈SSy(A). Since SSy(A) is a Sco sys em, he e exis s B|=T0coun able which is SSy(A)–sa u a ed; hence, Bis ecu si ely sa u a ed. Le c=B(c). Then, o each θ(x, ~z)∈Πn, i B|=∃~z θ(c, ~z) hen A|=∃~z ≤b θ(a, ~z). So, by F iedman’s heo em, he e exis s H:Be ≺e nAsuch ha H(c) = aand b /∈H(B). Le I=H(B). Then I|=T,I≺e nAand a < I< b.¤ Rema k 5.7.Condi ion (ii) in 5.6 canno be dele ed. We ha e used i he e in o de o p o e ha : IND-(i) =⇒IND-(ii). E en mo e, suppose ha T=⇒T0=⇒IΣnand ϕ(u, x, y)∈Σn+1 is a Πn–q–en elope o Tin T0 ha sa is ies Πn-IND o hese heo ies. Le ψ(x, y)∈Πnbe such ha T+BΣn+1 ` ∀x∃y ψ(x, y). Then, i holds ha he e is k∈ωsuch ha T0`ϕ(k, x, y)→ ∃z < y ψ(x, z). So, ThΠn+2 (T) = ThΠn+2 (T+BΣn+1). Rema k 5.8.Fo Π0–en elopes we ha e he ollowing o m o 5.6. Claim 5.9. Suppose ha T0=⇒I∆0+exp,Tis ecu si ely axioma izable and ThΠ2(T) = ThΠ2(T+BΣ1). Le ϕ(u, x, y)∈Σ1aΠ0–q–en elope o Tin T0. Then, wi h espec o Tand T0, ϕ(u, x, y)sa is ies Π0–ENV ⇐⇒ ϕ(u, x, y)sa is ies Π0–IND. In some cases his esul is also ue e en hough T0is no an ex ension o I∆0+exp. Using me hods ha appea s in [1], mainly he supe exponen ial unc ion (see he p oo o lemma 3 he e), i can be p o ed ha Claim 5.10. Suppose ha T=⇒BΣ1+exp =⇒T0=⇒I∆0, and Tis ecu si ely axioma izable. Le ϕ(u, x, y)∈∆0be a Π0–q–en elope o Tin T0. Then, wi h espec o Tand T0, ϕ(u, x, y)sa is ies Π0–ENV ⇐⇒ ϕ(u, x, y)sa is ies Π0–IND. 5.2. Exis ence heo ems o Πn–en elopes. In his and in he nex subsec ion we a e go- ing o use o mulas in he language and in he me alanguage. In o de o w i e exp essions ha a e easie o ead we shall use uppe case G eek le e s o o mulas in he me alan- guage ( eal o mulas) and lowe case G eek le e s o o mulas in he language (elemen s o a model ha i hinks ha a e o mulas). We shall use σ, τ, . . . as a iables (in he language o A i hme ic) o o mulas, and pas a iable (in he language o A i hme ic) o p oo s. Theo em 5.11. I Tis ecu si ely axioma izable, Πn– unc ional and, o n= 0,T`exp, hen he e exis s a Πn–en elope o Tin IΣn. P oo . Since Tis Πn– unc ional, Thas ∆n+1–collec ion and, o n≥1, T=⇒IΣn=⇒ BΣn. Le us conside he ollowing cases: 24 Case A: n≥1. Since Tis ecu si ely axioma izable, he e is P T(x, y)∈Σ1 ha ep esen s o {(σ, p)∈ω2:pis a p oo o σin T}in P−. Le Φ0(u, x, y)∈Πnbe a o mula equi alen in BΣn(so, also in T), o ∀p, τ ≤u½Fo mΠ− n(τ( 0, 1)) ∧P T(∀ 0∃ 1τ( 0, 1), p)→ → ∀x0≤x∃y0≤ySa Πn(τ( ˙x0,˙y0)) ¾ Whe e Sa Πn( ) is a u h de ini ion in IΣ1 o Πn– o mulas. Le Φ(u, x, y)∈Σn+1 be a o mula equi alen in BΣn(so, also in T), o ∃y0≤y[y=y0+u∧Φ0(u, x, y0)∧ ∀y00 < y0¬Φ0(u, x, y00)]. Le k∈ω. Since Thas ∆n+1–collec ion, T` ∀x∃yΦ(k, x, y). Mo eo e , as y=y0+k, IΣn`Φ(k+ 1, x, y)→ ∃z < y Φ(k, x, z) and T`IPF(Φ(k, x, y)). Le Ψ(x, y)∈Π− nsuch ha T` ∀x∃yΨ(x, y) and k > pΨ(x, y)q. Then IΣn` Φ(k, x, y)→ ∃z < y Ψ(x, z). So, Φ(u, x, y) sa is ies Πn–ENV o Tand IΣn. Case B: n= 0. Since Tis ecu si ely axioma izable, he e is P T(x, y, w)∈∆0such ha ∃wP T(x, y, w) ep esen s o {(σ, p) : pis a p oo o σin T}in P−. Le Φ0(u, x, y)∈Σ0 be ∀p, ρ, w ≤u    Fo mΠ− 0(ρ( 0, 1)) ∧P T(∀ 0∃ 1ρ( 0, 1), p, w)→ ∀z, z0≤y   y=hz, z0i → →½z= 2(x+z0+2)cu∧ ∀x0≤x∃y0≤z0V0(ρ, hx0, y0i, z)¾       Whe e V0( 1, 2, 3)∈∆0is a u h de ini ion in I∆0+exp o ∆0 o mulas and c∈ω is a cons an which depends upon he explici de ini ion o V0( 1, 2, 3) (see [10], V.5.4). Le Φ(u, x, y)∈Σ0de ined as in case A. Now, as he e, i is p o ed ha Φ(u, x, y) is a Π0–en elope o Tin I∆0.¤ Rema k 5.12.Le Tbe Πn– unc ional and Φ0(u, x, y, w)∈Πnsuch ha ∃wΦ0(u, x, y, w) is a Πn–en elope o Tin IΣn. Le us see ha he e exis s a Πn o mula which is a Πn–en elope o Tin IΣn. Le Ψ(u, x, y)∈Πnbe ∃w, y0≤y[y=hw, y0i ∧ Φ0(u, x, y0, w)]. Fo each k∈ω, le Ψk(x, y) be Ψ(k, x, y). Then T` ∀x∃yΨk(x, y). Le CΨk(x, y) be as in he p oo o 3.8. The de ini ion o CΨk(x, y) is uni o m in k; so, using kas a pa ame e we ob ain CΨ(u, x, y)∈Πn. Le Θ(u, x, y)∈Πnbe Seq(y)∧lg(y) = u+ 1 ∧ ∀j≤uCΨ(j, x, (y)j). Then Θ(u, x, y)isaΠn–en elope o Tin IΣn. Theo em 5.13. (1) Fo all m≥n(m≥1, o n= 0) he e exis s a Πn–en elope o IΣmin IΣn,Φ(u, x, y)∈Πn, such ha (a) IΣm+1 ` ∀u∀x∃yΦ(u, x, y). (b) IΣm+1 ` ∀u, x, y1, y2[Φ(u, x, y1)∧Φ(u+ 1, x, y2)→y1< y2]. (2) Fo all n∈ω he e exis s a Πn–en elope, Φ(u, x, y)∈Πn, o PA in IΣnsuch ha (a) Th(N)` ∀u∀x∃yΦ(u, x, y). (b) Th(N)` ∀u, x, y1, y2[Φ(u, x, y1)∧Φ(u+ 1, x, y2)→y1< y2]. P oo . Le 1 ≤n≤m. We will p o e ha he Πn–en elope ob ained in 5.12, om he one gi en in 5.11, sa is ies he p ope ies o 1–(a) and 1–(b). Le Φ0(u, x, y)∈Πn he o mula 25 Theo em 6.11 (The Hie a chy Theo em).Le Tbe a Πn– unc ional heo y (i n= 0 we assume ha T`exp), ϕ(u, x, y)a s ong Πn–en elope o Tin Tand T0an ex ension o Tsuch ha T0` ∀u∀x∃y ϕ(u, x, y), and T0`ϕ(u, x, y1)∧ϕ(u+ 1, x, y2)→y1< y2. Then (1) Fo each A|=T0 Γϕand a∈Anons anda d, KΓϕ 0(A, a)|=I∆n+1(T)and KΓϕ 0(A, a)6|= I∆n+1(T0). (2) I∆n+1(T0)|=⇒I∆n+1(T). P oo . Pa (2) ollows om (1). By 6.10–(7),KΓϕ 0(A, a)|=I∆n+1(T). Since ∃y ϕ(u, x, y)∈ ∆n+1(T0) and, by 6.9,∃y ϕ(u, a, y) de ines ωin KΓϕ 0(A, a), hen KΓϕ 0(A, a)6|=I∆n+1(T0). ¤ Theo em 6.12. (1) Fo all m≤n,I∆n+1(IΣm)⇐⇒ IΣn. (2) Fo all m≥n,I∆n+1(IΣm+1)|=⇒I∆n+1(IΣm). (3) I∆n+1(N)|=⇒I∆n+1(PA). P oo . (1) ollows om 2.18. Le us see (2). By 5.22–(1), o e e y m≥n he e exis s a s ong Πn–en elope ha sa is ies he hypo hesis o 6.11 o T=IΣmand T0=IΣm+1; hence, (2) ollows om 6.11–(1). Pa (3) is p o ed in a simila way using 5.22–(2).¤ Lemma 6.13. Fo e e y m≥n,BΣn+1 ×=⇒I∆n+1(IΣm+1). P oo . Since I∆n+1(IΣn+1) is a Πn+2–axioma izable heo y (see [8], heo em 1.1, o [7], [15]) and, by 6.12,I∆n+1(IΣn+1)|=⇒IΣn, he esul ollows om 1.3.¤ Theo em 6.14. (1) Fo all m≥n,I∆n+1(IΣm+1)|=⇒B∗∆n+1(IΣm+1). (2) I∆n+1(PA)|=⇒B∗∆n+1(PA). (3) I∆n+1(N)|=⇒B∗∆n+1(N). P oo . Fi s obse e ha o e e y heo y T,BΣn+1 =⇒B∗∆n+1(T), and i Thas ∆n+1– collec ion hen, by 2.10,I∆n+1(T) =⇒B∗∆n+1(T). Since IΣm+1,m≥n,PA and Th(N) ha e ∆n+1–collec ion, hen (1),(2) and (3) ollow om 6.13.¤ 7. Rema ks and open ques ions The main p oblem we ha e conside ed in his wo k is he Pa is–F iedman’s Conjec u e in h ee e sions (1) Pa is–F iedman’s Conjec u e: I∆n+1 ⇐⇒ L∆n+1. (2) Uni o m Pa is–F iedman’s Conjec u e: UI∆n+1 ⇐⇒ UL∆n+1. (3) Pa ame e F ee Pa is–F iedman’s Conjec u e: I∆− n+1 ⇐⇒ L∆− n+1. F om Slaman’s esul , i holds I∆n+1 ⇐⇒ L∆n+1, o n≥1. We ha e s udied he e he ela i iza ion o hese p oblems o ∆n+1 o mulas in a heo y T. This gi es a new e sion o he Conjec u e. 4. Rela i ized Pa is–F iedman’s Conjec u e: I∆n+1(T)⇐⇒ L∆n+1(T). 32 We ha e p o ed ha i Tsa is ies some condi ions hen he ela i ized Pa is–F iedman’s Conjec u e o Tholds. So, we conside he ollowing s ong o ms o hese Conjec u es. P oblem 1.Does i hold ha o all Tex ension o IΣn (1) I Tis ∆n+1–closed hen Thas ∆n+1–collec ion? (2) I Thas ∆n+1–induc ion hen Thas ∆n+1–collec ion? (3) I Tis ∆n+1–PF hen Thas ∆n+1–collec ion? Le us obse e ha i e e y (comple e) ex ension o IΣnsa is ies 1–(2) hen he Uni o m Pa is–F iedman’s Conjec u e holds. Condi ion 3.10–(2) is ela ed wi h he Uni o m Pa is-F iedman’s Conjec u e. Le A|= UI∆n+1 and ϕ(x, y)∈Π− nsuch ha A|=∀x∃y ϕ(x, y). Le Fϕ:A−→ Abe de ined by: Fϕ(a) = (µy)[ϕ(a, y)]. Le F∗ ϕbe, he bounding map o Fϕ, de ined by F∗ ϕ(a) = (µx)≤a[∀u≤a(Fϕ(u)≤Fϕ(x))] Claim. Le A|=UI∆n+1. I o each ϕ(x, y)∈Π− nsuch ha A|=∀x∃!y ϕ(x, y), i holds ha F∗ ϕis a o al unc ion on A hen A|=UL∆n+1. Le us conside he ollowing ques ion. P oblem 2.In he abo e condi ions. Is F∗ ϕa o al unc ion? In 3.12 we ha e ob ained a conse a i eness p ope y, ThΠn+2 (T) = ThΠn+2 (T+ BΣn+1), unde which Tis Πn– unc ional and, hence, sa is ies he Rela i ized Pa is– F iedman’s Conjec u e. We ha e also ex ended his esul in 3.13 o Σn+2 ex ensions o Πn+2 axioma izable heo ies. Le us conside he ollowing p oblems. P oblem 3.(1) Le Tbe a heo y such ha T+BΣn+1 is consis en . A e he ollowing condi ions equi alen ? (a) Tis Πn– unc ional. (b) ThΠn+2 (T) = ThΠn+2 (T+BΣn+1). (c) ThΠn+2 (T) = ThΠn+2 (T+BΣ− n+1). (2) Le Tbe a Πn+2–axioma izable ex ension o IΣnand le T0be Σn+2–axioma izable such ha T+T0is consis en . Does i hold ha Tis Πn– unc ional ⇐⇒ T+T0is Πn– unc ional? In 5.11 i is p o ed ha i Tis Πn– unc ional and ecu si ely axioma izable hen Thas a Πn–en elope in IΣn( o n= 0 we add ha T`exp). Fo all n∈ω,ThΠn+2 (N) is Πn– unc ional and p o es exp. Ne e heless, ThΠn+2 (N) does no ha e a Πn–en elope in IΣn. So, i canno be omi ed ha Tis ecu si ely axioma izable. Now, we will conside i T`exp could be elimina ed o n= 0. The heo y IΠ− 1has Π0–collec ion, is ecu si ely axioma ized and IΠ− 10exp. I holds ha i ϕ(x, y)∈∆− 0 and IΠ− 1` ∀x∃y ϕ(x, y) hen he e exis s k∈ωsuch ha IΠ− 1` ∃z∀x[z < x → ∃y < xkϕ(x, y)] (see [5]). F om his i ollows ha ϕ(u, x, y)≡xu+u=yis a Π0–en elope o IΠ− 1in ThΠ1(N). Le us conside he ollowing p oblem. 33 P oblem 4.Is he e a Π0–en elope o IΠ− 1in I∆0? In sec ion 6 he models KΓ 0(A, a) ha e been used o sepa a e he agmen s I∆n+1(IΣm), m≥n. Theo em 1.1 sums up esul s ob ained using hese models. Le us conside he ollowing p oblem. P oblem 5.Is s ic he ollowing chain o heo ies? B∗∆n+1(N) =⇒B∗∆n+1(PA) =⇒...=⇒B∗∆n+1(IΣn+1) =⇒B∗∆n+1(IΣn) Re e ences [1] P. D’Aquino. A sha pened e sion o McAloon’s heo em on ini ial segmen s o models o I∆0. Annals o Pu e and Applied Logic 61(1–2):49–62, 1993. [2] L.D. Beklemishe . Induc ion ules, e lec ion p inciples and p o ably ecu si e unc ions. Annals o Pu e and Applied Logic 85(3):193–242, 1997. [3] L.D. Beklemishe . A p oo - heo e ic analysis o collec ion. A chi e o Ma hema ical Logic 37(5– 6):275–296, 1998. [4] L.D. Beklemishe . On he induc ion schema o decidable p edica es. The Jou nal o Symbolic Logic 68(1):17–34, 2003. [5] T. Bigo ajska. On Σ1–de inable Func ions P o ably To al in IΠ− 1. Ma hema ical Logic Qua e ly, 41:135–137, 1995. [6] P. Clo e, J. K aj´ıcek. Open P oblems. In P. Clo e, and J. K aj´ıcek, edi o s, A i hme ic, P oo Theo y and Compu a ional Complexi y, pages 1–19. Ox o d Logic Guides 23. Ox o d Uni e si y P ess, Ox o d, 1993. [7] A. Co d´on F anco, A. Fe n´andez Ma ga i , F.F. La a Ma ´ın. F agmen s o A i hme ic wi h Ex ensions o Bounded Complexi y. P ep in , Se illa, Augus 2003. [8] A. Co d´on F anco, A. Fe n´andez Ma ga i , F.F. La a Ma ´ın. On he quan i ie complexi y o ∆n+1(T)–induc ion. A chi e o Ma hema ical Logic, o appea . [9] A. Fe n´andez Ma ga i , F.F. La a Ma ´ın. Some esul s on L∆− n+1. Ma hema ical Logic Qua e ly, 47(4):503–512, 2001. [10] P. H´ajek, P. Pudl´ak. Me ama hema ics o Fi s O de A i hme ic. Sp inge Ve lag, Be lin, Heidelbe g, New-Yo k, 1993. [11] R. Kaye. Diophan ine and Pa ame e – ee Induc ion. Ph.D. Thesis. Uni e si y o Manches e , 1987. [12] R. Kaye. Models o Peano A i hme ic. Ox o d Logic Guides 15. Ox o d Uni e si y P ess, Ox o d 1991. [13] R. Kaye. Model– heo e ic p ope ies cha ac e izing Peano A i hme ic. The Jou nal o Symbolic Logic, 56(3):949–963, 1991. [14] R. Kaye; J. Pa is; C. Dimi acopoulos. On pa ame e ee induc ion schemas. The Jou nal o Symbolic Logic, 53(4):1082-1097, 1988. [15] F.F. La a Ma ´ın. Inducci´on y Recu si´on: Las eo ´ıas I∆n+1(T). Ph.D. Thesis. Uni e sidad de Se illa, 2000. [16] D. Lei an . The op imali y o induc ion as an axioma iza ion o a i hme ic. The Jou nal o Symbolic Logic, 48(1):182–184, 1983. [17] J.B. Pa is, L.A.S. Ki by. Σn–collec ion schemas in a i hme ic. In A.J. Macin y e e al. edi o s, Logic Colloquium’77, pages 199–209. No h–Holland, Ams e dam, 1978. [18] C. Pa sons. On n–quan i ie induc ion. The Jou nal o Symbolic Logic, 37(3):466–482, 1972. [19] T. Slaman. Σn–Bounding and ∆n–Induc ion. P oceedings o he Ame ican Ma hema ical Socie y, o appea . 34