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