Prev: Q.E.D.
Next: infinity in the large needs a boundary and infinity in the small needs a boundary #641 Correcting Math
From: Bill Taylor on 7 Jul 2010 01:33 Is anything much known of the ones above w_1^CK ? What "naturally occurring" ones are there, way up there? -- Baffled Bill And God said Let there be numbers And there *were* numbers. Odd and even created he them, He said to them be fruitful and multiply And he commanded them to keep the laws of induction
From: David Libert on 7 Jul 2010 20:13
Bill Taylor (w.taylor(a)math.canterbury.ac.nz) writes: > Is anything much known of the ones above w_1^CK ? > > What "naturally occurring" ones are there, way up there? > > -- Baffled Bill I don't know much about these, but I tell you the bits I have heard. One point along these lines was mentioned in passing in my old expository article on Kleene's O : [1] David Libert "Kleene's O" sci.math April 2, 2001 http://groups.google.com/group/sci.math/msg/fa9122b35b775ad7 The part of [1] touching on this point, in describing Kleene's O was: > The ordinal 0 will have a unique notation: the natural number 1. >Ie, O will turn out to be not univalent, but it will turn out finite >ordinals have unique notations. > > The ordinal successor operation will correspond to exponentiating by >2: if n denotes an ordinal 2^n will denote the successor >ordinal. > > Limit ordinals will have a marker on their notations to represent >that these are limit ordinals, and then will also have a number >representing the q_O value: ie the Turing machine enumerating the >cofinal sequence. > > The actual definition Rogers uses is limit ordinal notations will >all be of the form 3*5^n, where n will later be seen to denote that >Turing machine. > > All we really needed was one number to denote ordinal 0, and then a >category of notations for successor ordinals to code the precessor >ordinal, and a category of notations for limit ordinals to include the >parameter for the Turing machines. > > To do this using omega more fully, we could have let natural 0 >represent ordinal 0, let odds be successors where 2n + 1 is the >notation for the successor of the ordinal with notation n, and let >positive evens be limits, where 2(n+1) denotes the limit ordinal >with cofinal sequence given by the n'th Turing machine. > > But I will follow Rogers who follows Kleene. Rogers mentions that >Kleene uses 3*5^n because this was part of a broader notation system >Kleene was using, which included analogues of ordinals beyond >omega_1. But Rogers' book just talks about up to omega_1^CK, which >would be the recursive analogue of omega_1. > > Kleene used the 3 to code this level as opposed to later ones that >Rogers won't be discussing. But Rogers notes he is maintaining this >definition for compatibility. So apparently Kleene originally had O as part of a broader system of notations for countable ordinals reaching beyond w_1^CK . There has been later work done by others on this. Some can be found in [2] http://en.wikipedia.org/wiki/Large_countable_ordinals [3] http://en.wikipedia.org/wiki/Ordinal_analysis There is a subtheory of ZF, Kripke-Platek set theory, KP. A definative reference for this relating it also to recursion theory and model theory is Jon Barwise, Admissible Sets and Structures. You would probably find KP interesting Bill, because it seems to me similar to a lot of the ideas you have about cutting back set theory to a more definitional form. Anyway, admissibles ordinals are defined to be those ordinals alpha s.t. L_apha |= KP. w_1^CK is the least admissible ordinal. L_w_1^CK is isomorphic to a submodel of every well-founded model of KP. So in [2] above, there are sections Beyond Admissible Ordinals and "Unprovable" ordinals. Those take you to the big guns. [3] has sections leading up to the Bachmann-Howard ordinal, what I called the Howard ordinal in previous posts. So that and the earlier sections of [3] are below w_1^CK. But then [3] after that has Theories with larger proof theoretic ordinals, which get beoyond w_1^CK. Later proof theory has generalalized Gentzen's proof to higher ordinal notations and stronger theoreies. The Howard ordinal appears that was, as discussed in that section in [3]. That is still < w_1^CK though. But further later work as that closing section of [3], even generalized Gentzen to above w_1^CK. There is a further topic along the lines, beyond [3]. I had heard talk of high powered proof theory using reflecting ordinals. These are countable ordinals beyond w_1^CK. I couldn't find anything about them in Wikipedia. I have heard that these mimic properties of large cardinals (ie beyond ZF), in countable ordinals. These are also apparently used in proofs generalizing Gentzen. But already at the levels form [3], you are beyond recursive notations. I found a bunch of hits googling reflective ordinal. Here is another result I just realized recently, and it surprised me. The assumption that there is a well-founded model of ZF is somewhat strong. Well not realtive to large cardinals, but it does prove the consitency of iterations of Con(ZF) sat through small ordinal notations. If ZF is consistent, it is consistent with ZF that there are no well-founded models of ZF, and in particular no minimal well-founded ZF model. But work for a moment in the theory ZF + there are well-founded models of ZF. In this theory there is provably a minimal well founded model (ie as discussed in Cohen '66 as recently mentioned in one of your other threads). That model is also taken to be a standard model, and with that this is a definition of the model in that theory, ie there is a unique such. The ordinal of that model, ie the order type of the "ordinals" in the model, is similarly definable, and is a countable ordinal, beyond w_1^CK. In fact I just remembered you recently posted asking about that model Bill. Anyway there is another definable (in stronger theory) countable ordinal beyond w_1^CK. What I just realized recently, is in this theory to even get this ordinal exists, it is provable that this ordional is isomorphic to a specific Sigma^1_2 ordering on omega. So not recursive. Couldn't be. But not that high in the arithmetic hierarchy either. I think most of what has been done with these ordinals is proof theory. -- David Libert ah170(a)FreeNet.Carleton.CA |