The proofs I have so far seen for the undecidability of $\beta$-normalisation all make use of Gödel numbering in order to first prove the more general Scott-Curry theorem. As an exercise, I have tried to write a proof that does not use Gödel numbering and would appreciate some feedback on whether it is sound/complete, and whether there is redundancy or not. (Some trivial facts are left implicit, such as the fact that if $X =_\beta Y$, then $X$ and $Y$ both normalise or they are both unnormalisable.)
Some preliminary conventional definitions: \begin{aligned} \mathbf{I} &\; \equiv (\lambda x.x) \\ \Omega &\; \equiv (\lambda x.xx)(\lambda x.xx) \end{aligned}
Note that I assume the Turing completeness of the $\lambda$-calculus.
Theorem. $\beta$-normalisation is undecidable. That is, there does not exist a combinator $D$ such that $\forall X \in \Lambda$: \begin{aligned} DX =_\beta \mathbf{T} \; &\Longleftrightarrow X \text{ has a } \beta\text{-normal form} \\ DX =_\beta \mathbf{F} \; &\Longleftrightarrow X \text{ has no } \beta\text{-normal form} \end{aligned} with $\mathbf{T}$, $\mathbf{F}$ two distinct $\beta$-nfs.
Proof. Suppose $D$ exists.
According to Böhm's theorem, since $\mathbf{T}$ and $\mathbf{F}$ are distinct $\beta$-nfs, $\exists L_1,\ldots,L_n$ with $n \geq 0$ such that \begin{aligned} \mathbf{T}L_1\ldots L_nAB \; &=_\beta A \\ \mathbf{F}L_1\ldots L_nAB \; &=_\beta B \end{aligned}
Define $\mathbf{P} \equiv (\lambda x.D(xx)L_1 \ldots L_n\Omega \mathbf{I})$.
$\mathbf{PP}$ either has a $\beta$-nf or it does not.
$\mathbf{PP}$ has a $\beta$-nf, i.e. $D(\mathbf{PP}) =_\beta \mathbf{T}$. Then: \begin{aligned} \mathbf{PP} \; &\equiv (\lambda x.D(xx)L_1 \ldots L_n\Omega \mathbf{I}) \mathbf{P} \\ &=_\beta D(\mathbf{PP}) L_1 \ldots L_n \Omega \mathbf{I} \\ &=_\beta \mathbf{T}L_1 \ldots L_n \Omega \mathbf{I} \\ &=_\beta\Omega \end{aligned} Since $\Omega$ has no $\beta$-nf, neither does $\mathbf{PP}$. Contradiction.
$\mathbf{PP}$ has no $\beta$-nf, i.e. $D(\mathbf{PP}) =_\beta \mathbf{F}$. Then: \begin{aligned} \mathbf{PP} \; &\equiv (\lambda x.D(xx)L_1 \ldots L_n\Omega \mathbf{I}) \mathbf{P} \\ &=_\beta D(\mathbf{PP}) L_1 \ldots L_n \Omega \mathbf{I} \\ &=_\beta \mathbf{F}L_1 \ldots L_n \Omega \mathbf{I} \\ &=_\beta\mathbf{I} \end{aligned} Since $\mathbf{I}$ has a $\beta$-nf, so does $\mathbf{PP}$. Contradiction.
Thus there can be no such $D$. $\square$
One particular question:
Can I make assumptions about $\mathbf{T}$ and $\mathbf{F}$ without it affecting the validity of my proof? For example, a decider is usually understood to map each input to $\{0, 1\}$ or $\{True, False\}$. Might I just as well choose $T \equiv (\lambda xy.x)$, $F \equiv (\lambda xy.y)$, $P \equiv (\lambda x. D(xx) \Omega \mathbf{I})$ and thereby drop the dependency on Böhm's theorem altogether?
To me it seems unsatisfactory, because in that case it might not be clear that the contradiction cannot be avoided by choosing different $\lambda$ representatives for $\mathbf{T}$ and $\mathbf{F}$. Then again, I have seen a proof that explicitly used the Church numerals for 0 and 1 and a different choice for $P$.
Other feedback is very welcome too.