Is there an axiomatic approach to ordinal arithmetic?

Solution 1:

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.

Solution 2:

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.