NP vs co-NP and second-order logic

Question

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?

Answer 1

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$.