Timeline for Is deciding whether a Turing machine *provably* runs forever equivalent to the halting problem?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 22, 2013 at 4:49 | comment | added | Joel David Hamkins | Yes, that seems to work! I think it is a fun problem; the key was to find a program that in any case wouldn't halt, but would do so in a provable way when a given program halts, and not otherwise. What the arguments show is that the sets are not only Turing equivalent, but also $1$-equivalent, for we seem to have $1$-reductions both ways. So the two decision problems are computably isomorphic. | |
| May 22, 2013 at 4:43 | comment | added | Scott Aaronson | However, notice that both my argument and yours only used the assumption that ZF is consistent, nothing more! Admittedly ZF doesn't prove that the reduction works, but ZF does prove the conditional result that the reduction works assuming Con(ZF). And I said at the outset that I was happy to assume even the soundness of ZF! | |
| May 22, 2013 at 4:38 | comment | added | Scott Aaronson | Thanks, Joel! Here's my simplification of your argument, avoiding the use of the recursion theorem. Given a TM M, construct a new TM M' that simulates M, but that while it runs, also (in parallel) searches for a proof in ZF that 0=1, and halts if it ever finds one. Meanwhile, if M ever halts, then M' terminates the 0=1 branch and simply runs forever. Then in any case M' runs forever. But if M halts then ZF proves that M' loops, while if M loops then ZF doesn't prove that M' loops (assuming ZF is consistent). So by running PROVEHALT on M', we also decide whether M halts, QED. | |
| May 22, 2013 at 4:33 | vote | accept | Scott Aaronson | ||
| May 22, 2013 at 4:01 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
added 142 characters in body; added 160 characters in body; added 11 characters in body; added 18 characters in body
|
| May 22, 2013 at 3:34 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
added 34 characters in body; added 6 characters in body
|
| May 22, 2013 at 3:29 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
added 194 characters in body; deleted 280 characters in body
|
| May 22, 2013 at 3:16 | history | answered | Joel David Hamkins | CC BY-SA 3.0 |