Proving BB(748)=X for some concrete X in ZFC is equivalent to proving Con(ZFC) in ZFC.
Yes, but I'm not "proving BB(748)=X in ZFC" in my previous comment.
I clearly stated:
> as long as we assume ZFC is consistent
In other words, I'm talking about proving BB(748)=X in ZFC+Con(ZFC), which is not fundamentally impossible. It's practically impossible simply because you need to reason out the sheer amount of TMs with 748 states.
Is there reason to believe that there's not a similarly sized turing machine that halts iff Con(ZFC + Con(ZFC)) (which is independent of ZFC+Con(ZFC) by godel's)?
Certainly there's some sized machine that does that... it seems to me that all you're doing is playing games with adding axioms to maybe change the exact value of "748"... and I don't even see that you've established that you've successfully changed it.
Well, yes, my previous comment was sloppy. Of course it's also possible that 748 is such a high upper limit that we can add a lot of axioms to ZFC and BB(748) is still independent to it. We just don't know it.
And in theory we can prove BB(748)=X, where X is a plain big natural number, as long as we just assume ZFC is consistent. It's practically impossible, but not fundamentally impossible like proving Con(ZFC) in ZFC itself.