The Smallest Non-Computable Busy Beaver Number: Is it Knowable?

[johnkclark]

We know for sure the first four Busy Beaver numbers exist are finite and are computable because they have in fact been computed, they are 1,6,21 and 107. And we know for sure that the 7918th Busy Beaver number exists and is finite but is NOT computable thanks to the work of Scot Aaronson, but it would be really nice if that gap between 4 and 7918 could be narrowed. I'd really like to know what the smallest non computable Busy Beaver number is, but even that may be non computable. Does anybody know?

John K Clark

 

[jedishrfu]

Here's some background for other posters:

https://en.wikipedia.org/wiki/Busy_beaver

and from Computerphile:

 

[SSequence]

We know for sure the first four Busy Beaver numbers exist are finite and are computable because they have in fact been computed, they are 1,6,21 and 107. And we know for sure that the 7918th Busy Beaver number exists and is finite but is NOT computable

You may have some confusion here. It doesn't have much meaning to say that a given number (or for that matter a given finite list of numbers) is computable or not.
On that other hand, if that means talking about a "constant function" say a function f:ℕ→ℕ where f(x)=c for all x (here c is a constant), then ofc it is always computable.

The more precise claim is different. I believe other members well-versed in logic can comment better on this, but the basic idea is not difficult to understand. Anyway here are the relevant links I think:
https://www.scottaaronson.com/busybeaver.pdf
https://www.scottaaronson.com/blog/?p=2725
https://www.scottaaronson.com/blog/?p=2741 (see second heading)

 

[johnkclark]

Why wouldn’t it be meaningful to say a Real Number is not computable if no finite algorithm exists that can approximate it with arbitrary precision?

John K Clark

 

[SSequence]

I was just talking about natural numbers (since this is the domain and co-domain of the function in question).

 

[johnkclark]

The 7918th Busy Beaver number is huge but it’s finite and a natural number, but Scot Aaronson proved it is not computable, no algorithm can find it. I wanted to know if its possible to find the smallest non-computable Busy Beaver number or is that non-computable too. I wouldn’t be very surprise if just the fifth Busy Beaver is not computable but I don’t know that for a fact.John K Clark

 

[SSequence]

The 7918th Busy Beaver number is huge but it’s finite and a natural number, but Scot Aaronson proved it is not computable, no algorithm can find it. I wanted to know if its possible to find the smallest non-computable Busy Beaver number or is that non-computable too. I wouldn’t be very surprise if just the fifth Busy Beaver is not computable but I don’t know that for a fact.John K Clark

No it is different from this. See the first half of post#3.

Here is the basic idea ... every reasonable "reasoning system" (assuming it is sound) is going to prove that certain programs (on blank input) do not halt. However, because of incompleteness, it will fail to prove all instances of non-halting.
If one looks at the size of smallest instance (in terms of program size) where the instance of non-halting isn't proved, this is the smallest value (of the function $BB$) that the "reasoning system" simply can't tell much about.

The given results place an upperbound on this value. So yes, there is a highly likely possibility of getting a better (more strict) upperbound by getting a smaller value.

Now one could exploit the fact (w.r.t. reasoning systems based on FOL and furthermore satisfying the conditions for incompleteness theorems I think) that a given reasoning system S can't prove its own consistency and then simply try to build a program which halts iff the system is inconsistent. Proving the non-halting of this program would prove that S is consistent, so by second incompleteness theorem S can't prove the non-halting of this program. Hence the corresponding $BB$ entry (and hence basically all greater values) is also beyond the given system S.
However, it isn't necessary to just look for consistency statements of course.

============================

However, the existence or non-existence of the function $BB$ as a valid mathematical function is a deep question and isn't suitable for this thread.

 

[TeethWhitener]

The 7918th Busy Beaver number is huge but it’s finite and a natural number, but Scot Aaronson proved it is not computable, no algorithm can find it. I wanted to know if its possible to find the smallest non-computable Busy Beaver number or is that non-computable too. I wouldn’t be very surprise if just the fifth Busy Beaver is not computable but I don’t know that for a fact.John K Clark

No, Aaronson and Yedidia showed that the value of the 7918th Busy Beaver number can not be proven from within Zermelo-Frankel set theory (+ Choice) assuming ZFC is consistent. This is equivalent to saying that the question "Is x = BB(7918)?" is independent of ZFC. With stronger axioms, this question can be answered (at least in principle). In fact, the way the proof works is to construct a (7918-state) Turing machine that asks a question about a certain large cardinal property that is independent of ZFC. (In this context, "independent" means "cannot be proven either true or false within a given axiomatic system.")

As @SSequence 's link points out in post 3, Stefan O'Rear has gotten the number down from 7918 to 1919 by modifying the language that compiles down to the Turing machine. I don't know if any progress has been made since then. Decreasing this number further would require finding more efficient ways to encode the independence statement, but Aaronson suggests on his blog that lowering this number to its minimum would require drastically rethinking the problem. Increasing the lower bound would presumably require brute-forcing your way through increasingly complex Turing machines.

 

[SSequence]

This is equivalent to saying that the question "Is x = BB(7918)?" is independent of ZFC. With stronger axioms, this question can be answered (at least in principle). In fact, the way the proof works is to construct a (7918-state) Turing machine that asks a question about a certain large cardinal property that is independent of ZFC. (In this context, "independent" means "cannot be proven either true or false within a given axiomatic system.")

Well I shouldn't probably nitpick ... since my own posts are often very incomplete (and probably often contain some inaccuracies when talking about logic related stuff) ...

However, I think it might be better to say:
"With stronger axioms, this question may possibly be answered (at least in principle)."
Because, as far as I can guess/understand, even if one assumes that adding stronger axioms (currently known ones) everything proved is sound ... it doesn't tell us much about what is the smallest value (of $BB$) that will elude "given system+stronger axioms".

... Increasing the lower bound would presumably require brute-forcing your way through increasingly complex Turing machines.

Well 'assuming' that maths (relevant to number theory one way or other) gets more advanced (and assuming it is sound at least as far its consequences for number theory are concerned), the lower bound can be increased then.

 

[johnkclark]

Regardless of what reasoning system is used a given Turing Machine will either halt or it won’t, so the Busy Beaver number always exists, the question is if we can ever know what it is. We know for sure that BB(5) is at least 47,176,870 because one 5 state Turing Machine has been found that halts after it goes through 47,176,870 operations (and prints 4098 1’s on the tape), but there are 28 other 5 state machines displaying non-regular behavior that are well past 47,176,870. If one of them eventually halts then that larger number of operations will be BB(5), if none of them ever stops then 47,176,870 really is BB(5); but the trouble is we'll never be able to know it’s 47,176,870 because we'll never know than that none of those other 28 5 state machines will ever stop.

It could be that in the coming years we’ll notice that all 28 eventually stop then we will know for sure what BB(5) is, whatever program took the longest to halt; but Aaronson prove that could never happen for BB(7918). I’d love to know what the largest computable BB number is, it might be BB(4) but its certainly less than BB(7918).

John K Clark

 

[johnkclark]

I agree that with stronger axioms the question could be answered, but could it be correctly answered? Most people are pretty confident that ZFC is consistent, me too, but if more axioms are added my confidence drops fast. If a Turing Machine is connected to a bomb that will go off if it ever halts and ZFC says it will never halt I wouldn't mind sitting next to it, but if ZFC+X says it will never halt I'm running for the hills.

John K Clark

 

[SSequence]

... Most people are pretty confident that ZFC is consistent ... If a Turing Machine is connected to a bomb that will go off if it ever halts and ZFC says it will never halt I wouldn't mind sitting next to it

Consistency of a system doesn't imply soundness (even for arithmetic statements), since its conceivable that a system is consistent and yet is wrong about truth value of arithmetic statements.

Of possible interest: https://arxiv.org/abs/0905.1680
More specifically see the second point "Anti-platonist defenses of ZFC".
This specific part (from linked essay) also seems to summarise the point:
"It is important to recognize that the legitimacy of ZFC as a foundational system involves more than its mere alleged consistency. If it is to be taken as the rightful foundation of mathematics we should at the very least have good reasons for believing it is Σ₁-valid. Yet “soft” justifications of ZFC which merely aim to show that it is consistent or pleasing in some way do not speak to this question."

 

[johnkclark]

That was an interesting link, thanks. But if a "much weaker system” than ZFC is good enough for "virtually all mainstream mathematics” and if ZFC can’t determine what BB(7918) is then a much weaker system certainly can’t either. That just gives me more confidence that Aaronson was correct when he said BB(7918) will never be known.

John K Clark

 

[TeethWhitener]

Well I shouldn't probably nitpick ... since my own posts are often very incomplete (and probably often contain some inaccuracies when talking about logic related stuff) ...

However, I think it might be better to say:
"With stronger axioms, this question may possibly be answered (at least in principle)."
Because, as far as I can guess/understand, even if one assumes that adding stronger axioms (currently known ones) everything proved is sound ... it doesn't tell us much about what is the smallest value (of $BB$) that will elude "given system+stronger axioms".

The question I was referring to is “Does x = BB(7918)?” The 7918-state Turing machine in the paper doesn’t halt, assuming SRP. But it can’t be proven to halt in ZFC.

Well 'assuming' that maths (relevant to number theory one way or other) gets more advanced (and assuming it is sound at least as far its consequences for number theory are concerned), the lower bound can be increased then.

I have no idea what this means.

I agree that with stronger axioms the question could be answered, but could it be correctly answered? Most people are pretty confident that ZFC is consistent, me too, but if more axioms are added my confidence drops fast. If a Turing Machine is connected to a bomb that will go off if it ever halts and ZFC says it will never halt I wouldn't mind sitting next to it, but if ZFC+X says it will never halt I'm running for the hills.

John K Clark

Why? ZFC can only be proven consistent within the framework of ZFC + X, per Godel.

That was an interesting link, thanks. But if a "much weaker system” than ZFC is good enough for "virtually all mainstream mathematics” and if ZFC can’t determine what BB(7918) is then a much weaker system certainly can’t either. That just gives me more confidence that Aaronson was correct when he said BB(7918) will never be known.

John K Clark

This is not what Aaronson said. He said that it is not possible to answer the question “what is BB(7918)” within ZFC. Simply based on practicality, it’s unlikely BB(10) will ever be known, even if it is provable in principle within ZFC.

 

[stevendaryl]

I agree that with stronger axioms the question could be answered, but could it be correctly answered? Most people are pretty confident that ZFC is consistent, me too, but if more axioms are added my confidence drops fast. If a Turing Machine is connected to a bomb that will go off if it ever halts and ZFC says it will never halt I wouldn't mind sitting next to it, but if ZFC+X says it will never halt I'm running for the hills.

John K Clark

Adding more axioms doesn't necessarily weaken the faith in a system. The most obvious example is consistency: There is a sentence, Con(ZFC), which is not provable by ZFC (if ZFC is consistent), but if you already believe that ZFC is a good system for doing mathematical reasoning, then of course you should also be willing to believe Con(ZFC).

So there is an infinite hierarchy of theories all of which are equally believable:

• ZFC
• ZFC + Con(ZFC)
• ZFC + Con(ZFC) + Con(ZFC + Con(ZFC))
• etc.

 

[SSequence]

The question I was referring to is “Does x = BB(7918)?” The 7918-state Turing machine in the paper doesn’t halt, assuming SRP. But it can’t be proven to halt in ZFC.

I was just making the simple point that was that if a given system S can't answer the value of say $BB(7918)$, then it doesn't mean that "S+some stronger axioms" will be able to give that answer. Because, of course, to answer that one needs to identify the non-halting of all programs of size 7918 (and not just a few of them).

==============

It seems that two variations of this would probably be interesting:
(1) Choose a slightly more direct programming language. As one example (probably PL knowledgeable people could think of many), a language with simple addition (by 1) and subtraction (by 1) commands and a basic control structure. Then the number of lines could be counted (number of characters would ofc also work but number of lines seems better in this case).

(2) Some bounds for this question for, say, PA?

 

[stevendaryl]

I was just making the simple point that was that if a given system S can't answer the value of say $BB(7918)$, then it doesn't mean that "S+some stronger axioms" will be able to give that answer. Because, of course, to answer that one needs to identify the non-halting of all programs of size 7918 (and not just a few of them).

Yes, for the Busy-Beaver problem. Very good point.

When you go to a stronger theory, you can decide more instances of the halting problem, but the new ones that you decide don't typically come in order of their size. So if we define a "busy-beaver strength" of a theory T, $bbs(T)$ to be the largest number $n$ such that $T$ decides the halting problem for all Turing machines of size $n$ or less, than $bbs(T)$ grows extremely slowly as you move to more and more powerful theories. It might not budge at all in moving from Peano Arithmetic to ZFC.

 

[johnkclark]

An axiom should be as simple and self evidently true as possible and Con(ZFC) is certainly not simple, and although I think its probably true it would be pushing it to say the truth of it was self evident. Con(ZFC) is just the claim that ZFC is consistent, sticking that in as an axiom does not increase my confidence that ZFC really is consistent, just as the presadent saying “I am not lying” does not increase my confidence that he really is not lying. And besides, just adding one Con statement does not solve the basic problem, you’d need a infinite number of iterated ones and logical systems should only have a finite number of axioms, or at least they should in my opinion.

If I knew of something so simple and self evidently true that adding it as an axiom would not degrade my confidence that ZFC is consistent but would increase its completeness by allowing me to prove or disprove the continuum hypothesis for example then I’d be all for it, but I don’t think anything like that exists, if it did we’d have found it by now because it is so simple. So Aaronson’s statement "it is not possible to answer the question “what is BB(7918)” within ZFC” is equivalent to the statement “it is not possible to correctly answer the question “what is BB(7918)” period”.

John K Clark

 

[johnkclark]

I agree that if we add some stronger axiom to ZFC the question "what is BB(7918)?” can be answered, for example it can be answered in the system ZFC+X if X is “BB(7918) = 42”. But I don’t just want answers, I want correct answers.

John K Clark

 

[stevendaryl]

An axiom should be as simple and self evidently true as possible and Con(ZFC) is certainly not simple, and although I think its probably true it would be pushing it to say the truth of it was self evident. Con(ZFC) is just the claim that ZFC is consistent, sticking that in as an axiom does not increase my confidence that ZFC really is consistent

Of course it doesn't. But if you already believe that ZFC is consistent, then why not assume Con(ZFC) when doing a proof? Adding Con(ZFC) gives additional proving power, but doesn't cost anything, as far as increasing your doubt in the truth of the theorems.

 

[johnkclark]

I don’t see what additional power adding Con(ZFC) would bring other than being able to prove the consistency of ZFC, and if it solved that problem it would immediately create another one that is too obvious to point out; it certainly wouldn’t help in figuring out what large but finite number BB(7918) is. Proof is not the same as truth, a proof is only as good as the axioms its built on so we should be super conservative about adding new ones.

John K Clark

 

[stevendaryl]

I don’t see what additional power adding Con(ZFC) would bring other than being able to prove the consistency of ZFC.

Well, proving Con(ZFC) means that you can decide more instances of the halting problem than if you can't prove Con(ZFC). In particular, you can prove that a Turing machine that searches for a proof of a contradiction from the axioms of ZFC will never halt. You can't prove that with just ZFC.

Proof is not the same as truth, a proof is only as good as the axioms its built on so we should be super conservative about adding new ones.

If a theory $T$ proves that a Turing machine doesn't halt on some particular input, then there are two possibilities:

1. It is true that it doesn't halt on that input.
2. The theory $T$ is inconsistent.

So in general, truth is not the same as provability, but for consistent theories, proofs about the halting problem are the same as truth. And ZFC + Con(ZFC) proves more true statements than ZFC alone. (Assuming that both are consistent)

...it certainly wouldn’t help in figuring out what large but finite number BB(7918) is.

That might be a good way to bet, but there is no definitive proof of that. ZFC + Con(ZFC) can correctly decide more instances of the halting problem than ZFC alone. Whether it can decide all of the ones with size less than or equal to 7918 seems unlikely, but it's not a priori impossible.

 

[stevendaryl]

That might be a good way to bet, but there is no definitive proof of that. ZFC + Con(ZFC) can correctly decide more instances of the halting problem than ZFC alone. Whether it can decide all of the ones with size less than or equal to 7918 seems unlikely, but it's not a priori impossible.

Actually, now that I think about it, it's not possible for ZFC + Con(ZFC) to solve BB(7918), for the following reason: The Turing machine that searches for a proof of an inconsistency in ZFC + Con(ZFC) would have size less than 7918. So solving BB(7918) would involve proving that ZFC + Con(ZFC) is consistent.

However, we could iterate the process, and create a theory that is

T = ZFC + Con(ZFC) + Con(ZFC + Con(ZFC)) + ...

If the resulting theory has billions and billions of axioms, then it's possible that the Turing machine that checks for the consistency of that theory would have a size greater than 7918. That being the case, I can't see any definitive argument that T does not solve the question of BB(7918).

 

[johnkclark]

You can't get something from nothing and when you add Con(ZFC) to ZFC you're really adding nothing, all you're doing is saying ZFC is consistent without any evidence to back it up . A critic could simply say "oh yeah, says you!". I don't see the point of having a proof if it can't be trusted, it should tell you something new about the nature of reality and a proof with axioms that are not even built on sand but on vapor can't do that because it can't be trusted. Adding billions of axioms won't help, even adding a infinite number won't help because the Busy Beaver function grows faster than exponentially, it grows faster than iterated exponentiation, it even grows faster than Ackermann's function, it grows faster than ANY computable function . You're never going to get ahead of it. And never mind BB(7918), I wouldn't be one bit surprised if BB(5) was not computable either.

John K Clark

 

[stevendaryl]

You can't get something from nothing and when you add Con(ZFC) to ZFC you're really adding nothing.

That's just not true. I gave you the example of a Turing machine that searches for a proof of a contradiction from the axioms of ZFC. That Turing machine will never halt. But it's not possible for ZFC to prove that it will never halt. But it is possible for ZFC + Con(ZFC) to prove that it will never halt. So that's one example of an instance of the halting problem that is decidable in ZFC + Con(ZFC), but is not decidable in ZFC.

So what you're saying is provably false.

 

[johnkclark]

If all you want is a proof there is a far far easier way to get one than adding an infinite number of iterated axioms, you can get a very simple proof by just adding one axiom, “BB(7918) = 42”. But I tend to think truth is more important than proof.

John K Clark

 

[stevendaryl]

If all you want is a proof there is a far far easier way to get one than adding an infinite number of iterated axioms, you can get a very simple proof by just adding one axiom, “BB(7918) = 42”.

But that's almost certainly an inconsistent axiom. In contrast, adding Con(ZFC) is most likely a true axiom.

But I tend to think truth is more important than truth.

I consider them equally important.

 

[johnkclark]

If ZFC+Con(ZFC) can figure out what BB(7918) is why can't ZFC alone figure out what BB(5) is? It is after all VASTLY smaller. No matter how many times you say "ZFC is consistent" it won't help you determine if a given Turing Machine will halt, and that's what you need to do to figure out what the Busy Beaver number is. Of course what I'm saying may be provably false, but that doesn't mean it is false if the axioms the proof is based on are suspect. A proof that doesn't tell you the truth has no more intellectual profundity than a crossword puzzle, it's just a silly symbol manipulation game

John K Clark

 

[stevendaryl]

No matter how many times you say "ZFC is consistent" it won't help you determine if a given Turing Machine will halt

That's not true. I don't know why you keep saying it.

I don't see how what you're saying makes any sense.

Look at the title of the forum: Set theory, logic, etc. If you reject set theory and logic, then I don't see the point in your posting in this forum.

I am bowing out of this discussion.

 

[PeterDonis]

Thread closed for moderation.

 

[fresh_42]

I don't know why you keep saying it. ... If you reject set theory and logic, then I don't see the point in your posting in this forum.

There is nothing to add.

As long as there is no common base, which has to be first-order logic unless stated otherwise, I can prove that a discussion is meaningless. Repeating false statements doesn't add facts. Furthermore a distinction like

But I tend to think truth is more important than proof.

doesn't make sense in mathematics, because mathematics doesn't search truth, only logical consistent conclusions, which we call proofs, and is philosophically highly undetermined here. For those interested in truth, I refer to https://en.wikipedia.org/wiki/Truth and the links therein - some of which led to other logical systems like constructivism.

Thread remains closed.