<p>If there is an optimal pps (pps = <a href="http://en.wikipedia.org/wiki/Propositional_proof_system">propositional proof system</a>, an optimal pps is a pps that can p-simulate any other proof system) then the pps EF (Extended Frege) strengthened with propositional axioms stating the soundness of the optimal propositional proof system will be optimal. More generally EF + Soundness of pps P can p-simulate P for any P. So EF has a kind of generality that you don't need to change the logic or the underlying pps structure, but just add propositional axioms to it to get any arbitrary strong pps.</p>

<p>In particular, if there is a super pps (a pps which has polynomial size proofs for all tautologies) then EF + Soundness of that pps will be a super pps. Note that $NP = coNP$ is equivalent to the existence of a super pps.</p>

<p>Soundness of a pps P is a (sequence of) propositional formulas stating that if $\pi$ is a proof in P for $\varphi$, then $\varphi$ is true.</p>

<p>In summery, there is no need to go outside propositional logic.</p>

<p>ps: Note that all pps are effective by definition, a pps has a polynomial time verifier, and therefore its theorems are computably enumerable. $NP=coNP$ means that there is a super pps for the <em>propositional</em> formulas. Being propositional is important here. We know that there is no such thing for stronger logics but their nonexistence does not seem to have any effect on $NP$ vs $coNP$.</p>

CC BY-SA 2.5
2010-11-22T04:30:19.253Z
The answer is over my head, but the Arabic text in it made me curious. :)
Tsuyoshi Ito
CC BY-SA 2.5
2010-11-22T04:57:25.297Z
@Tsuyoshi: That was "the" typed using Persian keyboard. :)
Kaveh
CC BY-SA 2.5
2010-11-22T04:59:41.347Z
Oops, sorry for the mistake!
Tsuyoshi Ito
CC BY-SA 2.5
2010-11-22T06:48:28.593Z
Thanks for the answer. Do you know of a reference for the statement "NP=coNP is equivalent to the existence of a super pps"? Thanks!
Opt
CC BY-SA 2.5
2010-11-22T06:52:16.833Z
That is a classic result from Cook-Reckhow 1979 paper but the proof is not difficult. A pps is a certificate checker for TAUT and TAUT is a coNP complete language. If the lengths of proofs are polynomial for some pps, TAUT will be in NP. For the other direction, if NP=coNP, then there is a NP algorithm for TAUT, the certificates are the proofs and the verifier is the pps.
Kaveh
CC BY-SA 2.5
2010-11-22T02:04:42.650Z
2010-11-22T06:40:56.587Z
2010-11-22T06:40:56.587Z
Kaveh
<p>Assume that NP=co-NP and polynomial $p(x)$ bounds the length of the proof of unsatisfiability for a 3-CNF instance $x$. Then are there any results on what <em>form</em> any proof of unsatisfiability for $x$ of length $\leq p(x)$ can take? <br>
I.e. in general, would such a proof have to, for instance, use the full power of second-order logic over infinite structures (I am aware that the proposition to prove - that a formula is unsatisfiable can be expressed in second-order logic over finite structures but intermediate steps in the proof to get to that might require reasoning over infinite structures). <br>
Since there is no effective, complete and sound system of inference for second-order logic, would it be possible to use such a result to prove NP $\neq$ co-NP?</p>

CC BY-SA 2.5
2010-11-22T00:51:50.140Z
Related (but not an exact duplicate): http://cstheory.stackexchange.com/questions/3064/conp-certificate-for-graph-isomorphism
Tsuyoshi Ito
<cc.complexity-theory><lo.logic><np><proof-complexity>
NP vs co-NP and second-order logic
Opt
# NP vs co-NP and second-order logic

(Asked by: username_0 on 2010-11-22)

Assume that NP=co-NP and polynomial $p(x)$ bounds the length of the proof of unsatisfiability for a 3-CNF instance $x$. Then are there any results on what *form* any proof of unsatisfiability for $x$ of length $\leq p(x)$ can take?   
I.e. in general, would such a proof have to, for instance, use the full power of second-order logic over infinite structures (I am aware that the proposition to prove - that a formula is unsatisfiable can be expressed in second-order logic over finite structures but intermediate steps in the proof to get to that might require reasoning over infinite structures).   
Since there is no effective, complete and sound system of inference for second-order logic, would it be possible to use such a result to prove NP $\neq$ co-NP?

**Tags:** cc.complexity-theory, lo.logic, np, proof-complexity

> **Comments:**
> **username_1**: Related (but not an exact duplicate): http://cstheory.stackexchange.com/questions/3064/conp-certificate-for-graph-isomorphism  

---

## 1 answers

### Answer by username_2 on 2010-11-22. Score: 7 | Accepted answer

If there is an optimal pps (pps = [propositional proof system](http://en.wikipedia.org/wiki/Propositional_proof_system), an optimal pps is a pps that can p-simulate any other proof system) then the pps EF (Extended Frege) strengthened with propositional axioms stating the soundness of the optimal propositional proof system will be optimal. More generally EF + Soundness of pps P can p-simulate P for any P. So EF has a kind of generality that you don't need to change the logic or the underlying pps structure, but just add propositional axioms to it to get any arbitrary strong pps.

In particular, if there is a super pps (a pps which has polynomial size proofs for all tautologies) then EF + Soundness of that pps will be a super pps. Note that $NP = coNP$ is equivalent to the existence of a super pps.

Soundness of a pps P is a (sequence of) propositional formulas stating that if $\pi$ is a proof in P for $\varphi$, then $\varphi$ is true.

In summery, there is no need to go outside propositional logic.

ps: Note that all pps are effective by definition, a pps has a polynomial time verifier, and therefore its theorems are computably enumerable. $NP=coNP$ means that there is a super pps for the *propositional* formulas. Being propositional is important here. We know that there is no such thing for stronger logics but their nonexistence does not seem to have any effect on $NP$ vs $coNP$.

> **Comments:**
> **username_1**: The answer is over my head, but the Arabic text in it made me curious. :)  
> **username_2**: @Tsuyoshi: That was "the" typed using Persian keyboard. :)  
> **username_1**: Oops, sorry for the mistake!  
> **username_0**: Thanks for the answer. Do you know of a reference for the statement "NP=coNP is equivalent to the existence of a super pps"? Thanks!  
> **username_2**: That is a classic result from Cook-Reckhow 1979 paper but the proof is not difficult. A pps is a certificate checker for TAUT and TAUT is a coNP complete language. If the lengths of proofs are polynomial for some pps, TAUT will be in NP. For the other direction, if NP=coNP, then there is a NP algorithm for TAUT, the certificates are the proofs and the verifier is the pps.  

---

