Hacker News Reader

Comment by ikeboy | Hacker News Reader

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?

View on HN

> Therefore, there is a smallest such program that's independent of ZFC.

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.

  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...

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.

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?

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.

It's not letting me reply any deeper, but that makes sense, thanks!

I think it's that you can't reply to posts that are too new.

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

The idea is that proof systems can be formulated as a grammar for a recursively enumerable language (Type 0 grammars in the Chomsky hierarchy): https://en.wikipedia.org/wiki/Chomsky_hierarchy#Summary, such that if there is a proof of a particular statement a corresponding word can be derived by the corresponding grammar. But this can easily be done by a Turing machine (either check through all possible derivations in the grammar or, more abstract, let the Turing machine let non-deterministically choose a possible derivation and use the fact that the expressiveness of non-deterministic Turing machines is the same as for deterministic Turing machines).

Reply on news.ycombinator.com