A proof complexity conjecture and the Incompleteness theorem

Título: Uma conjectura de complexidade de prova e o Teorema da Incompletude

Autor: Jan Krajíček (Universidade Charles, Praga)
Fonte: arXiv:2303.10637v2 [cs.LO]

---

1. Problema e Contexto

O artigo aborda uma antiga conjectura na teoria da complexidade de prova: a existência de um gerador de prova (proof complexity generator) que seja "duro" para todos os sistemas de prova.

• A Conjectura: Existe uma função computável em tempo polinomial ($p$-time), $g: \{0, 1\}^* \to \{0, 1\}^*$, que estica cada entrada em exatamente um bit (ou seja, $|g(u)| = |u| + 1$), tal que o seu conjunto imagem (range) intersecta todos os conjuntos infinitos da classe NP.
• Implicação: Se tal gerador existir, ele seria um objeto fundamental para separar classes de complexidade (especificamente implicando $NP \neq coNP$) e resolveria problemas centrais sobre a existência de sistemas de prova ótimos.
• Objetivo do Artigo: O autor constrói uma função baseada em teorias de primeira ordem para demonstrar a incompletude de Gödel e, em seguida, propõe uma versão proposicional dessa construção para estabelecer uma disjunção de três condições fundamentais na teoria da complexidade computacional.

---

2. Metodologia e Construção

O autor utiliza uma abordagem híbrida, combinando lógica matemática (teoria de modelos e provas) com complexidade computacional.

A. Versão em Lógica de Primeira Ordem (Seção 2)

O autor define uma função $g_T$ baseada em uma teoria de primeira ordem $T$ (que contém a teoria $S^1_2$ de Buss, capaz de formalizar a sintaxe da lógica de primeira ordem e é computável em tempo polinomial).

1. Definição da Função $g_T(u)$:

   • Dada uma entrada $u$, o algoritmo procura uma fórmula $\Phi$ (com uma variável livre $x$) que seja um prefixo de $u$ e tenha tamanho logarítmico em relação a $u$.
   • Se nenhuma tal fórmula existir, $g_T(u) = 0$.
   • Caso contrário, para cada possível extensão $w$ (de tamanho $c+1$), o algoritmo busca uma prova em $T$ da sentença $\Phi_w$:
     $$\exists y \forall x > y (\Phi(x) \to \neg(w \subseteq_e x))$$
     (Intuitivamente, esta sentença afirma que a sequência $w$ não aparece como prefixo em infinitos elementos definidos por $\Phi$).
   • Se uma prova for encontrada para todas as $w$, a saída é 0.
   • Se houver uma $w_0$ para a qual nenhuma prova é encontrada, a saída é $w_0$ concatenada com o restante de $u$.

2. Propriedades:

   • $g_T$ é computável em tempo polinomial e estica a entrada em 1 bit.
   • O complemento da imagem de $g_T$ é infinito.

3. Conexão com Incompletude:

   • O Teorema 2.2 mostra que, se $T$ for são (verdadeira no modelo padrão) e completa, então a imagem de $g_T$ deve intersectar qualquer conjunto infinito definível em $L$.
   • Como o complemento da imagem de $g_T$ é um conjunto infinito e definível, isso cria uma contradição: se $T$ fosse completa, a imagem de $g_T$ cobriria seu próprio complemento, o que é impossível.
   • Conclusão: Isso fornece uma prova alternativa do Primeiro Teorema da Incompletude de Gödel para teorias $p$-time.

B. Versão Proposicional (Seção 3)

O autor tenta "descer" a construção para a lógica proposicional para evitar a incompletude e focar em limites inferiores de tamanho de prova.

• Tradução Proposicional: Utiliza-se a tradução canônica de fórmulas $\Sigma^b_1$ (da hierarquia polinomial) para fórmulas proposicionais $\phi_{n,w}$.
• Desafio: A busca por provas em $T$ é substituída pela busca por provas em um sistema proposicional $P$.
• Hipóteses de Falha: Para construir a função desejada, o autor assume que:
  1. Existe um sistema de prova proposicional $p$-ótimo (negando a afirmação 1 do teorema principal).
  2. $E \subseteq P/poly$ (negando a afirmação 2 do teorema principal).
• Construção da Função $h_P$: Sob essas hipóteses, define-se uma função $h$ que busca provas proposicionais de fórmulas traduzidas. A busca é limitada a circuitos de tamanho sub-exponencial, permitindo que a função seja computada em tempo sub-exponencial.

---

3. Principais Resultados e Contribuições

O resultado central do artigo é o Teorema 3.1, que estabelece que pelo menos uma das seguintes três afirmações deve ser verdadeira:

1. Não existe sistema de prova proposicional $p$-ótimo.
   • Nota: Isso é equivalente à inexistência de um algoritmo de busca de prova proposicional que seja ótimo em tempo de execução.
2. $E \not\subseteq P/poly$.
   • Isso significa que a classe de complexidade $E$ (problemas decidíveis em tempo exponencial $2^{O(n)}$) não está contida em circuitos booleanos de tamanho polinomial. É uma afirmação forte sobre a dureza de circuitos.
3. Existência de um gerador "duro" sub-exponencial.
   • Existe uma função $h$ que estica todas as entradas em um bit, é computável em tempo sub-exponencial ($2^{O((\log n)^{\log \log n})}$) e cuja imagem intersecta todos os conjuntos infinitos de NP.

Contribuições Específicas:

• Reformulação da Incompletude: Oferece uma nova perspectiva sobre o Teorema de Gödel, vinculando-o diretamente à existência de geradores de prova e à complexidade computacional, em vez de apenas à aritmética.
• Problema Aberto (Problema 2.4): O autor deixa em aberto se, para alguma teoria $T$, a função $g_T$ satisfaz a conjectura original (interseção com todos os conjuntos NP infinitos). Uma resposta afirmativa implicaria $NP \neq coNP$.
• Conexão entre Lógica e Circuitos: Demonstra como a estrutura de provas em teorias formais pode ser traduzida em propriedades de circuitos booleanos e sistemas de prova proposicionais.

---

4. Significado e Impacto

Este trabalho é significativo por várias razões:

• Ponte entre Áreas: Conecta profundamente a teoria da prova (lógica matemática) com a teoria da complexidade computacional (classes P, NP, E, circuitos).
• Abordagem Alternativa para $NP \neq coNP$: A conjectura de geradores de prova é uma das principais vias para atacar o problema $P$ vs $NP$. O artigo mostra que, se não houver sistemas de prova ótimos ou se certas classes de circuitos forem duras, então tal gerador (ou algo muito próximo) deve existir.
• Limites Inferiores: O resultado sugere que provar a inexistência de tais geradores (ou provar que $NP = coNP$) exigiria refutar afirmações muito fortes sobre a estrutura de circuitos ($E \not\subseteq P/poly$) ou a existência de sistemas de prova ótimos.
• Incompletude Eficiente: A prova de Gödel apresentada é "eficiente" no sentido de que utiliza apenas teorias que podem ser formalizadas e verificadas em tempo polinomial, destacando que a incompletude é uma barreira intrínseca mesmo para sistemas computacionalmente eficientes.

Em resumo, Krajíček demonstra que a existência de geradores de prova "duros" é uma consequência inevitável da estrutura da complexidade computacional, a menos que existam colapsos significativos nas classes de complexidade (como $E \subseteq P/poly$) ou a existência de sistemas de prova proposicionais perfeitamente eficientes.