I am trying to work through some basic order theory so as to consolidate my shaky grasp of ordinal arithmetic.
My source work "Discovering Modern Set Theory I: The Basics" by Winfried Just and Martin Weese (1996) sets as an exercise to prove that:
$$(\alpha + \beta) + \gamma = \alpha + (\beta + \gamma)$$
where the summands are order types.
That is, translating back into pure set-theoretical terms, to prove that:
$$((S_1, \preccurlyeq_1) \oplus (S_2, \preccurlyeq_2)) \oplus (S_3, \preccurlyeq_3) \cong (S_1, \preccurlyeq_1) \oplus ((S_2, \preccurlyeq_2) \oplus (S_3, \preccurlyeq_3))$$
where:
- each of the $(S_n, \preccurlyeq_n)$ is a general ordered set, may be partly, totally, well-ordered, it's immaterial
- $\cong$ denotes order isomorphism
- $\oplus$ denotes order sum:
$$(A, \preceq_A) \oplus (B, \preceq_B) := (A \sqcup B, \preceq)$$ where $A \sqcup B$ denotes the disjoint union and $\preceq$ denotes the ordering defined as:
$$\forall a, b \in A \sqcup B: a \preceq b \iff \begin{cases} a \in A \text { and } b \in B \\ a, b \in A \text { and } a \preceq_A b \\ a, b \in B \text { and } a \preceq_B b \end{cases}$$
(Just and Weese make it more rigorous, but more visually opaque, by not actually formally defining the disjoint union but instead immediately going to $C = A \times \{0\} \cup A \times \{1\}$ which is of course a standard definition of disjoint union without stating what it is or why this is done, for which they probably have reasons.)
Intuitively it is clear that this means that the structure of the order sum is such that "all the elements of the first set precede all the elements of the second set".
Hence it is intuitively obvious that the composite order sum of three such ordered sets is merely "all the elements of the first set come before all the elements of the second and third sets, and all the elements of the second set come before all the elements of the third set", but proving it rigorously looks dauntingly arduous and cumbersome.
My plan is to make a start on this by setting up a mapping $\phi$ from $(((S_1 \sqcup S_2) \sqcup S_3), \preccurlyeq_a)$ to $((S_1 \sqcup (S_2 \sqcup S_3)), \preccurlyeq_b)$, where $\preccurlyeq_a$ and $\preccurlyeq_b$ are defined appropriately, and demonstrate that $\phi$ is order-preserving both ways, or is a surjective order embedding (whichever works out easier to do).
I have tried to google around a bit for anything online that I can crib, but all I get is something like "addition of order types is clearly associative" without actually throwing the poor student a bone to suggest an efficient means of going about it.
For example, showing that $(S_1 \sqcup S_2) \sqcup S_3$ is "the same" as $S_1 \sqcup (S_2 \sqcup S_3)$ is a good place to start, but that in itself becomes a tangle of Cartesian products:
$$((S_1 \times \{0\} \cup S_1 \times \{1\}) \times \{0\}) \times (S_3 \times \{1\}) \cong (S_1 \times \{0\}) \times ((S_2 \times \{0\} \cup S_3 \times \{1\}) \times \{1\})$$
at which point I'm in danger of losing track of my parentheses.
I presume there is no "royal road" for demonstrating these sorts of technical low-level but essential result. However, can anyone suggest a more-or-less efficient strategy for breaking it down into existing readily-available results so that I won't have to go all the way back to these first principles?
One of the steps that needs to be taken is to demonstrate that addition of order types is well-defined, which effectively means that order type addition on two ordered sets is independent of the specific elements of the order isomorphism classes that you pick to perform the order sum on, which again is something I have bypassed as "hard work" (to which I am averse).
Or is the answer to this "just get on with it, bite the bullet, write off your weekend"?
(Once I've done this, I need to do the same for the various types of order product, most importantly antilexicographical order, and then there's distributivity of the latter over order sum to demonstrate. The motivator of course is ultimately to show that ordinal arithmetic is well defined and obeys at least some of the rules of conventional arithmetic.)