How to solve ~(P → Q) : P & ~Q by natural deduction? I'm trying to solve the following by natural deduction:
~(P → Q) : P & ~Q
It's a trivial problem if identities are used, as can be seen by the following:

{1}      1.   ~(P → Q)                    Prem.
{1}      2.   ~(~P ∨ Q)                   1 Mat. Impl.
{1}      3.   ~~P & ~Q                    2 De Morgan's
{1}      4.   P & ~Q                      3 DNE

Starting from step 2 of the previous proof, it's also fairly straightforward to reach a conclusion using natural deduction; i.e. starting from ~(~P ∨ Q), which is an identity of ~(P → Q):
~(~P ∨ Q) :  P & ~Q

{1}      1.   ~(~P ∨ Q)                   Prem.
{2}      2.   ~P                          Assum.
{2}      3.   ~P ∨ Q                      2 ∨I
{1,2}    4.   ~(~P ∨ Q) & (~P ∨ Q)        1,3 &I
{1}      5.   P                           2,4 RAA
{6}      6.   Q                           Assum.
{6}      7.   ~P ∨ Q                      6 ∨I
{1,6}    8.   ~(~P ∨ Q) & (~P ∨ Q)        1,7 &I
{1}      9.   ~Q                          6,8 RAA
{1}      10.  P & ~Q                      5,9 &I

I also found that it's fairly easy to conclude ~Q:

{1}      1.   ~(P → Q)                    Prem.
{2}      2.   Q                           Assum.
{3}      3.   P                           Assum.
{2,3}    4.   P & Q                       2,3 &I
{2,3}    5.   Q                           4 &E
{2}      6.   P → Q                       3,5 CP
{1,2}    7.   ~(P → Q) & (P → Q)          1,6 &I
{1}      8.   ~Q                          2,7 RAA
...
{1,2}    12.  P & ~Q

In spite of how easy it looks, I can't figure out how to do it. I believe it can be done in 12 steps. Thanks!
 A: We need Double Negation and I need 13 steps:
1) $\lnot (P \to Q)$ --- premise
2) $Q$ --- assumed [a]
3) $P \to Q$ --- from 2) by $\to$I
4) $\bot$ --- from 1) and 3)
5) $\lnot Q$ --- from 2) and 4), discharging [a]
6) $\lnot P$ --- assumed [b]
7) $P$ --- assumed [c]
8) $\bot$ --- form 6) and 7)
9) $Q$ --- from 8) by $\bot$E: $\bot \vdash \varphi$
10) $P \to Q$ --- from 7) and 9) by $\to$I, discharging [c]
11) $\bot$ --- from 1) and 10)
12) $P$ --- from 6) and 11) by Double Negation, discharging [b]

13) $P \land \lnot Q$ --- from 5) and 12) by $\land$I.

A: Although some identities such as material implication are not defined as inference rules in natural deduction systems, one can always derive the desired result when needed. It is useful to know how to do that.
Consider the following proof in a Fitch-style proof checker:

Although you were able to reach line 10 in one move using equivalences it took lines 2-9 for me to derive the same result.  What is important is that I was able to derive the result. What is useful to know is that one can convert from conditionals to disjunctions and negations if one has to.
Note that this subproof would have been shorter if I had something like "double negative introduction", but all I have is double negative elimination (DNE) which I used on line 13. That meant that I had to derive line 6 from a subproof on lines 4 and 5 rather than reference an inference rule.  
Still, what is important is that I was able to derive those results. The natural deduction system is complete. It can derive every formula that is true.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
