Solution

ID: past-exam-of-the-mathematics-course-of-the-university-of-cambridge/2022/iii/paper-120/3/b/solution

A combinator is a lambda term without free variables. It is a fixed-point combinator when
for every lambda term .
The fixed-point theorem for the untyped lambda calculus states that every untyped lambda term has a fixed point up to beta equivalence. Put
One beta reduction gives
which proves the theorem. Equivalently,
is a fixed-point combinator.
Apply the theorem to the lambda term . Its fixed point is a nonnormalizing lambda term satisfying ; 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 satisfying .

New to topics? Read the docs here!