Have we found a Turing Machine for which halting/non-halting is unprovable?

The undecidability of the Halting Problem implies that there exist Turing Machines such that you can't prove whether they halt or not in whatever logical system you're using (let's say ZFC)$^1$.

Have we found any such machines, and proven their halting's independence of ZFC?

It's easy to come up with problem specifications for which no proof could be found either way, but I'm looking for concrete programs you could write in any programming language. Put another way, I'm looking for a constructive proof of the Halting Problem.

$^1$ Proof: Consider a program H which takes a number N, enumerates all statements in ZFC searching for a proof that the Nth Turing Machine halts or does not halt. If every TM has such a proof, then H will eventually find an answer, and thus will solve the halting problem (unless there's a contradiction in ZFC, in which case the proof of halting for any machine can be found trivially).

Whether the halting of a particular Turing machine is provable (or disprovable) depends on which axioms you would accept a proof starting from, of course.

However, Gödel's Incompleteness Theorem shows how to construct, for every "reasonable" theory (that is, set of axioms) $T$, a particular logical formula $G$ where it is not provable from $T$ whether $G$ itself has a proof from $T$.

Thus, once you've chosen your theory $T$ (which could be for example Peano Arithmetic or ZFC set theory) construct a Turing machine $M$ which iterates through all possible strings of symbols and checks whether each of them is a valid proof of $G$. If it finds a valid proof it halts; otherwise it keeps searching.

Since $T$ cannot tell us whether $G$ has a proof, it cannot tell us whether $M$ will halt either.

The Gödel sentence itself is rather long and complicated if we want to write it out completely -- but fortunately we don't need to do that here: We can just program $M$ such that it starts by computing $G$ according to Gödel's instructions, and then begins looking for proofs. Writing an algorithm that will output $G$ is much more tractable than writing down $G$ itself. So if you want to see $M$ explicitly, a competent CS graduate student would probably be able to write it down in at most a few thousand lines of Scheme or Haskell.

Shorter solution: If we strip away the parts of Gödel's construction that are not immediately relevant here, we get this machine:

1. Let M be my own source code (using any standard quine technique)
2. Search for a proof in ZFC of "M does not halt".
3. If one is found, stop.

If ZFC proves that the machine doesn't halt, then it will halt (so ZFC can't be true). On the other hand if ZFC proves that it does halt, then (assuming ZFC is true) it will halt, which must be because it eventually finds a proof that it doesn't halt, so ZFC is inconsistent.

• Aha! The answer was pretty much in my own footnote :) Mar 31 '15 at 20:33
• @hjfreyer: Yes, plus a standard diagonalization argument. I've added a postscript that says this explicitly. Mar 31 '15 at 20:54
• You can also look for contradictions in a system. Aug 2 '16 at 1:08
• "However, Gödel's Incompleteness Theorem shows how to construct, for every "reasonable" theory (that is, set of axioms) TT, a particular logical formula GG where it is not provable from TT whether GG itself has a proof from TT." I've never found this to be convincing. If you can't prove whether something has a proof, then: If it has a proof, then you can come up with the proof, proving that is exists. Thus the proof can't exist. And that in turn proves that the proof doesn't exist. So how it's possible that it's impossible to prove whether a proof exists? May 6 '17 at 18:01
• @Barteks2x: If you want to question the incompleteness theorem itself, it is better to do that as a separate question post. There are too many subtleties involved to handle in a comment thread to an answer that is merely applying the theorem. May 7 '17 at 9:01

As announced in postings on Scott Aaronson's blog (The 8000th Busy Beaver number eludes ZF set theory and Three announcements), here are two explicit Turing machines whose halting/nonhalting behavior is claimed to be independent of ZFC:

7918 states (by Adam Yedidia and Scott Aaronson)

1919 states (by Stefan O’Rear)