Programa de Hilbert - Hilbert's program

Na matemática , o programa de Hilbert , formulado pelo matemático alemão David Hilbert no início do século 20, foi uma solução proposta para a crise fundamental da matemática , quando as primeiras tentativas de esclarecer os fundamentos da matemática sofreram de paradoxos e inconsistências. Como solução, Hilbert propôs fundamentar todas as teorias existentes em um conjunto finito e completo de axiomas e fornecer uma prova de que esses axiomas eram consistentes . Hilbert propôs que a consistência de sistemas mais complicados, como a análise real , poderia ser provada em termos de sistemas mais simples. Em última análise, a consistência de toda a matemática poderia ser reduzida à aritmética básica .

Os teoremas da incompletude de Gödel , publicados em 1931, mostraram que o programa de Hilbert era inatingível para áreas-chave da matemática. Em seu primeiro teorema, Gödel mostrou que qualquer sistema consistente com um conjunto computável de axiomas que é capaz de expressar aritmética nunca pode ser completo: é possível construir uma afirmação que pode ser mostrada como verdadeira, mas que não pode ser derivada da regras formais do sistema. Em seu segundo teorema, ele mostrou que tal sistema não poderia provar sua própria consistência, então certamente não pode ser usado para provar a consistência de algo mais forte com certeza. Isso refutou a suposição de Hilbert de que um sistema finitístico poderia ser usado para provar a consistência de si mesmo e, portanto, de qualquer outra coisa.

Declaração do programa de Hilbert

O principal objetivo do programa de Hilbert era fornecer bases seguras para toda a matemática. Em particular, isso deve incluir:

  • Uma formulação de toda a matemática; em outras palavras, todas as declarações matemáticas devem ser escritas em uma linguagem formal precisa e manipuladas de acordo com regras bem definidas.
  • Completude: uma prova de que todas as afirmações matemáticas verdadeiras podem ser provadas no formalismo.
  • Consistência: uma prova de que nenhuma contradição pode ser obtida no formalismo da matemática. Essa prova de consistência deve preferencialmente usar apenas raciocínios "finitos" sobre objetos matemáticos finitos.
  • Conservação: uma prova de que qualquer resultado sobre "objetos reais" obtido usando o raciocínio sobre "objetos ideais" (como conjuntos incontáveis) pode ser provado sem usar objetos ideais.
  • Decidibilidade: deve haver um algoritmo para decidir a verdade ou falsidade de qualquer declaração matemática.

Teoremas da incompletude de Gödel

Kurt Gödel mostrou que a maioria dos objetivos do programa de Hilbert eram impossíveis de alcançar, pelo menos se interpretados da maneira mais óbvia. O segundo teorema da incompletude de Gödel mostra 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 representa um desafio para o programa de Hilbert:

  • Não é possível formalizar todas as afirmações matemáticas verdadeiras dentro de um sistema formal, pois qualquer tentativa de tal formalismo omitirá algumas afirmações matemáticas verdadeiras. Não há extensão completa e consistente até mesmo da aritmética de Peano baseada em um conjunto recursivamente enumerável de axiomas.
  • Uma teoria como a aritmética de Peano não pode nem mesmo provar sua própria consistência, portanto, um subconjunto "finitista" restrito dela certamente não pode provar a consistência de teorias mais poderosas, como a teoria dos conjuntos.
  • Não há algoritmo para decidir a verdade (ou provabilidade) das declarações em qualquer extensão consistente da aritmética de Peano. A rigor, essa solução negativa para o Entscheidungsproblem apareceu alguns anos depois do teorema de Gödel, porque na época a noção de um algoritmo não havia sido definida com precisão.

O programa de Hilbert depois de Gödel

Muitas linhas atuais de pesquisa em lógica matemática , como teoria da prova e matemática reversa , podem ser vistas como continuações naturais do programa original de Hilbert. Muito disso pode ser recuperado mudando ligeiramente suas metas (Zach 2005), e com as seguintes modificações, algumas delas foram concluídas com sucesso:

  • Embora não seja possível formalizar toda a matemática, é possível formalizar essencialmente toda a matemática que qualquer pessoa usa. Em particular, a teoria dos conjuntos de Zermelo-Fraenkel , combinada com a lógica de primeira ordem , fornece um formalismo satisfatório e geralmente aceito para quase todas as matemáticas atuais.
  • Embora não seja possível provar completude para sistemas que podem expressar pelo menos a aritmética de Peano (ou, mais geralmente, que tem um conjunto computável de axiomas), é possível provar formas de completude para muitos outros sistemas interessantes. Um exemplo de uma teoria não trivial para a qual a completude foi provada é a teoria dos campos algébricamente fechados de determinada característica .
  • A questão de saber se existem provas de consistência finitária de teorias fortes é difícil de responder, principalmente porque não existe uma definição geralmente aceita de uma "prova finitária". A maioria dos matemáticos da teoria da prova parece considerar a matemática finitária como estando contida na aritmética de Peano e, neste caso, não é possível fornecer provas finitárias de teorias razoavelmente fortes. Por outro lado, o próprio Gödel sugeriu a possibilidade de dar provas de consistência finitária usando métodos finitários que não podem ser formalizados na aritmética de Peano, então ele parece ter uma visão mais liberal de quais métodos finitários poderiam ser permitidos. Alguns anos depois, Gentzen deu uma prova de consistência para a aritmética de Peano. A única parte desta prova que não foi claramente finitária foi uma certa indução transfinita até o ordinal ε 0 . Se essa indução transfinita for aceita como um método finitário, então pode-se afirmar que há uma prova finitária da consistência da aritmética de Peano. Os subconjuntos mais poderosos da aritmética de segunda ordem receberam provas de consistência de Gaisi Takeuti e outros, e pode-se novamente debater sobre o quão finitárias ou construtivas são essas provas. (As teorias que foram comprovadas consistentes por esses métodos são bastante fortes e incluem a maioria da matemática "comum".)
  • Embora não haja nenhum algoritmo para decidir a verdade das afirmações na aritmética de Peano, existem muitas teorias interessantes e não triviais para as quais tais algoritmos foram encontrados. Por exemplo, Tarski encontrou um algoritmo que pode decidir a verdade de qualquer afirmação em geometria analítica (mais precisamente, ele provou que a teoria dos campos fechados reais é decidível). Dado o axioma de Cantor-Dedekind , este algoritmo pode ser considerado um algoritmo para decidir a verdade de qualquer afirmação na geometria euclidiana . Isso é substancial, pois poucas pessoas considerariam a geometria euclidiana uma teoria trivial.

Veja também

Referências

  • G. Gentzen, 1936/1969. Die Widerspruchfreiheit der reinen Zahlentheorie. Mathematische Annalen 112: 493–565. Traduzido como 'A consistência da aritmética', em Os documentos coletados de Gerhard Gentzen , ME Szabo (ed.), 1969.
  • D. Hilbert. 'Die Grundlegung der elementaren Zahlenlehre'. Mathematische Annalen 104: 485–94. Traduzido por W. Ewald como 'The Grounding of Elementary Number Theory', pp. 266-273 em Mancosu (ed., 1998) De Brouwer a Hilbert: O debate sobre os fundamentos da matemática na década de 1920 , Oxford University Press. Nova york.
  • SG Simpson, 1988. Realizações parciais do programa de Hilbert . Journal of Symbolic Logic 53: 349-363.
  • R. Zach , 2006. Programa de Hilbert então e agora. Philosophy of Logic 5: 411–447, arXiv: math / 0508572 [math.LO].

links externos

  • Richard Zach. "Programa de Hilbert" . Em Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .