# Ordinal Numbers within Simple Type Theory

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!

• As a side note, let me point out that one reason mathematicians like first-order logic is that it has a complete recursive proof system. In higher-order logic, the set of validities is extremely complicated, and proofs may be infinitely long (in the sense that $\varphi$ may be a consequence of $\Gamma$, but not a consequence of any finite subset of $\Gamma$). In fact, in a certain sense first-order logic is the strongest logic which has a nice proof system; this is Lindstrom's theorem. The point is, categoricity comes at a cost. – Noah Schweber Sep 25 '15 at 7:04
• Higher-order type theory, despite the name, is not a higher-order logic. – Zhen Lin Sep 25 '15 at 7:19
• Noah - thanks for the comment. I had the sense that that was the case, but I wasn't completely sure about it. Zhen - the introduction to STT that I linked above disagrees with you, but that may be a technical point that I am not grasping. – Matt Dickau Sep 25 '15 at 16:45
• Ordinal numbers are not the only place where it's awkward that all elements of a set have to be of the same type. In elementary geometry, people often think of a line as a set of points, and then talk about configurations that have some lines and some points as elements. So these configurations are not sets in the sense of simple type theory. It's not difficult to circumvent this problem in simple type theory, but it doesn't just work automatically the way it does if you have (as in ZF set theory) cumulative types. – Andreas Blass Sep 27 '15 at 19:35
• This paper presents a scheme for ordinals up to the first uncountable ordinal cse.chalmers.se/~coquand/ordinal.ps – Q the Platypus Nov 30 '16 at 7:04