# Why are some Busy Beaver values independent from ZFC if ZFC can always prove that a halting Turing Machine does in fact halt?

It has been proven that BB(745) is independent of ZFC (Johannes Riebel, 2023). Many experts believe that this will be true of BB(k) for values of k much smaller than 745 (some people say 15, 20, or even 10).

Now my understanding is that ZFC can always prove that a Turing Machine M will halt, if indeed it does halt. The difficulty comes when M does not halt, and ZFC has to prove that. (Per Gödel's theorem, there will be a non-halting Turing Machine T that is undecidable from ZFC (assuming ZFC is consistent))

But then why can't ZFC come up with the value of BB(745)? After all, the 745-state BB is a halting Turing Machine (by definition of Busy Beaver), and we have established that ZFC can always prove that a TM halts, if indeed it does. So why can't ZFC have a proof of the value of BB(745)?

An answer that comes to mind is that there is a difference between ZFC proving that 745-state BB halts (which ZFC can do), and ZFC having a proof of the value of BB(745) (which ZFC cannot do). Is that distinction accurate and answers my question?

Any feedback would be appreciated. Thanks!

• ZFC can prove that the 745-state BB halts, whichever TM that is, but it can't prove that it is the 745-state BB. There are other 745-state TMs that don't halt but ZFC can't prove they don't halt, so ZFC can't exclude the possibility that one of them is actually the 745-state BB. Commented Jan 1 at 4:07
• @spaceisdarkgreen Thanks for answer. Could you please expand on it? I think I understand but want to make sure. You're saying that if ZFC "stumbles" upon the 745-state BB, ZFC can prove that it halts, but will not be able to prove that this TM is indeed the BB of TMs with 745 states. Is that accurate? Commented Jan 1 at 4:14
• Correct, it can prove it halts (and for that matter calculate its 'production', whichever metric is being used, i.e. what we know to be the value BB(745)), but it can't prove it is the BB. Commented Jan 1 at 4:17
• @spaceisdarkgreen Got you, thanks. So ZFC can determine the actual value of BB(745), but will not know that this value is indeed the Busy Beaver of 745-state TMs? Commented Jan 1 at 4:26
• Well, "determining the actual value of BB(745)" would require 1) showing a particular 745-state TM is the BB. 2) Computing its production, which is the value of BB(745), so it can't do that. It can calculate the production of whatever TM happens to be the BB... but it can't prove it's the BB, hence can't prove that production value is BB(745). Commented Jan 1 at 4:39