Timeline for Using Busy Beavers to prove conjectures
Current License: CC BY-SA 4.0
25 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Jan 16 at 14:21 | history | suggested | Hermann Gruber |
added tags
|
|
| Jan 16 at 10:21 | review | Suggested edits | |||
| S Jan 16 at 14:21 | |||||
| Jan 7 at 13:02 | comment | added | Timothy Chow | @schnitzi If I understand your question correctly, this is what Joel David Hamkins is saying in his answer below. | |
| Jan 7 at 11:34 | comment | added | schnitzi | Ah, so then if BB(n) is theoretically determinable (though maybe not computable), does this imply that Riemann's and Goldbach's (or any other statement that can be proven or disproven via a Turing machine) do NOT belong to the class of statements that are true but not determinable within ZF? Regardless of how impractical a method the BB approach is for solving these statements, it is still an approach that would establish their truth or falsehood, yes? | |
| Jan 7 at 7:44 | comment | added | usul | @TimothyChow It may also help to mention that to prior-me, and presumably other untrained people, intuitively there can appear to be a difference between "BB(n) has a well-defined value in ZFC" and "ZFC proves BB(n) = m for some m". | |
| Jan 6 at 21:19 | comment | added | Ben Millwood | just to add a little more to the intuition that BB(n) can't be determined, I believe all existing values of BB(n) are computed essentially by looking at all the apparently-nonterminating machines and doing whatever is necessary to prove that they are all really nonterminating (or finding that they do terminate after all). So the sense in which BB(n) helps you prove theorems is fairly trivial, analogous to "in order to prove theorem X, simply write a book listing the proofs of all statements no longer than X, and then look up X in the book" | |
| Jan 6 at 2:54 | comment | added | Timothy Chow | @usul Fair enough, but still, if every sentence of the form BB(n) = m were either provable or disprovable in ZFC, then under the assumption that ZFC is sound, this would give us an algorithm for the halting problem. Given a Turing machine with n states, we could determine in finite time the unique m for which ZFC proves BB(n) = m, and conclude that the Turing machine doesn't halt if it takes more than m steps. | |
| Jan 6 at 2:29 | comment | added | usul | @TimothyChow to me, that appears to confuse two notions of determinable, i.e. of course BB(n) is not computable by reduction from halting, but it's much less obvious that BB(n) could be independent of ZFC. | |
| Jan 5 at 21:36 | comment | added | rus9384 | "any axiomatic system will have true statements that can't be proved within that system". A TM with more states than the given TM is like a an axiomatic theory with stronger axioms than the given axiomatic system. Just as how no consistent axiomatic system can prove its completeness, no total TM can prove it itself halts. But some TMs with larger amount of states can prove total TMs with smaller amounts of states halt. Just non-uniformly, you could encode $BB_n$ in, say, a TM that has $n+100$ states and just simulate the input TM. | |
| Jan 5 at 14:09 | comment | added | Timothy Chow | @usul Perhaps a simpler way to point out the flaw in the reasoning is to note that the halting problem is undecidable, so it is not determinable which Turing machines halt and which don't. | |
| Jan 5 at 2:08 | comment | added | usul | @WillSawin speaking for myself, my intuition that BB(n) is determinable would be that every Turing Machine either halts or does not, and there is a finite set of Turing Machines of size n. (See my previous comment for how I learned the flaw in this reasoning.) | |
| Jan 5 at 2:04 | comment | added | usul | "any BB number seems determinable" - Noah Schweber gave me a an illuminating comment: there are Turing Machines that "do not halt", except that in some models of ZFC, they "do halt" in a technically finite but nonstandard number of steps. So BB(n) can be independent of ZFC. | |
| Jan 4 at 18:45 | comment | added | Sam Hopkins | Fundamentally this is not different than the belief "for each $n$ there is some $N$ so that for any statement of size $\leq n$, there is either a proof of it or of its negation of size $\leq N$." (Of course, you have to be a little careful about what we mean by "size" of a statement/proof, but you can imagine a definition.) If we knew the right $N$ for a given $n$, and had a statement we wanted to check of size $\leq n$, we could simply test all proofs/disproofs of size $\leq N$. But in the end this belief is misguided because there are statements independent of our axiomatic system. | |
| Jan 4 at 17:56 | comment | added | Timothy Chow | In a nutshell, the problem is that even if someone hands you a machine which happens to be the true busy beaver (which runs BB(n) steps and then halts), someone else could hand you another Turing machine M which runs longer than BB(n) steps. In reality, M won't halt, but you might have no way of proving that M will never halt. That is, you have no way to rigorously rule out the possibility that M is the true busy beaver. | |
| Jan 4 at 17:51 | history | became hot network question | |||
| Jan 4 at 16:35 | comment | added | Will Sawin | What is the source of your intuition that BB(n) is determinable in principle? | |
| Jan 4 at 15:49 | history | reopened |
Joel David Hamkins Alex M. Yemon Choi Ulrich Pennig Dustin G. Mixon |
||
| Jan 4 at 15:21 | review | Reopen votes | |||
| Jan 4 at 15:49 | |||||
| Jan 4 at 15:19 | history | closed |
Kostya_I Carl-Fredrik Nyberg Brodda Max Horn Dave Benson Sam Hopkins |
Not suitable for this site | |
| Jan 4 at 14:59 | answer | added | Joel David Hamkins | timeline score: 28 | |
| Jan 4 at 10:36 | answer | added | John Tromp | timeline score: 13 | |
| Jan 4 at 10:32 | review | Close votes | |||
| Jan 4 at 15:22 | |||||
| Jan 4 at 10:13 | answer | added | Corentin B | timeline score: 32 | |
| S Jan 4 at 9:50 | review | First questions | |||
| Jan 4 at 10:41 | |||||
| S Jan 4 at 9:50 | history | asked | schnitzi | CC BY-SA 4.0 |