On this site there are many variants on the question whether TMs can decide the halting problem, whether for all other TMs or certain subsets. This question is somewhat different.
It asks whether the fact the halting problem applies to all TMs can be decided by a TM. I believe the answer is no, and wish to check my reasoning.
- 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.