[dtech]

I am also not an expert, but this does not sound right to me. Godel's incompleteness theorem shows that there are certain things that cannot be proven. Being independent of ZFC means that something is such a case. So BB(643) being independent of ZFC means that we cannot prove or disprove that a certain number is BB(643). Aka we don't have the math to know for certain.

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

[ajkjk]

Yeah, but the vexing part is "how can that be true for e.g. N=643 but not N=642"? What happens at whatever number it starts true at?

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

[LegionMammal978]

> What happens at whatever number it starts true at?

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.

[thaumasiotes]

> 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

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.

[ajkjk]

I'm saying that if you want to understand why Gödel's theorem is true, look at the one-paragraph proof based on the halting problem, not the like 20-page one with Gödel numbers.

[wasabi991011]

Wow that might be the best, most entertaining, and most elucidating academic article I've ever read. Thanks for sharing.