A little preamble:
I recently came across the system of higher-order logic known as simple type theory, and I was immediately intrigued by it, as it seemed to be exactly what I was looking for as an alternative to set theory. Essentially, it seems much more natural to me both to allow urelements rather than insisting that everything be pure sets, and to restrict elements of sets to all be of the same type. Type theory does both of these. Furthermore I find the categoricity and expressiveness of higher-order logic to be more attractive than whatever it is that makes mathematicians prefer first-order logic. (In the comments Noah pointed out that first-order logic's proof system is one of the things that gives it its prominence in modern mathematics.)
For those unfamiliar with Simple Type Theory, there is an introduction to it here: http://www.sciencedirect.com/science/article/pii/S157086830700081X
The question:
There seems to be one thing that set theory makes a lot easier than simple type theory, however: the definition of ordinal numbers. In type theory hereditarily transitive sets are impossible, since they contain elements of different types ("sets", "sets of sets", "sets of sets of sets", etc.). So how does one define the ordinal numbers in type theory?
It seems to me that you would use something like the Peano axioms, but with a Supremum function on sets of ordinals in addition to the Successor function on ordinals. (And a transfinite induction axiom in place of the usual induction.) The problem becomes how to define this supremum function. I am not sure how to do it in the first place, and I can also see that there is the possibility of running into the largest ordinal paradox, since in type theory there is nothing stopping you from defining a set that contains every member of a given type. (Sets in type theory are identified with their indicator functions, so a set is the same thing as a predicate. The set of all ordinals would just be a function from ordinals to truth values that always returns "true".)
There is a similar question here: Is there an axiomatic approach to ordinal arithmetic? But the answer given there doesn't seem to work (I can't see how it would even get up to $\omega^2$, for instance).
I would very much appreciate it if anyone out there can offer some insight on this! Thanks!