8
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ See Pudlák's On the length of proofs of finitistic consistency statements in first order theories. $\endgroup$ – Yuval Filmus Jun 30 '19 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 '19 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 '19 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 '19 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 '19 at 17:01
5
$\begingroup$

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 "$M$ is halting" and "$M$ is not halting" 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 "not all true statements have a short proof" and "all statements have a short proof" if there are no true statements.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thank you for your answer. I made a mistake by using the word "true" instead of "provable" and I just changed the wording in my question to avoid any reference to models. My point is that a formal proof of P!=NP would establish a lower bound for some provable statements, but as you point out, an exponential lower bound would do the same. So this part of my question was not suggesting that P!=NP is a necessary condition but rather a sufficient one. $\endgroup$ – Ari Jul 27 at 1:39
  • $\begingroup$ @Ari Try repeating your reasoning but replace ZF by a clearly inconsistent theory T (e.g. add 1 = 0 to ZF). Is it then still true that if P!=NP, then there must be long proofs in the modified theory T? I believe this sentence implicitly assumes that T is consistent. $\endgroup$ – sdcvvc Jul 29 at 20:33
1
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\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 '19 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 '19 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 '19 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.