4 ms·

> 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 machi

> 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.

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.