6
$\begingroup$

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.

Improve this question
$\endgroup$
6
  • 4
    $\begingroup$ 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. $\endgroup$
    – Thomas Klimpel
    Commented Jul 1, 2015 at 18:04
  • $\begingroup$ @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. $\endgroup$
    – nikita
    Commented Jul 1, 2015 at 18:41
  • 3
    $\begingroup$ The first-order theory of ordinals is studied in depth in the Doner, Mostowski, Tarski paper referenced in mathoverflow.net/a/35982 . $\endgroup$
    – Emil Jeřábek
    Commented Jul 1, 2015 at 18:56
  • 2
    $\begingroup$ 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 $\endgroup$
    – user21349
    Commented Jul 1, 2015 at 19:08
  • 6
    $\begingroup$ @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. $\endgroup$
    – Asaf Karagila ♦
    Commented Jul 1, 2015 at 20:14

2 Answers 2

Reset to default
5
$\begingroup$

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).

Improve this answer
$\endgroup$
0
3
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ Only gives constructive ordinals or countable ordinals? $\endgroup$
    – David Roberts ♦
    Commented Jul 1, 2015 at 23:46
  • 1
    $\begingroup$ I meant to say countable, thanks. It also gives constructible ordinals, depending on your ambient theory... $\endgroup$
    – cody
    Commented Jul 2, 2015 at 13:44

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .