Prove the theorem $\vdash A \rightarrow (\neg B \rightarrow \neg(A \rightarrow B))$
I proved a variety of other theorems in the Theorem List that my university professors created http://mathsci2.appstate.edu/~cookwj/courses/math2510-spring2010/Proofs_in_L.pdf but I never quite understood how to do so. I'm not sure how to go about solving this.
$A \implies B \equiv \neg A \lor B$
$\neg (A \implies B) \equiv \neg(\neg A \lor B) \equiv A \land \neg B$
$(\neg B \implies \neg(A \implies B)) \equiv (\neg B \implies (A \land \neg B))$
$(\neg B \implies (A \land \neg B)) \equiv \neg \neg B \lor (A \land \neg B)\equiv B \lor (A \land \neg B)$
$A \implies (B \lor (A\land \neg B)) \equiv \neg A \lor (B \lor (A\land \neg B))$
$\neg A \lor (B \lor (A\land \neg B)) \equiv \neg A \lor ((B \lor A) \land (B \lor \neg B))$
$\equiv (\neg A \lor B \lor A) \land (\neg A \lor B \lor \neg B) \equiv (B \lor \top) \land (\neg A \lor \top) \equiv \top$
HINT
Assuming you have $\vdash \neg \neg A \to A$, you can quickly show that $A, \neg \neg (A \to B) \vdash B$, and then use that with the following instantiation of Axiom 3:
$(\neg \neg (A \to B) \to \neg B) \to ((\neg \neg (A \to B) \to B) \to \neg (A \to B)$
To obtain: $A, \neg B \vdash \neg \neg (A \to B) \to \neg (A \to B)$
And since $\vdash \neg \neg (A \to B) \to \neg \neg (A \to B)$
We can use Axiom 3 again:
$((\neg \neg (A\to B) \to \neg \neg (A \to B)) \to ((\neg \neg (A \to B) \to \neg (A \to B)) \to \neg (A \to B))$
To obtain: $A, \neg B \vdash \neg (A \to B)$
And now it's two applications of D.T. and you're there.
