Solution (source code)

= Solution

The inductive definition of <ordinal addition> is the <transfinite recursion>
$$
\alpha+0=\alpha,
\qquad
\alpha+(\beta+1)=(\alpha+\beta)+1,
\qquad
\alpha+\lambda=\sup_{\gamma<\lambda}(\alpha+\gamma)
$$
for every nonzero <limit ordinal> $\lambda$. The synthetic definition takes disjoint <well-orders> $A$ and $B$ of order types $\alpha$ and $\beta$, puts every member of $A$ before every member of $B$, and defines $\alpha+\beta$ to be the order type of this ordered sum.

These definitions agree by <transfinite induction> on $\beta$. The empty second order contributes nothing; adjoining a greatest element gives the successor clause; and a limit well-order is the union of all of its proper initial segments, so its ordered sum with $A$ has order type $\sup_{\gamma<\lambda}(\alpha+\gamma)$.