[tromp]

What makes BB(748) independent of ZFC is not its value, but the fact that one of the 748-state machines (call it TM_ZFC_INC) looks for an inconsistency (proof of FALSE) in ZFC and only halts upon finding one.

Thus, any proof that BB(748) = N must either show that TM_ZF_INC halts within N steps or never halts. By Gödel's famous results, neither of those cases is possible if ZFC is assumed to be consistent.

[Diggsey]

I think what's most unintuitive is that most (all?) "paradoxes" or "unknowables" in mathematics involve infinities. When limiting ourselves to finite whole numbers, paradoxes necessarily disappear.

BB(748) is by definition a finite number, and it has some value - we just don't know what it is. If an oracle told us the number, and we ran TM_ZFC_INC that many steps we would know for sure whether ZFC was consistent or not based on whether it terminated.

The execution of the turing machine can be encoded in ZFC, so it really is the value of BB(748) that is the magic ingredient. Somehow even knowledge of the value of this finite number is a more potent axiomatic system than any we've developed.

[waluigi]

It’s even more counterintuitive than you let on! If you are working in ZFC along with the axiom “ZFC is consistent” then there’s no issue: just a normal number[1]. Where things get really strange is in ZFC plus the axiom “ZFC is inconsistent”.

This already sounds like an inconsistent theory, but surprisingly isn’t: Godel’s second incompleteness theorem directly gives us that Con(ZFC) is independent, so there are models that validate both Con(ZFC) and ~Con(ZFC). The models that validate ~Con(ZFC) are very confused about what numbers are: from the models perspective, there is a number corresponding to a Godel code for the supposed proof of inconsistency, but from the external view this is a “nonstandard number”: it’s not not a finite numeral!

Getting back to BB(748): what does this look like in a model of ZFC + ~Con(ZFC)? We can prove that the machine internal to the model will find that astronomically large Godel code, so BB(748) will be a nonstandard number. In other words, you can tell if a 748 state machine will terminate in this model: you’ve just got to run it for a number of steps that’s larger than every finite numeral!

[1]: unless there’s some machine that with 748 that enumerates theorems of ZFC+Con(ZFC) but that’s a different discussion.

[raincole]

BB(748) is a finite number, but I'd argue its magic also comes from infinites: the fact some Turing Machines run forever and never halt.

[joelthelion]

Is it? If it's not possible to prove that it's the best solution to bb(748), does it even exist in any meaningful way?

[raincole]

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.

[raincole]

(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.)

[gpm]

Proving BB(748)=X for some concrete X in ZFC is equivalent to proving Con(ZFC) in ZFC.

[raincole]

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.

[edanm]

> BB(748) is by definition a finite number, and it has some value - we just don't know what it is. If an oracle told us the number, and we ran TM_ZFC_INC that many steps we would know for sure whether ZFC was consistent or not based on whether it terminated.

This doesn't sound right to me.

You can prove that ZFC is consistent. You could do it today, with or without the magic number, using a stronger axiom system. If an Oracle told you that BB(748) = 100 or whatever, that would constitute proof that ZFC is consistent.

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.

> I think what's most unintuitive is that most (all?) "paradoxes" or "unknowables" in mathematics involve infinities. When limiting ourselves to finite whole numbers, paradoxes necessarily disappear.

I might be missing something, but all of these assertions deal with finite whole numbers, not infinity. Unless you count a Turing machine running forever an infinity, in which case, it seems counterintuitive to me that encoding a while loop that runs forever somehow makes paradoxes appear.

[Diggsey]

> 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.

[panpog]

There is only one integer k that we can actually write down (given much more paper than could fit in the universe) such that ZFC+ “BB(748)=k” is consistent. However, given that same k, ZFC+ “BB(748)≠k” is also consistent. ZFC+ “BB(748)≠k” has theorems that can be thought of as it being wrong about what “finite” means.

[zmgsabst]

You’d know the value in a more powerful system than ZFC (as it includes such an oracle) — but you can already reason about ZFC in a more powerful system.

We already have more powerful systems, but what causes the inability to self-reason is exactly that power: only first order logic can prove its own consistency. Once you get powerful enough to model arithmetic, you can build statements with self-referential weirdness.

I don’t see it as a paradox, but as growth: a sufficiently rich system can pose questions which suggest a richer system — and thereby scaffold up the universe hierarchy.

[edanm]

> Thus, any proof that BB(748) = N must either show that TM_ZF_INC halts within N steps or never halts. By Gödel's famous results, neither of those cases is possible if ZFC is assumed to be consistent.

Isn't it more accurate to say that any proof that BB(748) = N in ZFC must either show that TM_ZF_INC halts within N steps, or never halts?

Meaning, it's totally possible to prove that BB(748) = N, it just can't be done within the axioms of ZFC?

[woopsn]

Does the fact that BB(k)=N is provable up to some k < 748 mean that all halting problems for machines with k states are answered by a proof in ZFC?

[legobmw99]

748 is not tight. As given in the article, k=643 is independent of ZFC, and the author speculates that it's possible that something as small as BB(9) could be as well.

The 748/745/643 numbers are just examples of actual machines people have written, using that many states, that halt iff a proof of "false" is found.

At any rate, given the precise k, I believe your intuition is correct. I've heard this called 'proof by simulation' -- if you know a bound on BB(N), you can run a machine for that many steps and then you know if it will run forever. But this property is exactly the intuition for why it grows so fast, and why we will likely never definitively know anything beyond BB(5). BB(6) seems like it might be equivalent to the Collatz conjecture, for example.

[Scarblac]

I don't understand, surely if we assume ZFC is consistent then it's obvious that it won't halt? Even if its consistency can't be proven, neither can its inconsistency, so it won't halt. Or is that only provable outside of ZFC?

I guess it's also hard when we have an arbitrary Turing machine and have to prove that what it's doing isn't equilavent to trying to prove an undecibable statement.

[LegionMammal978]

If you believe that ZF is consistent, then you believe that the machine cannot halt (assuming you trust its construction). But you cannot write a proof in ZF that the machine cannot halt. Such a proof must include a new axiom "ZF is consistent", or some stronger axiom.

[tromp]

If we assume ZFC to be consistent, then Gödel's 2nd incompleteness theorem tells us that it cannot prove its own consistency. So in particular it cannot prove than TM_ZFC_INC will never halt.