This post is based loosely on a previous post, but the presentation is somewhat different and hopefully much more succinct.
Basically, I'm wondering if it is plausible for there to be a formal proof of P!=NP if ZF is consistent (obviously the converse is true). The idea is this: since proofs to sentences in ZF can be viewed as witnesses in an NP-language, if P!=NP then this means that for some fixed $k$ not all provable sentences $\phi$ of ZF have a proof of length $\leq {|\phi|}^k$. But if ZF is inconsistent, then every sentence of sufficient length has a relatively short proof derived from a fixed contradiction. So we get that P!=NP implies that ZF is consistent. So if we have a formal proof of P!=NP then this would imply through Godel's Second Incompleteness Theorem that ZF is inconsistent (and thus P=NP) as well. Is there a problem with this approach?