P vs. NP and Godel's Theorems 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?
if P!=NP then this means that for some fixed $k$ not all true sentences $\phi$ of ZF have a proof of length ≤ $|ϕ|^k$.

You do not need to assume $P \neq NP$ to prove this claim. If all true sentences $\phi$ of ZF have a proof of length $\leq |\phi|^k$ then the halting problem could be solved by enumerating all proofs of &quot;$M$ is halting&quot; and &quot;$M$ is not halting&quot; up to that size. So it's not possible for all true sentences to have a short proof. Instead of  $|\phi|^k$ we can take a function that grows even faster, e.g. $2^{2^{2^{|\phi|}}}$. There's no computable limit on how long a proof can be compared to its statement.
However, to speak about true sentences, we are assuming implicitly that ZF already has a model. So this reasoning does not prove that ZF is consistent - it assumes it from the start. There's no contradiction between &quot;not all true statements have a short proof&quot; and &quot;all statements have a short proof&quot; if there are no true statements.