Comment by Sniffnoy | Hacker News Reader

Comment by Sniffnoy | Hacker News Reader

Parent Full thread

When you say "provably", do you mean that in the mathematical sense or in a practical sense?

For the practical sense, other commenters have already replied.

For the mathematical sense, I would say it would be pretty surprising to me if BB(5) had been undecidable -- 5 states and 2 symbols is just so few with which to try to encode undecidable behavior.

However, it's worth noting that as a consequence of the incompleteness theorem, there must be some n such that standard mathematics cannot prove the value of BB(n). And in recent years various people have been working on finding such n and seeing how low they can get the number. The current record[0] is 745.

I expect that record can be probably be brought lower (more easily than the record for computing BB can be brought higher!), but even so, that's a lot of distance between 5 (the highest we know) and 745 (the lowest we know to be unknowable).

[0]This is the current record both for ZFC and for PA, in case you're wondering what I mean by "standard mathematics"... so it at least ought to be possible to bring it down further for PA! I think so far nobody's found a way to do better for PA than for ZFC, even though, like, that has to be possible, right?

Are there any interesting mathematical problems that can be encoded with 5 states and 2 symbols, which now we can prove using BB(5)?

I don't believe so. But even if there were, unfortunately, these things basically work the other way around.

If you can encode a problem in n states, and you know BB(n), then, as you say, you could use that to solve the problem. Trouble is, how do you know BB(n)? In reality, the only way to determine BB(n) is to go and solve all such problems; there isn't any other easier method that you can apply that would then let you get answers for these problems as a consequence.

So, the value of BB(n) will always be a summation of "we did all the hard work of solving all the n-state problems", not something you do separately to get those answers out.

Mostly no: we did find some non-halting TMs that required new proofs, but none of those had the flavor of new math, per se. Indeed, we found that all but 30 of them could be proved by finite automata methods, meaning the TM's state/tape at any step could be reduced to one of finitely many states and we'd still know all we needed to know about future steps. I would argue that such a non-halting proof can't have much mathematical content. (Maybe a bit, in about the same way that an integer equation is sometimes proved unsolvable by considering it modulo n and checking every case.) Also, I learned some math I wasn't personally familiar with from the analysis of a particular machine: https://www.sligocki.com/2023/03/14/skelet-10.html (Zeckendorf's Theorem).

Tangential, but fun fact about Zeckendorf: In addition to Zeckendorf representation, there's also dual Zeckendorf (sometimes also called lazy Fibonacci), where instead of requiring no two consecutive ones, you require no two consecutive zeroes. (Not counting the implicit zeroes at the big end, of course.) It was surprising to me that this also works, but it does!

Actually, just as you can do bijective base-b [0], you can also do bijective Zeckendorf (using 1 and 2 with no two consecutive 1s). Although, as happens with bijective binary, bijective Zeckendorf is closely tied to ordinary Zeckendorf, so it doesn't offer much new. But bijective dual Zeckendorf doesn't work -- lots of numbers can't be represented!

One more fun fact about Zeckendorf and dual Zeckendorf: Write n>0 in Zeckendorf, and count how many zeroes it ends in. This will be even if the dual Zeckendorf representation of n ends in a 1, and odd if it ends in a 0. Similarly, if you write n in dual Zeckendorf and count how many 1s it ends in, this will be even if the (ordinary) Zeckendorf representation ends in a 0 and odd if it ends in a 1.

[0] https://en.wikipedia.org/wiki/Bijective_numeration

So I know we can prove that we cannot solve the halting problem for all TM.

But for any given TM, can we decide whether it is provable or not? Or will we meet some that we will never know if we can solve or not?

Sadly, we can't, for such a test would already be enough to solve the halting problem: if a TM's status is provable, enumerate possible proofs (of halting and non-halting) until we find one and know the result; if the status is not provable, then the machine certainly cannot halt.

My memories of theoretical computer science are quite rusty, but I seem to see an issue with your argument: if you need enumeration you meet semidecidability. In other words, if you start generating the proofs and you find the one you were looking for, then problem solved. But if you can't find the proof, you would need to keep generating them at infinity to find the one you need. You can't conclude the result in this way without enumerating all possible proofs. Unless, you have a way of limiting the number of proofs that need to be generated?

You are bounded by the fact that the statement is provable. Let a statement M be provable with a proof length K. By contradiction, if K is non finite, the statement must not be provable. Thus, there must be some positive integer K s.t. the proof length < K. Thus, it suffices to enumerate all proofs of length < K.

Insofar as we are given provability, we can solve halting.

> 5 states and 2 symbols is just so few with which to try to encode undecidable behavior.

Would you be brave enough to say the same thing about BB(6) or BB(7)?

Yeah, that would definitely surprise me.

Would you consider the Collatz conjecture as potentially undecidable?

Because that one needs to be solved for BB(6) already: https://wiki.bbchallenge.org/wiki/Antihydra

Considering how we made basically no real progress on it mathematically in a whole generation, solving BB(6) within the next decades would be a miracle, and I would bet a lot against it.

I can't see us EVER getting to BB(10), no matter how advanced humanity grows (and it would be meaninglessly large anyway).

I think 765 is just a huge overestimation based on the fact that it is somewhat straightforward to construct.

First off, it's not Collatz, it's a Collatz-like problem.

But yes, I'd be very surprised if Collatz were actually undecideable, even if it's well beyond the reach of current mathematics.

I agree with your statements about BB(10) and BB(6), but they just aren't very relevant. I agree those involve extremely difficult problems likely well beyond the reach of current mathematics, but I'd still be very surprised to find anything undecideable in there. There's a big difference between being truly undecideable and merely well beyond the reach of current mathematics!

(Also, the current record for undecideability is 745, or 765.)

BB(745) being independent of ZFC isn’t due to incompleteness theorems. It encodes a different theorem which is also independent of ZFC.

https://scottaaronson.blog/?p=2725

Well, that post is about 8000, not 745; but yes, in general, you are not going to use a Gödel sentence when trying to drive down the record.

This isn't disagreeing with what I was saying, though; I said incompleteness requires there is some such n, and then also said what we know about the record, I didn't say the record comes from a Gödel sentence.

You are right, sorry about that :-)

Hope my comment addresses a common confusion despite its unnecessarily corrective tone.

Reply on news.ycombinator.com