5 Corrected statement

I think there is some vagueness inherent in the "similarly define ...". How is one to assign the consistency statement $Con(ZF_\lambda)$ for computable $\lambda$? This looks trivial but it is not.

I think also ZF is something of a red herring here. The question arises in PA (since we are looking at $\Pi_1$ sentences quantifying over natural numbers.)

Feferman has shown ("Transfinite Recursive Progression of Theories" JSL 1962) that it is possible to assign for every n in an effective manner a $\Sigma_1$-formula $\varphi_n(v_0)$ where each of the latter is to be thought of as enumerating (integer codes of) axiom sets (which I'll call "theories."). This is done in such a fashion so that if $a,b$ are integers with $b = 2^a$ that $T_b$ is $T_a$ together with the statement

$$\forall \psi \in \Sigma_1\forall x [ Prov_{T_a}\psi(x) \longrightarrow \psi(x)]$$

(This is thus a "1-Reflection Principle" - for $\psi\in\Sigma_1$ here). He does this with a view to considering those integers $a$ that are notations for recursive ordinals (in the sense of the notation system devised by Kleene - "Kleene's $O$".)
(There are clauses for $a$ representing a notation for a limit ordinal, when $a = 3^e$).

He proves that there are linear paths through the system of notations of computable ordinals, going through all recursive ordinals $\alpha$,so that

*Every true $\Pi_2$ sentence in arithmetic is proven by one of the theories along the path*.

The starting theory $T_0$ here can be PA (or ZFC if you want). Such a path gives a definite meaning to $ZF_0, \ldots, ZF_\alpha, \ldots$ etc. for recursive $\alpha$.

Moreover for such a particular progression of theories one would would construe the answer to the question to be "No".

Feferman's starting point was the 1939 paper of Turing ("On Systems of Logic Based on Ordinal"). Turing also considered such paths through Kleene's $O$, but could just prove a theorem for $\Pi_1$ sentences, (using simpler "Consistency" statements"). Feferman shows that if one takes "$n$-Reflection" statements for every $n$ each time one extends the theory then there are paths along which every true statement of arithmetic is proven.

The moral of the story is that there are very complex ways of simply defining sequences of theories, (because there are infinitely many ways, or Turing programs, of representing a recursive ordinal) which can hide/disguise all sorts of information.

A very readable survey is Franzen: "On Transfinite Progressions" BSL 2004.

Update (This is an answer to Scott Aaronson's Update.)

He asks: given a positive integer k, can we say something concrete about which iterated consistency statements suffice to prove the halting or non-halting of every k-state Turing machine?

Let $M_0, \ldots ,M_{n-1}$ enumerate the $k$-state TM's. Let $P$ be the subset of $n$ of those indices of TM's in the list that halt.

The statement

$\forall i (i \in P \roghtarrow M_i \mbox{ rightarrow M_i$ halts } $\wedge \, i \notin P \rightarrow M_i \mbox{$ does not halt }$)$

is a $\Pi_2$ statement. In Feferman's paper (op.cit.) he shows that every true $\Pi_2$ statement is proven by a theory $T_a$ in a 1-Reflection sequence, where $a$ is a notation for an ordinal of rank equal to $\omega^2 + \omega + 1$.

So in terms of the question we do not need to vary the $\alpha$ depending on what ordinals a $k$-state machine can produce. (Just fix $\alpha$ as given above.) Of course it gives us zero practical information: there are infinitely many such notations of that rank, and we may not know which one to look at.

4 Corrected nonsense

I think there is some vagueness inherent in the "similarly define ...". How is one to assign the consistency statement $Con(ZF_\lambda)$ for computable $\lambda$? This looks trivial but it is not.

I think also ZF is something of a red herring here. The question arises in PA (since we are looking at $\Pi_1$ sentences quantifying over natural numbers.)

Feferman has shown ("Transfinite Recursive Progression of Theories" JSL 1962) that it is possible to assign for every n in an effective manner a $\Sigma_1$-formula $\varphi_n(v_0)$ where each of the latter is to be thought of as enumerating (integer codes of) axiom sets (which I'll call "theories."). This is done in such a fashion so that if $a,b$ are integers with $b = 2^a$ that $T_b$ is $T_a$ together with the statement

$$\forall \psi \in \Sigma_1\forall x [ Prov_{T_a}\psi(x) \longrightarrow \psi(x)]$$

(This is thus a "1-Reflection Principle" - for $\psi\in\Sigma_1$ here). He does this with a view to considering those integers $a$ that are notations for recursive ordinals (in the sense of the notation system devised by Kleene - "Kleene's $O$".)
(There are clauses for $a$ representing a notation for a limit ordinal, when $a = 3^e$).

He proves that there are linear paths through the system of notations of computable ordinals, going through all recursive ordinals $\alpha$,so that

*Every true $\Pi_2$ sentence in arithmetic is proven by one of the theories along the path*.

The starting theory $T_0$ here can be PA (or ZFC if you want). Such a path gives a definite meaning to $ZF_0, \ldots, ZF_\alpha, \ldots$ etc. for recursive $\alpha$.

Moreover for such a particular progression of theories one would would construe the answer to the question to be "No".

Feferman's starting point was the 1939 paper of Turing ("On Systems of Logic Based on Ordinal"). Turing also considered such paths through Kleene's $O$, but could just prove a theorem for $\Pi_1$ sentences, (using simpler "Consistency" statements"). Feferman shows that if one takes "$n$-Reflection" statements for every $n$ each time one extends the theory then there are paths along which every true statement of arithmetic is proven.

The moral of the story is that there are very complex ways of simply defining sequences of theories, (because there are infinitely many ways, or Turing programs, of representing a recursive ordinal) which can hide/disguise all sorts of information.

A very readable survey is Franzen: "On Transfinite Progressions" BSL 2004.

Update (This is an answer to Scott Aaronson's Update.)

He asks: given a positive integer k, can we say something concrete about which iterated consistency statements suffice to prove the halting or non-halting of every k-state Turing machine?

Let $M_0, \ldots ,M_{n-1}$ enumerate the $k$-state TM's. Let $P$ be the subset of $n$ of those indices of TM's that halt.

The statement

$\forall xi (x$ codes a TM $i \rightarrow in P \exists y (y$ codes a run of a computation on $x$ that halts$) roghtarrow M_i \vee mbox{ halts } \forall y( y$ wedge i \notin P \rightarrow M_i \mbox{ does not code such a run))halt })$is a$\Pi_2$statement. In Feferman's paper (op.cit.) he shows that every true$\Pi_2$statement is proven by a theory$T_a$in a 1-Reflection sequence, where$a$is a notation for an ordinal of rank equal to$\omega^2 + \omega + 1 $. So in terms of the question we do not need to vary the$\alpha$depending on what ordinals a$k$-state machine can produce. (Just fix$\alpha$as given above.) 3 Updated answer to a new question; deleted 9 characters in body; added 7 characters in body Update (This is an answer to Scott Aaronson's Update.) He asks:given a positive integer k, can we say something concrete about which iterated consistency statements suffice to prove the halting or non-halting of every k-state Turing machine? The statement$\forall x( x $codes a TM$ \rightarrow \exists y (y$codes a run of a computation on$x$that halts$) \vee \forall y( y$does not code such a run)) is a$\Pi_2$statement. In Feferman's paper (op.cit.) he shows that every true$\Pi_2$statement is proven by a theory$T_a$in a 1-Reflection sequence, where$a$is a notation for an ordinal of rank equal to$\omega^2 + \omega + 1 $. So in terms of the question we do not need to vary the$\alpha$depending on whatordinals a$k$-state machine can produce. (Just fix$\alpha\$ as given above.)

2 Corrected a garbled sentence.
1