Hmm, ex falso isn't part of this method, we're supposed to solve disjunction by rewriting it to an implication.

Which brings me to my next question:

Code:

Derive: ((P => Q) => ~P) => (P => ~Q)
(P => Q) => ~P [ 1, H]
P [ 2, H]
Q [ 3, H]
{Now, I've to conclude false from Q. I have both a P and a ~P in my premiss,
from which I can derive a contradiction.
But, how am I allowed to eliminate the ~P from 1?
Since I have both P and Q assumed I would say I actually have P => Q,
on the other hand, introducing the => means I;ve to end the assumption 'Q'.
^-Intro isn't useful either? Or is it possible to eliminate
the P=>Q on the basis that P ^ Q is a stronger proposition than P=>Q?
I know I've to 'get' the ~P, but I'm not sure by which rule I'm allowed to do this.}
{ One possibility I've explored is this: }
P => Q [H]
~P [ =>E 1]
False [Contradiction P, ~P]
~(P => Q) [False Intro on P => Q and False]
False [Contradiction P=>Q, ~(P =>Q), but is this allowed???]
~Q
P => ~Q
((P => Q) => ~P) => (P => ~Q)