Думать о Σ* кодирование каких-то объектов, и Qкак совокупность всех объектов, удовлетворяющих некоторому свойству. Думать оP как функция, которая принимает (кодирование) пары (x,p) где x это объект и p якобы "доказательство" x∈Q, ФункцияP является «проверкой проверки»: она проверяет, что p на самом деле представляет собой достоверное доказательство того, что x∈Q, Если так, то возвращаетсяxв противном случае он возвращает элемент по умолчанию Q,
В качестве примера предположим, Σ∗ кодирует графики и позволяет Qбыть множеством (кодировок) гамильтоновых графов. ВозможноP это: декодировать ввод как (G,ℓ) где G это график и ℓ список вершин G; подтвердите этоℓ гамильтонов цикл G; если так то вернисьG в противном случае верните график в одну точку.
Вы рассмотрели случай плоских графов. Чтобы получить подходящийP нам нужно понятие поли-проверяемого времени доказательства плоскостности.
В общем вход на P не нужно кодировать пару (x,p), Важно то, чтоP может извлечь две части информации из своего ввода: рассматриваемый объект и предполагаемые доказательства того, что объект принадлежит Q, Например, давайте возьмем в качествеQмножество всех предложений, доказуемых в некоторой теории первого порядка. Сейчас жеPдекодирует свой ввод как формальное доказательство. Если кодировка неверна, возвращается⊤, Если кодировка представляет действительное доказательство, оно возвращает утверждение, которое было подтверждено доказательством (которое, вероятно, является корнем дерева доказательств или последней формулой в последовательности утверждений, в зависимости от того, как вы формализуете доказательства).