# Finite subsets of the Halting problem are decidable. Can I prove the correctness of Turing machines computing these subsets?

I am trying to wrap my hand around the undecidability proof of the Halting problem, and to me it really seems to be more of a proof about representation than decidability. Namely, the proof that some languages are undecidable by Turing machines seems to simply state that I cannot find finite representations for arbitrary countably infinite sets. So far so good. However, I do not see how this might ever be a problem in practice.

If I fix some machine $M$ and consider the language $L_M = \{M \mid \textrm{$M$halts on empty input}\}$. Clearly, $L_M$ is decidable, because it either denotes the singleton set $\{ M \}$ or the empty set, but:

(1.) Can I always prove the correctness of some machine that decides $L_M$?

(2.) Suppose I cannot always find a proof. Can I find some specific machine $M$, for which I can find a proof that I cannot prove or disprove whether it halts on a specific input?

My first question can also be seen from another viewpoint: If I was to formulate the Halting problem in natural language, it would state

"Does there exist a fixed strategy, so I can decide for every TM whether it halts or not."

But I am interested in the problem:

"Given some TM, can I come up with a strategy to decide whether it halts or not."

I guess that that this question is more about provability than decidability, but unfortunately I know very little about the former.

• I don't understand why you decided that $L_M$ is either singleton or empty. There infinely many TM halting on empty input. – fade2black Jul 16 '17 at 13:14
• I am curious what you mean by "fintite representation for arbitrary countably infinite set". Consider the set of natural even numbers. The function $f(x) = 2x$ defined on the set $N$ represents/denotes the set of nonnegativel even numbers where $f$ has a finite form. This is an example of representing of infinite set through finite number of symbols. – fade2black Jul 16 '17 at 13:35
• I guess my notation was somewhat ambigious. I precisly meant a fixed $M$ as stated above, not the collection of all possible $M$'s which halt on empty input. Regarding your second comment: Yes, my only point was that in this sense one can view Turing machines which solve decision problems as such finite representations. The Turing machine which only accepts even numbers accepts a subset of the natural numbers. And the undecidability result for Turing machines now simply states that there can't exist a Turing machine for every arbitrary subset. – Max Jul 16 '17 at 20:24
• I think you meant to say $L_M = \{N \mid N = M \land M \text{halts}\}$, or less weirdly, $$L_M = \begin{cases} \{M\} & \text{ if } M \text{ Halts} \\ \emptyset &\text{ otherwise } \end{cases}$$ – DanielV Jul 16 '17 at 22:32

You cannot always prove the correctness of the true value of $L_M$ (unless your proof system is inconsistent). Indeed, if you could, then given $M$, you could search for proofs that $L_M = \emptyset$ and for proofs that $L_M = \{M\}$, and eventually you'll find one, thus solving the halting problem.
Gödel's incompleteness theorem gives you a specific such machine. Suppose that your proof system is $P$ (for example, ZFC), and consider the machine $M$ that goes over all possible proofs in $P$, searching for a proof of contradiction, and halting if it finds one. Assuming that $P$ is consistent, we have $L_M = \emptyset$, but if $P$ could prove that, then it follows that $P$ proves its own consistency, which is ruled out by Gödel's second incompleteness theorem (assuming $P$ is not too weak).
• Thank you! This is exactly the type of answer I was looking for, and the example of an $M$ which enumerates all proofs of $P$ is very insightful! – Max Jul 16 '17 at 20:33