Exercise 7.5
As Exercise 7.2(b):
(a) $¬(A ⇒B) ⇒A$ (hint: use Exercise 7.1(b))
(b) $¬(A ⇒B) ⇒(A∧¬B)$ (hint: use Exercise 7.1(d))
As a reminder of exercise 7.2(b), we need to "verify that the following expression is a tautology in classical logic, by giving a corresponding flag-style derivation in λC (use DN)".
(a) The type corresponding to $¬(A ⇒B) ⇒A$ is
$$ ((A \to B) \to \bot) \to A $$
The following is a λC derivation of an inhabitant of this type.
(b) The type corresponding to $¬(A ⇒B) ⇒(A∧¬B)$ is
$$((A \to B) \to \bot) \to \Pi C:*.((A \to (B \to \bot) \to C) \to C)$$
The following is a λC derivation of an inhabitant of this type.
