4 ms·

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 provin

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.

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.