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$

cc.complexity-theory lo.logic np proof-complexity

— Optować
źródło

Powiązane (ale nie dokładny duplikat): cstheory.stackexchange.com/questions/3064/…

— Tsuyoshi Ito

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$

— Kaveh
źródło

Odpowiedź jest nad moją głową, ale tekst w języku arabskim wzbudził we mnie zainteresowanie. :)

— Tsuyoshi Ito

@Tsuyoshi: To był „ten” napisany za pomocą klawiatury perskiej. :)

— Kaveh

Ups, przepraszam za błąd!

— Tsuyoshi Ito,

Dziękuję za odpowiedź. Czy znasz odniesienie do stwierdzenia „NP = coNP jest równoważne istnieniu super pps”? Dzięki!

— Opt

To klasyczny wynik z pracy Cook-Reckhow 1979, ale dowód nie jest trudny. Pps to narzędzie do sprawdzania certyfikatów dla TAUT, a TAUT to kompletny język coNP. Jeśli długości prób są wielomianowe dla niektórych pps, TAUT będzie w NP. W przeciwnym kierunku, jeśli NP = coNP, to istnieje algorytm NP dla TAUT, certyfikaty są dowodami, a weryfikatorem jest pps.

— Kaveh