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.
źródło
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 wNP 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 wNP 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ścin100 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 ”.
ź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.
źródło