An alternative way of deciding within a nondeterministic complexity class is to present a verifier-prover pair. To recall, let $\mathsf{L}$ be a language, and let $\mathsf{w}$ be a word. To decide whether $\mathsf{w} \in \mathsf{L}$:
The prover, a magical machine, will immediately find a proof that $\mathsf{w} \in \mathsf{L}$ and send it to the verifier. If $\mathsf{w} \notin \mathsf{L}$, however, the proof will be a fake. (In this sense the prover is said to be malicious.)
The verifier, a Turing machine (or an equivalent), having received the proof, will decide whether the proof is true.
Here, there is no time/space restriction for the verifier, meaning that our complexity class in concern is $\mathsf{RE}$.
It is well-known that $\mathsf{HALT}$, the halting problem, is in $\mathsf{RE}$. In a simple sense, the verifier-prover pair would look like this. Let $\mathsf{w}$ be the program concerned whether to halt:
If $\mathsf{w} \in \mathsf{HALT}$, the prover will immediately know how many Turing machine iterations are needed for $\mathsf{w}$ to halt.
- The verifier will run $\mathsf{w}$ for exactly that many Turing machine iterations, see that $\mathsf{w}$ actually halted, and accept.
If $\mathsf{w} \notin \mathsf{HALT}$, the prover will immediately know that $\mathsf{w}$ wouldn't halt, and will send the verifier a random number.
- The verifier will run $\mathsf{w}$ for exactly that many Turing machine iterations, see that $\mathsf{w}$ actually didn't halt, and reject.
But what about its complement, $\mathsf{\text{NOT-HALT}}$? It is well-known that it is not in $\mathsf{RE}$. As such, I presume it means there cannot be a working verifier-prover pair for $\mathsf{\text{NOT-HALT}}$. But which machine should I blame? I see several ways of interpreting this:
There is no way of proving $\mathsf{w}$ wouldn't halt. It's the prover's fault.
It is possible to prove that $\mathsf{w}$ wouldn't halt, but there is no way of deciding whether the proof is true. It's the verifier's fault.