Ordinal Addition

For Ordinal , we define by recursion on with fixed as follows:


for limit

This is NOT commutative in general, e.g. , but
Synthetic Definition of Ordinal Addition

Remark

Technically, we should fix an ordinal and define by recursion on in the Well-ordered set .
By uniqueness in recursion, this gives a well-defined for all .
In general, this justifies recursive definition on all ordinals like the one above.

Similarly, proof by induction on all ordinals works:

Lemma

Let be some property of an ordinal .
Then

Proof

Assume otherwise.
Then there is an ordinal such that .
Then there is also a least ordinal such that .
If , then and so holds. By assumption holds.

Proposition

Proof

By induction on ( fixed).
Consider three cases:
If if then so .
If if then WLOG , and so .
So by induction

Finally, if is a limit. WLOG .
Then there is some such that .
By induction

Lemma

Let be a nonempty set of ordinals.
Then for any ordinal ,

Proof

Cases on whether has a greatest element.

Proposition

Proof

By induction on with , fixed. We consider three cases:


a limit