Exercise 7.14
Let $Γ ≡ S : *, P : S →*, Q : S →*$. Consider the following λC-expression:$$\begin{gather}M ≡ λu : (∃x : S. (P x∧Qx)). λα : ∗. λv : (Πx : S. (P x →α)). \\ uα(λy : S. λw : (P y∧Qy). vy(w(P y)(λs : P y. λt : Qy. s)))\end{gather}$$
(a) Find a type $N$ such that $Γ ⊢M : N$.
(b) Which logical tautology is expressed by $N$ and proved by $M$?
(c) Give a derivation of $Γ ⊢M : N$.
(a) The following derives $M$ and in doing so, establishes $N$ as
$$(\exists x : S. (P x \land Qx)) \quad \to \quad \Pi \alpha:*.( (\Pi x:S.(Px \to \alpha)) \to \alpha)$$
(b) The logical tautology is
$$\exists _{x \in S}(P (x) \land Q(x)) \; \implies \; \exists_{x \in S}(P(x))$$
That is, if there exists an $x$ in $S$ such that $P(x)$ and $Q(x)$ are true, then there exists an $x$ in $S$ such that $P(x)$ is true.
(c) A derivation is given above in (a).
