Exercise 3.12
As mentioned in Section 3.8, we have in λ2 the polymorphic Church numerals. They resemble the untyped Church numerals, as described in Exercises 1.10 and 1.13(b). For example:
$Nat ≡ Πα : ∗. (α →α) →α →α$,
$Zero ≡ λα : ∗. λf : α →α. λx : α. x$, having type Nat,
$One ≡ λα : ∗. λf : α →α. λx : α. f x$, with type Nat, as well,
$Two ≡ λα : ∗. λf : α →α. λx : α. f(f x)$.
We define $Suc$ as follows as a λ2-term:
$$Suc ≡λn : Nat . λβ : ∗. λf : β →β. λx : β. f(nβf x)$$
Check that $Suc$ acts as a successor function for the polymorphic Church numerals, by proving that $Suc \; Zero =_β One$ and $Suc \; One =_β Two$.
Let's start with $Suc \; Zero =_β One$.
$$\begin{align} Suc \; Zero & \equiv ( λn : Nat . λβ : ∗. λf : β →β. λx : β. f(nβf x) ) \; ( λα : ∗. λf : α →α. λx : α. x ) \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (λα : ∗. λf : α →α. λx : α. x) βf x) \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (λf : β →β. λx : β. x) f x) \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (λx : β. x) x) \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. fx \\ \\ &=_\beta One \tag*{$\Box$} \end{align}$$
Note the penultimate line is the definition of $One$ with the variable $\alpha$ renamed to $\beta$.
Now let's consider $Suc \; One =_β Two$.
$$\begin{align} Suc \; One & \equiv ( λn : Nat . λβ : ∗. λf : β →β. λx : β. f(nβf x) ) \; ( λα : ∗. λf : α →α. λx : α. f x ) \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (λα : ∗. λf : α →α. λx : α. fx) βf x) \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (λf : β →β. λx : β. fx) f x) \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (λx : β. fx) x) \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (fx) \\ \\ &=_\beta Two \tag*{$\Box$} \end{align}$$
Again the penultimate line is the definition of $Two$ with the variable $\alpha$ renamed to $\beta$.
