NP vs co-NP e lógica de segunda ordem

11

Suponha que NP = co-NP e polinômio limita o comprimento da prova de insatisfação para uma instância 3-CNF x . Então, existem resultados de que forma qualquer prova de insatisfação para x de comprimento p ( x ) pode levar? Ou seja, em geral, essa prova teria que, por exemplo, usar todo o poder da lógica de segunda ordem sobre estruturas infinitas (estou ciente de que a proposição para provar - que uma fórmula é insatisfatória pode ser expressa na lógica de segunda ordem sobre estruturas finitas, mas etapas intermediárias na prova para chegar a isso podem exigir raciocínio sobre estruturas infinitas).p(x)xxp(x)

Como não existe um sistema de inferência eficaz, completo e sólido para a lógica de segunda ordem, seria possível usar esse resultado para provar NP co-NP?

Optar
fonte
2
Relacionado (mas não uma cópia
Tsuyoshi Ito

Respostas:

7

Se houver um pps ideal (pps = sistema de prova proposicional , um pps ideal é um pps que pode simular p qualquer outro sistema de prova), o pps EF (Extended Frege) fortalecido com axiomas proposicionais que indicam a solidez do sistema de prova proposicional ideal será ótimo. Em geral, EF + a solidez dos pps P pode simular P de P para qualquer P. Portanto, o EF tem um tipo de generalidade que você não precisa alterar a lógica ou a estrutura subjacente dos pps, mas apenas adicionar axiomas proposicionais a ele para obter pps fortes arbitrários.

NP=coNP

πφφ

No verão, não há necessidade de sair da lógica proposicional.

NP=coNPNPcoNP

Kaveh
fonte
1
A resposta está na minha cabeça, mas o texto em árabe me deixou curioso. :)
Tsuyoshi Ito
@ Tsuyoshi: Esse foi "o" digitado usando o teclado persa. :)
Kaveh
Opa, desculpe pelo erro!
Tsuyoshi Ito
Obrigado pela resposta. Você conhece uma referência para a afirmação "NP = coNP é equivalente à existência de um super pps"? Obrigado!
Opte
3
Esse é um resultado clássico do artigo de Cook-Reckhow de 1979, mas a prova não é difícil. Um pps é um verificador de certificado para TAUT e TAUT é um idioma completo do coNP. Se o comprimento das provas for polinomial para alguns pontos, TAUT estará em NP. Para a outra direção, se NP = coNP, existe um algoritmo NP para TAUT, os certificados são as provas e o verificador é o pps.
Kaveh