Exercise 7.9
Verify that each of the following expressions is a tautology in constructive logic, (1) by giving a proof in first order natural deduction, and (2) by giving a flag-style derivation in λC:
(a) $∀x∈S(¬P(x) ⇒(P(x) ⇒(Q(x)∧R(x))))$
(b) $∀x∈S(P(x)) ⇒∀y∈S(P(y)∨Q(y))$
(a) The following is a first order natural deduction.
The corresponding type is
$$ \Pi x:S . ((Px \to \bot) \to (Px \to ( \Pi C:*.(Qx \to Rx \to C) \to C ) ) ) $$
with a context of $S:*, \; P, Q, R : S \to*$.
The following is a flag-style derivation in λC.
(b) The following is a first order natural deduction.
The corresponding type is
$$( \Pi x:S.Px ) \to ( \Pi y:S. ( \Pi C:*.( (Py \to C) \to (Qy \to C) \to C) ) ) $$
with a context of $S:*, \; P, Q, : S \to*$.The following is a flag-style derivation in λC.
