7 ms·

That’s the thing, I don’t think busy beaver numbers are undecidable. Every TM with n states will or won’t halt, and there isn’t any reason to think we can’t pro

That’s the thing, I don’t think busy beaver numbers are undecidable. Every TM with n states will or won’t halt, and there isn’t any reason to think we can’t prove whether it halts or not. Every proof for undecidability use hypothetical TM constructions with a logical property and a trick. Busy beaver numbers are concrete.

ogogmad 3y ago
Oh dear God. The BB function is uncomputable precisely because of the halting problem, which you think is a "logical trick".
eigenket 3y ago
If you can solve the halting problem there is an algorithm to easily solve the busy-beaver problem and vice-versa. They are exactly equivalent.
- srcreigh 3y ago
  Yes but no. Algorithm for BB numbers and halting problem can implement each other, but both provably don’t exist in the first place, so that’s a bit like proving 2 is odd implies 3 is even and vice versa. 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.
  - eigenket 3y ago
    > 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). 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.
    - srcreigh 3y ago
      > 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.
      - eigenket 3y ago
        > Source? AFAIK we aren’t aware of any TMs which are impossible to prove loops forever 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).
        srcreigh 3y ago
        Thanks, fun discussion. I think we understand each other. 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.
  - tshaddox 3y ago
    > 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). 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.
    - srcreigh 3y ago
      Yeah. In the most egregious case it could come down to simply listing the numbers that we have proofs for. 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.
tshaddox 3y ago
> Every TM with n states will or won’t halt, and there isn’t any reason to think we can’t prove whether it halts or not. 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.
- srcreigh 3y ago
  That’s the halting problem, I’m referring to busy beaver numbers.
  - tshaddox 3y ago
    And you cannot decide busy beaver problems without developing a TM that can prove, for each and every TMs, whether they halt.
    - srcreigh 3y ago
      Busy beaver series is uncomputable as a whole, but not for its individual values. So in theory we can solve arbitrarily many busy beaver numbers, just can’t write a program to list them endlessly. 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.)
      - practal 3y ago
        Sorry, you are wrong here. We may never solve BB(6) exactly because of undecidability. We don't have an algorithm for computing BB(6). If we had one, BB(6) would be computable (= decidable). Of course, as soon as we know BB(6) = n, for some numeric literal n, it is trivially clear that BB(6) is computable/decidable: function BB(k) { if (k === 6) return n; } Granted, we don't know if BB(6) is decidable or not, because we don't know if there are proofs in reasonable axiomatic theories which show for each of the 6-state TMs which don't halt that they don't halt. That there are only finitely many such TMs does not really matter here. For something like BB(3) there are only 21 TMs, so we can try our luck to prove that those TMs which don't seem to halt actually don't halt, and hey, we got lucky, we can! Nobody knows if we have the same kind of luck for BB(6). Indeed, for BB(745) we know that at least for ZFC, we don't have this kind of luck. Of course, if we knew BB(745) = n, for some numeric literal n, then in ZFC + {BB(745) = n} we have that BB(745) is decidable, but if you don't like logical tricks, then you won't like that result too much, either. 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).

ogogmad 3y ago

Oh dear God. The BB function is uncomputable precisely because of the halting problem, which you think is a "logical trick".

eigenket 3y ago

If you can solve the halting problem there is an algorithm to easily solve the busy-beaver problem and vice-versa. They are exactly equivalent.

srcreigh 3y ago
Yes but no. Algorithm for BB numbers and halting problem can implement each other, but both provably don’t exist in the first place, so that’s a bit like proving 2 is odd implies 3 is even and vice versa. 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.
- eigenket 3y ago
  > 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). 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.
  - srcreigh 3y ago
    > 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.
    - eigenket 3y ago
      > Source? AFAIK we aren’t aware of any TMs which are impossible to prove loops forever 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).
      - srcreigh 3y ago
        Thanks, fun discussion. I think we understand each other. 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.
- tshaddox 3y ago
  > 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). 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.
  - srcreigh 3y ago
    Yeah. In the most egregious case it could come down to simply listing the numbers that we have proofs for. 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.

tshaddox 3y ago

> Every TM with n states will or won’t halt, and there isn’t any reason to think we can’t prove whether it halts or not. 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.

srcreigh 3y ago
That’s the halting problem, I’m referring to busy beaver numbers.
- tshaddox 3y ago
  And you cannot decide busy beaver problems without developing a TM that can prove, for each and every TMs, whether they halt.
  - srcreigh 3y ago
    Busy beaver series is uncomputable as a whole, but not for its individual values. So in theory we can solve arbitrarily many busy beaver numbers, just can’t write a program to list them endlessly. 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.)
    - practal 3y ago
      Sorry, you are wrong here. We may never solve BB(6) exactly because of undecidability. We don't have an algorithm for computing BB(6). If we had one, BB(6) would be computable (= decidable). Of course, as soon as we know BB(6) = n, for some numeric literal n, it is trivially clear that BB(6) is computable/decidable: function BB(k) { if (k === 6) return n; } Granted, we don't know if BB(6) is decidable or not, because we don't know if there are proofs in reasonable axiomatic theories which show for each of the 6-state TMs which don't halt that they don't halt. That there are only finitely many such TMs does not really matter here. For something like BB(3) there are only 21 TMs, so we can try our luck to prove that those TMs which don't seem to halt actually don't halt, and hey, we got lucky, we can! Nobody knows if we have the same kind of luck for BB(6). Indeed, for BB(745) we know that at least for ZFC, we don't have this kind of luck. Of course, if we knew BB(745) = n, for some numeric literal n, then in ZFC + {BB(745) = n} we have that BB(745) is decidable, but if you don't like logical tricks, then you won't like that result too much, either. 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).