Incompletude e Computação de Gödel

Os teoremas da incompletude de Gödel demonstram que qualquer sistema formal suficientemente forte e consistente contém afirmações verdadeiras que não pode provar, um resultado profundamente interligado com a indecidibilidade descoberta na teoria da computabilidade.

Definition

Os teoremas da incompletude afirmam que qualquer sistema formal consistente capaz de expressar aritmética básica é incompleto, com afirmações aritméticas verdadeiras que não pode provar, e não pode provar sua própria consistência; em termos computacionais, o conjunto de afirmações prováveis é reconhecível, mas seu complemento não é, espelhando a indecidibilidade.

Scope

Este tópico abrange os primeiros e segundos teoremas da incompletude, a técnica de aritmetização e autorreferência através da numeração de Gödel, a estreita relação entre a incompletude e a indecidibilidade do problema da parada e da lógica de primeira ordem, e as consequências para os limites do raciocínio formal e da prova automatizada.

Core questions

• Por que nenhum sistema formal consistente e suficientemente forte pode provar todas as afirmações aritméticas verdadeiras?
• Como a autorreferência via numeração de Gödel produz uma sentença verdadeira indemonstrável?
• Como a incompletude e a indecidibilidade do problema da parada são duas visões de um mesmo fenômeno?
• O que a incompletude implica para os limites da prova de teoremas automatizada?

Key theories

Primeiro teorema da incompletude

Qualquer sistema formal consistente forte o suficiente para codificar a aritmética contém uma afirmação verdadeira que não pode provar nem refutar, construída por uma sentença que efetivamente afirma sua própria indemonstrabilidade.

Incompletude via computabilidade

A incompletude decorre da indecidibilidade do problema da parada: se toda verdade aritmética fosse provável, poder-se-ia decidir a parada procurando por provas, de modo que a existência de problemas indecidíveis força a existência de verdades indemonstráveis.

Clinical relevance

A incompletude e sua contraparte computacional impõem limites rígidos ao raciocínio automatizado: nenhum algoritmo pode decidir todas as verdades aritméticas ou resolver todas as questões matemáticas, portanto, os provadores de teoremas e os sistemas de verificação devem depender de orientação humana, teorias restritas ou prova interativa, em vez de decisão automática completa.

History

Gödel provou os teoremas da incompletude em 1931, frustrando a esperança de Hilbert de uma formalização completa e autojustificável da matemática. Em cinco anos, Church e Turing conectaram esses limites à indecidibilidade, e a leitura computacional da incompletude através do problema da parada tornou-se um pilar da teoria da computabilidade.

Key figures

• Kurt Gödel
• Alan Turing
• Alonzo Church
• John Barkley Rosser

Seminal works

• godel1931
• boolos2007

Frequently asked questions

A incompletude significa que a matemática está quebrada?

Não. Significa que nenhum sistema formal consistente pode provar todas as verdades aritméticas, não que a matemática seja inconsistente ou não confiável. Os matemáticos trabalham dentro e entre sistemas formais, e a incompletude simplesmente marca um limite intrínseco ao que qualquer sistema fixo pode capturar.

Como o teorema de Gödel está relacionado ao problema da parada?

Eles estão intimamente ligados. A insolubilidade do problema da parada implica incompletude: se um sistema formal pudesse provar toda a verdade sobre quais programas param, poder-se-ia decidir a parada procurando por provas, contradizendo o resultado de Turing. Ambos expressam, na lógica e na computação, os mesmos limites fundamentais do método formal.