Exercise 1.12
We define the λ-terms true and false (the booleans) and not (resembling the logical ¬-operator) by:
$true := λxy. x$ (so it happens that true ≡ K)
$false := λxy. y$ (and false ≡ zero)
$not := λz. z \; false \; true$
Show that $not(not\; p) =_β p$ for all λ-terms $p$, in each of the following two cases: (a) $p \to_β \; true$ or (b) $p \to _β \; false$.
Let's do some algebra first.
$$\begin{align} not(not \;p) & = (λz.z (false) (true)) ((λy.y (false) (true) ) p) \\ \\ & = (λz.z (λab.b) (λef.e) )((λy.y (λcd.d) (λgh.g) ) p) \\ \\ & \to (λz.z (λab.b) (λef.e) )(p (λcd.d) (λgh.g) ) \\ \\ & \to (p (λcd.d) (λgh.g) ) (λab.b) (λef.e) \end{align} $$
(a) When $p \to_β \; true$
$$\begin{align} not(not \; true) & \to ((true) (λcd.d) (λgh.g) ) (λab.b) (λef.e) \\ \\ &= ((λxy. x) (λcd.d) (λgh.g) ) (λab.b) (λef.e) \\ \\ & \to ( λcd.d ) (λab.b) (λef.e) \\ \\ & \to (λef.e) \\ \\ & = true \end{align} $$
(b) When $p \to_β \; false$
$$\begin{align} not(not \; false) & \to ((false) (λcd.d) (λgh.g) ) (λab.b) (λef.e) \\ \\ &= ((λxy. y) (λcd.d) (λgh.g) ) (λab.b) (λef.e) \\ \\ & \to ( λgh.g ) (λab.b) (λef.e) \\ \\ & \to (λab.b) \\ \\ & = false \end{align} $$
So we have shown $not(not\; p) =_β p$ .
