10

Subsystems of PA
I cannot bringa world quite round, Although I patchit as I can. I s i n g a h e r o ' sh e a d , l a r g e e y e A n d b e a r d e db r o n z e , b u t n o t a m a n , Although I patchhim as I can A n d r e a c h t h r o u g h h i m a l m o s tt o m a n . If to serenadealmost to man I s t o m i s s ,b y t h a t , t h i n g sa s t h e y a r e , Saythat it is the serenade O f a m a n t h a t p l a y sa b l u e g u i t a r .

From : Tlter,", *,,Y'),)r':;i rr:.'i:i,2i

In this chapterwe return to considering the subsystems 12,, 82,, of PA d e fi n e d i n S e cti o n 7 .1 . (The r eadershouldconsult the diagr amin Exer c i s e 7 .3 a sa g u i d eto th e va r ious implications between these theor ies.) The t w o main resultsof this chaptershow that thesesubsystems form a hierarchy, and thereforePA is not finitelv axiomatized.

10.1 :,-DEFINABLEELEMENTS Le t MF P A - a n d ,u q l M. W e shallconsider the substr uctur es K"( M;A) of M, which are definedin a similarway to K(M; A) of.Chapter8, exceptthat only elements definedby ),, formulasare in I((M;A). D E p t l t r r o r vL . et MEPA-, let n>I and let Ac:M. K"(M;A\ su b stru ctu re o f M co n sistins of all b e M suchthat ME 0( b, d) AVx( 0( x,a) - - > x: b) forsome ee A . ( S u c h baresaidtobe),,-definablein 0 ( x , y ) e^ I , , a n d s o ma M o v e rA . \ of NI: for exampl e i f It i s cl e a r th a t K " (M ; A) is a substr ttctur e w , here b , c e K " ( M ; A ) a r e d e f i n e db y n 0 , a ) a n d [ ( 2 , 1 7 )r e s p e c t i v e l y 130 in the

2,,-clefi nable ele ments rl,Ee-I,, a n d n 2 I , t h e nb * c i s c l e f i n e b c ly t h e ^ I , , forrnula a y , z ( , ? ( ya , ) A g ( 2 ,a ) A x : y + z ) .

l3l

J u s tas i n C h a p te r8 w e d e noteK"( lvl;{ a} ) and K"( M;A) mor esim plyby K "( NI; rz)a n d K ^ (M) re sp e ctively. The n e xt th e o re m i s th e analosueof Theor em 8.1 for the str uctur es I ( "( M ; A ) . T l t e o t r e u 1 0 . 1 .L e t n > k > 1 A c- I("(lvl: A) <,rM. a n d s u p p o s eA = M F l Z k - , . Then

P r o of. A c. I(" (M;.4 ) si n ceeachae A is definedby the for m ulax:a. ( x , , . . . , x 1 )h a v eA 1 g R e c a l lt h a t , f o r e a c h/ > 2 t h e f u n c t i o n s , r a p ha n d are one-to-one correspondences betweenMI and M for all modelsMF ILt). T h u s , r f x , y e M a n d x : ( y r , . . . , l t l e I ( ( M ; A ) , t h e n e a c hl i i s i n K " ( M ; A ) , s i n c ei f x i s d e f i n e c bl y 6 ( r , r i ) w i t h e e 2 , , a n da e . 4 , t h e n y , i s definedby a x ,y r ,
,li-1, !i+t,

xa )A x : ( t t , , y , ( E (,

) J

lr.
I t

,f))

which is ),,. T h i s r e d u c e s t h e p r o b l e mo f s h o w i n gK " ( M ; A ) < z o M t o th a t s h o wi n g if b e K " (M; A) and E@, b) e [I*- 1 then

M F a x E @ ,6 ) ) a c e K " ( M ; A ) s . t .M F E @ ,6 ) by the Tarski-Vaughttest(Exercise 7.4) usingthe function(t) to replacea : f l p - , fo rmu l a E (i .6 ; w i tfrV y < x( x ( t) - - q( t , b) ) . Now suppose f u l F a x c p (6 x) , , r pe I 7 r - , , 6 e K " ( M ; A ) a n d6 : ( b , , . . . , b , ) M F I Z k - 1a n d w i t h e a c hb , d e f i n e d () aeA). Since b y t h e) , , - f o r m u l ^ r l i ( u i , a for E(x,6) b,y t h e l e a s tn u m b e rp r i n c i p l e IZ*-t Lnk-' (Exercise7.3) <r z - t E @ ,b ) ) . MFa,.rlq(r,6)AVr n. 2 ) s o N o w l c p ( u , 6 ) i s I * - , a n d , i f k > z , I Z k - i B Z k ' , ( P r o p o s i t i o7 V t t l z - 1 c p ( u , 6 )i s e q u i v a l e n it n l v l t o a 2 t - 1 f o r m u l ab y P r o p o s i t i o7 n. 1 . I f

r r : 1 t h e n Y u { z 1 E ( u , 6 ;i s A , , r pi s .T h u s i n b o t hc a s e s since
M F a t z 1 u , ,. . . , r i p ( \ 1 = a 14i(ui , ) A q ( 2 , D ) A V a < z - 1 E @ ,D ) l of - I,,,ilr - ,, a n d th e fo rmL rl a i n si cl e sq u ar e br ackets her e is a conjunction t h i sf o r m u l at h e n u r : b i f o r a l l i a n d I o - , f o r m u l a s ,s o i s t , . I f D ,z s a t i s f y

132

Subsystem.r of PA

a n d s o t h e u n i c l l r e z s a t i s f y i n g i r , , . , oj l f A l = 1 r y 1 ( u u;),A c p ( 2A , ) A Y u { z - l c p ( u ,u ) ] i s i t t K " ( M ; , 4 ) a n d M E c p ( 2 , 6 ; , a s r e q u i r e c l .E N o t i c et h a t , e v e n i f t l : A a n c f ll:1, I('(fu|:A) may be nonstandard. Th i s r,vi l h l a p p e nfo r e xar nple when M FPA+ axy@) , wher e X is A,, a nd N F V T IX (x). (S u ch ful exist by the incompleteness r heor em.) Th en K t ( A 4 ) : " N a n dc o n t a i nts h e l e a sx t eM such t h a tM F y ( x ) . B u t a sN { o , , M we cannot h a v ex : n e N , s i n c e otherwise N FX(n). N o w i f l (" (fu |;A ) i s n onstandar d, n77, ancl A is finite( A: { c1} say) ,then th e n K " (M;,4 ) w i l l fa i l to satisfy P,4. This is because for all cel( ( M ;A ) th e ree xi sts e e N su chthat M FS a rr,,( e c) )A Vy( Sat, y) ) - , y : c) . ,ld, , fct, ,,( e
Since this formula is the conjr-rnction of a I,, formula and a I1,, formula, T h e o r e m 1 0 . 1g i v e s u s

I(" (M ;A ) FS at' ,,( e, ld,c])AVy( Sat;,,( e, [a,y]) - + y : c) . Th u s fo r a n y n o n sta n dar d cle K"( M; A) I ( ' ( M ; A ) F V c a e< d [ S a t ' , e , (, l a , c ] ) A V y ( S a r,,, ( r , l d ,y l ) - y : . ) ] . Ho w e ve r i f K " (M; A )F PA ther ewouldbe a least suchd e K"( M ; A) , d1 1s,ay sa ti sfyi n th g e a b o vefo rmula.But this would im ply d,,eN, sinceit n- r usbe t le ssth a n o r e q u a l to any nonstandar d de I( ' ( M;,zl) , and so I( ' ( M;A ) wo r.rl o d n l y h a vefi n i te l ymany elements, which is im possible. Thus T n e o n e vr1 0 .2 . N o co nsistent extension of PA is finitelyaxiomatized . Proof. If Zr PA is finitely axiomatized, then for sornen e N all axiomsof T a re II,,. C o n si d e ra ny nonstandar d MFZ and take a> N in M . L et I(:K " (fu [;a )<2 ,,M. -l hen KFT sinceM ET and each axiom of ?" is I I,,, Ire n ce K F P A , w h i ch i s i mpossible sinceK is nonstandar d. t- J T h e o re m1 0 .2i s d u e ( essentially) ( 1952) .W e sh al l to Ryll- Nar dzewski no w d i scu ss, i n ra th e rmor e detail,whichinduction axiomshold and wh i c h f a i li n t h e m o d e l s I("(M;A\. P n o p o s t r r o1 N 0.3. I f N l F I Z k ,A c . M a n dn > k > 0 . T h e n I ( " ( f u | ; A ) E I Z k .

Proof . Let b e K"(M;A) andconsider a 11 formula 9(x,D. rc

-, , g(x K " ( t uA | ;) F0 Q , 6 ) A V . v ( Ob () x + 1 ,6 ) )
thetr, s i n c et h i s i s e q u i v a l e ntto a I { * 1 f o r m u l az r n cK l "(M;A)<r*,,M by

E,,definuble element,s Theorem l0.I, l vlF0 (0 ,1 i ) A vx( 0(x , 6) - .- 0( x + I , 6) ) ,

1 1 a I J-)

lretrce Mrvx7(x, b_) sincc lvlFI z:t,, zrnclyxT(x, b) is also Ir,,*, hence K"( f u|;A )E V x7 (x, 6 ), b y T h eor em10.I again,as r equir ed. tr T h e n e xt re su l t sh o l vs that in gener al pr opositon 10.3 cannot be i m p r o ve ciIt . h a sth e co n se cluence that 1r ,,- ft Bz,,forall nz r , a r esultclue t o P a rso n s (1 9 7 0 ). T h e p ro o f we giveher eis due to Par isancl l( ir by ( 1978) . T r r E o r r g1 v0 r . 4 .L e t M F P A , A c . M a f i n i t e s u b s e o tf M . a n d l e tn > I w i t h K "( M ;,4 ) n o n sta n d a rdT . h en I( ( A4; A) V B 2,,. Proof. Using the pairingfunction,everyb e I("(M; A) is clefinable in ful by a f o n nu l a o f th e fo rm ayy( *, y , a) , w h e r e), i s [r,,-t, A : {a } a n cly is a singlevar iable.( For if b is clefined by --aZd(x,2 , u) then b is alsoclefinecl : by Ay(VZ(y <Z> d(x, Z, c1)) which is of t l r e a p p ro p ri a te fo rm.) T h u s for all beK"( M;,4) ther e is ee N ( nar nely e : ' y ( u u , u , , D ) ,f o r a s u i t a b l e y) sLrct hh a t , Aux: bA Satn,, M l a u f3 u r, u ,(u : (L to u,) u,, af) ,( e, fu,,, -1Satn,, AV z I uYz 11, z, < z (z : (Z o,z) ---> _,(r, ft u,2,, al)Dl -lSatr7,,_, Since Satr,,,_, is I1,,-,, is -I,,_1, &Dd),,_, is closedunder bonclecl q u a n ti fi ca ti oin n P A , th efo rmulain squar e br ackets aboveis equivalent ( in PA) to a ),, formula A(a,b, e, u). Thus, if t e I((M; ,4) is nonstandard, for all b e K"(M; A) we have MF Je < tatt) ,( a, b, e, u) a n d h en ce(si n ceth i s fo rmu l ais I,,) by Theor em 10.1we have
I ( " ( f u ( ;A ) E l e 1 t A u A ( a , b , e , u ) . But b here was arbitrarry (as long as it was a member of I("(M;A)) cleducethat so we

K " ( M ; A ) F V b < t * I A e < t S u A ( ab , , e,u).

''')

Bu t t he fo rmu l a o n th e ri ght- hand side of ( "' ) is a ) ,, for mula with a b o r . r n cl eu cl n i ve rsa l q u a n ti fier pr ececling it, so if I?( M ; A) F BZ,, this fornrula woulcl LreeqLrivalent in both K"(&1;A ) ancl M to a .I,, fonnula

134

Snbsystems of PA
would have

tl- r en we But P ro p o sition 7.L by X Q,a ), , ) b y T h e o r e m1 0 . 1 ,h e n c e K " ( M ; A ) F y ( t ,a ) ) n t E X Q a , , e,u). l v lF Vb < I * 1 f e < t S u A ( ab

5.12) ,sinc e pr inciplcin M ( Exer cise th e pigeonhole T h i s w o u l d co n tra d i ct gu L @ , b , e , u ) ,b b e i n g d e t e r m i n eb d y ^ n y e s a t i s f y i na clearly b isuniquely u, where u:(uu,u,) and u is the least elementof M satisfying n S a t;7 ,(t,l ,, u u ,u r, a l ). Exercises for Sectionl0.I thatN < t,,Miff K"( M ): N. n >I. Show 10 .1 L e t MFP A a n d 1,0 .2L e t n >-L . of sets of II,,+:Sentences (a) Showthat both1.X,, and 82,, canbe axiomatizedby
Q

(Uj Snowthat neither/.X, nor 82,, areaxiomatized by a set of t,+2 sentences. (Hint: Take MFTh(N) nonstandard with a ) N in lvl and show K " ( l v l; a ) F2 u* 2 - T h ( N ) .) with by 1A1y together 10.3 Let 82" denotethe theoryaxiomatized aYtazVx < tay< z9(x,y, a) YaVxay?@,y, d) --->Y for all 0(r, y , a) in 2,,. (a) Show that BI, | 12,,-1. by a set of I,,n2sentences. (b) Showthat BE^ is axiomatized ( c ) L e t M F P A - . S h o wt h a t K " ( M ) F B > , , i t t K ^ ( M ) F B I ; . ( d ) D e d u c et h a t 1 I , , ' t V B > ; f o r a l l n > 1 ' . in Chapter 9 are I0,4 Assume that all the propertiesof Sats*(x,y)described and B),,*r are finitely provable in I.Xy (see Exercise9.10). Show that 1.X,, for all n>7. axiomatizable (Hint: Considerthe sentence b)) Va, b[Sat;,,(n, [0, b])AV.r(Sat2,,Qt,lx, --+Sat:,,(4, * 1, b]))-+VxSat2,,(a, [t, b])] [x or B)1 are linitely similarfor BI,,*,. It is unknown whether1A11 and something axiomatizable.)

I O . 2 ' , , - E L E M E N T A R YI N I T I A L S E G M E N T S We n o w tu rn o u r a tte ntionto the im plication12,,+ 8t,,. Our aim is to show that this does not reverse,that is we will constructa model of BE,, th a t d o e s n o t sa ti sfy I2,,.The idea is to constr uct a suita bl e of a model of PA. initial segment .X,,-,-elementary

2,,-eLemerttury initial segnrcnts

135

PnoposrrroN 1 0 . 5 .L e t n 7 l , N I F I Z , , _ ; ,z t r c l l e t I c , . M b e e l p r o p e r I , , - 1 - e l e me n ta ry i n i ti a lse g ment of M closecl uncler* anc'.. l Then IEBZ,,. P r o o f. N o te th a t .fF 1 A 0 ( See si n ccI - - o,,lll and 1A,, is fI,- axior natizccl. F1A,, Exercise 6 . 5( b ) ) . S L r p p o s rr e e l ancI l F Y x l a a S l Q ( ; , y )w i t h 0 e I I , , - , .T h e n for every x e M w i t h x { u , x i s a n e l e m e no t f , I( s i n c e I c " M ) a n cs l o t h e r ei s y e l s u chth a t 0 (x,l ) i s tru e i n /, anclhence0( x,y) is alsotr tr ein lz1( since 0 ( * , y ) i s I I , , - , a n d / ( r , _ , M ) . T h e r e f o r ef o r a l l b e l v l \ 1 , M F V - r < u 3 y < b 0 ( x , y ). T h i s fo rmu l ai s e q u i valent ( in IE,,- ,) to a [1,,- ,for m ula,sinceit is f o r r n edb y a p p l yi n g b o u n d e dquantifier s to a II,,- ,for m r - r la. Thus wc may u s et h e l e a st n u mb e rp ri n ci p le, LII,,- ,, to cleduce tliat ther eis a leiistlt in M s u c ht h z titV I F Y x < c t 3 t < b 0 ( x , l ) .C l c a r l y t h i sl e e r s stu c h b i s i n 1 ,s o f o r a n y x l a t h e r ei s , y < b s u c ht h a tM F 0 ( x , y ) . B u t t h i s y i s i r r/ s i n c eb e l c " M , a n c la s 1 1 r , , - t M ,I F 0 ( * , ! ) , h e n c el F V x < a a t < b ) ( x , y ) , a s r e q u i r e d . n W e n e e cla w a y o f co n structing segm ents of zr ) ,,- ,- eler nentar initial y m o d el M. DenNrrroNL . e t M F P A - w i t h A c . M a n c ln > 1 . I " ( M ; , 4 ) i s t h e i n i t i a l segment { x e M l M r x < b f o r s o m eb e K " ( M ; A ) } o f M . I" (*) a n d I" (M; c? )d enote I"( M ,A) anclI"( M;{ r ;} ) r cspectivcly. N o t i c e th a t l " (M;A ) i s a n 9 o- str uctur e, uncler- F ancl.. sinceit is closed For example i f x < b e K " ( M ; A ) a n dy { c K " ( I V I ; . zt h e nx + - y < b + c . l) . < b y c a n dh + c e K " ( M ; A ) . x" ' i W e w i l l p r o v et h a t i f M F I 2 , , - 1 ,t h e n I " ( M ; A ) ( r , ,, M . T h e s u r p r i s i n g t h i n g a b o u tth i si s th a t u reo n l y needMFIZ,,- 1for thisto wor k. Essentially, t h e r e a so n i s i n th e fo l l o w i n glemm a. L e u r u rn 1 0 .6 . L e t n 7 l . II,,-col lectionscheme 12,, pr oves the following instancesof the

c p ( x , l ,a ) V a Z l s c p ( x , 2 , a ) ) V a ,r i s V x < / ( V t - T f o r a l l cp ff,,-r. by consiclering Proof. The aboveinstances are provablein ll,,-collection

Vx < EzlYy-t E(*,t, a)VE(x,2, r1)1, prove it in 1),,. l1,,.We must theformula brackets being insicle square
[ I , , - , . L e t c \ ( w , x )b e t h e I n a m o d e lM E I Z , , , l e t a e M a n c c l p(x,y,d)e Ar(PA) formula

3 y ,u < w ( y< 2 ' A w : y + 2 ' + 2 ' * ' ' u ) ,

136

of PA Sultsy.stems

'th e of n, is l' . All the of the lr inar y expar r sion x) e xp re sse s xth cligit s o r)(r,r,, he ecltrivai n / I , , i n c l t r c l i ntg sf r)(w,x)are provable o b v i o L rp sr o p e r t i e o l , f o r m s( s o r ) ( w , x )i s i n f a c tA , ( 1 I ' ) ) a n c la l l t h e o t h e r lence o f i t s f l l a n cI nrr a y c h c c k . B y c o l t s i c l c l ' i n g w c w i l l n c e t lh e r c , a s t h c r e z r c l e propertics cclLra to l l)wc havc ha sa l l i t s b i n a r yc l i g i t s w : 2 ' - I ( r , v h i ch -+ d ( r'r,, < t (a z rp(x,2, t7) x) ) ] . wIE1 1a.'[V;i so usingL[l,,ir t M ther e is a her e is I1,,, b rackets i naS cl u a re T he 1 'rrrn tL rl sa y y.F o r this leastsucht' v,we hetve l e a stsu chw , t'v1 2, d) - ' r ) ( w,,, x) ) M F Yx < t( lZcp( x, t h e n w o : ! + 7 ' + 2 ' + t ' u f o r s o m ey < 2 ' ' s i n c ei f d ( w , , , x ) A l a i c p ( x , i , c l ) l ilso satisfy , o u l cz zrnc sfo r n e u{vt, andwi:y+2t+t. Lt1w,w

2, d) ---> 61*;, *11. Yx < r(aZcp(x,

o L r rc h o i c e o f w , , . contraclicting 2 , d ) ) , s o b y a p p l y i n g t h e 1 1 , ,'B t r t t h e r r M F V x < t l | ( - l r ) ( w , y ,x ) y c p ( x , to this. there is s e M suchthat c o l l e c t i o ns c h e r n e

x) y gr(x,2, A)) tVI FYx < tAZ<,t(-l r)(u,,,, M F Y x < r ( A Z 1 , s q ( x . 2 , d ) f V y l c p ( x , i , A ) ) ,a s r e c l t t i r e c l . a r i ds c r D

i l r c lA q M . T h e n I " ( M ; A ) < r , , , l v l . TneorrEu 1 0 . 7 .L e t n 7 I . M F I 2 , , - 1 , l n c l e r* , ' , I " ( M ; A ) < o , , M . P r o o f . S i n c eI " ( M ; A ) g " M a n c li s c l o s e cu to test, it is sufficient n >- 2. By the Tar ski- Vaught T h trsw e ma y a ssu me is ther e Eai7( t,1i) 1 ie I"( [V, A) , 0( i, 61en,,- . ancltVl s ho wth a t w h e n cve r f u n c t i o n( x , y l : z t h a t t V 1 t 0 G l,) 7 .S y u s i n gt h e p a i r i n g Cel"(lvl;A)sLrch if , ((il):xA(u):bn}(il,0)) tg h e l I , , - , f o r m u l t iV r 7 D a n c lb y c o n s i c l e r i n in 0( x,b) . vi' r r iables thztt e x, b ar esingle w e mzl yzl ssLlm n e ce ssa ry, 1c wher e c i s b b) and lvlFax?( x, fI,,., 0 (x, b ) e N o rv sL rp p o se i n N l b y th e for mr - r la ) ,,-d e fi n e cl r y@,d)( aeA) . By Lemr na 10.6tlier e i s
cleM strchthat

l v lF Y y< c ( a x < d ) ( x , y ) y V z - t ) ( t , y ) ) . in M to a I1,,- 2 Tl ri s fo rmu l a i s i l ,,-t, s ince ax< d?( x,- y) is eqr - r ivalent l orrn u l a ,a n clso th e rei s a leastsuchr / in M. whichsatisfies

-1 (:, ri) A Vy < c(ax < d0(x, y) V Vz 0(2, y )) M Ea r'1ry _1 ( r.r 0(x,Y)A3z0(z, Y\l AVl, < day < c:(Vx

2,,-e lertentary initial seg men t.s

131

T h i s ' l ast fo rmr" rl a i s a I,, clefir r ition of d in fu|, so de l ( " ( N l ;A ) . B u t MFax<d1(x,b), so there is xe I"(M;A) satisfying N I F 0 ( x ,b ) , a s r e qu i r e cl . T T h e fo l l o w i n grcsu l tzi b o u tthe sr .r bstr uctur I"( es A4;A) is alsouseful. T t t e o n p .rvt 1 0 .8 . L e t n > l , MF BZ,,ancl,4 q &1.Then I" (fuI ; A) En,,* | - Th(tvl,0) uu,t, t h e s e t o f a l l 1 1 ,,n fo , rmu l a sd ( r i)with par am eteraeA s tl' tat ar e tr ue in M. P r o o f . L e t 0 ( a ) b e V i A y t p ( i , r , r 7 ) w i t h t p f 1 , , _ , ,l e t b e l ( ' ( M ; A ) b e a r b i t r ary, a n cl cl e fi n e cl b y the 2,, for mula e@,A) . W e show that I "( M ; A)F V x < b a ytp (x, A) s,yl"( M ; A) . since IK"( M; t, a ), whichsr .r ffices S i n ceMF B Z ,, th e re i s ce 11 such that IVI and FVi< bat< ct1,t( i,y,17) , s i n c eVi <b l t<ctp i s e q u i valentinltl to a I1,,- ,for m ula,ther e is a least suchc. This c is clefined in M by a ),, formr"rla equivalentto a b [q (b ,a ) A V i < b A t < ct1,t(j, x, a) AVu <cai < bVt 1u*]tl.t( i,y, a) l T h u s c e l " ( M ; , 4 ) . B u t V i < b a t < a p ( i , y , r i ) i s e q u i v a l e ntto t h e s a m e I / , , - , f o r m u l ai n b o t h M a n d I " ( M ; , 4 ) , s i n c eI " ( M ; A ) F B Z , , b y T h e o r e r n 1 0 . 7a n c lP r o p o s i t i o 1 n 0 . 5 .h e n c e I " ( M ; A ) F Vi < b a y I c t p ( i ,y , d ) , a sI " ( M ; A ) 1 r , - , l v l , a s r e q u i r e d . n

A v ery u se fu lco ro l l a ryth at can be dr awn fr om Theor em 10.7 is the f o l l o w i n gre su l t,d u e (i n d e p endently) to Jeff Par isand Har vey Fr iedman. C o n o rl n n v 1 0 .9 (P a ri s, F ri edm an) .For all n70, s e r v a ti ve o ve r 1 2 ,,; th a t i s, fo r all II,,*2sentences o, 82,,*1 is ll,,*2- con-

1 2 , , 1 o iff

B2,,n r Fo .

P r o o J'. L e ft-to -ri g h its o b vi o Lr s, as BZu*tl12,. For the conver se, suppose t h a t o isY *a ytp (t,t) w i th Q e II,,andII,,#o. W e mustshow that 8Z,,nfto. L e t t re M F 1 2 , , + V y - l ! t ( d , y ) a n d l e t l v l ' > M b e s u c ht h a t , " + t ( M ' ; c i ) * M ' . T o d o th i s, l e t & 1 'sa ti sfy

e ME0(6),0 a n9 ^ - f o r m u l a } {0(6)lb U{ 3 l , r r 7 (c x) ,- 3 x 1 c y ( x ,a ) l n e I , , , , }

138

of PA StLbsystems

b for each be M anclzl in the languagegoexpanded by addingconstants further new constantc. The reduct of.M' to 9a clearly has the requirecl c is in M' but not i n the constant th e e l e me ntof A4' r ealizing pro ' 1 " *p le 7 rty, M ' ,a as7 .1 Then by Theorem 10.7, del"*t(M';d)1r,,M', so by BZ,,*1. B ut P ro p o si ti o n 1 0 .5 a n d our choice of Ivl', ,"*t( lvl' ; cl) F , ) for all b e I"*'(M' ; n), so M' Fvt-1!)(cy l ,) , s o M ' F - 1 q ( a6 -l4t is 8,,' Thus I'*'(M'; a)FVy1V@,y) as I"n'(M'; a) 12,,M' ancl n B\,,n1Vo. hence , lo ancl s X , , n* , " + r ( M ' ;a ) s a t i s f i eB one together'than are'closer thatI2,,and 82,,+, 1 0 . 9s h o w s Corollary r esultbetween82,,*,a nd conser vation mi g h tth i n k. T h e rei s n o non- tr ivial but 82,,* tV fo r e xa mp l eit can be shownthat - f) ,,*lFcon( 1) ,,) I Z ,,*rsi n ce '1),, is con(1),,), where con(.{I,,) is a natural [I1 sentenceexpressing consistent'. theoremthat BZ,,#1I,,.This this chapterwith the promised We conclucle theoremwas first proved by Paris ancll(irby (1978)and, indeperrdently, (1978).The proof here is Lessan's' Lessan T H e o n E v r1 0 . 1 0 .L e t M F P A , A c M f i n i t e , n 7 I , a n d s u p p o s et h a t Then I"( M ; A) F BZ,,but I"( M ; A) fl 8,,. I" (M;A ) i s n o n -sta n d ar d. Proof. We havealreadyseenthat I"(M; A)F 82,,. Let A: {A}and suppose ( b and a is to finclw e M with r,v Our strategy b e I"(M;,rt) is nonstandard. I,, fo rmu l a0 (x, w ) su chthat, for all xe I"( M;A) , x e N I"(M; A)F 0(x,w) f o r t h e nI " ( M ; A ) t l - 0 , a sI " ( M ; A ) + N . The followingis obviouslytrue for allx e N: We find w by usingoverspill. ( ) > x A l w ] n : [ ( u u :0 ) ] M F A w< b { l e nw - 0) 1,l) Aly Sat,r ,,- ,( [r ],, a ]) ) n V i < l e n (w)( [r ],< max( l( v,, [y' : lwf,- ' A ( l 3z Satr 7,,- ,( i, al) A V I < l e n (w)( l > 0 - ' ( [ur ], lz, y V y ( S a t o , - , ( [ r ] ,, -, \ y , a ] ) - > 3 2 { y S z r t r ,,,(,i , f z ,, i ] ) ) ) ) V([r]r: i A a z S a t , r ,, ,( i . [ 2 ,a ) ) { z S a t p , , - , ( [ r ] , -[1 A V z ( S a t r , , , - , ( i , [o r] ,) - - > a y 2,, r i ] ) ) ) ) ] , [' ]' .- | such that (In w o rd s, w co d e s the sequence[,],,, [t]r : only eitherlwf,:l andthishappens i r ] , , : t ( u u = 0 ) r a n d f o r e a c h0 < l < x , V) such that the least wtrenI is the Godel number of a fI,,-, formula 0(v,1' MF 0 (tt,a) existsand is gr eaterthan the least1e &1s uc h tte l vl sa ti sfyi n g ar) )l w l , : l w l , - , ( w h e n i d o e s n o t h a v e t h e t h a t M F S a i r , , , - , 1 ; w ) , , l t t ,o a b ove) . p ro p e rtyd e scri b e d

2,,-elementury initiul .tegments

139

. e rei s n;( b in fulsuchthat the for mulaaboveinsic' le b y o ve rsp i l lth T l r u s,. a c u r l y bra cke ts is tliat r v now t ) b o vei s tr ue for som ex> N. The iclea o f II,,-1fo rmulas a se q L l e n ce in [4, the leasty cocles r ,vhich ar e all satisfied s a t i s f yi n g Iru ];b e i n ga t l e a sta s lar geas the leasty satisfying Ir ],- ,, and all stagei. I1 ,,-,fo rmu l a s a re consicler ed at som e ( stanclar d) s t a n c l a rd s agr aph,zr ncl W e cl a i m th a t, w i th w chosen as in the pr evior .rpar c e N h oldsiff c e I "( M; a ) a rb i tra ry, I " ( l v l ;A ) F A y S a t , , ,,,( [ r ] , . ,[ y , a ) ) . T o p r o veth i s, su p p o se fi rstth at ce N. Then M F a y S a t n , , , ( [ r ] ,l,y , a ) ) . I v v ]:, k ' i s t ( V , , : 0 ) l ) ,s o I r 1 , . : / ce N , a t t da st h e f o r m r , r l' a B u t I w ] , . <m a x ( c , A , uI," ( l v l ;A ) F l w l , : k . A l s o M Fay Satp,,.. ,(k, ly , cll) Theorem 1 0 . 8 I " ( M ; A ) F a y S a t p ,,,( k , f y , c 7 ] ) by so if 1 , , ( MA ; ) FS a t n , , _ , ( [ r ] , , al). Conversely, ly, hence

c ,y e I " ( M ; A ) F S a t r r,,(,[ t " ] , l,y , a ) ) , 2 t h e nM F S a t o , - , ( [ r ]l,y , , o l ) s i n c e' 1 1 4 r , , , _ , I " ( M ; AB ) .u t y e I " ( M ; A ) , s o y < d for some by a formulaf D1(d, 0, d) (0 e [1,, d e M thatis ^X,,-defined - r). : 0(r,S,V)) and let i : V) be the II,,-, formulaVr, J((r,5) v,,--+ Let r/(v,,, tr!(vu, if u e M satisfies r/(u,c) thenu>d>y. Thus,by inducV)r.Clearly
tion on j in M, we have

t,,,,(l*li,lu.a))-n u> y)) )+ V r ( S ar M F Vj > i ( j < l e n ( w ce N. t h a tc { i , a n dh e n c e w h i c hs h o w s Exercises for Section10.2

o such that E x e r c i s e1 0 . 3s h o w t h a t t l i e r e i s L r2 , , r 2 s e t r t e n c e 10.5 By considering alteredto b e c a n n o t 1 0 . 9 , n c lh e n c e l h e ' I I , , a 2 ' i n C o r o l l a r y I 2 , , V o b u t B X , , * 1 1 - oa ' 2 , , + 2 ' o f' [ , , * . r ' . 1 0 . 6 P r o v e t h a t t h e w e a k f o r m o f t h e I I , , c o l l e c t i o n s c h e m ei n L e n r t n a 1 0 . 6 , to /-X,,. together with 1A,,,is actually eqr"rivalent ( l - l i n t : I f l b 1 i c p ( b , x ) h o l d s , r , v i t he e i l , , - 1 , i n s o m e m o d e l , u s e t h e c o l l e c t i o n schemeto fincl c such that

tr

V r r< b ( 3 x { c E ( u , . r ) ! V x - l c p ( ui,) )

140

Subsystems of PA

ys s u m i ntg a n d ( i n d u c t i v e la Z , , - , )c o n s i d etrh e l e a s t - n u m b e r h a t t h e m o d e ls a t i s f i eIs principle applied t o 3 ; < c c p ( ui,) . ) , o r m u l a0 ( x ) w i t h 1 0 . 7 L e t M F T h ( N ) w i t h a > N i n M . S h o wt h a t t h e r ei s n o . X , f o n l y o n e f r e e - v a r i a b ls e u c ht h a t x eN iff l " ( t u | ;a ) F 0 ( x )

w in the proof of f o r a l l x e l " ( M ; a ) . F l e n c ec l e c l u cte he useof the parameter T h e o r e m1 0 . i 0 c a n n o tb e a v o i d e d . 1 0 . 8 * P r o v e I Z , n * t c o n ( 1 I , , )f o r a l l n 7 0 , a s f o l l o w s :i n t h e n a t u r a ld e d u c t i o n I,,E (whereg is an 9o-formula) the induction axioms system of Exercise 9.6 replace by the inductionrule + 1.) l , - 1 c p ( u )c , p(u
f , -T9(0),9(s)

(u any variable not occurring free in f, s any ?a-term, E any X,, formula of 9). (a) Show that each induction axiom I.,E of /X,, is provable in this system. Hence is a provability deduce that the correspondingprovability predicate provableTa,(x) predicatef.or 12,, in Exercise 3.8. defined as (b) The cut eliminaton theorem for this system says that if p is a proof of the sequentf then there is a second proof, r7,of I such that in any instanceof the cut rule A,, cp A,,1cp

A in q, the formulzr E is eitheran axiomof P,{ or a formulain one of the equality in the inductionaxiom above.State and axiomsor a 2,, formula g(s) occurring provethis theoremin 1.I1. 1977.) {Hint: Modify the proof in Schwichtenberg ( i n 1 X , ) t h a t i f t h e r ei s a p r o o fo f 0 : 1 f r o m t h i ss y s t e mt,h e n t h e r ei s a Deduce proof of 0: 1 such that all the formulas occurring in it are 2,, or f1,,. (c) Let q be a proof of 0: I, all formulasin q being I,, or 7,,. Using II,,*r induction showthat Vx Sat4, ,,(V/ f , .r) equivalent to f in q, where \(/ f is some il,+ r formula for all Seqlrents --1provable,r,,(0 = l) is the disjunction of all formulas in f . Deduce that provable in /I,,n1.