Teoria da prova

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.

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

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. 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, 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

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.

References

• J. Avigad, E.H. Reck (2001). “Clarifying the nature of the infinite”: the development of metamathematics and proof theory. Carnegie-Mellon Technical Report CMU-PHIL-120.
• J. Barwise (ed., 1978). Handbook of Mathematical Logic. North-Holland.
• 2πix.com: Logic Part of a series of articles covering mathematics and logic.
• A. S. Troelstra, H. Schwichtenberg (1996). Basic Proof Theory. In series Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, ISBN 0-521-77911-1.
• G. Gentzen (1935/1969). Investigations into logical deduction. In M. E. Szabo, editor, Collected Papers of Gerhard Gentzen. North-Holland. Translated by Szabo from “Untersuchungen über das logische Schliessen”, Mathematisches Zeitschrift 39: 176-210, 405-431.
• Luis Moreno & Bharath Sriraman (2005).Structural Stability and Dynamic Geometry: Some Ideas on Situated Proof. International Reviews on Mathematical Education. Vol. 37, no.3, pp. 130–139 [1]
• J. von Plato (2008). The Development of Proof Theory. Stanford Encyclopedia of Philosophy.
• Wang, Hao. Popular Lectures on Mathematical Logic. [S.l.]: Van Nostrand Reinhold Company, 1981. ISBN 0442231091