Se P = NP, poderíamos obter provas da conjectura de Goldbach, etc.?

Esta é uma pergunta ingênua, fora dos meus conhecimentos; desculpas antecipadamente.

A conjectura de Goldbach e muitas outras questões não resolvidas em matemática podem ser escritas como fórmulas curtas no cálculo de predicados. Por exemplo, o artigo de Cook "Os computadores podem descobrir rotineiramente provas matemáticas?" formula essa conjectura como

\forall n [(n > 2 \land 2 | n) \supset \exists r \exists s (P (r) \land P (s) \land n = r + s)]

$\forall n [( n > 2 \wedge 2 | n) \supset \exists r \exists s (P(r) \wedge P(s) \wedge n = r + s) ]$

Se restringirmos a atenção a provas polinomialmente longas, os teoremas com tais provas estarão em NP. Portanto, se P = NP, poderíamos determinar se, por exemplo, a conjectura de Goldbach é verdadeira no tempo polinomial.

Minha pergunta é: também poderíamos exibir uma prova em tempo polinomial?

Edit . De acordo com os comentários de Peter Shor e Kaveh, eu deveria ter qualificado minha afirmação de que poderíamos determinar se a conjectura de Goldbach é verdadeira se é realmente um dos teoremas com uma breve prova. O que, é claro, não sabemos!

cc.complexity-theory proof-complexity automated-theorem-proving proof-search Joseph O'Rourke
fonte

Primeiro, para exibir uma prova curta (<1000 páginas?) Da conjectura de Goldbach, deve haver uma prova curta. P = NP não tem influência nisso.

quer

@Suresh, @Kaveh: Você parece estar entendendo errado. Aqui temos uma instância concreta de um problema de pesquisa NP. O quantificador que é relevante aqui é a existência de uma prova (em um sistema formal adequado) do teorema.

Kristoffer Arnsfelt Hansen

Outra observação é que podemos realmente escrever um algoritmo, que se P = NP encontrará uma prova para uma determinada afirmação, se existir no polinômio de tempo no comprimento da afirmação e no comprimento da prova mais curta. (esse polinômio é um limite que vale para todos os teoremas); no entanto, será um algoritmo "astronômico".

Kristoffer Arnsfelt Hansen

@ Joe: Não, eu posso escrever o algoritmo agora mesmo! (Mesmo sem saber se P = NP). A idéia é o que é conhecido como busca universal de Levin.

Kristoffer Arnsfelt Hansen

@Kristoffer: Cool! Não sabia sobre LS. Vejo que Marcus Hutter tem uma espécie de aprimoramento no LS: "O algoritmo mais rápido e mais curto para todos os problemas bem definidos". International Journal of Foundations of Computer Science, 13 (3): 431-443, 2002.

Joseph O'Rourke

Respostas:

De fato!

Se P = NP, não apenas podemos decidir se existe uma prova de comprimento n para a Conjectura de Goldbach (ou qualquer outra afirmação matemática), mas também podemos encontrá-la com eficiência!

Por quê? Porque podemos perguntar: existe uma prova condicionada ao fato de o primeiro bit ser ..., então, existe uma prova condicionada ao fato dos dois primeiros bits serem ...., e assim por diante ...

E como você saberia n? Você apenas tentará todas as possibilidades, em ordem crescente. Quando damos um passo na i-ésima possibilidade, também tentamos um passo em cada uma das possibilidades 1 .. (i-1).

Dana Moshkovitz
fonte

Não é esse algoritmo de busca universal de Levin?

Mohammad Al-Turkistany

@turkistany: sim, é!

Dana Moshkovitz

Dana respondeu à pergunta. Mas aqui estão alguns comentários sobre o lado prático.

Observe que é indecidível verificar se uma determinada sentença é comprovável no ZFC. não tem conseqüências nisso. (na verdade ) significa que é fácil de encontrar provas para tautologias proposicional $P=NP$ $P=NP$ $P=coNP$ , frases não de primeira ordem, como GC.

$NP$ $l$ $P=NP$ $l$

$P=NP$ $l$ $l$ $P=NP$ $P$ $DTime(n^2)$ ), então é possível pegar esse algoritmo e executá-lo para verificar se há provas de um tamanho viável, mas muito grande, que será maior do que qualquer prova que qualquer ser humano possa apresentar e, se o algoritmo não encontrar uma resposta, o sentença é praticamente impossível de provar. O truque que Dana mencionou também funcionará aqui para encontrar a prova.

Para fins práticos:

$P=NP$ $DTime(10000n^{10000})$
ele encontrará uma prova apenas se houver uma (ou seja, a sentença não é uma frase indecidível no ZFC); além disso, a prova deve ser possível de forma curta.
$P\neq NP$ $NP=DTime(n^{\log^* n})$

Kaveh
fonte

(n^{10})

$(n^{10})$