Programa de Hilbert

O programa de Hilbert foi uma proposta feita em 1921 pelo matemático alemão David Hilbert de reformular as bases da matemática de forma rigorosa, partindo da aritmética. Segundo ele, toda a matemática poderia ser reduzida a um número finito de axiomas consistentes. Assim, qualquer proposição da matemática poderia ser provada dentro desse sistema (e o sistema seria dito completo).

O programa de Hilbert foi uma solução proposta para a crise fundamental da matemática, quando as primeiras tentativas de deixar os fundamentos matemáticos mais claros foram consideradas paradoxais e inconsistentes. Hilbert sugeriu basear todas as teorias existentes para um finito, um conjunto completo de axiomas, e então promover uma prova que esses axiomas eram consistentes. Hilbert propôs que a consistência de sistemas mais complexos, tais como análise real, poderiam ser provadas em termos de sistemas mais simples. Por fim, a consistência de toda a matemática poderia ser reduzida a aritmética básica.

Em 1931, o matemático Kurt Gödel provou, através do seu teorema da incompletude, que esta tarefa era impossível. No teorema, Gödel mostra que um sistema axiomático consistente não pode provar sua própria consistência. Assim, ele só pode ser inconsistente. Além disso, em sistemas com o poder de definir os números naturais (como o que Hilbert idealizou), sempre há proposições (chamadas de "indecisíveis") que não podem ser provadas dentro do sistema, portanto, ele é incompleto. Uma vez que o sistema não pode ser simultaneamente completo e consistente, a exigência hilbertiana de completude e consistência não pode ser colocada em prática.

Em outras palavras, a teoria de Gödel refutou a suposição de Hilbert que um sistema finito poderia ser usado para provar a consistência de uma teoria mais complexa.

Gödel deixou em aberto a possibilidade de existir um método geral para determinar se uma dada proposição é decisível. Em 1936, entretanto, o matemático Alan Turing provou que tal método não pode existir.

Enunciado do programa de Hilbert

O principal objetivo do programa de Hilbert foi o de fornecer bases seguras para toda a matemática. Em particular este deve incluir:

• A formalização de toda a matemática; em outras palavras, todos os enunciados matemáticos devem ser escritos em uma linguagem formal e manipulados de acordo com regras bem definidas;
• Completude: prova de que todos os enunciados matemáticos verdadeiros podem ser provados no formalismo;
• Consistência: prova de que nenhuma contradição pode ser obtida no formalismo. Esta prova de consistência deve preferencialmente usar somente o raciocínio “finitista” sobre objetos matemáticos finitos;
• Conservação: prova de que qualquer resultado sobre “objetos reais” obtido usando o raciocínio sobre “objetos ideais” (tais como um conjunto incontável) pode ser provado sem o uso de objetos ideais;
• Decisibilidade: deve haver um algoritmo para decidir a veracidade ou a falsidade de qualquer declaração matemática, ou seja, deve haver um algoritmo para decidir, dado qualquer enunciado matemático, se ele é verdadeiro ou falso.

O teorema da incompletude de Gödel

Kurt Gödel mostrou que a maioria dos objetivos do programa de Hilbert eram impossíveis de se alcançar, pelo menos se interpretados de uma maneira mais óbvia. Seu segundo teorema da incompletude afirmou que qualquer teoria consistente poderosa o suficiente para codificar adição e multiplicação de inteiros não pode provar sua própria consistência. Isso contradiz a maior parte do programa de Hilbert, pois:

• Não é possível formalizar toda a matemática, uma vez que qualquer tentativa de formalismo irá omitir alguma sentença matemática verdadeira;
• Uma consequência fácil do teorema da incompletude de Gödel é que nem mesmo há extensão completa e consistente da aritmética de Peano com um conjunto numérico recursivo de axiomas, então, de modo particular, as mais interessantes teorias matemáticas não são completas;
• Uma teoria como a aritmética de Peano não pode nem provar sua própria consistência, por isso um subconjunto finito restrito certamente não pode provar a consistência das mais fortes teorias, como a teoria dos conjuntos;
• Não há algoritmo para decidir a veracidade (ou prova) das declarações em qualquer extensão consistente da aritmética de Peano (estritamente falando, este resultado só apareceu alguns anos depois da teoria de Gödel, porque até aquele momento a noção de algoritmo não estava definida com precisão).

Programa de Hilbert após Gödel

Várias correntes de pesquisa em matemática lógica, prova de teorias e matemática reversa podem ser vistas como uma continuação natural do programa original de Hilbert. Muito do programa pode ser recuperado ao se trocar superficialmente seus objetivos.

Com as seguintes mudanças, uma parte do programa de Hilbert foi completo com sucesso:

• Embora não seja possível formalizar toda a matemática, é possível essencialmente formalizar toda a matemática que qualquer pessoa usa. Em particular, a teoria dos conjuntos de Zermelo-Fraenkel, combinada com lógica de primeira ordem, tem um formalismo satisfatório, geralmente aceito por essencialmente toda matemática;
• Embora não seja possível provar a corretude para sistemas tão poderosos quanto a aritmética de Peano - a menos que haja um conjunto computável de axiomas -, é possível provar formas de completude para vários sistemas interessantes. O primeiro grande sucesso foi do próprio Gödel. Antes de ele ter provado o teorema da incompletude, provou o teorema da completude para a lógica de primeira ordem, mostrando que qualquer consequência lógica de uma série de axiomas é demonstrável. Um exemplo de uma teoria não-trivial cuja completude foi provada é a teoria de corpos fechados algebricamente de uma dada característica;
• A questão de se há provas finitas consistentes de teorias fortes é difícil de se responder, principalmente porque não há uma definição geral de um “prova finitária”. Muitos matemáticos que trabalham em provas de teorias parecem considerar “matemática finita” como contida na aritmética de Peano, e nesse caso não é possível dar provas finitas de teorias razoavelmente fortes. Por outro lado, Gödel sugeriu a possibilidade de dar provas finitas consistentes usando métodos finitos que não podem ser formalizados na aritmética de Peano, então ele parece ter tido uma visão mais liberal de quais métodos finitos podem ser permitidos. Poucos anos depois, Gentzen deu uma prova consistente para a aritmética de Peano. A única parte dessa prova que não era claramente finita era uma indução transfinita até o ordinal ε0. Se essa indução transfinita for aceita como um método finito, então pode-se afirmar que há uma prova finita consistente para a aritmética de Peano. Subconjuntos mais poderosos de segunda ordem aritmética têm gerado provas consistentes de acordo com o trabalho de Gaisi Takeuti e outros, e pode-se de novo debater sobre o quão finitas ou construtivas essas provas são. As teorias que têm sido provadas consistentes por esses métodos são bem fortes e incluem as matemáticas mais “ordinárias”;
• Embora não haja algoritmo para comprovar a verdade das afirmações da aritmética de Peano, há várias teorias interessantes e não-triviais para as quais tais algoritmos têm sido encontrados. Por exemplo, Tarski encontrou um algoritmo que pode comprovar qualquer enunciado da geometria analítica (mais precisamente, ele provou que a teoria de corpos reais fechados é decidível). Dado o axioma de Cantor-Dedekind, esse algoritmo pode ser considerado como o algoritmo que comprova qualquer afirmação da geometria euclidiana. Isso é substancial, uma vez que poucas pessoas considerariam a geometria euclidiana como uma teoria trivial.