Why doesn't Godel's Second Incompleteness Theorem rule out a formalizable proof of P!=NP?
There seems to be a flaw as alluded to by Arno in his answer.  While the reduction $SAT \leq B$ seems innocuous enough (and is indeed a textbook exercise as pointed out by Ariel in his comment) it implicitly assumes the consistency of ZF. Otherwise, if ZF is inconsistent, since every statement of ZF would then have a proof, unsatisfiable SAT-instances would not necessarily be mapped to wffs $\varphi$ which do not have a relatively short proof.  

Thus, if we assume that ZF is consistent and $ZF \vdash P \neq NP$ then although we can conclude metamathematically that $B \notin P$ (because being NP-complete, $B$ could not be in $P$ since we are assuming $P \neq NP$) we would not have a formal deduction of $ZF \vdash B \notin P$ (since this depends on $B$ being an established NP-complete set, so if we want to use the reduction above, we must assume that ZF is consistent, which cannot be formally asserted by Godel's Second Incompleteness Theorem).  Thus this argument cannot suggest any necessary implications of $ZF \vdash P \neq NP$.