NP vs co-NP i logika drugiego rzędu

Załóżmy, że NP = co-NP i wielomian ogranicza długość dowodu niezadowolenia dla instancji 3-CNF . Czy są więc jakieś wyniki w jakiej formie może przyjąć jakiś dowód niezadowolenia dla długości ? Tzn. Ogólnie, czy taki dowód musiałby na przykład wykorzystać pełną moc logiki drugiego rzędu nad nieskończonymi strukturami (zdaję sobie sprawę, że propozycja udowodnienia - że formuła jest niezadowalająca, może być wyrażona w logice drugiego rzędu struktury skończone, ale pośrednie kroki w dowodzie, aby do nich dojść, mogą wymagać rozumowania ponad strukturami nieskończonymi).$p(x)$$x$$x$$\leq p(x)$

Skoro nie ma skutecznego, kompletnego i solidnego systemu wnioskowania dla logiki drugiego rzędu, czy byłoby możliwe wykorzystanie takiego wyniku do udowodnienia, że ​​NP co-NP?$\neq$

Jeśli istnieje optymalny pps (pps = system dowodu propozycyjnego , optymalny pps to pps, który może p-symulować dowolny inny system dowodu), to pps EF (Extended Frege) wzmocniony aksjomatami twierdzenia określającymi solidność optymalnego systemu dowodu propozycyjnego będzie optymalny. Bardziej ogólnie EF + Dźwięk pps P może p-symulować P dla dowolnego P. Tak więc EF ma pewien rodzaj ogólności, że nie musisz zmieniać logiki lub podstawowej struktury pps, ale po prostu dodaj do niego aksjomaty zdań, aby uzyskać dowolny dowolne silne pps.

W szczególności, jeśli istnieje super pps (pps, który ma wielomianowe proofy wielkości dla wszystkich tautologii), wówczas EF + Soundness tego pps będzie super pps. Zauważ, że jest równoważne istnieniu super pps.$NP = coNP$

Poprawność pps P jest (sekwencją) formuł zdaniowych stwierdzających, że jeśli jest dowodem w P dla , to jest prawdziwe.$\pi$$\varphi$$\varphi$

W lecie nie trzeba wychodzić poza logikę zdań.

ps: Zauważ, że wszystkie pps są z definicji skuteczne, pps ma wielomianowy weryfikator czasu, a zatem jego twierdzenia są obliczalne. oznacza, że ​​istnieje super pps dla formuł zdań . Ważna jest tutaj propozycja. Wiemy, że nie ma czegoś takiego dla silniejszej logiki, ale ich nieistnienie nie wydaje się mieć żadnego wpływu na porównaniu z .$NP=coNP$$NP$$coNP$