¿Es el análisis ordinal un proyecto no-recursiva?

Question

Un recursiva ordinal es un ordinal, que es el orden de tipo para algunos recursiva relación (es decir, un recursiva bien el pedido). Podemos representar recursiva ordinales como números naturales utilizando Kleene $O$, con un ordinal sistema de notación. Por desgracia, el conjunto de números naturales que se encuentran en Kleene $O$ no es recursivo, o incluso recursivamente enumerable. Y no es efectivamente decidable si dos números representan el mismo ordinal o no.

Pero supongamos que usted tenía un oráculo $M$ que se podría decir con precisión lo que los números son notaciones de Kleene $O$, y si dos números representan el mismo ordinal. Deje $O'$ el conjunto de clases de equivalencia de los elementos de Kleene $O$, en virtud de la equivalencia de la relación de dos números que representan el mismo ordinal. Enumeremos (o código) de forma recursiva todos los axiomatized teorías con números naturales, por lo que el $T_n$ representa el $n^{th}$ tal teoría. A continuación, vamos a definir una función de $f$ desde el conjunto de los números naturales a $O'$ como sigue: $f(n)$ es el elemento de la $O'$ correspondiente a la prueba de la teoría ordinal de la teoría de la $T_n$. (La prueba de la teoría ordinal de una teoría es el menor ordinal que la teoría no puede demostrar el fundamento de.)

Mi pregunta es, ¿existe una máquina de Turing, la cual, dado el acceso a oracle $M$, se puede calcular la función de $f$? Para decirlo de otra manera, si un programa de ordenador sabía exactamente lo que recursiva ordinales hubo, no podía encontrar la prueba teórico-ordinal de todos los recursivamente axiomatizable teorías? Si la respuesta es no, como yo sospecho que puede ser, ¿qué otras oracle qué se requiere para hacerlo?

Cualquier ayuda sería muy apreciada.

Gracias de Antemano.

Answer 1

Creo que la respuesta que queremos es "sí, una vez que se puede hacer es rigurosa". Por ejemplo, si estamos hablando de teorías de segundo orden de la aritmética, entonces es claro lo de "T demuestra que el índice de $e$ calcula un bien de pedido" significa. Para las teorías de primer orden de la aritmética, la definición es más sutil, pero, por ejemplo, puede significar que el $T$ demuestra un cierto axioma esquema que representa la inducción transfinita a a $e$ o $T$ demuestra algún otro axioma esquema.

En cualquier caso, será de aplicación lo siguiente siempre y cuando "T demuestra que el índice de $e$ calcula un bien de pedido" significa que $T$ demuestra que algunos (posiblemente infinita) conjunto de oraciones que r es uniformemente.e. dado el índice de $e$; llamaremos el conjunto $S(e)$.

Hay otra advertencia de que estoy más nervioso acerca de. Estás hablando de la arbitraria índices para computable bien ordenamientos. Generalmente, cuando hacemos el ordinal análisis, nos fijamos en particular "agradable" índices, que calcular el bien de la orden en una forma agradable. Se sabe que hay varios trucos que pueden hacer con los índices de ocultar lo que están haciendo. Por ejemplo, hay un índice de $e$ que realmente calcula un orden de tipo $\omega$, pero la Aritmética de Peano no prueba que el orden calculada por $e$ tiene al menos un elemento. Así que ¿significa eso que, en su configuración, que el menor ordinal que PA no puede probar a estar bien fundada es $\omega$?

Así que, realmente, las declaraciones que pretenden identificar la prueba de la teoría ordinal tiene que ser entendido como informal interpretaciones de determinados resultados, en lugar de ser declaraciones acerca de una definición formal de "prueba teórica ordinal". Ver http://mathoverflow.net/questions/52926/proof-theoretic-ordinal/52927#52927

Voy a ignorar que temporalmente, y dar una respuesta en el espíritu de la pregunta, porque muestra un hecho clave acerca de $\mathcal{O}$. Pero no estoy convencido de que lo que se encuentra es realmente "la prueba teórica ordinal de $T$".

Ahora voy a proceder a la construcción. Dado un índice $t$$T$, la declaración "Para cada $i \in S(e)$, $T$ demuestra la frase con Goedel número $i$" se puede escribir como una fórmula aritmética $\phi(t,e)$, donde la misma fórmula $\phi$ funciona para todas las $t$$e$. Básicamente, $\phi$ dice: siempre que $e$ enumera una fórmula $i$, existe una prueba formal de que la fórmula de un conjunto de axiomas enumerados por $t$.

Así también hay una fórmula aritmética $\psi(t,e)$ que dice que $e$ calcula un orden lineal de $\omega$, e $\phi(t,e)$ no posee, pero que, para cada $e' <_e e$, $\phi(t,e')$ no se sostiene. La última parte se cuantifica más adecuada de cada segmento inicial de la posición calculada por $e$. Tenga en cuenta que si $e$ realmente calcula bien el pedido, a continuación, $\psi(t,e)$ mantiene si y sólo si el tipo de orden de $e$ (en algunos impreciso sentido, pero creo que el que quieres decir) la "prueba teórica ordinal de $T$."

El índice de $\mathcal{O}$ es muy fuerte. En particular, dada cualquier fórmula aritmética, podemos usar $\mathcal{O}$ decir si esa fórmula es verdadera o falsa. Formalmente, esto es el hecho de que $\emptyset^{(\omega)} <_T \text{HJ}(\emptyset) = \mathcal{O}$. Ahora bien, dado $t$, podemos hacer lo siguiente: enumerar todos los valores de $e$. Para cada uno, preguntar primero si $e \in \mathcal{O}$. Si no, pasar al siguiente valor de $e$. Si $e \in \mathcal{O}$, pregunte si $\psi(e,t)$ mantiene. Si es así, hemos encontrado que el número ordinal $t$. De lo contrario, pasar al siguiente valor de $e$. Esta va a encontrar algún tipo de "prueba teórica ordinal" $e$, con sujeción a mi advertencia anterior.