3 ms·

I'm trying to get an intuition about why this whole game can even be played, and it's proving (ha) rather tricky. I'm ok with the idea that things sometimes cro

I'm trying to get an intuition about why this whole game can even be played, and it's proving (ha) rather tricky. I'm ok with the idea that things sometimes cross into the realm of the impossible when transitioning from discrete/finite to continuous/infinite, or maybe from countably to uncountably infinite, but the notion that there's some constant threshold seems so counterintuitive. The link at the end of the article is pretty good [1] as is wikipedia [2], but I'm clearly missing some intuition here. Help! [1] https://johncarlosbaez.wordpress.com/2011/10/28/the-complexity-barrier/ https://johncarlosbaez.wordpress.com/2011/10/28/the-complexi... [2] https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin.27s_incompleteness_theorem https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin....

ikeboy 10y ago
You can't solve the halting problem. Therefore, if you take a program that takes a Turing machine as input, searches for a proof in ZFC (or your favorite alternative) that the program halts or that it doesn't, and if it doesn't find a proof either way then it runs forever, your program is not a halting solver. Therefore, there are some Turing machines which can't be proven to halt or run forever in any given consistent system that can be computed. (Because if every TM had a proof, then the program above would solve the unsolvable halting problem). Therefore, there is a smallest such program that's independent of ZFC. Does that help?
- andrewflnr 10y ago
  Therefore, there are some Turing machines which can't be proven to halt or run forever in any given consistent system that can be computed. I feel like it's worth clarifying the quantifiers here. For all consistent systems, there exist Turing machines whose halting behavior can't be proven in that system. Unless I have some disastrous misunderstanding...
  - ikeboy 10y ago
    Well a consistent system that can't be computed can prove things about all Turing machines. E.g. ZFC plus an infinite set of axioms of the sort "machine X halts" for all machines that halt. We can't compute all the axioms, but the system is perfectly consistent. We could compute the axioms if we had a halting Oracle. It wouldn't be able to prove the halting behavior of some Turing machines that have halting oracles attached, though.
- pdkl95 10y ago
  > Therefore, there is a smallest such program that's independent of ZFC. http://www.scottaaronson.com/blog/?p=2725 http://www.scottaaronson.com/blog/?p=2725 we give a 7,918-state Turing machine, called Z (and actually explicitly listed in our paper!), such that: Z runs forever, assuming the consistency of a large-cardinal theory called SRP (Stationary Ramsey Property), but Z can’t be proved to run forever in ZFC [...], assuming that ZFC is consistent. edit: Just saw that this was linked at the bottom of the article. As pohl mentioned, the article really buried the lede.
- shmageggy 10y ago
  Yeah a bit. This part > searches for a proof in ZFC (or your favorite alternative) is tripping me up though. It's not obvious to me that you can do this in an automated fashion. I assume this is a standard tool for theorists though? How does such a program work?
  - deleted 10y ago
    [deleted]
  - deleted 10y ago
    [deleted]
  - ikeboy 10y ago
    Proofs can be expressed using a string and verified to check every step is valid. So brute force over every string, checking if it's a valid proof for the claim you want.
    - deleted 10y ago
      [deleted]
  - shmageggy 10y ago
    It's not letting me reply any deeper, but that makes sense, thanks!
    - wging 10y ago
      I think it's that you can't reply to posts that are too new.
      - tomjakubowski 10y ago
        You can, you just have to click on the timestamp to visit the comment's item page first, something like https://news.ycombinator.com/item?id=11750351 https://news.ycombinator.com/item?id=11750351
  - wolfgke 10y ago
kordless 10y ago
May I ask if you are able to visualize things using your mind's eye at at what levels (size, detail, color/brightness)? Just curious about correlation with the subject matter.

ikeboy 10y ago

You can't solve the halting problem. Therefore, if you take a program that takes a Turing machine as input, searches for a proof in ZFC (or your favorite alternative) that the program halts or that it doesn't, and if it doesn't find a proof either way then it runs forever, your program is not a halting solver. Therefore, there are some Turing machines which can't be proven to halt or run forever in any given consistent system that can be computed. (Because if every TM had a proof, then the program above would solve the unsolvable halting problem). Therefore, there is a smallest such program that's independent of ZFC. Does that help?

andrewflnr 10y ago
Therefore, there are some Turing machines which can't be proven to halt or run forever in any given consistent system that can be computed. I feel like it's worth clarifying the quantifiers here. For all consistent systems, there exist Turing machines whose halting behavior can't be proven in that system. Unless I have some disastrous misunderstanding...
- ikeboy 10y ago
  Well a consistent system that can't be computed can prove things about all Turing machines. E.g. ZFC plus an infinite set of axioms of the sort "machine X halts" for all machines that halt. We can't compute all the axioms, but the system is perfectly consistent. We could compute the axioms if we had a halting Oracle. It wouldn't be able to prove the halting behavior of some Turing machines that have halting oracles attached, though.
pdkl95 10y ago
> Therefore, there is a smallest such program that's independent of ZFC. http://www.scottaaronson.com/blog/?p=2725 http://www.scottaaronson.com/blog/?p=2725 we give a 7,918-state Turing machine, called Z (and actually explicitly listed in our paper!), such that: Z runs forever, assuming the consistency of a large-cardinal theory called SRP (Stationary Ramsey Property), but Z can’t be proved to run forever in ZFC [...], assuming that ZFC is consistent. edit: Just saw that this was linked at the bottom of the article. As pohl mentioned, the article really buried the lede.
shmageggy 10y ago
Yeah a bit. This part > searches for a proof in ZFC (or your favorite alternative) is tripping me up though. It's not obvious to me that you can do this in an automated fashion. I assume this is a standard tool for theorists though? How does such a program work?
- deleted 10y ago
  [deleted]
- deleted 10y ago
  [deleted]
- ikeboy 10y ago
  Proofs can be expressed using a string and verified to check every step is valid. So brute force over every string, checking if it's a valid proof for the claim you want.
  - deleted 10y ago
    [deleted]
- shmageggy 10y ago
  It's not letting me reply any deeper, but that makes sense, thanks!
  - wging 10y ago
    I think it's that you can't reply to posts that are too new.
    - tomjakubowski 10y ago
      You can, you just have to click on the timestamp to visit the comment's item page first, something like https://news.ycombinator.com/item?id=11750351 https://news.ycombinator.com/item?id=11750351
- wolfgke 10y ago

kordless 10y ago

May I ask if you are able to visualize things using your mind's eye at at what levels (size, detail, color/brightness)? Just curious about correlation with the subject matter.