NP vs co-NP and second-order logic
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$.