I am working on Exercise 3.6 from Jech's Set Theory.
Ex. 3.6: There is a well ordering of the class of all finite sequences of ordinals such that for each $\alpha$, the set of all finite sequences in $\omega_{\alpha}$ is an initial segment and its order-type is $\omega_{\alpha}$.
With the help of this post, I have the well-ordering that gives $[\omega_{\alpha}]^{<\omega}$ as an initial sequence. Now I must show that the order type is $\omega_{\alpha}$.
The post linked above and also this one say to use transfinite induction, but I'm not so sure that it is even true (given this well-ordering.) For example, if $\alpha=0$, then in $[\omega]^{<\omega}$, the single-term sequence $\langle2\rangle$ has infinitely many predecessors, (all finite sequences of just $0$ and $1$). This means that the order type of $[\omega]^{<\omega}$ is strictly greater than $\omega$.
I haven't thought too much about $\alpha>0$, having been disheartened when the base case failed. If transfinite induction is the way to go, then $\alpha=1$ needs to be proven on its own, (as a new base case.) I don't have a whole lot of intuition for that, but my counterexample above doesn't seem to generalize, so it may be doable.
Any advice would be greatly appreciated. Specifically, I want to know how to resolve the issue of $\alpha=0$. (Is it possible that $\alpha=0$ is an edge case Jech forgot to mention?) Clearing that up will probably clear up the rest.
Thanks!
EDIT: I think I can actually do it for $\alpha>0$, using transfinite induction with $\alpha=1$ as a base case. Perhaps the order can be modified to make $\alpha=0$ work too?
EDIT 2: Okay, so I did it for $\alpha>0$ without induction by looking at how many sequences less than a sequence of order $\omega_\alpha$ one would have remaining. Since there are only countably many finite sequences of finite ordinals, one can simply redefine $<$ to work for $\alpha=0$ without disturbing the rest. I am not confident that this is the best solution - I am happy to hear what anyone else has to say.
Here's a simpler way to think about it. If you were to have a well-ordering with the desired properties, then it must have the following form. First, you pick a bijection $\omega^{<\omega}\to\omega$, and use this to order $\omega^{<\omega}$. Then you pick a bijection $\omega_1^{<\omega}\setminus \omega^{<\omega}\to\omega_1$, and use it to order $\omega_1^{<\omega}\setminus \omega^{<\omega}$ (putting all of these elements after the elements of $\omega^{<\omega}$ you've already ordered). Then you pick a bijection $\omega_2^{<\omega}\setminus \omega_1^{<\omega}\to\omega_2$, and use it to order $\omega_2^{<\omega}\setminus \omega_1^{<\omega}$, and so on. For every $\alpha$, the cardinality of $\omega_{\alpha+1}^{<\omega}\setminus \omega_\alpha^{<\omega}$ is indeed $\aleph_{\alpha+1}$, so all the bijections you need to construct such a well-ordering do exist. (Note that you don't need to worry about limit steps, since if $\alpha$ is limit then $\omega_\alpha^{<\omega}$ contains no new elements that were not already in $\omega_\beta^{<\omega}$ for some $\beta<\alpha$.)
Now there's a small technical point you have to be careful about here, which is that you are trying to give a definable well-ordering of all of $Ord^{<\omega}$ at once. This means you need that all the bijections $\omega_{\alpha+1}^{<\omega}\setminus \omega_\alpha^{<\omega}\to\omega_{\alpha+1}$ to be definable, and in fact definable in a uniform way for all $\alpha$ (that is, there is one definition with $\alpha$ as a parameter that works for all $\alpha$). But this is not hard (just rather messy): if you chase through the standard way you would prove that $|\omega_{\alpha+1}^{<\omega}\setminus \omega_\alpha^{<\omega}|=\aleph_{\alpha+1}$, at every step of the way the bijection you use can actually be defined uniformly in terms of $\alpha$. Basically, you are just repeatedly using the fact that $|\kappa^2|=\kappa$ for any infinite $\kappa$ and Schroder-Bernstein. Both of these facts give you definable bijections: there is a bijection $\kappa^2\to\kappa$ uniformly definable in $\kappa$ (using the standard well-ordering of $Ord^2$), and the bijection given by Schroder-Bernstein is uniformly definable in terms of the two injections you start with.