Propositional Logic Proof of $\vdash \lnot (p \supset q) \supset (p \land \lnot q)$ $\vdash \lnot (p \supset q) \supset (p \land \lnot q)$
I need to prove the above proposition via intuitionistic logic rules and/or natural logic rules. I guess it is not possible to prove with intuitionistic logic becuase we cannot use PBC rule.
 A: It is evidently enough to prove (i) $\neg(p \supset q) \vdash p$ and (ii) $\neg(p \supset q) \vdash \neg q$. And plainly we can't get the target result if we can't prove those (assuming $\land$-elimination and modus ponens are available).
But note (i) is inuitionistically invalid, so we indeed do need to be working in a classical framework. (Given (i), we'd have in particular $\neg(p \supset \bot) \vdash p$, i.e. $\neg\neg p \vdash p$, as Henning Makholm remarked.)
For (i) a proof with a standard set of ND rules for the conditional and classical negation would go
$$\begin{array}{cccccccl}
1 & \neg(p \supset q) & & & & & & premiss\\
2 & & | & \neg p & & & & assumption\\
3 & & | & & | & p  & & assumption\\
4 & & | & & | & \bot  & & from\ 2, 3\\
5 & & | & & | & q  & & from\ 4\\
6 & & | & (p \supset q) & & & & from\ 3-5\\ 
7 & & | & \bot & & & & from\ 1, 6\\
8 & \neg\neg p & & & & & & from\ 2-7\\ 
9 & p & & & & & & from\ 8, DN\\
\end{array} $$
Note the use of the intuitionistically unwarranted step at the last line. 
For (ii) we can argue
$$\begin{array}{cccccccl}
1 & \neg(p \supset q) & & & & & & premiss\\
2 & & | & q & & & & assumption\\
3 & & | & & | & p  & & assumption\\
4 & & | & & | & q  & & from\ 2, reit\\
5 & & | & (p \supset q) & & & & from\ 3-4\\ 
6 & & | & \bot & & & & from\ 1, 5\\
7 & \neg q & & & & & & from\ 2-6
\end{array} $$
Obviously, with a different set of classical ND rules, the proofs will have to go differently but similarly, mutatis mutandis.
A: My proof strategy basically assumes the negation of each part of the conjunction in turn, shows that each part leads to a contradiction, then conjuncts the results.  
With the rules of conditional introduction (Ci), conditional elimination (Co), conjunction introduction (Ki), negation introduction (Ni) as "if we have a derivation starting with p, and we derive a contradiction, we may infer Np, the negation of p.", and negation elimination (No) "if we have a derivation starting with Np, and we derive a contradiction, we may infer p." a possible proof (in Polish notation which helps identify the type of wff you have, which can help when thinking of proof techniques) goes as follows:
1  |     NCpq hypothesis
2  ||    Np hypothesis
3  |||   p hypothesis
4  ||||  Nq hypothesis
5  ||||  KpNp 2, 3 Ki
6  |||   q 4-5 No
7  ||    Cpq 2-6 Ci
8  ||    KCpqNCpq 1, 7 Ki
9  |     p 2-8 No
10 ||    q hypothesis
11 |||   p hypothesis
12 ||||  q hypothesis
13 |||   Cqq 12-12 Ci
14 |||   q 10, 13 Co
15 ||    Cpq 11-14 Ci
16 ||    KCpqNCpq 15, 1 Ki
17 |     Nq 10-16 Ni
18 |     KpNq 9, 17 Ki
19       CNCpqKpNq 1-18 Ci

