# Understanding non-equivalence of proof lengths according to proof systems

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?

• 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. Nov 11 '19 at 16:59
• 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. Nov 12 '19 at 9:35
• 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. Nov 17 '19 at 5:20
• @Joshua, you should make your last comment an answer. Many thanks. Nov 19 '19 at 13:57
• 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. Nov 20 '19 at 8:18