Ordinal multiplication $\alpha \cdot \beta$

Let $\alpha$ and $\beta$ be ordinals (Ordinal (von Neumann)). The product $\alpha \cdot \beta$, also written $\alpha\beta$, is defined by recursion on $\beta$, in the three cases of Successor and limit ordinals:

$\alpha \cdot 0 = 0, \qquad \alpha \cdot \beta^{+} = \alpha \cdot \beta + \alpha, \qquad \alpha \cdot \lambda = \bigcup\{\, \alpha \cdot \beta : \beta \in \lambda \,\} \quad (\lambda \text{ a limit ordinal}),$

with $+$ the ordinal addition of Ordinal addition $\alpha + \beta$. That exactly one operation satisfies these three clauses, and that all its values are ordinals, is Ordinal multiplication exists and is unique, and its values are ordinals, proved immediately above. The union in the limit clause is the least upper bound of the values already produced (claim (e) of Basic closure properties of ordinals).

The convention, stated where it is made. The successor clause appends a copy of $\alpha$ on the right, so $\alpha \cdot \beta$ is "$\beta$ copies of $\alpha$", laid end to end in the order given by $\beta$. Made precise, this is $\alpha \cdot \beta$ is the order type of $\alpha \times \beta$ ordered by last differences, that is $\beta$ copies of $\alpha$: $\alpha \cdot \beta$ is the order type of $\alpha \times \beta$ ordered by last differences, that is, by comparing the $\beta$-coordinate first and using the $\alpha$-coordinate only to break a tie.

Both conventions occur in the literature and they give genuinely different operations, since multiplication is not commutative. Under the one adopted here $\omega \cdot 2 = \omega + \omega$ while $2 \cdot \omega = \omega$; under the opposite convention those two values are exchanged. This library always uses the convention above, which is the one of Jech and of the Wikipedia article cited below.

• Why $\alpha \cdot 0 = 0$ and not $1$. The empty concatenation of copies of $\alpha$ is empty. The multiplicative unit appears one clause later: $\alpha \cdot 1 = \alpha \cdot 0^{+} = \alpha \cdot 0 + \alpha = 0 + \alpha$, and $0 + \alpha = \alpha$ is proved in Monotonicity of ordinal $+$ and $\cdot$: strictly increasing and continuous in the right argument, weakly increasing in the left, with left cancellation, and the identities $0 + \beta = \beta$ and $1 \cdot \beta = \beta$, so $\alpha \cdot 1 = \alpha$.

• The limit clause is a supremum, and it is where the product loses commutativity. $2 \cdot \omega = \sup\{2 \cdot n : n \in \omega\}$, and each $2 \cdot n$ is a finite ordinal, so the supremum is $\omega$; whereas $\omega \cdot 2 = \omega \cdot 1 + \omega = \omega + \omega$, which is strictly larger. Both computations are carried out in FALSE: ordinal multiplication is commutative.

• Notation. $\alpha\beta$ abbreviates $\alpha \cdot \beta$, and the product binds tighter than the sum, so $\alpha\beta + \gamma$ means $(\alpha \cdot \beta) + \gamma$. Ordinal expressions in this library are always written with that convention.

• Agreement with the natural numbers. Below $\omega$ the limit clause never fires, and the two remaining clauses are literally the Peano clauses for multiplication on $\mathbb{N}$. That the ordinal product of two natural numbers is their natural-number product is On $\omega$ the ordinal $+$ and $\cdot$ are the Peano operations: $\omega$ is closed under ordinal $+$, $\cdot$ and exponentiation, and for naturals $m, n$ the ordinal $m + n$ and $m \cdot n$ are the natural-number sum and product.