- Define the meta-halting language $L_{MH}$ as the language composed of TMs that decide whether a TM halts.
$$L_{MH} = { M : forall_{M’,w} M(M’, w) text{ accepts if $M'(w)$ halts, rejects otherwise}}$$
- $L_{MH}= emptyset$ due to the halting problem.
Thus, the title question more precisely stated: is it decidable whether $L_{MH} = emptyset$?
- Per Rice’s theorem, it is undecidable whether an r.e. language is empty.
In both cases, if $L_{MH}$ is or is not r.e., it is undecidable whether $L_{MH} = emptyset$. - Therefore, it is undecidable whether $L_{MH} = emptyset$.
This proves a TM cannot decide whether the halting problem applies to all TMs. Is my understanding correct? UPDATE: I am trying to show that a TM cannot “prove the halting problem” for some definition of “prove” that seems intuitively correct. Below is an illustration of why I think this is correct. We can create a TM $M_{MH}$ that generates $L_{MH}$ in the following way. The TM takes a tuple $(M_i,M_j,w_k,steps)$. It simulates $M_i(M_j, w_k)$ for $steps$ iterations. If $M_i$ accepts all $(M_j, w_k)$ pairs that halt, and rejects all others then $M_{MH}$ accepts $M_i$. Otherwise, it rejects $M_i$ if $M_i$ decides incorrectly or fails to halt. $M_{MH}$ does not halt, because it must evaluate an infinite number of pairs for each $M_i$. Additionally, all the $M_i$s will fail to halt. $M_{MH}$ will be unable to accept or reject any $M_i$ as it will not know from the simulation that all $M_i$s will fail to halt. Thus, the language it defines is not r.e. and not decidable. $M_{MH}$ captures my intuition of what I think it means for a TM to prove the halting problem. Other suggestions, such as $M_{MH}$ rejecting all $M_i$ or outputting a known proof give $M_{MH}$ prior knowledge that the halting problem applies to all $M_i$. This cannot count as $M_{MH}$ proving something since the $M_{MH}$’s premise is the conclusion it is proving, and thus is circular.
Asked By : yters
Answered By : Vor
- the set $P = { x mid x mbox{ is a valid proof of } varphi mbox{ in ZFC}}$ is decidable;
- you can also build a TM $M$ that enumerates the proofs in ZFC and halts if it founds a proof of $varphi$ or a proof of $neg varphi$; clearly $M$ halts;
- the set ${ M mid M mbox{ decides } P }$ is undecidable
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/60985