Solution (source code)

= Solution

The recursive definitions of <ordinal addition> and <ordinal multiplication> are
$$
\alpha+0=\alpha,\quad\alpha+(\beta+1)=(\alpha+\beta)+1,\quad
\alpha+\lambda=\sup_{\beta<\lambda}(\alpha+\beta),
$$
$$
\alpha\cdot0=0,\quad\alpha\cdot(\beta+1)=\alpha\cdot\beta+\alpha,\quad
\alpha\cdot\lambda=\sup_{\beta<\lambda}(\alpha\cdot\beta),
$$
where the limit clauses apply to nonzero limit <ordinals>. <Ordinal exponentiation> has $\alpha^0=1$, $\alpha^{\beta+1}=\alpha^\beta\cdot\alpha$, and for $\alpha>0$, $\alpha^\lambda=\sup_{\beta<\lambda}\alpha^\beta$. Complete the zero-base convention by $0^\beta=0$ for $\beta>0$, with $0^0=1$. Stating the zero-base exception avoids including the value $0^0$ in a naive supremum at a positive limit.

For finite $n$, induction gives $1+n=n+1$. Now prove commutativity for finite $m,n$ by induction on $m$. The case $m=0$ is immediate. Associativity, the finite identity just obtained, and the induction hypothesis give
$$
(m+1)+n=m+(1+n)=m+(n+1)=(m+n)+1=(n+m)+1=n+(m+1).
$$
Thus $\boxed{m+n=n+m\text{ for finite ordinals}}$.

It fails for general <ordinals>: $\boxed{1+\omega=\omega<\omega+1}$. The equality follows from the limit clause, since the finite sums $1+n$ are cofinal in $\omega$.