<p>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.</p>

CC BY-SA 4.0
2019-11-19T16:39:31.877Z
2019-11-19T16:39:31.877Z
Joshua Grochow
<p>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.</p>

<p>If NP != CoNP then P != NP. </p>

<p>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.</p>

CC BY-SA 4.0
2019-11-20T04:58:15.943Z
2019-11-20T04:58:15.943Z
Parry
<p><a href="https://doi.org/10.1145/1562164.1562186" rel="nofollow noreferrer">Here</a>, in section 4.3, Fortnow says:</p>

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

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

<ol>
<li><a href="https://doi.org/10.1016/0304-3975(85)90144-6" rel="nofollow noreferrer">Haken</a> showed that under a Frege proof system, solving the pigeonhole principle for <span class="math-container">$m=n+1$</span> is intractable.</li>
<li>However, with <strike>an extended Frege</strike> a proof system based on cutting planes, solving the pigeonhole principle for <span class="math-container">$m=n+1$</span> is always achievable in polynomial time.</li>
<li>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.    </li>
</ol>

<p>Is that right? Else, what am I missing? </p>

CC BY-SA 4.0
2019-11-11T16:59:13.723Z
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.
Joshua Grochow
CC BY-SA 4.0
2019-11-12T09:35:08.073Z
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.
Mikolas
CC BY-SA 4.0
2019-11-17T05:20:31.747Z
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.
Joshua Grochow
CC BY-SA 4.0
2019-11-19T13:57:03.723Z
@Joshua, you should make your last comment an answer. Many thanks.
Jérôme Verstrynge
CC BY-SA 4.0
2019-11-20T08:18:00.377Z
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.
Jan Johannsen
<sat><lower-bounds><np><proof-theory>
Understanding non-equivalence of proof lengths according to proof systems
Jérôme Verstrynge
# Understanding non-equivalence of proof lengths according to proof systems

(Asked by: username_0 on 2019-11-11)

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?

**Tags:** sat, lower-bounds, np, proof-theory
> **Comments:**
> **username_1**: 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.  
> **username_2**: 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.  
> **username_1**: 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.  
> **username_0**: @Joshua, you should make your last comment an answer. Many thanks.  
> **username_3**: 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.  

---

## 2 answers

### Answer by username_1 on 2019-11-19. Score: 2 | Accepted answer

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.


---

### Answer by username_4 on 2019-11-20. Score: 1

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.


---

