> This doesn't sound right to me.

Which bit?

> You can prove that ZFC is consistent. You could do it today, with or without the magic number, using a stronger axiom system.

Right but then just replace ZFC with that stronger system and you're back where you started - the point is that whatever the "strongest" system is that we've yet considered, BB(N) for sufficiently large N is stronger than that - and in all likelihood N can be much smaller than 748 for all such systems we've yet conceived, since we are not great at efficiently encoding things in turing machines.

> If an Oracle told you that BB(748) = 100 or whatever, that would constitute proof that ZFC is consistent.

The number alone is not the proof - you'd still need to actually run the corresponding turing machine to finish the proof.

> But it wouldn't negate the fact that BB(748) is independent of ZFC, because you haven't proved within the axioms of ZFC that ZFC is consistent, which is what makes it independent.

Normally when we say some predicate P is independent of some axiomatic system it means we could add a new axiom to the system (P or !P) that would produce a new system that is still consistent.

BB(N) being "independent of ZFC" is a very different statement - it doesn't mean we are free to pick different values of BB(N). It's easy to prove this:

1. Let's say there are two possible values of BB(748) - V1 and V2 such that V2 > V1 and both are consistent with ZFC.

2. Simulate every possible 748 state turing machine for V2 steps.

3. See if any one terminated after more than V1 steps.

4. If they did, then V1 is inconsistent with ZFC - contradiction. If they did not, then V2 is inconsistent with ZFC - contradiction (since at least one turing machine must terminate after exactly V2 steps).

This entire process takes finite time since there are finitely many 748 state turing machines and V1 and V2 are also finite.

So what does it even mean to say that BB(748) is independent of ZFC? BB(N) is not even a predicate so it definitely feels like a category error to say it's independent.

We certainly can't prove that a candidate value is correct within ZFC, but given any "overestimate" of BB(748) we can prove that it's wrong:

1. Let's say we have VC - an estimate of BB(748) that's too large.

2. Simulate every possible 748 state turing machine for VC steps.

3. If no turing machine terminated after exactly VC steps, then VC is wrong.