NP vs co-NP y lógica de segundo orden

Suponga que NP = co-NP y el polinomio limita la longitud de la prueba de insatisfacción para una instancia de 3-CNF x . Entonces, ¿hay algún resultado sobre qué forma puede tomar cualquier prueba de insatisfacción para x de longitud ≤ p ( x ) ? Es decir, en general, ¿tal prueba tendría que usar, por ejemplo, todo el poder de la lógica de segundo orden sobre estructuras infinitas (soy consciente de que la proposición para demostrar que una fórmula no es satisfactoria puede expresarse en lógica de segundo orden sobre estructuras finitas pero los pasos intermedios en la prueba para llegar a eso pueden requerir razonamiento sobre estructuras infinitas).$p(x)$$x$$x$$\leq p(x)$

Dado que no existe un sistema de inferencia efectivo, completo y sólido para la lógica de segundo orden, ¿sería posible utilizar dicho resultado para probar NP co-NP?$\neq$

Si hay un pps óptimo (pps = sistema de prueba proposicional , un pps óptimo es un pps que puede simular p cualquier otro sistema de prueba), entonces el pps EF (Extended Frege) se fortalece con axiomas proposicionales que indican la solidez del sistema de prueba proposicional óptimo Será óptimo. Más generalmente, EF + Solidez de pps P puede simular p para cualquier P. Por lo tanto, EF tiene un tipo de generalidad que no necesita cambiar la lógica o la estructura de pps subyacente, sino simplemente agregar axiomas proposicionales para obtener cualquier pps fuertes arbitrarios.

$NP = coNP$

$\pi$$\varphi$$\varphi$

En resumen, no hay necesidad de salir de la lógica proposicional.

$NP=coNP$$NP$$coNP$