Editing Well-quasi-ordering (section)

==Constructing new wpo's from given ones==

Let <math>X_1</math> and <math>X_2</math> be two disjoint wpo sets. Let <math>Y=X_1\cup X_2</math>, and define a partial order on <math>Y</math> by letting <math>y_1\le_Y y_2</math> if and only if <math>y_1,y_2\in X_i</math> for the same <math>i\in\{1,2\}</math> and <math>y_1 \le_{X_i} y_2</math>. Then <math>Y</math> is wpo, and <math>o(Y) = o(X_1) \oplus o(X_2)</math>, where <math>\oplus</math>  denotes [[Ordinal arithmetic|natural sum]] of ordinals.<ref name="dejongh_parikh" />

Given wpo sets <math>X_1</math> and <math>X_2</math>, define a partial order on the Cartesian product <math>Y=X_1\times X_2</math>, by letting <math>(a_1,a_2)\le_Y (b_1,b_2)</math> if and only if <math>a_1\le_{X_1} b_1</math> and <math>a_2\le_{X_2} b_2</math>. Then <math>Y</math> is wpo (this is a generalization of [[Dickson's lemma]]), and <math>o(Y) = o(X_1)\otimes o(X_2)</math>, where <math>\otimes</math> denotes [[Ordinal arithmetic|natural product]] of ordinals.<ref name="dejongh_parikh" />

Given a wpo set <math>X</math>, let <math>X^*</math> be the set of finite sequences of elements of <math>X</math>, partially ordered by the subsequence relation. Meaning, let <math>(x_1,\ldots,x_n)\le_{X^*} (y_1,\ldots,y_m)</math> if and only if there exist indices <math>1\le i_1<\cdots<i_n\le m</math> such that <math>x_j \le_X y_{i_j}</math> for each <math>1\le j\le n</math>. By [[Higman's lemma]], <math>X^*</math> is wpo. The ordinal type of <math>X^*</math> is<ref name="dejongh_parikh" /><ref name="schmidt">{{cite thesis |last=Schmidt |first=Diana |type=Habilitationsschrift |date=1979 |title=Well-partial orderings and their maximal order types |publisher=Heidelberg}} Republished in: {{cite book |last=Schmidt |first=Diana |date=2020 |chapter=Well-partial orderings and their maximal order types |title=Well-Quasi Orders in Computation, Logic, Language and Reasoning |publisher=Springer |pages=351–391 |editor-last1=Schuster |editor-first1=Peter M. |editor-last2=Seisenberger |editor-first2=Monika |editor-last3=Weiermann |editor-first3=Andreas |series=Trends in Logic |volume=53 |doi=10.1007/978-3-030-30229-0_13|isbn=978-3-030-30228-3 }}</ref> <math display="block">o(X^*)=\begin{cases}\omega^{\omega^{o(X)-1}},&o(X) \text{ finite};\\ \omega^{\omega^{o(X)+1}},&o(X)=\varepsilon_\alpha+n \text{ for some }\alpha\text{ and some finite }n;\\ \omega^{\omega^{o(X)}},&\text{otherwise}.\end{cases}</math>

Given a wpo set <math>X</math>, let <math>T(X)</math> be the set of all finite rooted trees whose vertices are labeled by elements of <math>X</math>. Partially order <math>T(X)</math> by the [[Kruskal's tree theorem|tree embedding relation]]. By [[Kruskal's tree theorem]], <math>T(X)</math> is wpo. This result is nontrivial even for the case <math>|X|=1</math> (which corresponds to unlabeled trees), in which case <math>o(T(X))</math> equals the [[small Veblen ordinal]]. In general, for <math>o(X)</math> countable, we have the upper bound <math>o(T(X))\le\vartheta(\Omega^\omega o(X))</math> in terms of the <math>\vartheta</math> [[ordinal collapsing function]]. (The small Veblen ordinal equals <math>\vartheta(\Omega^\omega)</math> in this ordinal notation.)<ref>{{cite journal |last1=Rathjen |first1=Michael |last2=Weiermann |first2=Andreas |title=Proof-theoretic investigations on Kruskal's theorem |journal=Annals of Pure and Applied Logic |date=1993 |volume=60 |pages=49–88 |doi=10.1016/0168-0072(93)90192-G|doi-access=free }}</ref>