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):
Most of these 'uncomputable' problems are uncomputable in the sense of the halting problem: you can write down an algorithm that should compute them, but it might never halt. That's the sense in which BB(x) is uncomputable: you won't know if you're done ever, because you can't distinguish a machine that never halts from one that just hasn't halted yet (since it has an infinite number of states, you can't just wait for a loop).
So presumably the independence of a number from ZFC is like that also: you can't prove it's the value of BB(745) because you won't know if you've proved it; the only way to prove it is essentially to run those Turing machines until they stop and you'll never know if you're done.
I'm guessing that for the very small Turing machines there is not enough structure possible to encode whatever infinitely complex states end up being impossible to deduce halting from, so they end up being Collatz-like and then you can go prove things about them using math. As you add states the possible iteration steps go wild and eventually do stuff that is beyond ZFC to analyze.
So the finite value 745 isn't really where the infinity/uncomputability comes from-it comes from the infinite tape that can produce arbitrarily complex functions. (I wonder if over a certain number of states it becomes possible to encoding a larger Turing machine in the tape somehow, causing a sort of divergence to infinite complexity?)
In a very real sense, a deep kind of infinite complexity can be generated from 745 objects of certain kind, but not from 5 objects of that kind..
Turing machines have infinite tape, not infinite state. The entire set of all halting machines of a given size collectively only use finite tape. Totally finite. Only (some of) the non-halting machines use infinite tape.
The problem is that we don't know in advance how large the (definitely finite) upper bound on the amount of tape all the size-N halting machines use, until after enough of them (one per known equivalence class) halt. And we don't know (in general) how to run all the halting ones until they halt, without also running a non-halting program for an unbounded amount of time.
TL:DR: unbounded is not infinite, but big enough to be a problem.
But the overall 'complexity' (at a timestep, say) is going to be due to the states and the tape together. The BB(5) example that was analyzed, iirc, was a Collatz-like problem (Aaronson describes it here: https://scottaaronson.blog/?p=8088 ). My interpretation of this is that:
1. collatz-like functions have a lot of complexity just due to math alone 2. 5 states turned out to be enough to "reach" that one that 3. more states means you're going to reach more possible Collatz-like functions (they don't have to be Collatz-like; it's just easier to think about them like that) 4. eventually you reach ones that ZFC cannot show to halt, because there is effectively no way to prove it other than running them, and then you would have to solve the halting problem.
The part that was helpful for me to be less unsettle by BB(745) being independent of the ZFC was the notion that it eventually boils down to a halting problem, and asking ZFC to "solve" it... which is more agreeable than the idea that "ZFC cannot compute a function that seems to be solvable by brute force".
But to me as a layman that seems true regardless of formal axioms chosen, but I guess I need to read that linked thesis.
Incidentally, Gödel's theorem eventually comes down to a halting-like argument as well (well, a diagonal argument). There is a presentation of it that is in like less than one page in terms of the halting problem---all of the Gödel-numbering stuff is essentially an antiquated proof. I remember seeing this in a great paper which I can't find now, but it's also mentioned as an aside in this blog post: https://scottaaronson.blog/?p=710
wait jk I found it: https://arxiv.org/abs/1909.04569
Usually, "what happens" is that the machines become large enough to represent a form of induction too strong for the axioms to 'reason' about. It's a function of the axioms of your theory, and you can add more axioms to stave it off, but of course you can't prove that your new axioms are consistent without even more axioms.
> There is a presentation of it that is in like less than one page in terms of the halting problem---all of the Gödel-numbering stuff is essentially an antiquated proof.
Only insofar as you can put faith into the Church–Turing thesis to sort out all the technicalities of enumerating and verifying proofs. There still must be an encoding, just not the usual Gödel numbering.
> There is a presentation of it that is in like less than one page in terms of the halting problem
Those are two very different ideas. Your second sentence says that Gödel's theorem is easy to prove if you have results about the halting problem. Your first one says that in order to prove Gödel's theorem, you need to establish results about the halting problem.
ZF & ZFC are as important as they are because they're the weakest set theories capable of working as the foundations of mathematics that we've found. We can always add axioms, but taking axioms away & still having a usable theory on which to base mathematics is much more difficult.
> So presumably the independence of a number from ZFC is like that also: you can't prove it's the value of BB(745) because you won't know if you've proved it; the only way to prove it is essentially to run those Turing machines until they stop and you'll never know if you're done.
These aren't similar ideas. You can't know if a machine that hasn't halted yet will ever halt. But you can easily know if a machine that has already halted was going to halt.
Independence is the second case. For the value of BB(x) to be independent of ZFC, one of two things must hold:
(1) ZFC is inconsistent, and therefore all statements are independent of it.
(2) ZFC is consistent with two different statements, "BB(x) = a" and "BB(x) = b" for two different a, b. This means that a disproof of either statement cannot exist.
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.
Neither value, a or b, can be more true than the other as the answer to the question "what is BB(x)?". It doesn't make sense to consider that question to have an answer at all.
> 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".
The interesting bit is they were able to construct a machine that halts if ZFC is consistent. Since a consistent axiomatic system can never prove its own consistency (another famous proof) ZFC can't prove that this machine halts. And ZFC can't prove that it never halts without running it for infinite steps.
That ZFC-consistency-proving machine has 643 states, so BB(643) either halts after the ZFC-consistency-proving machine or the ZFC-consistency-proving machine never halts. If BB(643) halts after the ZFC-consistency-proving machine, then ZFC is consistent and ZFC can't prove BB(643) halts since ZFC can't prove the ZFC-consistency-proving machine halts.