You can convert every atom of observable Universe into a substrate for supercomputer, you can harness energies of supermassive black holes to power it, but running a humble BB(6) to halting state would be forever out of its reach.
BusyBeaver(6) Is Quite Large
81–90 of 232 posts
Re: BusyBeaver(6) Is Quite Large
#82Earlier quoted context omitted.
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.
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.
Re: BusyBeaver(6) Is Quite Large
#83Earlier quoted context omitted.
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.
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 r…
> 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.
Re: BusyBeaver(6) Is Quite Large
#84So what is the richest logic whose proofs can be enumerated with only a five state TM?
Re: BusyBeaver(6) Is Quite Large
#85Earlier quoted context omitted.
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.
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.
Re: BusyBeaver(6) Is Quite Large
#86Earlier quoted context omitted.
No, that's one of the freakiest things about things like the Busy Beaver function. There is an exact integer that BB(748) defines. You can add one to it and then it would no longer be that number anymore. If you are refering to the idea that nothing that can't exist in the real universe "really exists", then the "Busy Beaver" portion of that idea is extraneous, as 100% of integers can't exist in the real universe, an…
This integer only exists if you assume classical logic. Otherwise, there is no such integer a priori, and actually there is none in general.
For that to be the case, there would have to be some symbol under the tape and some state the machine is in for which the action the machine takes and the next state it goes to would depend on the axioms taken somehow. There is no place where the Turing Machine has somehow been running for so long and just gotten so large that its behavior becomes non-deterministic somehow.
What this means is that even if we lived in a universe where we had the unfathomable resources to actually have this number somehow meaningfully "in hand", we would be unable to prove that it was the correct one with just ZFC. Maybe one of the really quite numerous other machines still spinning away would in fact terminate in the future and be the real BB winner, because even this staggeringly monstrously large universe is still piddling nothing next to infinity and the other machines still require infinite resources to run them to discover they never terminate. But that doesn't do anything to affect whether or not there in fact is a single concrete integer that corresponds to BB(748).
Although one imagines that any universe with the resources to "have" BB(748) in it might also have some much more powerful axiom systems to play with in the process. The amount of computational power this universe apparently possesses is beyond all comprehension and who knows what they could know. But even if they used a more powerful system, it wouldn't change what BB(748) is... it just might affect whether or not they were correct about it.
Re: BusyBeaver(6) Is Quite Large
#87It's known that BB(14) is bigger than Graham's number, but this new finding leads me to believe that BB(7) is probably bigger than Graham's number. Intuitively, the technology required to go from pentation to Graham's number feels simpler than the technology required to go from `47,176,870` to `2 5`.
Re: BusyBeaver(6) Is Quite Large
#88Any time I see such results from computation complexity theory, I realize that any current zeitgeist of "super-intelligent AI are gods" is complete bullshit. You can convert every atom of observable Universe into a substrate for supercomputer, you can harness energies of supermassive black holes to power it, but running a humble BB(6) to halting state would be forever out of its reach.
Re: BusyBeaver(6) Is Quite Large
#89Earlier quoted context omitted.
It boggles my mind that we ever thought a small amount of text that fits comfortably on a napkin (the axioms of ZFC) would ever be “good enough” to capture the arithmetic truths or approximate those aspects of physical reality that are primarily relevant to the endeavors of humanity. That the behavior of a six state Turing machine might be unpredictable via a few lines of text does not surprise me in the slightest. A…
Within ZFC one can prove that any two models of second order PA are isomorphic. ZFC proves that PA is consistent. ZFC is good enough to capture arithmetical truth.
https://jdh.hamkins.org/the-universal-algorithm-a-new-simple...
Re: BusyBeaver(6) Is Quite Large
#90Earlier quoted context omitted.
It boggles my mind that we ever thought a small amount of text that fits comfortably on a napkin (the axioms of ZFC) would ever be “good enough” to capture the arithmetic truths or approximate those aspects of physical reality that are primarily relevant to the endeavors of humanity. That the behavior of a six state Turing machine might be unpredictable via a few lines of text does not surprise me in the slightest. A…
This ignores the fact that it is not so easy to find natural interesting statements that are independent of ZFC. Statements that are independent of ZFC are a dime a dozen when doing foundations of mathematics, but they're not so common in many other areas of math. Harvey Friedman has done interesting work on finding "natural" statements that are independent of ZFC, but there's dispute about how natural they are. http…
> This ignores the fact that it is not so easy to find natural interesting statements that are independent of ZFC.
I’m not ignoring this fact—just observing that the sheer difficulty of the task seems to have encouraged mathematicians to pursue other areas of work beside foundational topics, which is a bit unfortunate in my opinion.