En un anterior MO pregunta, me dijeron que por varios comentaristas que
(a) se sabe que existe una computable ordinal $\alpha_{ZF}$ que "codifica la fuerza de la teoría de conjuntos ZF" (es decir, un mínimo computable ordinal que ZF no puede probar está bien fundada), pero
(b) en la actualidad, carecemos de cualquier descripción de una máquina de Turing computing $\alpha_{ZF}$.
Esta afirmación intrigado y me sorprendió, ya que es raro que podemos probar que una determinada máquina de Turing existe, pero sólo en un completamente manera no constructiva.
Pensando en ello aún más, sin embargo, me parece que nos puede dar una explícita máquina de Turing que define a $\alpha_{ZF}$, por supuesto, bajo la suposición de que ZF es el sonido. Así que estaría muy agradecido si alguien me pudiera decir si estoy cometiendo un error en la siguiente.
Lo que queremos, claramente, es el supremum de todos los countably-muchos de los ordinales que ZF no resultar bien fundada. Pero el siguiente programa de computadora, llame a $P$, debe calcular el orden de relación de ese límite ordinal:
- Set $t:=0$. Recorrer todas las posibles derivaciones en ZF, la búsqueda de pruebas de las declaraciones de la forma, "la máquina de Turing $M$ calcula el orden de relación de una bien fundada contables ordinal." Cualquier momento en una prueba se encuentra, establezca $t:=t+1$, e iniciar un proceso paralelo marcados por $t$ (en la "convergencia" de moda) que simula $M$, y que los resultados "$\langle t,x \rangle < \langle t,y \rangle$" siempre $M$ salidas "$x < y$". Mientras tanto, también se definen $\langle t,x \rangle < \langle u,y \rangle$ siempre $t<u$.
Suponiendo ZF es el sonido (al menos en sus afirmaciones sobre ordinal notaciones, si no sus afirmaciones sobre la transfinito conjuntos), la salida de $P$ debe ser el fin de la relación de
$\alpha_1 + \alpha_2 + \cdots$,
donde $\alpha_1, \alpha_2, \ldots$ es algunos de enumeración (no necesariamente en orden creciente) de los ordinales que ZF demuestra ser bien fundada. Pero algunos ordinal simple aritmética debe entonces demostrar que esa ordinal es igual a $\alpha_{ZF}$, ya que la única cosa que importa para la determinación de su tamaño es la parte fundamental de la secuencia de $\alpha_{ZF}$ que contiene por definición.
Por supuesto, si ZF es inconsistente, entonces $P$ finalmente la salida de una completa tontería, aunque si ZF es consistente, pero no, $P$ podría salida de un orden de relación que no esté bien fundada. En particular, la declaración de "$P$ define válido ordinal $\alpha_{ZF}$" implica Con(ZF), y por lo tanto no puede ser comprobado en ZF (suponiendo que Con(ZF)). Esto es como sería de esperar.
Ahora, si lo anterior funciona, entonces me da una comprensión diferente del programa de ordinal prueba de la teoría de la---algo que he estado tratando de aprender un poco acerca de los muy conocedores del Profesor MO. En particular, esto significa que, cuando la gente pregunta por un "ordinal análisis de ZF," que no estamos pidiendo cualquier descripción explícita de los ordinales $\alpha_{ZF}$---eso es fácil de conseguir, por la de arriba. En lugar de que están pidiendo una "combinatoria" descripción: un vago requisito, pero que básicamente significa que nuestro programa de ordenador que describe el ordinal no debería hacer ninguna referencia directa a ZF sí mismo. De esta manera, uno podría imaginar que alguien la formación de una intuición $\alpha_{ZF}$ está bien fundado y , por tanto, que ZF es consistente, sin circularmente presupone Con(ZF) (como mi programa $P$ nos obligó a hacer).
