Exercise 1.13
Consider the λ-terms zero, true and false from Exercises 1.10 and 1.12.
Let $iszero := λz. z(λx. \; false) \; true$.
(a) Prove that iszero zero reduces to true.
(b) A natural number $n > 0 $ may be represented by the following Church numeral: $λfx. f(f(...(x)))$, with $n$ copies of the variable $f$.
Prove that iszero n reduces to false for any Church numeral $n$ except 0. (Consequently, iszero represents a test-for-zero.)
(a)
$$\begin{align} iszero \; zero & = (λz. z(λx. \; false) \; true) \; zero \\ \\ & = (λz. z(λx. (λab . b)) (λcd.c)) (λfx.x) \\ \\ & \to (λfx.x) (λx. (λab . b)) (λcd.c) \\ \\ & \to (λcd.c) \\ \\ & = true \end{align}$$
(b) We'll do this by induction, first showing that iszero 1 reduces to false, then showing iszero $n$ reduces to false implies iszero $n+1$ reduces to false.
The base case $n=1$.
$$\begin{align} iszero \; 1 & = (λz. z(λx. \; false) \; true) \; 1 \\ \\ & = (λz. z(λx. (λab . b)) (λcd.c)) \; (λfx. f x) \\ \\ & \to (λfx.f x)(λx. (λab . b)) (λcd.c) \\ \\ & \to (λx. (λab . b)) (λcd.c) \\ \\ & \to (λab . b) \\ \\ & = false \end{align}$$
The induction step, using inductive hypothesis $iszero \; n \to false$
$$\begin{align} iszero \; (n+1) & = (λz. z(λx. \; false) \; true) \; (n+1) \\ \\ & = (λz. z(λx. (λab . b)) (λcd.c)) \; (λfx. f^{n+1} x) \\ \\ & \to (λfx.f^{n+1} x)(λx. (λab . b)) (λcd.c) \\ \\ & \to (λx. (λab . b))^{n+1} (λcd.c) \\ \\ & = (λx. (λab . b)) (λx. (λab . b))^{n} (λcd.c) \\ \\ & \to (λx. (λab . b)) \; false \; \text{ using inductive hypothesis} \\ \\ & = (λx. (λab . b)) \; (λcd.d) \\ \\ & \to (λab . b) \\ \\ & = false \end{align}$$
So by induction we have shown iszero $n$, for $n > 0$.
