What Is the Point of Decidability
lists.ugent.be
lists.ugent.be
Busy beaver numbers step around this by looking at TMs of one size at a time.
Now, the busy beaver numbers are enormous and we will likely never solve even BB(6). But that’s not for reasons of logical paradoxes like “this sentence is false” or “the smallest positive integer not definable in under sixty letters”.
The reasons we can’t solve small busy beaver numbers:
- There’s an enourmous number of 6-state TMs let alone 100 state TMs.
- BB(6) has been proven to be at least 10^10^10^…^10 (15 times total). So what could BB(20) be.
- some small busy beaver numbers are conjectured to be independent of ZFC, meaning we’d need new math foundations. Conjectured to be BB(20), proven at least as high as BB(745) is independent of ZFC.
- various unsolved math problems are equivalent to TMs of particular sizes: Goldbach’s conjecture, Riemann hypothesis, etc
At least with busy beaver numbers there isn’t some stupid paradox, we just can’t practically solve them.
Also, the enormous size of BB(n) for any particular n is no argument for why it's so hard to determine what BB(n) is. It's actually the other way around. Undecidability sheds light on the enormous sizes of BB(n). Suppose you had a computable function which was known to be an upper bound for BB. Well, then you can play some tricks and leverage it to solve the halting problem by simulating machines for only so many steps before realizing whether you're looking at a halting one or a non-halting one. Therefore, no such upper bound function exists. Therefore, you can write down the fastest growing computable function you can think of, and BB will outpace it.
Ex: we already know BB(745) is independent of ZFC, any more powerful system should have its own independence limit, etc.
source: page 6 here https://www.scottaaronson.com/papers/bb.pdf
Since BB computing code is halting problem solving code, it goes back to my point about “one finite program to solve halting for countably infinitely many TMs and inputs” seeming intractable compression-wise. On the contrary, maybe countably many BB computing programs for each countably many BB number would be doable.
It absolutely means that, unless you don't believe the Church-Turing thesis and claim that humans have the ability to carry out computations that machines physically cannot.
I think you are misunderstanding the difference between having an algorithm to determine BB(n) for all n, and figuring out what BB(n) is for certain special n.
This doesn’t seem computable, yet we can definitely figure out its values.
Anyways, I believe my point above is in alignment with Scott Aaronson, so if you’ve read that I’m curious what you think the differences are.
Even if we supposed that, for every n, there was some reasonable
extension of ZF set theory that was powerful enough to settle the
value of BB(n) — even so, there could be no systematic way to find
those extensions.
It's definitely an interesting way to frame things. But imo the halting-problem insights still seem more naturally applicable to typical related issues in computer science and engineering. How do you prefer BB(n), when does it ever come up? Honestly curious. Appreciated the link.
No, the idea of incalculable simply means that it can’t be enumerated using one program. As humans we can write different programs and it’s fine.
Imagine code which exhaustively checks all math proofs. That code will have an axiomatic system built into it such as ZFC. This says that that code still can’t calculate busy beaver numbers at a point, because at a certain point ZFC is no longer enough. But if we had similar code with some ordinal stuff thrown in, maybe we could get a little farther. Etc.
Practically, undecidability and busy beaver numbers are both very, very untenable. I always had a philosophical objection to undecidability, it felt wrong that knowledge was limited in theory because of “this sentence is false” logical tricks. Practically, who cares if we can’t prove “this sentence is false”. (Turings undecidability argument is a halt program encoding of this sentence is false.)
I wanted a different more satisfying answer, and busy beaver numbers are that answer: math is unfathomably complicated, and we don’t have powerful enough axiomatic systems to understand even small computer programs yet.
At a certain point it just becomes a mess. No process can keep up. In general most logical systems (all of them become relevant as n grows) are completely random, with no characteristic structure.
I'm getting frustrated reading your comments. LLMs show that human beings are likely to themselves admit simulations by computer programs. So computability limits apply to human beings as much as to computers. I've never seen anyone misunderstand these topics in quite the way you have.
> I wanted a different more satisfying answer, and busy beaver numbers are that answer
Listen, you're wrong. This entire thread you've started is wrong. The Busy Beaver function is uncomputable precisely because the Halting problem is unsolvable -- that's how you prove it. It provides no additional insight into "undecidability" except for a bunch of misunderstandings you have that other people have been trying to point out to you.
Thinking in terms of concrete machines is great. The work on Abstraction Logic has made me a Platonist in a Goedel way as well. I insist that the mathematical universe is real: there are mathematical objects, and they have their own independent, real existence. If you admit that 1 and 2 and 3 are real, then it is difficult to argue that Turing Machines are not real, and of course the models of consistent theories are real as well.
In fact, I would go as far as saying, if you are not a Platonist, then good luck making any kind of argument for correct reasoning.
I think you're going down the wrong path re "uncomputable". BB(n) is easily computable, just write a little program that enumerates (generates) and runs all n-state BB machines. BB(n) is the largest lifetime of any those n-state machines. BB(n) is known and easily computable for small n.
The problem is that the number of machines increases very quickly with n, and the time taken to evaluate each machine often increases quickly with n. So for even moderate n, it is completely impractical to brute-force compute BB(n). But impractical is not uncomputable.
Just because you don't wait to wait past the heat-death of the universe, doesn't mean that you wouldn't have got an answer eventually. And eventually = computable.
Running all n-state machines won't work, because you may have some machines that continue indefinitely, but without repeating. (Remember that while the number of states is finite, the tape is infinite.) No matter how long you run them for, you can't be sure whether they are going to terminate at some point in the future, or if they'll continue forever without halting.
This is why computing BB(n) for arbitrary n is equivalent to solving the halting problem.
Te winning strategy is to A) prove all the machines that don’t halt and B) find the largest runtime of machines that do halt.
That’s why BB(745) is important because we can’t use ZFC to prove A for BB(745), even if we could run all the halting machines to find BB(745).
Busy beaver problems are interesting in their own right, particularly for 1) demonstrating the huge amount of complexity that can arise from very simple rules and 2) for the epiphany that a busy beaver function grows asymptotically faster than any computable. But I don't find them to be great as an introduction to undecidability.
Every proof for undecidability use hypothetical TM constructions with a logical property and a trick. Busy beaver numbers are concrete.
Anyway, the point is that the halting procedure in its full generality cannot exist, while each individual busy beaver number can be solved in theory (even if there’s no algorithm that can list them all).
In other words, busy beaver numbers admit countably many theoretically tractable sub problems. It’s in a way the most natural way to break the halting problem down into tractable pieces.
I don't understand this point at all. Busy beaver lets you solve halting and vice-versa. If there are some special cases in which you can solve busy beaver then you can use them to solve halting.
Each individual busy beaver number can't be solved in theory for the same reason that the halting problem can't - if you try to check all n-state Turing machines to compute BB(n) some of them won't halt, and some of those you won't be able to prove that they don't halt.
Source? AFAIK we aren’t aware of any TMs which are impossible to prove loops forever. Turing’s proof only applies to finite halting code that works for arbitrary TMs and inputs. There will never be a solution for every busy beaver number for that reason. However I suspect for ex the program to compute BB(6) to be much larger than 6 states, (even just to print the number) so turings diagonalozation argument doesn’t fit.
There are explicitly known Turing machines which it is impossible to prove their whether or not they halt within ZFC. You could argue that you can construct a stronger logical system within which it is possible to prove one of these machines halts, the problem is that you can never be sure your stronger system is consistent. If you manage to come up with a proof within some stronger system that the machine halts, it may also be possible to come up with a proof that it does not halt (if the system is inconsistent).
I’m not so worried about consistency. Even ZFC has the issue you describe. I found this paragraph from Wikipedia about Gödels 2nd incompleteness theorem very interesting.
> The corollary also indicates the epistemological relevance of the second incompleteness theorem. It would actually provide no interesting information if a system F proved its consistency. This is because inconsistent theories prove everything, including their consistency. Thus a consistency proof of F in F would give us no clue as to whether F really is consistent; no doubts about the consistency of F would be resolved by such a consistency proof. The interest in consistency proofs lies in the possibility of proving the consistency of a system F in some system F' that is in some sense less doubtful than F itself, for example weaker than F. For many naturally occurring theories F and F', such as F = Zermelo–Fraenkel set theory and F' = primitive recursive arithmetic, the consistency of F' is provable in F, and thus F' cannot prove the consistency of F by the above corollary of the second incompleteness theorem.
It's possible to prove the values of certain busy beaver numbers, of course, but that's equivalent to noting that you can prove whether certain TMs halt. For example, it is possible to run every n-state TM long enough that, for each TM, you've either observed it halt or you've proved that it's in an infinite loop. The problem is that, for any TM that you haven't observed halt and you haven't been able to prove it's in an infinite loop, you just gotta keep waiting until one or the other happens. And, critically, you can't know if you'll ever come up with a proof that it's in an infinite loop.
Another interesting thought is whether we can prove the limit of say ZFC in busy beaver numbers with just ZFC. We have BB(745) limit for ZFC. It would be fascinating if “BB(20) is independent of ZFC” turns out to be independent of ZFC as well.
It's not that there is necessarily any particular TM that you can't prove halts or doesn't halt. It's that you can't develop a TM that can prove, for each and every TMs, whether they halt.
Ex: no reason yet in theory why we can’t solve and list the first 100k busy beaver numbers or 200k, covering many practical uses for halting problem. But there’s always a limit, we can’t compress the infinite list of values into some code to generate them.
(In theory.. we may never solve BB(6), but that’s not because of undecidability at all.)
function BB(k) {
if (k === 6) return n;
}
The fact that BB(745) is undecidable in ZFC doesn't mean that it will stay unknown forever. But we will have to come up with some other mathematical explanation than ZFC to know BB(745), and nobody knows if such an explanation exists. It could also be that you come up with such an explanation, but many others don't agree with it. Now, on which grounds would you defend your explanation?
But I am a Platonist, so I do agree with you that there is some sort of mathematical explanation for BB(745) = n for some n formulated in a suitable mathematical theory. Because obviously, such an n must exist. Because TMs are real, and they either halt or they don't (Platonist leap of faith I). And then there must be a way to explain why that is (Platonist leap of faith II). But it may be that we never find such an explanation, and/or that humans are too limited to understand the explanation. Certainly, there is no known general algorithm to find human-understandable answers to all human-understandable mathematical questions, and that's why undecidability is the reason we may never know BB(6).
In jest. If I am lacking a source of heat, the reason for my being unable to cook food isn't my lack of Superman heat vision eye laser beams. Similarly, the fact that we can never skip all of math with one finite algorithm isn't the reason why we can't discover BB(6).
In any case, at a Platonic level there is no such algorithm, so us lacking it can't be the reason why we can't solve BB(6). In a way it's even less realistic than Superman heat vision eye laser beams.
Can you clarify what you mean by this? You prefer one to the other in what circumstances?
> Now, the busy beaver numbers are enormous and we will likely never solve even BB(6). But that’s not for reasons of logical paradoxes like “this sentence is false” or “the smallest positive integer not definable in under sixty letters”.
Also please clarify this. BB is hard to compute because it is essentially defined in terms of solving the halting problem (that's known to be pretty hard). You alluded to a proof of that fact. What is your point? And what is your problem with those kinds of proofs? What do BBs have to do with undecidability besides being directly defined in terms of an undecidable operation?
Whereas the halting problem is known to be unsolvable.
I just prefer things that are solvable in theory to things that aren’t.
There is no known reason why we can't tell if any specific program halts. We just can't write code to tell if an arbitrary program halts. This result is exactly what you are using when talking about preferring BB(k) for some fixed k, each k requires solving a bunch of halting problems. The paradox proofs you seem to dislike are only needed for the general case, the general halting problem or, and this is to me the confusing part, the general BB(n). So you are comparing BB(k) for some fixed k to something infinitely more general in the general halting problem. So, again, why would you compare these two things? When is that a useful thing to do?
No! In computability theory we work with Turing Machines that have unlimited memory. Since they have unlimited memory, the sizes of individual busy beaver numbers are not the problem. Individual busy beaver numbers are in fact all computable because every integer is computable. What is uncomputable is the busy beaver function. The busy beaver function is uncomputable because of the halting problem -- I suggest finding or reading a proof. Therefore the BB function provides zero additional insight into undecidability.
I'm also amazed that there are people on this technology website - like you - who see all of this progress happening in AI with programs that are close to human intelligence, and still think that human beings can do things like determine arbitrarily large busy beaver numbers. We have concrete evidence that human beings are themselves limited by computability. People cannot just write arbitrarily good programs (to determine the first n busy beaver number, let's say) because people are programs.
Here is a quick sketch of a proof:
Assume we have a machine (or algorithm) which we input a description of a Turing machine and it tells us whether or not it halts. Then to find the nth busy beaver you
1. Enumerate all n state Turing machines
2. In a "for loop" ask your machine whether each n-state Turing machine halts
3. For the ones that halt, run each of them until they halt and write down how many steps it took
4. The largest of these numbers is the busy beaver number BB(n)
Similarly lets say you have a machine (or algorithm) which tells you BB(n), you can solve the Halting problem like this
1. Run the Turing machine until it has completed BB(n) steps
2. Remember that if an n-state Turing machine hasn't halted in BB(n) steps then it will never halt
3. If it hasn't halted after BB(n) steps then it won't ever halt so you've solved the halting problem
Busy beaver and Halting are (from the point of view of decidability) exactly the same thing.
> And there are still cases going on today where undecidability results are of broad interest to those outside of logic. For example, the "spectral gap problem" in physics asked whether, given a description of a physical system, whether that system requires a minimum amount of energy to nudge it out of its ground state, or whether arbitrarily small amounts of energy can nudge it out of its ground state. This was proven to be undecidable in 2015, basically telling physicists that a theoretical problem of theirs, motivated entirely by physical considerations, is hopeless in full generality.
Well that sucks.[1] But I think it's cool that theoretical physics and theoretical computer science seem to meet together in these low places. Information has thermodynamic consequences and vice versa.
[1]: Where practical is in the sense of an engineer (or in their terms, a CS practitioner), not a theoretician. Most of the responders seem to interpret practical in the sense of a mathematician.
very astute observation. Now I'm left wondering how this comes to be?
what is it about the way in which a general CS practitioner's approach to problem solving that grounds the potential ideas (of how to solve problem) into the computationally decidable?
Configuration processing. E.g. I'd like my yamls to be decidable, though I'll settle for guaranteed to halt[1].
I don’t think I agree! For example, I strongly suspect that Malware detection researchers would be following many fruitless paths in the vein of “Let’s just figure out what the program is doing” if not guided by the fact that this is strictly harder than “Let’s just figure out if the program halts.”
https://googleprojectzero.blogspot.com/2021/12/a-deep-dive-i...
"JBIG2 doesn't have scripting capabilities, but when combined with a vulnerability, it does have the ability to emulate circuits of arbitrary logic gates operating on arbitrary memory. So why not just use that to build your own computer architecture and script that!? That's exactly what this exploit does. Using over 70,000 segment commands defining logical bit operations, they define a small computer architecture with features such as registers and a full 64-bit adder and comparator which they use to search memory and perform arithmetic operations. It's not as fast as Javascript, but it's fundamentally computationally equivalent.
The bootstrapping operations for the sandbox escape exploit are written to run on this logic circuit and the whole thing runs in this weird, emulated environment created out of a single decompression pass through a JBIG2 stream. It's pretty incredible, and at the same time, pretty terrifying."
1 billion dollars later: We discovered we can't do X because there's this thing called "undecidability."
Undecidability puts fundamental limits on what we can do with computers. You can't even do simple things like write a program which can { determine if two programs are equal, determine if two programs would have equal outputs given any input, if any program will return a "1", if any program would halt, ... }
This feels kinda important considering what people might try to build using AI.
https://www.digitalonus.com/the-origins-of-functional-progra...