# 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 true 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?

• – Yuval Filmus Jun 30 '19 at 21:42
• ... if P!=NP then this means that for some fixed $k$ not all true sentences $\phi$ of ZF have a proof of length $\leq {|\phi|}^k$. Why? – xskxzr Jul 1 '19 at 12:31
• @xskxzr because if they did, then we could always determine in polynomial time whether a statement is provable or not. – Ari Jul 1 '19 at 13:57
• How ? We could examine all proofs of length $\le |\phi|^k$ until we find one that proves or disproves $\phi$ but surely that requires exponential time ? – gandalf61 Jul 1 '19 at 15:17
• @gandalf61 Indeed, that would require exponential time, but for an NP problem it's enough to know that a proof exists and not know it specifically. If P=NP then the NP-complete language $L=\{\phi | \phi \text{ has a proof } <{| \phi |}^k \}$ for some fixed $k$ is in P. – Ari Jul 2 '19 at 17:01

Let $$k=1$$. Since there exist statements that have multiple very short proofs, there must be some sentence that has a shortest proof longer than its own length. So we already live in the "bad world" you're imagining. Since any short proof can have an irrelevant line introduced without changing anything as long as that line is a tautology, we even live in a pretty extreme version.
• No, you're right on that. However, if ZF is inconsistent, then every statement will have a proof of some length which is at most polynomial in its own length. I'm not just concerned about the case of $k=1$ but rather for any $k$. – Ari Jul 2 '19 at 17:38