Exercise 6.8
(a) Let $Γ ≡ S : *, P : S → *$. Find an inhabitant of the following type $N$ in context $Γ$, and prove your answer by means of a shortened derivation:
$$N ≡ [Πα : *. ((Πx : S. (P x →α)) →α)] → [Πx : S. (P x →⊥)] →⊥$$
(b) Which is the smallest system in the λ-cube in which your derivation may be executed?
(c) The expression $Πα : ∗. ((Πx : S. (P x →α)) →α$ may be considered as an encoding of $∃_{x∈S}(P(x))$. (We shall show this in Section 7.5.) In Section 7.1 we make plausible that $A →⊥$ may be considered as an encoding of the negation $¬A$. With these things in mind, how can we interpret the content of the expression $N$? (See also Figure 5.2.)
(a) The shortened derivation below proves the inhabitant is
$$\lambda f:[\Pi \alpha : *. ((\Pi x : S. (P x \to \alpha)) \to \alpha)].\lambda g:[\Pi x : S. (P x \to \bot)]. f \bot g$$
(b) The ∏-types and their corresponding (form) types are:
- $S \to *$ corresponds to $(*, \Box)$
- $(Px \to \alpha)$ corresponds to $(*,*)$
- $\Pi x:S.(Px \to \alpha)$ corresponds to $(*,*)$
- $((\Pi x:S.(Px \to \alpha))\to \alpha)$ corresponds to $(*,*)$
- $\Pi \alpha:*.((\Pi x:S.(Px \to \alpha))\to \alpha)$ corresponds to $(\Box,*)$
- $\bot$ corresponds to $(\Box,*)$
- $(Px \to \bot)$ corresponds to $(*,*)$
- $\Pi x:S.(Px \to \bot)$ corresponds to $(*,*)$
- $[\Pi x:S.(Px \to \bot)] \to \bot$ corresponds to $(*,*)$
- $[Πα : *. ((Πx : S. (P x →α)) →α)] → [Πx : S. (P x →⊥)] →⊥$ corresponds to $(*,*)$
The minimal system is therefore λP2.
(c) The interpretation of N is
$$\exists_{x \in S} (P(x)) \implies \neg (\forall_{x\in S}(\neg P(x) ) )$$
In words, if there exists at least one $x \in S$ for which $P(x)$ is true, that implies it is not the case that $P(x)$ is false for all $x \in S$.
