Czy dobre PCP dla NP dają nam dobre PCP dla całej hierarchii wielomianowej?

Twierdzenie PCP stwierdza, że każdy problem decyzyjny w NP ma probabilistycznie sprawdzalne dowody (lub równoważnie, że istnieje kompletny i quasi-dźwiękowy system dla twierdzeń w NP wykorzystujący stałą złożoność zapytań i logarytmicznie wiele losowych bitów).

„Mądrość ludowa” otaczająca twierdzenie PCP (ignorując przez chwilę znaczenie PCP dla teorii przybliżenia) polega na tym, że oznacza to, że dowody napisane w ścisłym języku matematycznym można skutecznie sprawdzić z dowolnym pożądanym stopniem dokładności, bez konieczności czytania całego dowód (lub większość dowodu).

Nie jestem w stanie tego całkiem zobaczyć. Rozważ rozszerzenie drugiego rzędu na logikę zdań z nieograniczonym użyciem kwantyfikatorów (co, jak mi powiedziano, jest już słabsze niż ZFC, ale nie jestem logikiem). Możemy już zacząć wyrażać twierdzenia, które nie są dostępne dla NP poprzez naprzemienne kwantyfikatory.

Moje pytanie brzmi, czy istnieje prosty, znany sposób „rozwijania” kwantyfikatorów w zdaniach zdania wyższego rzędu, tak aby PCP dla twierdzeń w NP stosowały się równie dobrze na dowolnym poziomie PH. Możliwe, że nie da się tego zrobić - że rozwinięcie kwantyfikatora kosztuje, w najgorszym przypadku, stałą część poprawności lub poprawności naszego systemu dowodowego.

lo.logic pcp polynomial-hierarchy

— Ross Snider
źródło

Wydaje mi się, że PCP dla problemu prawie z definicji umieszcza problem w BPP, co oznaczałoby, że jest on w autorstwa Sipser – Gács – Lautemann. Ale może zobaczymy to powiązane pytanie .

Σ_{2} \cap Π_{2}

$\Sigma_2 \cap \Pi_2$

— Peter Shor,

Brzmi rozsądnie, ale jestem zdezorientowany. Gdyby tak było, to czy nie postawiłoby NP w BPP?

— Ross Snider,

Ups Powinienem był powiedzieć, że MA jest również zawarte w .

Σ_{2} \cap Π_{2}

$\Sigma_2 \cap \Pi_2$

— Peter Shor,

to nie zadziała. PH jest odporny na zaangażowane lematy. rozważmy coś takiego jak EXP ^ 2. Może obsłużyć RP, RNP itp. Jako żart. Nie wchodzisz łatwo w tę hierarchię.

— Steve Uurtamo,

Odpowiedzi:

Prawda oświadczenia różni się od posiadania (krótkiego) dowodu w systemie dowodu. Język jest ekspresyjny, ale nie oznacza to, że wszystkie prawidłowe instrukcje w tym języku mają krótkie dowody w systemie.

Twierdzenie nie mówi, że można sprawdzić prawdziwość stwierdzenia, a nawet poprawność arbitralnego długiego dowodu lub dowolnych twierdzeń. To jest na dowód członkostwa w $\mathsf{NP}$ zestaw, które z definicji mają wielomianowe dowody wielkości (certyfikaty) członkostwa. Twierdzenie mówi tylko, że nie musisz czytać pełnego (wielomianowego) dowodu członkostwa w $\mathsf{NP}$ zestaw decydować o jego poprawności.

Jedną z implikacji tego twierdzenia jest zastosowanie go do zbioru twierdzeń w dowolnym języku, który ma krótkie (tj. Arbitralne wielomianowe) dowody w efektywnym systemie dowodowym (tj. Można rozstrzygać w czasie wielomianowym, jeśli dany ciąg jest dowodem danego komunikat). Na przykład twierdzenia ZFC, które mają dowody wielkości $n^{100}$ gdzie $n$ to rozmiar formuły. Jeśli system dowodowy jest sprawny, wówczas można probabilistycznie zweryfikować poprawność twierdzeń, które mają krótkie dowody, czytając niewielką część ich dowodów. Myślę, że takie jest zamierzone znaczenie nieformalnego stwierdzenia, że „ dowody napisane w ścisłym języku matematycznym można skutecznie sprawdzić z dowolnym pożądanym stopniem dokładności bez konieczności czytania całego dowodu ”.

— Kaveh
źródło

Pozwól mi spróbować wyjaśnić.

Rozważ następujący problem obliczeniowy: biorąc pod uwagę wyrażenie matematyczne (w twoim ulubionym systemie aksjomatów) i liczbę n podaną w reprezentacji jednoargumentowej, zdecyduj, czy wyrażenie ma dowód wielkości n.

Jest to problem NP: biorąc pod uwagę dowód, można skutecznie sprawdzić, czy ma on rozmiar n i czy jest to prawidłowy dowód twierdzenia. Uwaga: nawet jeśli instrukcja obejmuje kwantyfikatory takie jak WSZYSTKO, nie oznacza to, że weryfikator musi sprawdzić wszystkie możliwości, to po prostu oznacza, że weryfikator stosuje reguły wnioskowania dotyczące kwantyfikatora WSZYSTKIE.

Twierdzenie PCP ma zatem zastosowanie do tego problemu, dlatego istnieje (inny) format dowodu, który umożliwia weryfikację probabilistyczną.

Kolejna uwaga (dotycząca uwagi Petera): weryfikator PCP używa tylko losowości logarytmicznej. Oznacza to, że można go zastąpić standardowym, deterministycznym weryfikatorem, który analizuje cały dowód. To znaczy, że weryfikator PCP dla języka umieszcza go w NP.

— Dana Moshkovitz
źródło