Intuitionistic Proof of $(a \Rightarrow b) \Rightarrow (\lnot b \Rightarrow \lnot a)$

Question

I'm trying to prove

$$(a \Rightarrow b) \Rightarrow (\lnot b \Rightarrow \lnot a)$$

A seemingly natural way to start is by assuming the left side, as well as assuming a. This ends up proving what I want but I can't eliminate my assumption of a.

Any insight beyond a strictly mechanical derivation are appreciated.

Answer 1

1. Assume $a \to b$.
2. Assume $\lnot b$.
3. Assume $a$.
4. Then $b$.
5. Then $\bot$.
6. Eliminating (3), $\lnot a$.
7. Eliminating (2), $\lnot b \to \lnot a$.
8. Eliminating (1), $(a \to b) \to (\lnot b \to \lnot a)$.

I think everything is clear up to step 5; beyond that you need a clear grasp of the notion of conditional proof. (You also need to remember that $\lnot x$ is an abbreviation for $x \to \bot$.)

Answer 2

Assume "a => b" and "not b". Then "not a" because: If "a", then "b", but we assumed "not b". Contradiction, so "not a" holds.