I've always wondered, is there an axiomatic approach to the arithmetic of ordinal numbers?

If so, I imagine it would be on par with set theory in terms of its proof-theoretic strength.

  • $\begingroup$ I know ordinal arithmetic exists and it follow the Peano arithmetic axioms en.wikipedia.org/wiki/Ordinal_arithmetic. For example here en.wikipedia.org/wiki/Peano_axioms wikipedia says that the ordinal numbers (defined bye von Neumann in ZF) are a model of Peano arithmetic axioms. Here another link maybe can be intresting for you.en.wikipedia.org/wiki/… $\endgroup$ – MphLee Apr 4 '13 at 14:42
  • 2
    $\begingroup$ @MphLee, I don't get that... how can the ordinals satisfy the axioms of Peano arithmetic, when after all Peano arithmetic has an induction schema? $\endgroup$ – goblin Apr 5 '13 at 10:08
  • $\begingroup$ I'm not very expert for that i gave you links about the connection betwen ordinals and axioms of peano arithmetic.But I do not have enough knowledge to give you an answer. $\endgroup$ – MphLee Apr 5 '13 at 10:25
  • $\begingroup$ @MphLee: Your comment is not correct. $\endgroup$ – Martin Brandenburg Apr 16 '13 at 9:59
  • 5
    $\begingroup$ @user18921: Could you explain your question? What do you mean precisely by an axiomatic approach to ordinal arithmetic? Do you already know that ordinal sum and product are decategorifications of sum and product of well-orders? $\endgroup$ – Martin Brandenburg Apr 16 '13 at 10:29

I haven't seen explicit axioms used before, but I belive the following should be trivially sufficient to start with:

Let s(x) be the successor function. s, <, +, * are taken as primitive, alongside = and the axioms of equality
Define Lim(x) as ~(∃z)(S(z)=x) [for simplicity, 0 is taken as a limit ordinal]
Define NextLim(x,y) as Lim(y)&(∀z)( z > x & Lim(z) => (z > y)v(z=y))
Define nextlim(x) as the y such that NextLim(x,y)
Define Anc(x,y) as nextlim(x) > y & Lim(x)
Define anc(x) for the y such that Anc(x,y), or 0 if there is no such y
Define ω as nextlim(0)
1a. (∃y)( y < nextlim(x) & y = s(x) )
1b. (∃y)(y = nextlim(x))
2a. Lim(0)
2b. ~∃x(0 = nextlim(x))
3a. s(x)=s(y) => x=y
3b. anc(x)=anc(y)
3c. anc(x)=anc(s(x))
3d. nextlim(x)=nextlim(s(x))
4a. x < y & y < z => x < z
4b. x < y & y < z => x = z
4c. x < y v y < x v x=y
4d. x < s(x) & x < nextlim(x)
4e x < y => s(x) < s(y)
5a. x+0=x
5b. x+(s(y))=s(x+y)
5c. x + nextlim(y) = nextlim(x+y)
6a. x*0=0 6a. s(x*y) = (x*y)+x
6b. x * nextlim(y) = nextlim(x*y)
7a. (b < a) & (∀x < a)((P(x) & P(anc(x))) => P(s(x))) => P(b)
7b. (∀y)((∀x)(x < y => P(x)) => P(y))) => P(a)

The basic intuition is to limit the induction scheme to induction under an ordinal with regard to successor, and then add transfinite recursion. When quantifiers are bounded under ω, Peano Arithmetic should follow trivially from the above axioms.

I may have forgotten one or two (possibly for the relation of nextlim and <), and I highly suspect that there are a few redundant ones, but the basic intuition is to limit the induction scheme to induction under an ordinal with regard to successor, and then add unbounded transfinite recursion. I believe exponentiation is definable from + and * in this context, but I might be wrong. In that case, just add explicit axioms for exponentiation. In either case, once exponentiation is defined, you should be able to use use a transfinite Godel numbering to give a model of the theory of types. Once that is done, you can manipulate that model to provide axioms for larger and larger ordinals.

I threw these together somewhat hastily, so if anyone spots any errors, I blame someone else.


Ordinal arithmetic falls out of manipulations in set theory. You can define order and the ordinal operations in basic set theory and then prove things about these operations.

How big the ordinals you can construct depends on which axioms of ZF you allow or add. The theory behind this is called Reverse Mathematics.

The intent of Reverse Mathematics is to show which theorems of (nominally non-logical) mathematics are of equivalent strength, that is, can allow you to prove each other, and what logical axioms fit.

  • $\begingroup$ I have no idea what you mean to say. The usual way of reading what you wrote makes the first sentence false. Besides, reverse mathematics is not the right framework here. If you feel it is, you need to explain why second-order arithmetic suffices for the task at hand. And still this does not address the question of proof-theoretic strength. $\endgroup$ – Andrés E. Caicedo Feb 16 '18 at 23:22

protected by user26857 Aug 21 '15 at 21:27

Thank you for your interest in this question. Because it has attracted low-quality or spam answers that had to be removed, posting an answer now requires 10 reputation on this site (the association bonus does not count).

Would you like to answer one of these unanswered questions instead?

Not the answer you're looking for? Browse other questions tagged or ask your own question.