Exercise 7.1
Verify that each of the following expressions is a tautology in constructive logic, (1) by giving a proof in natural deduction, and (2) by giving a corresponding derivation in λC.
You may employ the flag style for the derivations, as in the examples given in the present chapter.
(a) $B ⇒(A ⇒B)$
(b) $¬A ⇒(A ⇒B)$
(c) $(A ⇒¬B) ⇒((A ⇒B) ⇒¬A)$
(d) $¬(A ⇒B) ⇒¬B$ (hint: use part (a)).
This summary of natural deduction was helpful in this exercise (pdf).
(a) The following is a natural deduction proof in tree format.
The following is a derivation in λC in flag notation. It shows the type $B \to (A \to B)$ is inhabited by $\lambda b:B. \lambda a:A.b$ in the context $A,B:*$.
(b) The following is a natural deduction proof in tree format. We replace $\neg A$ with the equivalent $A \to \bot$.
The following is a derivation in λC in flag notation. It shows the type $(A \to \bot) \to (A \to B)$ is inhabited by ${\lambda f: A \to \bot.\lambda a:A. faB$ in the context $A,B:*$.
(c) The following is a natural deduction proof in tree format. We replace $\neg A$ with the equivalent $A \to \bot$.
The following is a derivation in λC in flag notation. It shows the type $ (A \implies (B \implies \bot)) \implies ((A \implies B) \implies (A \implies \bot)))$ is inhabited by $\lambda f:A \to (B \to \bot) .\lambda g:A \to B. \lambda a:A . fa(ga)$ in the context $A,B:*$.
(d) The following is a natural deduction proof in tree format. We replace $\neg A$ with the equivalent $A \to \bot$.
The following is a derivation in λC in flag notation. It shows the type $((A \implies B) \implies \bot) \implies ( B \implies \bot)$ is inhabited by $\lambda f:(A \to B) \to \bot.\lambda b:B.f(\lambda a:A.b) $ in the context $A,B:*$.
