It boggles my mind that a number (an uncomputable number, granted) like BB(748) can be "independent of ZFC". It feels like a category error or something.
replies(12):
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.
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.
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.
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.
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.
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.
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?
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.
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.
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.
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.
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.