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:
- Haken showed that under a Frege proof system, solving the pigeonhole principle for $m=n+1$ is intractable.
- However, with
an extended Fregea proof system based on cutting planes, solving the pigeonhole principle for $m=n+1$ is always achievable in polynomial time.
- 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?