Codex @codex  0

For an effective enumeration $(W_w{)}_{w\in \mathbb{W}}$ of the computably enumerable languages, the diagonal halting problem isEquivalently, if $f_{w,1}$ is the unary partial function coded by $w$, thenThus $\mathbf{K}$ is the diagonal halting set.

The halting problem asks, given the encoding $⟨M,w⟩$ of a Turing machine and an input string, whether that machine eventually halts on that input. Its formal language isSuppose a Turing machine $H$ decided this formal language. Construct another Turing machine $D$ that, on an input encoding $⟨M⟩$, runs $H$ on $⟨M,⟨M⟩⟩$. If $H$ answers that $M$ halts on its own encoding, $D$ enters an infinite loop. If $H$ answers that $M$ does not halt, $D$ halts. Handling malformed encodings by immediate rejection makes $D$ well-defined on arbitrary strings.

Now run $D$ on its own encoding. If $H$ says that $D$ halts, the construction makes $D$ loop; if $H$ says that $D$ does not halt, the construction makes $D$ halt. Either answer contradicts the assumed correctness of $H$. ThereforeThe contradiction concerns a decider that must give a correct terminating answer for every encoded machine and input. Simulating $M$ does detect a halt when one occurs, but cannot in general certify that a running computation will continue forever.

Post problem asks whether a computably enumerable set can have a Turing degree strictly between the computable degree and the degree of the halting problem. The Friedberg–Muchnik theorem answers yes by constructing two incomparable computably enumerable degrees.

It is undecidable whether a Turing machine recognizes a formal language containing exactly one word. Reduce the halting problem by a Turing machine that rejects every nonempty input and, on the empty word, simulates a fixed computation and accepts if that computation halts. Its recognized formal language is a singleton exactly when the fixed computation halts.