¿Existe un enfoque axiomático para la aritmética ordinal?

Question

Siempre me he preguntado, ¿existe un enfoque axiomático de la aritmética de los números ordinales?

Si es así, me imagino que sería a la par de Fije la teoría en términos de su teoría de prueba de fuerza.

Answer 1

No he visto explícita axiomas utilizado antes, pero creo que el siguiente debería ser trivialmente suficiente para empezar:

Sea s(x) es la función sucesor. s, <, +, * son considerados como primitivos, junto a = y los axiomas de la igualdad
Definir Lim(x) ~(∃z)(S(z)=x) [por simplicidad, 0 se toma como límite ordinal]
Definir NextLim(x,y) como Lim(y) y(∀z)( z > x & Lim(z) => (z > y)v(z=y))
Definir nextlim(x) como y tal que NextLim(x,y)
Definir Anc(x,y) como nextlim(x) > y & Lim(x)
Definir anc(x) para la y tales que la Anc(x,y), o 0 si no hay tal y
Definir ω como nextlim(0)
Axiomas
1a. (∃y)( y < nextlim(x) y 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)=ran(y)
3c. anc(x)=ran(s(x))
3d. nextlim(x)=nextlim(s(x))
4a. x < y y y < z => x < z
4b. x < y y y < z => x = z
4c. x < y v y < x v x=y
4d. x < s(x) y 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) y (∀x < a)((P(x) y P(anc(x))) => P(s(x))) => P(b)
7b. (∀y)((∀x)(x < y => P(x)) => P(y))) => P(a)

La intuición básica es limitar el esquema de inducción a la inducción bajo un ordinal con respecto al sucesor y, a continuación, agregar la recursión transfinita. Cuando cuantificadores están delimitadas bajo ω, la Aritmética de Peano debe seguir trivialmente de los anteriores axiomas.

Puede que se me haya olvidado uno o dos (posiblemente por la relación de nextlim y <), y yo muy sospechoso que hay un par redundante, pero la intuición básica es limitar el esquema de inducción a la inducción bajo un ordinal con respecto al sucesor y, a continuación, añadir ilimitado de la recursión transfinita. Creo que la exponenciación es definible a partir de + y * en este contexto, pero puedo estar equivocado. En ese caso, sólo tiene que añadir explícita de axiomas para la exponenciación. En cualquier caso, una vez que la exponenciación se define, usted debería ser capaz de usar un transfinito de numeración de Gödel para dar un modelo de la teoría de los tipos. Una vez que haya terminado, usted puede manipular el modelo de proporcionar a los axiomas más grandes y más grandes los números ordinales.

Me arrojaron estos juntos un poco de prisa, así que si alguien spots de errores, puedo culpar a alguien más.