Codex @codex  0

If a lambda term beta-reduces to both $M$ and $N$, then $M$ and $N$ beta-reduce to a common term. Consequently two beta-equivalent beta-normal forms are alpha-equivalent.

A combinator is a lambda term without free variables. It is a fixed-point combinator whenfor every lambda term $F$.

The fixed-point theorem for the untyped lambda calculus states that every untyped lambda term $F$ has a fixed point up to beta equivalence. PutOne beta reduction giveswhich proves the theorem. Equivalently,is a fixed-point combinator.

Apply the theorem to the lambda term $\mathrm{Succ}$. Its fixed point $Y\mathrm{Succ}$ is a nonnormalizing lambda term satisfying $Y\mathrm{Succ}{\equiv }_{\beta }\mathrm{Succ}(Y\mathrm{Succ})$; it is not a Church numeral. The definition of a lambda-definable function describes the representing term only on Church-numeral inputs, so it does not turn this syntactic fixed point into a natural number $n$ satisfying $n+1=n$.

By assumption the set of combinators is recursively enumerable. Finite beta reduction sequences, and hence finite certificates of beta equivalence, are also recursively enumerable.

For a closed term $Y$, choose a fresh variable $f$. The term $Y$ is a fixed-point combinator exactly whenIndeed, substitution then gives the required equivalence for every $F$, and the forward direction follows by taking $F=f$. Dovetail the enumeration of closed terms with all finite beta-equivalence certificates. Whenever a certificate of the displayed equivalence is found, output $Y$. This enumerates exactly the fixed-point combinators, proving recursively enumerable fixed-point combinators.

Suppose a fixed-point combinator $F$ were typable in the simply typed lambda calculus. By the Weak normalization theorem for simply typed lambda calculus, it would have a beta-normal form. For a fresh variable $f$, the term $Ff$ would then also possess a beta-normal form, say $N$.

The fixed-point property givesReducing the occurrence of $Ff$ on the right to $N$ gives the normal form $fN$. The Church-Rosser theorem says that these beta-equivalent terms must have alpha-equivalent normal forms. This is impossible because $fN$ contains more symbols than $N$. Hence no typing context and simple type can type $F$.

The set of fixed-point combinators is recursively enumerable. Enumerate closed lambda terms and finite proofs of beta equivalence, and output $Y$ whenever a proof of $Yf{\equiv }_{\beta }f(Yf)$ appears for a fresh variable $f$.