Exercise 7.8
Give λC-derivations verifying the following tautologies of constructive logic (hint: use Exercise 7.7 and Section 7.2):
(a) $(A∨B) ⇒(B ∨A)$
(b) $¬(A∨B) ⇒(¬A∧¬B)$
(c) $(¬A∧¬B) ⇒¬(A∨B)$
Constructive logic means we don't have the double negation rule or the law of the excluded middle.
(a) The type corresponding to $(A∨B) ⇒ (B ∨ A)$ is
$$ (\Pi C:*.(A \to C) \to (B \to C) \to C) \to (\Pi C:*.(B \to C) \to (A \to C) \to C) $$
The following is a λC derivation of an inhabitant of this type.
(b) The type corresponding to $¬(A∨B) ⇒(¬A∧¬B)$ is
$$ ((\Pi C:*.(A \to C) \to (B \to C) \to C) \to \bot) \to (\Pi D:*.((A \to \bot) \to (B \to \bot) \to D) \to D) $$
The following is a λC derivation of an inhabitant of this type. The derivation uses $P$ and $Q$ as abbreviations for longer expressions.
(c) The type corresponding to$(¬A∧¬B) ⇒¬(A∨B)$ is
$$ (\Pi D:*.((A \to \bot) \to (B \to \bot) \to D) \to D) \to ((\Pi C:*.(A \to C) \to (B \to C) \to C) \to \bot) $$
The following is a λC derivation of an inhabitant of this type.
