Loading AI tools
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.
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."[1]
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.
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."[2]
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 ε0.[3] 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.
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.
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
