On 1/16/2014 7:23 PM, Ross A. Finlayson wrote: > On 1/16/2014 2:31 PM, Paul wrote: >> I saw it asserted without proof that all ordinals, alpha, less than >> epsilon_0, can be uniquely expressed as omega ^ beta * (gamma + 1), >> for some gamma and some beta such that omega ^ beta < alpha, where >> omega is the smallest infinite ordinal. This isn't clear to me. >> Could anyone help or give a reference? >> >> Thank You, >> >> Paul Epstein >> > > > Uh, gamma is not always "definable". Then it is to e_0 > (else it would be). > > This lets the tiniest little infinity that is undefinable, > be uncountable. > > Still, a "canonical form up to e_0" eg, the limits of > induction, that would be very interesting as canonical > forms up to large ordinals are very highly organized and > structured. Even the typical products of all the vector > spaces around us are usually in products of omega: > exactly as they are of integer spaces. > >
He should look in "Proof Theory" by Takeuti, Chapter 2 Section 11.
1) 0 is an ordinal
2) Let mu and mu_1, mu_2, ..., mu_n be ordinals. Then mu_1 + mu_2 + ... + mu_n is an ordinal and omega^mu is an ordinal
3) Only objects obtained using Rule 1 and Rule 2 are ordinals.
Of course, when mu = 0, then omega^mu = 1. So, that is the source of units.
Takeuti uses this definition of ordinal and an infinitary sequent calculus to present a version of Henkin's proof of the consistency of Peano arithmetic by transfinite induction.
This is not transfinite induction in the usual sense. The inductive definition of a polynomial given above plays its role as a syntactic representation. As a syntactic representation it can be syntactically decomposed. This is the sense of the proof-theoretic reduction by which the consistency proof proceeds.
The form asked for by the original poster is essential for the proof since any finite iteration of trailing units permits a finitary transformation in any given proof tree for an arithmetical statement. All of the possible polynomials are grouped into classes of syntactic forms and those forms are related to one another by syntactic decompositions to reestablish a form with the trailing units.
There may be some simpler discussion of this form, but, I know it can be found in Takeuti.