Exercise 5.9
Give proofs that the following propositions are tautologies, (first) in natural deduction and (second) by means of a shortened λP-derivation.
(a) $∀_{x∈S} (Q(x)) ⇒ ∀_{y∈S}(P(y) ⇒Q(y))$
(b) $∀_{x∈S}(P(x) ⇒Q(x)) ⇒ (∀_{y∈S} (P(y)) ⇒∀_{z∈S} (Q(z)))$
(a) The following is a natural deduction.
The corresponding λP type is
$$ \Pi a:(\Pi x:S . (Qx)) . ( \Pi y:S.(\Pi b:(Py). Qy)) $$
where the context is $S:*, Q:S \to *, P:S \to *$.
By inspection, an inhabitant is
$$ \lambda a:(\lambda x:S.ax).(\lambda y:S . (\lambda b:(Py).ay )) $$
The following is a shortened λP derivation.
(b) The following is a natural deduction.
The corresponding λP type is
$$ \Pi a: (\Pi x:S.(\Pi b:(Px).Qx)) . ( \Pi c:(\Pi y:S.Py) . (\Pi z:S.Qz)) $$
where the context is $S:*, Q:S \to *, P:S \to *$.
By inspection, an inhabitant is
$$ \lambda a: (\Pi x:S.(\Pi b:(Px).Qx)) . ( \lambda c:(\Pi y:S.Py) . ( \lambda z:S. az(cz) )) $$
The following is a shortened λP derivation.
