Creo que hay cierta vaguedad inherente en la "similar definición...". ¿Cómo asignar la declaración de consistencia $Con(ZF_\lambda)$ para lambda computable? Esto parece trivial pero no lo es.
También creo que ZF es algo así como una distracción aquí. La pregunta surge en PA (ya que estamos mirando oraciones $\Pi_1$ cuantificando sobre números naturales).
Feferman ha demostrado ("Progresión Recursiva Trasnifinita de Teorías" JSL 1962) que es posible asignar para cada n de manera efectiva una fórmula $\Sigma_1$ $\varphi_n(v_0)$ donde cada una de estas debería ser considerada como enumerando (códigos enteros de) conjuntos de axiomas (a los que llamaré "teorías"). Esto se hace de tal manera que si $a,b$ son enteros con $b = 2^a$ entonces $T_b$ es $T_a$ junto con la declaración
$$\forall \psi \in \Sigma_1\forall x [ Prov_{T_a}\psi(x) \longrightarrow \psi(x)]$$
(Esto es así un "Principio de 1-Reflexión" - para $\psi\in\Sigma_1$ aquí). Él hace esto con la intención de considerar aquellos enteros $a$ que son notaciones para ordinales recursivos (en el sentido del sistema de notación ideado por Kleene - "Kleene's $O$".)
(Hay cláusulas para $a$ representando una notación para un ordinal límite, cuando $a = 3^e$).
Él demuestra que hay caminos lineales a través del sistema de notaciones de ordinales computables, pasando por todos los ordinales recursivos $\alpha$, de manera que
Cada oración verdadera $\Pi_2$ en aritmética es probada por una de las teorías a lo largo del camino.
La teoría inicial $T_0$ aquí puede ser PA (o ZFC si lo prefieres). Un camino así le da un significado definitivo a $ZF_0, \ldots, ZF_\alpha, \ldots$ etc. para $\alpha$ recursivo.
Además, para tal progresión particular de teorías se interpretaría que la respuesta a la pregunta sería "No".
El punto de partida de Feferman fue el artículo de 1939 de Turing ("Sobre Sistemas de Lógica Basados en Ordinales"). Turing también consideró tales caminos a través de $O$ de Kleene, pero solo pudo probar un teorema para oraciones $\Pi_1$ (usando declaraciones de "Consistencia" más simples). Feferman muestra que si se toman declaraciones de "n-Reflexión" para cada $n$ cada vez que se extiende la teoría, entonces hay caminos a lo largo de los cuales cada enunciado verdadero de aritmética es demostrado.
La moraleja de la historia es que hay formas muy complejas de definir simplemente secuencias de teorías (porque hay infinitas maneras, o programas de Turing, de representar un ordinal recursivo) que pueden ocultar/disfrazar todo tipo de información.
Una encuesta muy legible es Franzen: "Sobre Progresiones Transfinitas" BSL 2004.
Actualización (Esto es una respuesta a la Actualización de Scott Aaronson.)
Él pregunta: dado un entero positivo k, ¿podemos decir algo concreto sobre qué declaraciones de consistencia iteradas son suficientes para probar la terminación o no terminación de cada máquina de Turing de k estados?
Permite que $M_0, \ldots ,M_{n-1}$ enumeren las TM's de $k$ estados. Permite que $P$ sea el subconjunto de $n$ de aquellos índices de las TM's en la lista que terminan.
La declaración
$\forall i (i \in P \rightarrow M_i$ termina $ \wedge \, i \notin P \rightarrow M_i $ no termina $)$
es una declaración $\Pi_2$. En el artículo de Feferman (op.cit.) muestra que cada declaración verdadera de $\Pi_2$ es probada por una teoría $T_a$ en una secuencia de 1-Reflexión, donde $a$ es una notación para un ordinal de rango igual a $\omega^2 + \omega + 1$.
Entonces, en términos de la pregunta no necesitamos variar el $\alpha$ dependiendo de los ordinales que una máquina de $k$ estados pueda producir. (Simplemente fija $\alpha$ como se indicó anteriormente). Por supuesto, no nos da ninguna información práctica: hay infinitas notaciones de esa rama, y es posible que no sepamos cuál mirar.
