ladkin@kestrel.ARPA (02/03/86)
(adams) >The question I don't know the answer to is the following: is there any >closed number-theoretic formula X, such that neither X nor not X is provable >in the system N(a) for any computable ordinal a? What is N(a)? It can't be Peano Arithmetic relativised to a, since the induction axiom is false if a isn't omega. There are non-standard models of PA but they're not well-founded, and a is supposed to be an ordinal. It is also no longer true that every number except 0 has a predecessor, when there are limit ordinals in the domain. If the ordinal's computable, then there's a notation for it embedded in PA ( a recursive function coding the well-order), which would mean that, whatever N(a) might be, it seems to have the same proof theory as N ? I'm running out of guesses. Peter Ladkin
weemba@brahms.BERKELEY.EDU (Matthew P. Wiener) (02/07/86)
In article <4516@kestrel.ARPA> ladkin@kestrel.ARPA writes: >>The question I don't know the answer to is the following: is there any >>closed number-theoretic formula X, such that neither X nor not X is provable >>in the system N(a) for any computable ordinal a? > >What is N(a)? It can't be Peano Arithmetic relativised to a, >since the induction axiom is false if a isn't omega. There >are non-standard models of PA but they're not well-founded, >and a is supposed to be an ordinal. It is also no longer >true that every number except 0 has a predecessor, when there >are limit ordinals in the domain. >If the ordinal's computable, then there's a notation for it >embedded in PA ( a recursive function coding the well-order), >which would mean that, whatever N(a) might be, it seems to >have the same proof theory as N ? >I'm running out of guesses. My guess is that N(a) is Peano Arithmetic + induction on well-orderings of type less than a. The proof strength does grow (like a step function) as you increase a among the recursive ordinals. For example, if e=epsilon_0, ie, the limit of w,w^w,w^w^w,w^w^w^w,... (where w=omega), then N(e) is, by Gentzen's theorem, able to prove the consistency of PA. ucbvax!brahms!weemba Matthew P Wiener/UCB Math Dept/Berkeley CA 94720
franka@mmintl.UUCP (Frank Adams) (02/08/86)
In article <4516@kestrel.ARPA> ladkin@kestrel.ARPA writes: >(adams) >>The question I don't know the answer to is the following: is there any >>closed number-theoretic formula X, such that neither X nor not X is provable >>in the system N(a) for any computable ordinal a? > >What is N(a)? This was in the original posting, but got cut out when it was quoted. N(0) is the formal system axiomitized by the Peano postulates. For each formal system N(a), P(a) is the Goedel sentence for the system. For any computable ordinal a, N(a) is the system whose axioms consist of the Peano postulates, plus the statements P(b) for every ordinal b<a. (In particular, N(a') has all the axioms of N(a), plus P(a).) The requirement that a be a computable ordinal is required in order for N(a) to be a formal system; if u is the smallest uncomputable ordinal, it is not decidable whether a statement P is an axiom of N(u). At that point the Goedelization fails, so there is no statement P(u). (I am going on vacation, and will not return until March. If you want me to see a response, mail it to me.) Frank Adams ihnp4!philabs!pwa-b!mmintl!franka Multimate International 52 Oakland Ave North E. Hartford, CT 06108
ladkin@kestrel.ARPA (02/08/86)
In article <11727@ucbvax.BERKELEY.EDU>, weemba@brahms.BERKELEY.EDU (Matthew P. Wiener) writes: > > My guess is that N(a) is Peano Arithmetic + induction on well-orderings of > type less than a. The proof strength does grow (like a step function) as > you increase a among the recursive ordinals. For example, if e=epsilon_0, > ie, the limit of w,w^w,w^w^w,w^w^w^w,... (where w=omega), then N(e) is, by > Gentzen's theorem, able to prove the consistency of PA. > That sounds reasonable, but notice Adams wanted N(a) for ANY ordinal a. Your interpretation doesn't address 0mega-1 Church Kleene and above, since these well-orders aren't in N, and have to be added somehow. Peter Ladkin