Exercise 7.6
Verify that each of the following expressions is a tautology in constructive logic, by giving a (‘second order’) flag-style derivation in λC. Use Exercise 7.4 and Section 7.2, I.
(a) $¬A ⇒ ¬(A ∧ B)$
(b) $¬(A ∧ ¬A)$
(c) $¬(A ∧ B) ⇒ (A ⇒ ¬B)$
Constructive logic means we don't have the double negation or law of the excluded middle.
(a) The type corresponding to $¬A ⇒ ¬(A ∧ B)$ is
$$ (A \to \bot) \to ( \Pi C:*.(A \to B \to C) \to C) \to \bot $$
The following is a derivation of an inhabitant of this type.
(b) The type corresponding to $¬(A ∧ ¬A)$ is
$$ ( \Pi C:*.(A \to (A \to \bot ) \to C) \to C) \to \bot $$
The following is a derivation of an inhabitant of this type.
(a) The type corresponding to $¬(A ∧ B) ⇒ (A ⇒ ¬B)$ is
$$ (( \Pi C:*.(A \to B \to C) \to C) \to \bot) \to (A \to (B \to \bot)) $$
The following is a derivation of an inhabitant of this type.
