# NP vs co-NP and second-order logic

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?

If there is an optimal pps (pps = 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$.

• The answer is over my head, but the Arabic text in it made me curious. :) – Tsuyoshi Ito Nov 22 '10 at 4:30
• @Tsuyoshi: That was "the" typed using Persian keyboard. :) – Kaveh Nov 22 '10 at 4:57
• Oops, sorry for the mistake! – Tsuyoshi Ito Nov 22 '10 at 4:59
• 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 Nov 22 '10 at 6:48
• 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 Nov 22 '10 at 6:52