Busy Beaver argument and Gödel's incompleteness theorem

Question

By Gödel's incompleteness theorem, it should not be possible to prove the consistency of ZFC within ZFC (if it is consistent).

It is well known that the Busy Beaver function is uncomputable, and that execution of this Turing machine (call it TM) for BB(8000) steps can amount to a proof ZFC is consistent.

It seems to me that one could formulate a statement in ZFC to the effect:

State of TM (BB(8000)) ≠ Halting

What is the fallacy in this argument?

It is easy to conceive that proofs of non-termination of many Turing machines up to 8000 are Collatz-like and very hard to prove; and absolutely obvious that no mortal could ever verify such a postulation.

However, it seems possible to state within ZFC, and to compute State of TM (BB(8000)) requires "merely" a finite enumeration of finite rules, which should be in theory admissible. Or is it the case that this statement is admissible in ZFC, but the implication statement that "Given State of TM (BB(8000)) ≠ Halting, ZFC is consistent" which is not expressible in ZFC?

Answer 1

The notation is maybe too compact here so it's hard to see what's going on. $BB(8000)$ is, by definition, the maximum number of steps a halting $8000$-state Turing machine runs before halting. This means if you expand this statement out in terms of this definition of $BB(8000)$, which involves writing down a quantification over a set of Turing machines that includes the Turing machine $TM$ in question, this statement is just straightforwardly equivalent to

TM runs forever

which is in turn equivalent to $\text{Con}(ZFC)$. So, this isn't a big mystery so far: of course ZFC is capable of stating this. The subtlety is here:

and to compute State of TM (BB(8000)) requires "merely" a finite enumeration of finite rules

We need to be careful at this point to distinguish between two possible meanings of "$BB(8000)$" here. I believe the argument you intend here is: whatever the true value of $BB(8000)$ is, it is just some positive integer $n$, and for any positive integer $n$, the true state of TM at step $n$ is the result of a finite computation, however unimaginably large, so it's something ZFC should be able to not only state but prove.

This is true. However, it does not follow that ZFC can prove $\text{Con}(ZFC)$ this way, because if you replace "$BB(8000)$" above (which I interpreted to mean a certain quantification over $8000$-state Turing machines) with the true value $n$ of $BB(8000)$, ZFC is not capable of proving that this $n$ really is the true value of $BB(8000)$, which means ZFC is not capable of proving that $TM(n)$ has anything to do with $\text{Con}(ZFC)$!

So this is quite pleasantly subtle. As I mentioned here in a previous question on this result, one has to distinguish carefully between numbers and descriptions of numbers to avoid getting hopelessly confused here.