Help for a Borkowski/Slupecki-Style Natural Deduction Proof

Question

Good afternoon,

i want to prove the following rule in the natural deduction calculus of Borkowski and Slupecki: $ \frac {\lnot(P\rightarrow Q)}{P \land \lnot Q} $

Up until now, I got to the point of deriving $\lnot Q$:

1. $\lnot(P\rightarrow Q)$ |Assumption
   11. $Q$ | Additional Assumption (AA)
   12. $P \rightarrow Q$ | EI, 1.1
2. $Q \rightarrow (P \rightarrow Q)$ |Elimination of additional assumption 1.1
3. $Q \rightarrow \lnot (P\rightarrow Q)$ | EI, 1
4. $\lnot Q$ | EN 2,3

However, I'm lost trying to derive $P$. Does anyone have an idea? I would appreciate any hint.

The following are the primary rules to be used in the system of Borkowski and Slupecki (I hope the German notation is self-explanatory - note that EI means "conditional introduction" as "E" stands for "Einführung", i.e. "introduction" in German and not "elimination" as you would expect in English):

Answer 1

Assuming what you did on line 2 is indeed a rule of the system (it is not listed among your rules ... but it is of course a conditional proof technique), you can do this: