Is there an axiomatic approach to ordinal arithmetic?
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.