In a previous MO question, I was told by several commenters that
(a) it's known that there exists a computable ordinal $\alpha_{ZF}$ that "encodes the strength of ZF set theory" (i.e., a least computable ordinal that ZF fails to prove is well-founded), but
(b) at present, we lack any description whatsoever of a Turing machine computing $\alpha_{ZF}$.
This claim intrigued and surprised me, since it's rare that we can prove that a certain Turing machine exists, but only in a completely nonconstructive way.
Thinking about it further, though, it seems to me that we can give an explicit Turing machine that defines $\alpha_{ZF}$, of course under the assumption that ZF is sound. So I'd be grateful if anyone could tell me if I'm making a mistake in the following.
What we want, clearly, is the supremum of all the countably-many ordinals that ZF does prove to be well-founded. But the following computer program, call it $P$, should compute the order relation of that limit ordinal:
-
Set $t:=0$. Loop over all possible derivations in ZF, searching for proofs of statements of the form, "the Turing machine $M$ computes the order relation of a well-founded countable ordinal." Any time such a proof is found, set $t:=t+1$, and start up a parallel process labelled by $t$ (in "dovetailing" fashion) that simulates $M$, and that outputs "$\langle t,x \rangle < \langle t,y \rangle$" whenever $M$ outputs "$x < y$". Meanwhile, also define $\langle t,x \rangle < \langle u,y \rangle$ whenever $t<u$.
Assuming ZF is sound (at least in its claims about ordinal notations, if not its claims about transfinite sets), the output of $P$ should be the order relation of
$\alpha_1 + \alpha_2 + \cdots$,
where $\alpha_1, \alpha_2, \ldots$ is some enumeration (not necessarily in increasing order) of the ordinals that ZF proves to be well-founded. But some simple ordinal arithmetic should then show that that ordinal is equal to $\alpha_{ZF}$, since the only thing that matters for determining its size is the fundamental sequence for $\alpha_{ZF}$ that it contains by definition.
Of course, if ZF is inconsistent, then $P$ will eventually output complete nonsense, while even if ZF is consistent but unsound, $P$ could output an order relation that fails to be well-founded. In particular, the statement "$P$ defines a valid ordinal $\alpha_{ZF}$" implies Con(ZF), and hence can't be proved in ZF (assuming Con(ZF)). This is as we'd expect.
Now, if the above works, then it gives me a different understanding of the program of ordinal proof theory—something I've been trying to learn a bit about from the extremely-knowledgeable Professor MO. In particular, it would mean that, when people ask for an "ordinal analysis of ZF," they're not asking for just any explicit description of the ordinal $\alpha_{ZF}$—that's easy to get, by the above. Instead they're asking for a "combinatorial" description: a vague requirement, but one that basically means that our computer program describing the ordinal shouldn't make any direct reference to ZF itself. This way, one could imagine someone forming an intuition that $\alpha_{ZF}$ is well-founded and therefore that ZF is consistent, without circularly presupposing Con(ZF) (as my program $P$ required us to do).
Best Answer
Theorem. The following are equivalent.
The relation on $\mathbb{N}$ computed by your program P is a well-order.
ZF is $\Pi^1_1$-sound.
Proof. You gave the argument for the reverse implication $(2\to 1)$, since you only needed to know that that whenever ZF proves that a certain computable relation is a well-order, that it really is, and these are instances of $\Pi^1_1$-soundness. Conversely, suppose that P computes a well-order. Thus, whenever ZF proves that a specific TM computes a well-order, then it really does compute a well order, for otherwise the ill-foundedness would show up in the relation computed by your program P. I claim that this implies $\Pi^1_1$-soundness. To see this, suppose that ZF proves a $\Pi^1_1$ assertion $\sigma$. It is a basic fact of descriptive set theory that every $\Pi^1_1$-assertion is equivalent to the well-foundedness of a certain explicit computable tree, which via the Kleene-Brouwer order means that $\sigma$ is equivalent to the assertion that a certain computable order, for which an explicit TM encoding can be extracted from the syntactic representation of $\sigma$, is a well-order. Since ZF proved $\sigma$, it follows that ZF proves that this computable order is a well-order. By (1), we've assumed that ZF is correct about that, and so the order really is a well order. And so $\sigma$ really is true. Thus, ZF is $\Pi^1_1$-sound. QED