patternMinor
Finite subsets of the Halting problem are decidable. Can I prove the correctness of Turing machines computing these subsets?
Viewed 0 times
problemcanfinitethethesearecorrectnesssubsetshaltingdecidable
Problem
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.
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.
Solution
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).
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).
Context
StackExchange Computer Science Q#77993, answer score: 4
Revisions (0)
No revisions yet.