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.
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))
2b. ~∃x(0 = nextlim(x))
3a. s(x)=s(y) => x=y
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)
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.
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?