Church encoding

Remarks

Example: the successor function is $\lambda$-definable by $\mathsf{S} = \lambda n.\, \lambda f.\, \lambda x.\, f\, (n\, f\, x)$. Indeed, $\mathsf{S}\, \overline{n} \to_\beta \lambda f.\, \lambda x.\, f\, (\overline{n}\, f\, x)$, and $\overline{n}\, f\, x \twoheadrightarrow_\beta f^n\, x$, so the result is $\lambda f.\, \lambda x.\, f^{n+1}\, x = \overline{n+1}$. Addition is defined by $\lambda m.\, \lambda n.\, \lambda f.\, \lambda x.\, m\, f\, (n\, f\, x)$ and multiplication by $\lambda m.\, \lambda n.\, \lambda f.\, m\, (n\, f)$.

Non-example: $\lambda f.\, \lambda x.\, x\, f$ is not a Church numeral. Its body applies $x$ to $f$, not $f$ some number of times to $x$.

The conditional "if $b$ then $P$ else $Q$" is just $b\, P\, Q$, since $\mathsf{T}\, P\, Q \twoheadrightarrow_\beta P$ and $\mathsf{F}\, P\, Q \twoheadrightarrow_\beta Q$. By results of Church and Kleene, the $\lambda$-definable functions are exactly the total computable functions.