Is this proof for the undecidability of $\beta$-normalisation in $\lambda$-calculus valid?

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.

1. $\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.

2. $\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:

1. 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.

I'm a little late to the party, but I think it might be useful to provide some answer here.

Your theorem is correct, there is no combinator $D$ such that for all $\lambda$-terms $X$, $DX=_\beta\mathbf{T}$ if $X$ has a normal form and $DX=_\beta\mathbf{F}$ otherwise.

Your proof is correct, and you do not need Böhm's theorem: $L_1,\ldots, L_n$ is just the empty list here ($\mathrm{T}AB=A$ for example)! You could replace $\mathrm{T}$ and $\mathrm{F}$ with any other distinct normal forms, and your proof would go through in a similar way, but you would need Böhm's theorem to reduce to the case with $\mathrm{T}$ and $\mathrm{F}$.

The more general remark though, is this:

It is incorrect that the statement of the theorem given in your question is "Normalization of untyped $\lambda$-terms is undecidable."

You've proven something much weaker: it is impossible to decide normalization of a $\lambda$-term using only combinators. But there are much simpler things you already cannot do with combinators! For example, determining whether the head of $X$ is a $\lambda$-abstraction, an application or a variable is already impossible!

What you want to prove is that no such $D$ exists, even if you are given access to the code of $X$. This is equivalent to saying that there is no $D$ such that

$$D\lceil X\rceil =_\beta\mathbf{T}$$

if $X$ is normalizing and

$$D\lceil X\rceil =_\beta\mathbf{F}$$

otherwise, where $\lceil X\rceil$ is an encoding of $X$ using, e.g. Church numerals.

This is strictly more general than the previous question, since it's always possible to write some $E$ ("eval") combinator such that $E\lceil X\rceil=_\beta X$. It's also possible to answer the syntactic questions I asked above.

The fact that there is no "trick" using the internals of the definition of $X$ to determine whether it terminates is the true undecidability result, and its proof probably cannot be made much simpler than the ones involving the Scott-Curry theorem.

• Even later to this party, but if its still going, I don't see how that this cannot be considered a valid proof of the undecidability of $\beta$-normalization. This is a direct translation/adaptation of a valid proof of the Halting problem within Turing machines but this time using combinators as the underlying computing model. If one accepts the Church-Turing thesis, then combinators/lambda calculus/TM's are all equally as powerful so that such transference, instead, becomes a natural byproduct of this established equivalence. Commented Apr 11 at 6:06
• The implication seems to be that because CL is so "weak" as a computational model, any result about CL's inability to solve a given problem cannot possibly have any bearing on the problem's decidability. But this can't be right. A priori, accepting the Church-Turing thesis means accepting CL's equivalent computational power. Hence the proof of CL's own version of the Halting problem--- "there does not exist a combinator D such that PredH(D, X)" does demonstrate the undecidability of $\beta$-normalization ... Commented Apr 11 at 6:10
• precisely because of the Halting-like nature of PredH (i.e. there is no encoding "trick" that can get around this - it also establishes the "undecidability of CL" by definition). That it is also the case that "there does not exist a combinator D such that PredS(D, X)" where PredS, is the mentioned "syntactic predicate" doesn't have any bearing on this. It doesn't, for example, imply PredS's [counterfactual] undecidability and simply alerts us to the fact that, for this predicate, there is a "trick", namely, that ... Commented Apr 11 at 6:24
• ... in order to implement "syntactical predicates" on function arguments, those arguments need to be encoded - in other words, what it tells us is that CL as a computing model does not support intensionality instead requiring encoding to implement these decidable properties. Commented Apr 11 at 6:24
• In the context of a direct proof of CL's undecidability, this answer asserts that "The proof ... is entirely analogous to the same proof for Turing machines" which tends to refute the notion that the OP's proof here is "much weaker". Commented Apr 11 at 8:30