4
$\begingroup$

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.

Improve this question
$\endgroup$
4
  • $\begingroup$ I don't understand why you decided that $L_M$ is either singleton or empty. There infinely many TM halting on empty input. $\endgroup$
    – fade2black
    Commented Jul 16, 2017 at 13:14
  • $\begingroup$ 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. $\endgroup$
    – fade2black
    Commented Jul 16, 2017 at 13:35
  • $\begingroup$ 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. $\endgroup$
    – Max
    Commented Jul 16, 2017 at 20:24
  • $\begingroup$ 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}$$ $\endgroup$
    – DanielV
    Commented Jul 16, 2017 at 22:32

1 Answer 1

Reset to default
4
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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! $\endgroup$
    – Max
    Commented Jul 16, 2017 at 20:33
  • $\begingroup$ Don't forget to upvote the answer if you like it. $\endgroup$
    – Yuval Filmus
    Commented Jul 16, 2017 at 20:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.