I'm not sure what you mean. First of all BB(n) is a function so it has value(s).
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.
(Late Edit: the above comment was rather sloppy. I meant that we don't know if it's impossible to prove BB(748)=X in ZFC+Con(ZFC). It's not necessarily possible either. We just haven't ruled out the possibility.)
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.
