Timeline for Will this Turing machine find a proof of its halting?
Current License: CC BY-SA 4.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| 2 days ago | comment | added | D.R. | For future visitors: I think I was able to fully write up a proof of Lob's theorem using (a slight tweak to) these funny machines, which may be of interest. I welcome any corrections: math.stackexchange.com/questions/4852746/… | |
| Dec 26, 2022 at 19:15 | comment | added | Akiva Weinberger | @mathlander This is a consequence of Kleene's recursion theorem (pronounced /ˈkleɪni/ KLAY-nee), believe it or not), which essentially states that we may assume programs can access their own source code. For a specific construction, see this comment I wrote above. | |
| Dec 26, 2022 at 18:38 | comment | added | mathlander | Why is it the case that such an $N$ exists? | |
| Oct 26, 2022 at 16:20 | history | edited | Akiva Weinberger | CC BY-SA 4.0 |
"a ZFC a proof" -> "a ZFC proof"
|
| Aug 4, 2022 at 20:12 | comment | added | Akiva Weinberger | @TimothyChow Note that that answer resolves it using Gödel's second incompleteness theorem. I think if you "unzip" the proof of the second incompleteness theorem (phrased using Turing machines), you essentially get the argument as I wrote it. | |
| Aug 4, 2022 at 19:37 | comment | added | Timothy Chow | The wackiness of the proof of Löb's theorem was noted by Nik Weaver in an answer to another MO question. | |
| Aug 4, 2022 at 12:03 | comment | added | Akiva Weinberger | @HenryYuen Wikipedia's proof is more general because it applies not just to the provability operator (what Hamkins calls $\text{Pr}_{ZFC}(\ulcorner\cdot\urcorner)$, which takes a ZFC formula as input and produces a ZFC formula as output), but to anything that behaves like the provability operator. It's also easier to verify, as it's all syntactic rules. The downside is it's harder to see what's going on. (I suppose this is a metaphor for formalization in general.) | |
| Aug 4, 2022 at 11:28 | comment | added | Akiva Weinberger | @HenryYuen Wikipedia does it by constructing a sentence $\Psi$ that satisfies $\vdash\Psi\leftrightarrow(\Box\Psi\rightarrow P)$ (where $P$ is "$M$ halts"). In words, that means it's a sentence $\Psi$ that's true iff, if $\Psi$ has a proof then $P$ holds. In other words, $\Psi$ is the sentence "If this sentence is provable then $P$ holds" (that is, $\Psi$ is the sentence "If this sentence is provable then $M$ halts"). Compare this to what I use, which is that $N$ halts iff, if there's a proof that $N$ halts then $M$ halts. | |
| Aug 4, 2022 at 11:04 | comment | added | Henry Yuen | Beautiful -- this is a lot more understandable to me than "modal logic" (what shows up on Lob's theorem's Wiki page). | |
| Aug 4, 2022 at 3:04 | history | edited | Akiva Weinberger | CC BY-SA 4.0 |
edited body
|
| Aug 4, 2022 at 2:50 | comment | added | Akiva Weinberger | I suppose, when I wrote that "$M$ finds this [proof that $M$ halts] so it halts", technically $M$ could have already found an earlier proof and halted already. (Similar for when I wrote a similar thing about $N$.) But it doesn't change the argument | |
| Aug 4, 2022 at 2:20 | comment | added | paul garrett | Yes, hilarious, indeed! Thanks for writing this out! | |
| Aug 4, 2022 at 2:07 | history | edited | Akiva Weinberger | CC BY-SA 4.0 |
added 4 characters in body
|
| Aug 4, 2022 at 1:56 | history | edited | Akiva Weinberger | CC BY-SA 4.0 |
added 61 characters in body
|
| Aug 4, 2022 at 1:53 | comment | added | Akiva Weinberger | Several edits because the details are pretty tricky. (My original version - which I think you can't find on the edit log because I fixed it quick enough - didn't actually use the behavior of $M$ in the proof… whoops.) | |
| Aug 4, 2022 at 1:51 | history | edited | Akiva Weinberger | CC BY-SA 4.0 |
added 61 characters in body
|
| Aug 4, 2022 at 1:44 | history | answered | Akiva Weinberger | CC BY-SA 4.0 |