Timeline for Will this Turing machine find a proof of its halting?
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 7, 2022 at 3:53 | comment | added | Akiva Weinberger | Another example: Suppose we write a machine $L$ that, if it finds proof that $L$ halts then it halts (and stops searching), and if it finds a proof that $L$ doesn't halt then it enters an infinite loop (and stops searching). Naïvely, we might think (since Con(ZFC) poisons our brains) that $L$ has the same behavior as $M$, so it halts. But since $L$ is searching for two things, our proof does not work. (I think that the fate of $L$ depends on implementation (unlike $M$ which halts no matter how you write it).) | |
| Aug 7, 2022 at 3:50 | comment | added | Akiva Weinberger | On the other hand, if you give me a proof that $M'$ halts at $\beta$, then $M'$ would eventually find it... unless it finds an earlier thing that makes it stop searching, which is an issue now because that earlier thing might be a proof that $M'$ halts at $\alpha$. (If ZFC is consistent then both proofs can't exist simultaneously, but we can't assume ZFC is consistent because we need this argument to work within ZFC.) | |
| Aug 7, 2022 at 3:47 | comment | added | Akiva Weinberger | @mjqxxxx Yeah, neither situation actually has the Löb condition (provable => true). The only reason $M$ (as given in the OP) has the Löb condition, is that it's only looking for one thing. If you give me a proof that $M$ halts, then $M$ would eventually find it... unless it finds an earlier thing that makes it stop searching proofs - but we don't care because it leads to the same conclusion ($M$ halting) anyway. (continued) | |
| Aug 5, 2022 at 21:18 | comment | added | Joel David Hamkins | You can't prove that these statements, if provable, are true, since what you would also need to know in each case is that the statement is provable before the other one is, in order for it to be true. For example, if the theory is inconsistent, then both proofs are there, but only one of them is found first, and so only that one is true. | |
| Aug 5, 2022 at 20:43 | comment | added | mjqxxxx | Hmm. Consider a variant, a machine $M'$ that searches for either of two proofs: a proof that $M'$ halts at a tape position where symbol $\alpha$ is written (assertion $\psi_\alpha$), or a proof that $M'$ halts at a tape position where symbol $\beta$ is written ($\psi_\beta$); and whichever proof it finds first, it writes out that symbol and halts. Your argument would seem to imply that we can prove both $\psi_\alpha$ and $\psi_\beta$ directly in ZFC, since either one, if provable, is true. But both can't be true. What am I missing? | |
| Aug 5, 2022 at 9:46 | comment | added | user21820 | What's the weakest you can go? PA− plus Σ1-induction? | |
| Aug 4, 2022 at 11:05 | vote | accept | Henry Yuen | ||
| Aug 4, 2022 at 11:03 | comment | added | Henry Yuen | I think Joel's was the first so I will accept that, but I wish I could accept both answers! | |
| Aug 4, 2022 at 2:20 | comment | added | paul garrett | And thanks to @JoelDavidHamkins for writing this explanation! Exhilarating ideas. :) | |
| Aug 4, 2022 at 1:49 | comment | added | Joel David Hamkins | Thanks--it seems very nice. | |
| Aug 4, 2022 at 1:45 | comment | added | Akiva Weinberger | I wrote an answer that expands out the proof of Löb. | |
| Aug 4, 2022 at 0:49 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
added 448 characters in body
|
| Aug 4, 2022 at 0:40 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
added 294 characters in body
|
| Aug 4, 2022 at 0:38 | comment | added | Steven Stadnicki | I was just about to mention Löb's theorem in a comment! | |
| Aug 4, 2022 at 0:37 | history | answered | Joel David Hamkins | CC BY-SA 4.0 |