= Solution
The <Church numeral> corresponding to the <natural number> $n$ is
$$
c_n=\lambda f.\lambda x.f^n x.
$$
A function $g:\mathbb N^k\to\mathbb N$ is a <lambda-definable function> if some closed lambda term $G$ satisfies
$$
G c_{n_1}\cdots c_{n_k}\equiv_\beta c_{g(n_1,\ldots,n_k)}
$$
for all natural numbers $n_1,\ldots,n_k$.
Define
$$
\operatorname{Succ}=\lambda n.\lambda f.\lambda x.f(nfx).
$$
Then <beta reduction> gives
$$
\operatorname{Succ}\,c_n
\equiv_\beta\lambda f.\lambda x.f(f^n x)
=c_{n+1}.
$$
Therefore the <successor function> is lambda-definable; this is the <lambda definition of the successor function>.
Back to article page
