Segundo problema de Hilbert

Na matemática, o segundo problema de Hilbert foi proposto por David Hilbert em 1900, sendo esse um dos seus 23 problemas. Esse problema consiste em provar que a aritmética é consistente - livre de qualquer contradição interna. No anos de 1930, Kurt Gödel e Gerhard Gentzen provaram resultados que voltaram a chamar atenção para esse problema. Alguns acham que esses resultados resolveram o problema, enquanto outros acham que ele ainda está em aberto.

O segundo problema de Hilbert e a sua interpretação

Hilbert explicava:

"Quando estamos engajados na investigação dos fundamentos de uma ciência, devemos montar um sistema de axiomas que contém uma descrição exata e completa das relações que existem entre as ideias elementares dessa ciência. [...] Mas acima de tudo, eu desejo formular a seguinte questão, como sendo a mais importante entre todas as numerosas questões que podem ser feitas a respeito dos axiomas: a de provar que eles não são contraditórios, ou seja, que um número finito de passos que se baseiem nesses axiomas não nos leve a um resultado contraditório. Na geometria, a prova da compatibilidade dos axiomas pode ser feita construindo-se um conjunto de números, em que relações análogas entre os números desse conjunto correspondem aos axiomas geométricos. [...]Por outro lado, um método direto é necessário para a prova da compatibilidade dos axiomas aritméticos."

Hoje, o que se pede no segundo problema de Hilbert é a prova de que os Axiomas de Peano são consistentes.

Existem muitas provas conhecidas que defendem a consistência dos axiomas de Peano e que são reconhecidas em sistemas fortes como a Teoria dos conjuntos de Zermelo-Fraenkel. Essas provas, porém, não resolvem o problema de fato, já que existem pessoas que duvidam da consistência dos axiomas de Peano pois não aceitam que a consistência deles possa ser provada usando essa teoria. No entanto, uma resposta satisfatória ao problema de Hilbert pode ser desenvolvida usando princípios que seriam aceitos por aqueles que não acreditam que os axiomas de Peano sejam consistentes. Esses princípios são frequentemente chamados de [Finitismo], visto que são completamente construtivos e não pressupõem a infinidade completa dos números naturais.

Teorema da incompletude de Gödel

Ver artigo principal: Teoremas da incompletude de Gödel

O segundo teorema da incompletude de Gödel mostra que não é possível alguma prova da consistência dos axiomas de Peano ser desenvolvida sem essa própria aritmética. Esse teorema diz que se os únicos procedimentos de prova aceitáveis forem aqueles que podem ser formalizados dentro da aritmética, então o problema de Hilbert não pode ser resolvido. No entanto, como Thomas Nagel e John Henry Newman explicaram, ainda há espaço para a prova que não pode ser formalizada na aritmética:

"Esse resultado imposto pela análise de Gödel não deve ser mal interpretado: ele não exclui provas meta-matemáticas da consistência da aritmética. O que ele exclui é a prova de consistência que pode ser espelhada por deduções formais da aritmética. Provas meta-matemáticas têm sido construídas, notadamente por Gerhard Gentzen, um membro da escola de Hilbert, em 1936, e por outros desde então. [...] Mas essas provas não podem ser representadas no cálculo aritmético, e, desde que elas não sejam finitas, elas não conseguem alcançar os objetivos propostos pelo problema original de Hilbert. A possibilidade de construir-se uma prova finita e absoluta para a consistência da aritmética não é excluída pelos resultados de Gödel. Ele apenas provou que essa prova não pode ser representada na aritmética. Mas hoje, ninguém parece ter uma ideia clara de como uma prova finita iria ser, já que não é capaz de ser expressada na aritmética."

Prova da consistência aritmética de Gentzen

Em 1936, Gentzen publicou a prova da consistência dos axiomas de Peano. Seus resultados mostraram que a prova de consistência pode ser obtida em um sistema muito mais fraco do que a teoria de Zermelo-Fraenkel.

A prova de Gentzen assinalava, a cada prova feita pelos axiomas de Peano, um Número ordinal baseado na estrutura da prova, com cada um desses números menores do que ε₀. Daí, Gentzen consegue provar por Indução transfinita nesses ordinais que nenhuma prova pode concluir em uma contradição. O método usado nessa prova também pode ser usado para provar o resultado do Teorema da eliminação do corte na aritmética de Peano numa lógica mais forte do que a lógica de primeira ordem, mas a prova da consistência, verdadeiramente, pode ser desenvolvida na lógica de primeira ordem, usando axiomas da [aritmética primitiva recursiva] e o princípio da indução transfinita. Tait(2005) deu uma interpretação em forma de um jogo teórico sobre o método de Gentzen.

A prova de Gentzen iniciou um programa de [análise dos ordinais] em teorias de prova. Nesse programa, teorias formais da aritmética ou teoria dos conjuntos eram identificadas como números ordinais que mediriam a força de consistência dessas teorias. Uma teoria seria incapaz de provar a consistência de outra se a primeira fosse representada por ordinal mais fraco.

Pontos de vista modernos sobre o status do problema

Apesar de os teoremas de Gödel e Gentzen serem, hoje em dia, muito bem entendidos pela comunidade de lógica matemática, nenhum consenso ainda foi formado sobre se (ou como) esses teoremas respondem ao segundo problema de Hilbert. Simpson(1988:sec.3) argumentou que o teorema da incompletude de Gödel mostrou que não é possível produzir uma prova finita de consistência em teorias fortes. Kreisel(1976) afirmou que, apesar de os resultados de Gödel implicarem na impossibilidade da existência de provas sintáticas, argumentos semânticos (em particular, Lógica de segunda ordem) podem ser usados para dar provas de consistência bastante convincentes. Detlefsen(1990) disse que o teorema de Gödel não proíbe a existência de uma prova de consistência, já que as hipóteses desse teorema podem não se aplicar a todos os sistemas em que uma prova de consistência pode ser desenvolvida. Dawson(2006) chamou a crença de que o teorema de Gödel elimina a possibilidade de uma prova de consistência persuasiva de "errônea", citando a prova de consistência dada por Gentzen e outra dada por Gödel em 1958.

Ver também

• [Conjectura de Takeuti]

Referências

• Dawson, John W. (2006) "Shaken foundations or groundbreaking realignment? A Centennial Assessment of Kurt Gödel’s Impact on Logic, Mathematics, and Computer Science". 2006 21st Annual IEEE Symposium on Logic in Computer Science, IEEE, pp. 339–341. ISBN 0-7695-2631-4 doi:10.1109/LICS.2006.47
• Michael Detlefsen (1990). «On an alleged refutation of Hilbert's Program using Gödel's First Incompleteness Theorem». Springer. Journal of Philosophical Logic. 19 (4): 343–377. doi:10.1007/BF00263316 
• Torkel Franzen (2005), Godel's theorem: An Incomplete Guide to its Use and Abuse, A.K. Peters, Wellesley MA. ISBN 1-56881-238-8
• Gerhard Gentzen (1936). "Die Widerspruchsfreiheit der reinen Zahlentheorie." Mathematische Annalen, v. 112, pp. 493–565.
• Kurt Gödel (1931), Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38: 173-98. Translated in Jean van Heijenoort, 1967. From Frege to Gödel: A Source Book on Mathematical Logic. Harvard University Press: 596-616.
• David Hilbert [1900] (1901) "Mathematische Probleme". Archiv der Mathematik und Physik, v. 3 n. 1, pp. 44–63 and 213–237. English translation, Maby Winton, Bulletin of the American Mathematical Society 8 (1902), 437–479. Available online at http://aleph0.clarku.edu/~djoyce/hilbert/problems.html .
• George Kreisel (1976). «What have we learnt from Hilbert's second problem?». Mathematical developments arising from Hilbert problems (Proc. Sympos. Pure Math., Northern Illinois Univ., De Kalb, Ill.,). Providence, R. I.: Amer. Math. Soc. pp. 93–130. ISBN 0-8218-1428-1 
• Nagel, Ernest and Newman, James R., Godel's Proof, New York University Press, 1958.
• Stephen G. Simpson (1988). «Partial realizations of Hilbert's Program». Journal of Symbolic Logic. 53 (2): 349–363. ISSN 0022-4812. JSTOR 2274508. doi:10.2307/2274508  Available online at http://www.math.psu.edu/simpson/papers/hilbert.pdf .
• [William W. Tait] (2005). "Gödel's reformulation of Gentzen's first consistency proof of arithmetic: the no-counterexample interpretation." Bulletin of Symbolic Logic v. 11 n. 2, pp. 225–238.

Ligações externas

• Original text of Hilbert's talk, in German
• English translation of Hilbert's 1900 address