Por que o Segundo Teorema da Incompletude de Godel não descarta uma prova formalizável de P! = NP?

Tenho certeza de que deve haver algo errado com o seguinte raciocínio, porque, caso contrário, muitas pesquisas de P vs. NP seriam reduzidas, mas não consigo determinar meu erro:

Para qualquer número inteiro fixo $k>0$ definir

B_{k} := {⟨ φ ⟩ | φ is a wff of ZF and has a proof of length \leq k {| φ |}^{k}}

$B_k := \{ \langle \varphi \rangle | \; \varphi \; \text{is a wff of ZF and has a proof of length} \; \leq k{|\varphi|}^k \; \}$

Agora para todos $k$ , o idioma $B_k$ está em NP desde que uma prova válida para $\varphi$ de comprimento $\leq k{|\varphi|}^k$ pode ser uma testemunha NP verificada por um verificador automático em tempo polinomial. Além disso, para suficientemente grande $k$ , $B_k$ é NP-completo, pois o SAT se reduz a ele: ou seja, para uma instância $\phi$ de SAT fazer um wff correspondente de ZF $\varphi$ usando quantificadores existenciais. Então, uma atribuição de verdade satisfatória de $\phi$ pode ser transformado em uma prova formal de $\varphi$ de comprimento polinomial em $|\varphi|$ desde uma atribuição de verdade de $\phi$ é linear em $|\phi|$ .

Agora, se ZF for inconsistente, isso significa que há uma declaração formal $\sigma$ de modo que ambos $\sigma$ e $\neg \sigma$ tem provas em ZF. Como é sabido, qualquer outra declaração $\tau$ pode então ser derivado da conjunção contraditória $\langle \sigma \wedge \neg \sigma \rangle$ (ou seja, seguindo o caminho:

⟨ σ \land \neg σ ⟩ ⟹ ambos σ e \neg σ são verdadeiras ⟹ ⟨ \neg τ \to σ ⟩ é verdadeiro (pois, independentemente de τ a implicação é válida desde σ é verdade) ⟹ ⟨ \neg σ \to τ ⟩ (por contraposição e dupla negação) ⟹ τ é verdade (por modus ponens com \neg σ)

$\langle \sigma \wedge \neg \sigma \rangle \implies \text{both} \; \sigma \; \text{and} \; \neg \sigma \; \text{are true} \implies \langle \neg \tau \rightarrow \sigma \rangle \; \text{is true (since regardless of} \; \tau \; \text{the implication is valid since} \; \sigma \; \text{is true)} \implies \langle \neg \sigma \rightarrow \tau \rangle \; \text{(by contraposition and double negation)} \implies \tau \; \text{ is true (by modus ponens with} \; \neg \sigma \, )$

) Assim, se ZF é inconsistente, então toda declaração $\varphi$ tem um polinômio de prova (me parece linear) em $|\varphi|$ .

Deixei $B:=B_k$ para um tamanho suficientemente grande $k$ referido acima para permitir $B$ ser NP-completo. Então, se ZF é inconsistente, existem apenas finitas $\varphi$ de tal modo que $\langle \varphi \rangle \notin B$ porque a tolerância polinomial de alto grau à prova de $B$ é suficiente para cobrir as provas curtas garantidas de wffs de comprimento suficiente. Isso implica que $B$ é decidível em tempo polinomial que, por sua completude NP, implica que P = NP. Se reformularmos essa cadeia de raciocínio em termos de contrapositivos, se P! = NP, então ZF não será inconsistente (ou seja, é consistente).

Portanto, se temos uma prova formal de P! = NP, temos uma prova formal da consistência de ZF. Mas pelo teorema da Segunda Incompletude de Godel, isso implica que ZF é inconsistente, o que, por sua vez, obtém P = NP conforme descrito acima (assim como a teorema de qualquer teorema negado).

Esta não é exatamente uma prova de que P vs. NP é independente de ZF. Pode ser que ZF seja consistente e que P = NP ou P! = NP possam ser comprovados através de técnicas não formalizáveis dentro da ZF. No entanto, apresenta outra barreira formidável para resolver P vs. NP.

complexity-theory np-complete logic p-vs-np Ari
fonte

Respostas:

Parece haver uma falha mencionada por Arno em sua resposta. Enquanto a redução $SAT \leq B$ parece bastante inócuo (e é realmente um exercício de livro didático, como apontado por Ariel em seu comentário), assume implicitamente a consistência de ZF. Caso contrário, se ZF for inconsistente, já que toda declaração de ZF teria uma prova, instâncias SAT insatisfatórias não seriam necessariamente mapeadas para wffs $\varphi$ que não têm uma prova relativamente curta.

Assim, se assumirmos que ZF é consistente e $ZF \vdash P \neq NP$ então, embora possamos concluir meta-esquematicamente que $B \notin P$ (porque ser NP completo, $B$ não poderia estar em $P$ desde que estamos assumindo $P \neq NP$ ) não teríamos uma dedução formal de $ZF \vdash B \notin P$ (já que isso depende de $B$ sendo um conjunto completo de NP estabelecido, portanto, se quisermos usar a redução acima, devemos assumir que ZF é consistente, o que não pode ser formalmente afirmado pelo Segundo Teorema da Incompletude de Godel). Portanto, este argumento não pode sugerir quaisquer implicações necessárias de $ZF \vdash P \neq NP$ .

Ari
fonte

Bom trabalho! este parece ser o problema.

Ariel #

O problema está na sua afirmação de que, para empresas suficientemente grandes $k$ , o idioma $B_k$ é NP-completo. Na sua redução proposta, você argumenta apenas que qualquer instância SAT satisfatória é para uma fórmula ZF com prova "curta". No entanto, você também precisa argumentar que sempre que a fórmula ZF resultante tiver uma prova curta, a instância SAT original é satisfatória. É claro que isso se resume apenas em dizer que, se o ZF provar que a instância do SAT é satisfatória, realmente é - mas aqui estamos usando a solidez do ZF.

Arno
fonte

Você está certo, pois estou assumindo implicitamente a solidez de ZF e a correção de um verificador de provas, mas como isso afeta a prova de que

B_{k}

$B_k$ o NP está completo? Essas são apenas premissas necessárias para o idioma

B_{k}

$B_k$ ser de qualquer interesse. De acordo com minha redução, apenas uma instância SAT satisfatória terá uma prova de qualquer extensão, porque uma insatisfatória corresponde a uma declaração ZF que é falsa.

Ari

@Ari Instâncias SAT insatisfatórias correspondem a declarações ZF que são falsas na sua meta-teoria. Portanto, para que a redução funcione, é necessário que as declarações ZF falsas não tenham uma prova ZF.

Arno #

A equivalência é clara, se a fórmula tiver uma prova, a instância SAT é satisfatória (ZF é bom, não vejo por que isso deve ser um obstáculo aqui). Veja esta pergunta para uma prova de sua integridade NP.

Ariel

@ Ariel A resposta nessa pergunta é imprecisa sobre quais são as suposições. Necessita necessariamente assumir que ZF é sólido. Apenas o lembrete: "Som" significa que, se uma afirmação tem uma prova, é realmente verdade. Se o ZF é inconsistente, prova tudo e, portanto, não pode ser bom. Em particular, vemos que "ZF é som" não é um teorema de ZF. Se a nossa meta-teoria provar que "ZF é sólida", ela também prova "ZF é consistente" e não há problema. Se não provar, não temos a prova de completude do NP e também não há problema.

Arno #

A correção da redução realmente depende da consistência do ZF, no entanto, nada tem a ver com a robustez. Lembre-se de que a sonoridade é definida em relação a algumas semânticas, e ZF é válido no sentido de que declarações prováveis são verdadeiras em todos os modelos, se ZF for inconsistente por ser vacuamente consistente, pois não possui modelos.

Ariel #