3
$\begingroup$

Here, in section 4.3, Fortnow says:

But to prove P != NP we would need to show that tautologies
cannot have short proofs in an arbitrary proof system.

I am trying to understand the logic leading to this conclusion. Do I get it right when I say:

  1. Haken showed that under a Frege proof system, solving the pigeonhole principle for $m=n+1$ is intractable.
  2. However, with an extended Frege a proof system based on cutting planes, solving the pigeonhole principle for $m=n+1$ is always achievable in polynomial time.
  3. Therefore, if one proves intractability of say k-SAT in a proof system, it does not imply that solving k-SAT would be intractable in another proof system.

Is that right? Else, what am I missing?

Improve this question
$\endgroup$
5
  • 3
    $\begingroup$ Haken's result is for Resolution, which is weaker than Frege. Similar results exist for bounded-depth Frege. But no such lower bounds are known for general Frege. $\endgroup$
    – Joshua Grochow
    Nov 11, 2019 at 16:59
  • 1
    $\begingroup$ I think that the argument you're looking for is this: There is a proof system under which all proofs for a tautology are polynomial iff NP = co-NP because you'd have short certificate for co-NP problems. $\endgroup$
    – Mikolas
    Nov 12, 2019 at 9:35
  • 2
    $\begingroup$ I believe everything you said is correct. I note that your point #3 could hold regardless of points #1 and #2 - points #1 and #2 are just a concrete example of where this has provably happened. $\endgroup$
    – Joshua Grochow
    Nov 17, 2019 at 5:20
  • $\begingroup$ @Joshua, you should make your last comment an answer. Many thanks. $\endgroup$
    – Jérôme Verstrynge
    Nov 19, 2019 at 13:57
  • 2
    $\begingroup$ A comment on your points 1 & 2: Extended Frege Systems (EF) are not based on Cutting Planes. They are two different proof systems that both have short proofs of the pigeonhole principle (PHP). In fact, EF and even just Frege systems simulate Cutting Planes, so - contrary to your claim in #1 - Frege systems have short proofs of PHP. Lower bounds for PHP are only known for Resolution (and some algebraic proof systems), as Joshua already said. $\endgroup$
    – Jan Johannsen
    Nov 20, 2019 at 8:18

2 Answers 2

Reset to default
2
$\begingroup$

I believe everything you said is correct. I note that your point #3 could hold regardless of points #1 and #2 - points #1 and #2 are just a concrete example of where this has provably happened.

Improve this answer
$\endgroup$
1
$\begingroup$

A propositional proof system in which all tautologies have a "short" proof is called a super-propositional-proof system. Such a system exists iff NP = CoNP.

If NP != CoNP then P != NP.

So, it's not necessarily the only way to prove P != NP, but you could do so by proving a super-propositional-proof system cannot exist.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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