Is there an axiomatic approach to ordinal arithmetic? 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.
 A: 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)
Axioms
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.
A: See A Formalization of the Theory of Ordinal Numbers by Gaisi Takeuti in  The Journal of Symbolic Logic, Vol. 30, No. 3 (Sep., 1965), pp. 295-317.

Although Peano's arithmetic can be developed in set theories, it can
  also be developed independently. This is also true for the theory of
  ordinal numbers... In this paper we shall develop the theory of
  ordinal numbers in the first order predicate calculus with equality as
  an extension of Peano's arithmetic. This theory will prove to be easy
  to manage and fairly powerful in the following sense: If A is a
  sentence of the theory of ordinal numbers, then A is a theorem of our
  system if and only if the natural translation of A in set theory is a
  theorem of Zermelo-Fraenkel set theory. It will be treated as a
  natural extension of Peano's arithmetic. The latter consists of axiom
  schemata of primitive recursive functions and mathematical induction,
  while the theory of ordinal numbers consists of axiom schemata of
  primitive recursive functions of ordinal numbers, of transfinite
  induction, of replacement and of cardinals. The latter three axiom
  schemata can be considered as extensions of mathematical induction.

A: 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.
