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?

  • 2
    $\begingroup$ See Pudlák's On the length of proofs of finitistic consistency statements in first order theories. $\endgroup$ – Yuval Filmus Jun 30 at 21:42
  • 2
    $\begingroup$ ... 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? $\endgroup$ – xskxzr Jul 1 at 12:31
  • $\begingroup$ @xskxzr because if they did, then we could always determine in polynomial time whether a statement is provable or not. $\endgroup$ – Ari Jul 1 at 13:57
  • 2
    $\begingroup$ 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 ? $\endgroup$ – gandalf61 Jul 1 at 15:17
  • $\begingroup$ @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. $\endgroup$ – Ari Jul 2 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.

I'm not sure exactly what your reasoning is or where it's going wrong, but I think where you're going wrong is that in a world where ZF is consistent the set of valid deductions is different from in a world in which ZF is inconsistent.

  • $\begingroup$ Yes, ZF is consistent iff there are statements with very long proofs, and that's exactly my point. A formal proof of NP!=P would establish that there exist statements only having long proofs, which implies a formal proof of the consistency of ZF, which implies through Godel's second incompleteness Theorem that ZF is inconsistent $\endgroup$ – Ari Jul 2 at 17:10
  • $\begingroup$ Do you disagree that I proved that some statements only have proofs longer than their length? $\endgroup$ – Stella Biderman Jul 2 at 17:17
  • $\begingroup$ 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$. $\endgroup$ – Ari Jul 2 at 17:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.