Exercise 7.3
Give λC-derivations proving that the following expressions are tautologies in classical logic (so you may use DN or ET):
(a) $(A ⇒B) ⇒(¬B ⇒ ¬A)$
(b) $(¬B ⇒ ¬A) ⇒(A ⇒B)$
(a) The expression $(A ⇒B) ⇒(¬B ⇒ ¬A)$ is equivalent to the following type:
$$ (A \to B) \to ((B \to \bot) \to (A \to \bot)) $$
The following is a λC derivation.
Note this derivation didn't use DN or ET.
(b) The expression $(¬B ⇒ ¬A) ⇒(A ⇒B)$ is equivalent to the following type:
$$ ((B \to \bot) \to (A \to \bot)) \to (A \to B) $$
The following is a λC derivation.
