Teoria da prova

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
NoFonti.svg
Este artigo ou se(c)ção cita uma ou mais fontes fiáveis e independentes, mas ela(s) não cobre(m) todo o texto (desde dezembro de 2011).
Por favor, melhore este artigo providenciando mais fontes fiáveis e independentes e inserindo-as em notas de rodapé ou no corpo do texto, conforme o livro de estilo.
Encontre fontes: Googlenotícias, livros, acadêmicoScirusBing. Veja como referenciar e citar as fontes.
Wikitext.svg
Este artigo ou seção precisa ser wikificado (desde dezembro de 2011).
Por favor ajude a formatar este artigo de acordo com as diretrizes estabelecidas no livro de estilo.

Teoria da prova é um ramo da lógica matemática que representa provas como objetos matemáticos formais, facilitando suas análises através de técnicas matemáticas. Provas são tipicamente representadas por estruturas de dados definidas indutivamente, como listas simples, listas encadeadas, ou árvores, as quais são construídas de acordo com os axiomas e regras de inferência da lógica. Portanto, a teoria da prova é sintática na natureza, ao contrário da teoria dos modelos, que é semântica na natureza. Juntamente com a teoria do modelo, teoria do conjunto axiomático, e teoria da recursão, a teoria da prova é um dos quatro tão falados pilares dos fundamentos da matemática.1

A teoria da prova é importante na lógica filosófica, onde o primeiro interesse é na idéia de provas teórico-semântica, uma idéia que depende de idéias técnicas na teoria da prova estrutural para ser factível.

Histórico[editar | editar código-fonte]

Apesar de que formalização da lógica estava bastante avançada graças ao trabalho de figuras como Gottlob Frege, Giuseppe Peano, Bertrand Russel e Richard Dedekind, a história da teoria da prova moderna é comumente atribuída a David Hilbert, quem iniciou o que é chamado de programa de Hilbert em Os Fundamentos da Matemática. O trabalho de Kurt Gödel na teoria da prova avançou inicialmente, mas um tempo depois refutou este programa: seu teorema de completude parecia inicialmente se encaixar no objetivo de Hilbert de reduzir a matemática para um sistema formal finito; posteriormente seus teoremas de incompletude mostraram que isso era inalcançável. Todo esse trabalho foi realizado com a prova de cálculos chamada de sistemas de Hilbert.

Em paralelo, as fundações da teoria da prova estrutural estavam sendo encontradas. Jan Łukasiewicz sugeriu, em 1926, que os sistemas de Hilbert poderiam ser melhorados como uma base para a apresentação axiomática da lógica se fosse permitida formulação de conclusões de pressupostos nas regras de inferência da lógica.

Em resposta a isso, Stanisław Jaśkowski (1929) e Gerhard Gentzen (1934) forneceram, de maneira independente, tais sistemas, chamados cálculos da dedução natural, com a aproximação de Gentzen introduzindo a idéia de simetria entre terrenos para proposições afirmativas, expressadas em regras de introdução, e as consequências de aceitar proposições em regras de eliminação, uma idéia que revelou-se muito importante na teoria da prova.2 Gentzen (1934), posteriormente, introduziu a idéia do cálculo subsequente, um cálculo avançado num espírito similar que expressou melhor a dualidade dos conectivos lógicos,3 e gerou avanços fundamentais na formalização da lógica intuicionista, e forneceu a primeira prova combinatória da consistência da aritmética de Peano. Juntos, a apresentação da dedução natural e o cálculo subsequente introduziram a idéia fundamental da prova analítica da teoria da prova.

Provas formais e informais[editar | editar código-fonte]

As provas informais da matemática são diferentes das provas formais da teoria da prova. Elas são mais parecidas com esboços de alto nível que iriam permitir um especialista a reconstruir uma prova formal ao menos no princípio, dados muito tempo e paciência. Para vários matemáticos, escrever uma prova formal inteira é muito pedante e trabalhoso para ser uma prática comum.

Provas formais são construídas com o auxílio de computadores em provas de teoremas interativos. Significativamente, essas provas podem ser checadas automaticamente também por um computador. (Checando provas formais é usualmente simples, que encontrar provas (prova do teorema automatizado) é geralmente difícil.) Uma prova informal na literatura matemática, por sua vez, requer semanas de revisões para ser checada, e talvez contenha erros.

Notes[editar | editar código-fonte]

  1. E.g., Wang (1981), pp. 3–4, and Barwise (1978).
  2. Prawitz (1965).
  3. Girard, Lafont, and Taylor (1988).

References[editar | editar código-fonte]