# Order Type of $[\omega_\alpha]^{<\omega}$ in Well-Ordering of Finite Sequences of Ordinals

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.
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.9487724304199219, "perplexity": 79.98774375859776}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2019-47/segments/1573496670156.86/warc/CC-MAIN-20191119144618-20191119172618-00390.warc.gz"}