# Ordinals separate from set theory

Is there an exposition and development of ordinals theory separate from set theory? That is, some first-order theory where terms are interpreted as ordinals, with constant $0$ (and maybe $\omega$), axioms for taking successor and limit (this might be easier to express in a second-order theory), an axiom schema for transfinite induction and with usual ordinal operations (sum, product, power) defined via transfinite recursion?

E.g., G. Boolos's system S has a separate variable sort for "stages" with appropriate axioms, but not enough to build a full theory of ordinals.

• en.wikipedia.org/wiki/Ordinal_notation and I really mean this! Using explicit ordinal notation is also more honest than using set theory, because the task to decide whether two different strings in the notation denote the same ordinal, or if not which ordinal is smaller, is then a very real and concrete computational problem. – Thomas Klimpel Jul 1 '15 at 18:04
• @ThomasKlimpel, I guess you mean a formal theory, where (at least some of) the terms correspond to the formulae of a particular ordinal notation. This would definitely be necessary, but in addition one still needs some axioms to prove theorems about ordinals. – nikita Jul 1 '15 at 18:41
• The first-order theory of ordinals is studied in depth in the Doner, Mostowski, Tarski paper referenced in mathoverflow.net/a/35982 . – Emil Jeřábek Jul 1 '15 at 18:56
• Conway's surreal numbers include the ordinals. They can be developed separately from set theory, and that's what Conway did in "On Numbers and Games." Some discussion here: personal.psu.edu/t20/fom/postings/9905/msg00074.html – Ben Crowell Jul 1 '15 at 19:08
• @Ben: People should really stop saying that like that. The usual ordinal arithmetic is non-commutative and non-cancelative. It does not embed into the surreal numbers. – Asaf Karagila Jul 1 '15 at 20:14

I think the following article by Takeuti does what you want:

Takeuti, Gaisi, A formalization of the theory of ordinal numbers. J. Symbolic Logic 30 1965 295–317.

The Mathematical Reviews / MathSciNet label for it is MR0197302 (33 #5467).

Building upon Thomas Klimpel's comment, usually ordinals are treated in type theory using the Brower Ordinals. In Coq notation:

Inductive Ord := Z : Ord | Suc : Ord -> Ord | Lim : (Nat -> Ord) -> Ord

Where Nat is the type of natural (non-negative) numbers.

This only gives c̶o̶n̶s̶t̶r̶u̶c̶t̶i̶v̶e countable ordinals, of course. One can then get ordinals of any cofinality by replacing Nat with the appropriate type. As can easily be seen here, the size of ordinals obtained in such a setting really depends on the size of the function space Nat -> Ord, which in turn depends on the expressiveness of the type theory you start with.

Martin Escardo has a nice development with additional references here.

• Only gives constructive ordinals or countable ordinals? – David Roberts Jul 1 '15 at 23:46
• I meant to say countable, thanks. It also gives constructible ordinals, depending on your ambient theory... – cody Jul 2 '15 at 13:44