Exercise 6.1
(a) Give a complete derivation in tree format showing that $⊥≡Πα : ∗. α$ is legal in λC (cf. Exercise 3.5).
(b) The same for $⊥→⊥$.
(c) To which systems of the λ-cube does $⊥$ belong? And $⊥→⊥$?
(a) The following is a tree derivation of $⊥≡Πα : ∗. α$.
$$(1) \quad \emptyset \vdash * \; : \; \Box \quad (sort)$$
$$\frac{(1) \quad \emptyset \vdash * \; : \; \Box}{(2) \quad \alpha:* \vdash \alpha \; : \; *} \quad (var)$$
$$\frac{(1) \quad \emptyset \vdash * \; : \; \Box \quad \quad (2) \quad \alpha:* \vdash \alpha \; : \; *}{(3) \quad \emptyset \vdash \Pi \alpha:*.\alpha \; : \; *} \quad (form)$$
So $\bot \equiv \Pi \alpha:*.\alpha$ is legal in λC since in the empty context $\bot$ has type $*$.
(b) We continue from above.
$$\frac{(3) \quad \emptyset \vdash \bot \; : \; *}{(4) \quad x:\bot \vdash x \; : \; \bot} \quad (var)$$
$$\frac{(3) \; \emptyset \vdash \bot \; : \: * \quad \quad (4) \quad x:\bot \vdash \bot \; : \; *}{(5) \quad \emptyset \vdash \bot \to \bot \; : \; *} \quad (form)$$
So $\bot \to \bot$ is legal in λC since in the empty context $\bot \to \bot$ has type $*$.
(c) Let's remind ourselves of the 8 systems of the λ-cube.
Let's first consider $\bot$. From the above tree derivation we can it is the result of the (form) rule with $s_1 = \Box$ and $s_2 = *$. The combination is $(\Box, *)$. That means $\bot$ belongs only in λ2, λω, λP2, and λC.
Now let's consider $\bot \to \bot$. From the tree derivation we can see it is the result of the (form) rule with $s_1=*$ and $s_2=*$. The combination is $(*,*)$. This suggests $\bot \to \bot$ belongs to all 8 systems of the λ-cube. However, since the sub-term $\bot$ can only be derived in λ2, λω, λP2, and λC, then $\bot \to \bot$ belongs only to those same systems.
