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:


Haken showed that under a Frege proof system, solving the pigeonhole principle for $m=n+1$ is intractable.
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.
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?
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.