Exercise 7.2
(a) Formulate the double negation law (DN) as an axiom in λC.
(b) Verify that the following expression is a tautology in classical logic, by giving a corresponding flag-style derivation in λC (use DN):
$$(¬A ⇒A) ⇒A$$
(a) The double negation law is, for some proposition $A$,
$$\neg \neg A \implies A$$
Using the fact that $\neg A$ is encoded as $A \implies \bot$, the double negation law can be encoded as the following type being inhabited
$$((A \to \bot) \to \bot) \implies A$$
We can further abstract away the $A$, as follows
$$\Pi \alpha : *. ((\alpha \to \bot) \to \bot) \to \alpha$$
(b) The following is a flag-format derivation showing that $(¬A ⇒A) ⇒A$ is a tautology. It uses $i_{DN}$ instantiated with $A:*$.
