[SAI_Peregrinus]

Independence from ZFC means we can't prove that any given number is BB(643) using ZFC. It doesn't mean we can't prove it at all, e.g. one could use a stronger set theory like NBG which can prove the consistency of ZFC to verify the value of BB(643). But there would be some n for which BB(n) is independent of that set theory, requiring a yet-stronger theory, and so on ad infinitum.

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.

[ajkjk]

sure, but it is still very hard to wrap one's head around how the value of a function can be independent of ZFC, and how it could not be for (e.g.) 642 but then be true for 643. That was the point of my post. It seems like you could just... run the function on every 643-state input and see what the value is, which would in some sense constitute a "proof" in ZFC? but maybe not, because you wouldn't even know if you had the answer? That's the part that is so intriguing about it.

[SAI_Peregrinus]

Some 643-state inputs never halt. Some 643-state inputs do eventually halt. Only if you can run them for infinite time can you determine whether a given machine halts in a finite length of time: for any finite time you pick, if the machine is still running it could still halt eventually. That's just the halting problem, the impossibility of solving it is quite famous and it's easy to find the proof stated more formally than I want to with the limits of HN's markdown.

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.

[Straw]

Don't you want the weakest (ie makes the fewest assumptions) theory that works?

[SAI_Peregrinus]

Yes, which is why ZFC gets used. NBG & MK are stronger and occasionally used, but ZFC being weaker meant it got more popular since it's almost always good enough.