The exercise I mentioned in class is the following: Let denote ordinal exponentiation. For ordinals , define as the set consisting of those functions such that there are only finitely many such that

(We haven’t formally defined “finite” yet, but we can take this to mean that the order type of the set is a natural number, using our formalized notion of natural number.)

For functions in set iff for largest such that

Then is a well-ordered set, and its order type is precisely

Advertisements