Exercise 5.8
(a) Let $Γ ≡ S : *, P : S → *, Q : S → *$. Find an inhabitant of $\Pi x : S. P x → Qx → Px$ with respect to $Γ$, and give a corresponding (shortened) derivation.
(b) Give a natural deduction proof of the corresponding logical expression.
(a) Given the context and variable $x:S$,
$$\begin{align} S &: * \\ P &: S \to * \\ Q &: S \to * \\ x &: S\end{align}$$
we have
$$\begin{align} Px &: * \\ Qx &: *\end{align}$$
By inspection, an inhabitant of $\Pi x : S. P x → Qx → Px$ should be
$$ \lambda x : S. \lambda p: P x. \lambda q: Qx . p $$
The following is a shortened derivation of the inhabitant and its type.
(b) The type $\Pi x : S. P x → Qx → Px$ corresponds to the following logical expression.
$$ \forall_{x \in S} ( \; P(x) \implies Q(x) \implies P(x) \; ) $$
The following is a natural deduction of this logical statement.
