[proofplan]
We prove first that the computable degree is below the halting degree, because every computable set has a decision procedure that can be run without using any oracle. The strictness is the content of the diagonal argument: if $K$ were computable, then one could build a computable partial function that disagrees with its own index on whether it halts. This contradiction shows that $K$ is not computable, so its Turing degree cannot be $0$.
[/proofplan]
[step:Place the computable degree below the halting degree]
Let $A \subseteq \mathbb{N}$ be a computable set. By definition of computability, its characteristic function
\begin{align*}
\mathbb{1}_A: \mathbb{N} &\to \{0,1\}
\end{align*}
is computable.
We construct an oracle computation for $A$ relative to $K$. On input $n \in \mathbb{N}$, the oracle machine ignores its oracle and computes $\mathbb{1}_A(n)$. Therefore $A \leq_T K$. Since $A$ was an arbitrary computable set, every representative of the degree $0$ is Turing reducible to $K$, and hence
\begin{align*}
0 \leq 0'.
\end{align*}
[/step]
[step:Diagonalize against a hypothetical decision procedure for $K$]
Assume, for contradiction, that $K$ is computable. Then its characteristic function
\begin{align*}
\mathbb{1}_K: \mathbb{N} &\to \{0,1\}
\end{align*}
is computable.
Define a partial function
\begin{align*}
\psi: \mathbb{N} &\rightharpoonup \mathbb{N}
\end{align*}
as follows: on input $n \in \mathbb{N}$, first compute $\mathbb{1}_K(n)$. If $\mathbb{1}_K(n) = 0$, output $0$; if $\mathbb{1}_K(n) = 1$, run forever. Since $\mathbb{1}_K$ is computable by the contradiction hypothesis, $\psi$ is partial computable.
Because $(\varphi_e)_{e \in \mathbb{N}}$ is an acceptable enumeration of all partial computable functions, there exists an index $d \in \mathbb{N}$ such that
\begin{align*}
\varphi_d = \psi.
\end{align*}
We evaluate at the input $d$.
If $d \in K$, then $\varphi_d(d)$ is defined. Since $\varphi_d = \psi$, this means $\psi(d)$ is defined. But the definition of $\psi$ says that when $\mathbb{1}_K(d)=1$, the computation $\psi(d)$ runs forever, so $\psi(d)$ is undefined. This is a contradiction.
If $d \notin K$, then $\varphi_d(d)$ is undefined. Since $\varphi_d = \psi$, this means $\psi(d)$ is undefined. But the definition of $\psi$ says that when $\mathbb{1}_K(d)=0$, the computation $\psi(d)$ outputs $0$, so $\psi(d)$ is defined. This is again a contradiction.
Thus the assumption that $K$ is computable is false.
[guided]
The goal is to show that no computable procedure can decide membership in $K$. We argue by contradiction and assume that such a procedure exists. Formally, assume that the characteristic function
\begin{align*}
\mathbb{1}_K: \mathbb{N} &\to \{0,1\}
\end{align*}
is computable.
Using this hypothetical decision procedure, define a partial function
\begin{align*}
\psi: \mathbb{N} &\rightharpoonup \mathbb{N}
\end{align*}
by reversing the predicted halting behaviour on the diagonal. On input $n \in \mathbb{N}$, compute $\mathbb{1}_K(n)$. If $\mathbb{1}_K(n)=0$, output $0$; if $\mathbb{1}_K(n)=1$, run forever. This construction is computable as a partial computation because the only nontrivial test it performs is the assumed computable test for $K$.
Since $(\varphi_e)_{e \in \mathbb{N}}$ enumerates all partial computable functions, the partial computable function $\psi$ has some index. Choose $d \in \mathbb{N}$ such that
\begin{align*}
\varphi_d = \psi.
\end{align*}
Now ask whether $d$ belongs to $K$. By definition of $K$,
\begin{align*}
d \in K \iff \varphi_d(d) \text{ is defined}.
\end{align*}
But since $\varphi_d = \psi$, this is equivalent to asking whether $\psi(d)$ is defined.
If $d \in K$, then $\mathbb{1}_K(d)=1$. The definition of $\psi$ says that in this case $\psi(d)$ runs forever, so $\psi(d)$ is undefined. Since $\varphi_d=\psi$, this says $\varphi_d(d)$ is undefined, contradicting $d \in K$.
If $d \notin K$, then $\mathbb{1}_K(d)=0$. The definition of $\psi$ says that in this case $\psi(d)$ outputs $0$, so $\psi(d)$ is defined. Since $\varphi_d=\psi$, this says $\varphi_d(d)$ is defined, contradicting $d \notin K$.
Both possible truth values of $d \in K$ lead to contradictions. Therefore the assumed computable decision procedure for $K$ cannot exist, and $K$ is not computable.
[/guided]
[/step]
[step:Conclude that the inequality of Turing degrees is strict]
We have proved $0 \leq 0'$. It remains to rule out equality.
If $0' = 0$, then $K$ would lie in the computable Turing degree. Equivalently, $K$ would be computable. This contradicts the diagonal argument above. Hence $0' \neq 0$.
Combining $0 \leq 0'$ with $0' \neq 0$, we obtain
\begin{align*}
0 < 0'.
\end{align*}
This proves that the halting degree is nonzero.
[/step]
