Una pregunta sobre el análisis ordinal

Question

Tengo varias preguntas relacionadas con el análisis ordinal.

Según [ 1 ], aquí están los ordinales de la teoría de la prueba de algunas teorías conocidas (usando $|T|$ denotan el ordinal teórico de prueba de $T$ ):

• $ |\text{ATR}_0|=\Gamma_0,|\text{ATR}|=\Gamma_{\varepsilon_0} $

• $ |\Pi^1_0-\text{CA}_0|=\varepsilon_0,|\Pi^1_0-\text{CA}|=\varepsilon_{\varepsilon_0}<\varphi(\varepsilon_0,0)=|\Delta^1_1-\text{CA}|$

• $|\Pi^1_1-\text{CA}_0|=|\Delta^1_2-\text{CA}_0|=\psi(\Omega_\omega)$

• $|\Pi^1_1-\text{CA}|=\psi(\Omega_\omega\varepsilon_0)<\psi(\Omega_{\varepsilon_0})=|\Delta^1_2-\text{CA}|$

(Fíjate cuando hay un subíndice 0 y cuando no lo hay. Por supuesto $\Pi^1_0-\text{CA}_0$ es $\text{ACA}_0$ .)

Nunca he visto $|\Delta^1_1-\text{CA}_0|$ mencionado en ningún sitio, pero al ver el $\Delta^1_2$ caso supongo que tiene ordinal teórico de prueba $\varepsilon_0$ .

En general, la siguiente igualdad parece una conjetura razonable: $ |\Pi^1_n-\text{CA}_0| = |\Delta^1_{n+1}-\text{CA}_0| < |\Pi^1_n-\text{CA}|<|\Delta^1_{n+1}-\text{CA}| $ para todos $n$ . ¿Alguien tiene una prueba o referencia de esto?

Además, cada vez que se elimina el subíndice 0, el ordinal $\varepsilon_0$ aparece en el ordinal teórico de la prueba de la teoría resultante. ¿Existe alguna razón o intuición sencilla para que esto ocurra?

Answer 1

En primer lugar, hay que tener en cuenta que (todavía) no tenemos análisis ordinales de los subsistemas de la aritmética de segundo orden más allá de $\Pi^1_2$ -CA $_0$ .

Aun así, podemos decir algo sobre el patrón que indicas utilizando resultados conocidos sobre estos sistemas. Una buena referencia es el libro de Stephen G. Simpson: Subsistemas de aritmética de segundo orden .

Allí encontramos, por ejemplo:

• $\Delta^1_{k+3}$ -CA $_0$ es una extensión conservadora de $\Pi^1_{k+2}$ -CA $_0$ para $\Pi^1_4$ -sentencias. (Cor. IX.4.12)
• $\Delta^1_{k+2}$ -CA demuestra la existencia de una codificación contable $\beta$ -modelo de $\Pi^1_{k+1}$ -CA $_0$ . (Cor. VII.7.9)
• $\Pi^1_{k+1}$ -CA $_0$ demuestra la existencia de un código contable $\beta$ -modelo de $\Delta^1_{k+1}$ -CA $_0$ . (Cor. VII.7.9)

Por último, permítame especular un poco sobre su última pregunta. No creo que exista un teorema formal al respecto. (Al menos no con la tecnología actual.) El subsistema $T$ sin el subíndice $0$ difiere de $T_0$ añadiendo la inducción completa. Cuando tenemos todas las herramientas para un análisis ordinal de $T_0$ A menudo podemos conseguir uno por $T$ iterando (en cierto sentido) nuestro procedimiento para $T_0$ a lo largo de $\varepsilon_0$ para hacer el corte-eliminación con inducción completa. Pero no es tan sencillo, ya que los pasos exactos difieren mucho en cada caso, por ejemplo, si hay que colapsar. Echa un vistazo al capítulo de Pohlers sobre Subsistemas de la teoría de conjuntos y de la teoría de números de segundo orden en el Handbook of Proof Theory. Allí verás algunos casos de este patrón, al menos en lo que respecta a los límites superiores.

Tal vez se podría haber hecho una declaración más general utilizando la frase de Girard $\Pi^1_n$ -lógica, pero eso es el reino de la especulación salvaje por mi parte, y no creo que esto se haya desarrollado lo suficiente, particularmente en relación con los subsistemas de la aritmética de segundo orden.