BusyBeaver(6) Is Quite Large

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.

Sure, you can come up with a set of axioms where the natural numbers include infinities. You may be able to use it to prove interesting things. But all that does here it make it so that the set of numbers describing how many steps a Turing machine runs before it stops is no longer the “natural numbers.”

I'm not sure what flavor of ultrafinitism you're referring here. If it's the "very big numbers, like TREE(3), are not natural numbers as they are far bigger than the number of atoms in this universe..." kind, then it has nothing to do with what this is about.

> physical representation

> your own eyes

Non standard models of ZFC have nothing to do with our physical world. That's why no physicist or engineer cares about them (or cares about axiom systems at all). So we need to be very careful when connecting the idea of physical, running "stuff" to the discussion of ZFC.

Anyway, back to

> you can run them both alongside in this universe and see which one finishes first

There are two Turing Machines, Foo and Bar. We build and run them in our physical universe. Foo halts at the standard BB(748) steps. Bar just keeps running and running. That's what we will see with our own eyes.

The issue is that when we try to reason out whether Bar will ultimately halts, ZFC doesn't prevent us from defining a non-standard model where Bar halts after a non-standard number of steps. Note that the physical Bar will not halt in our universe. The "non-standard number of steps" is as nonsense as it sounds. It's just that ZFC doesn't prevent us from defining such a nonsense. The point of ZFC is it's compatible with almost all the useful, sane math. It's not necessarily incompatible with bullshit and insane math.

That is it. The fact that Bar is still keeping running in our universe is completely irrelevant.

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.

> This, in turn, means that there is no observation you could ever make that would distinguish between the values a and b (for the identity of BB(x)). No matter what you believe the value of BB(x) might secretly be, there are no consequences; nothing anywhere could ever change if the value turned out to be different. Because, if there were an observable consequence of the value being different, the hypothetical observation of that consequence would be a disproof of the value that didn't cause it, and no such disproof can exist.

There's one part of this I don't understand. "BB(x) = n" means "there is at least one x-state Turing machine that halts after exactly n steps, and there are no x-state Turing machines that halt after more than n steps", right? Then why wouldn't this approach work (other than the numbers being way too big to actually do in this universe)? WLOG, assume a < b. Run all possible x-state Turing machines for b steps. If any halted on step b, then you've disproved "BB(x) = a". If not, then you've disproved "BB(x) = b".