LIMSwiki

A teoria das provas, teoria da prova ou teoria da demonstração é um ramo importante da lógica matemática^[1] que representa provas como objetos matemáticos, facilitando sua análise por técnicas matemáticas. Provas são tipicamente representadas por estruturas de dados definidas indutivamente, como listas simples, listas encadeadas, árvores, cada uma construída de acordo com os axiomas e regras de inferência do sistema lógico. Consequentemente, a teoria da prova é de natureza sintática, em contraste com a teoria dos modelos que é de natureza semântica.^[2] Juntamente com a teoria dos modelos, teoria axiomática dos conjuntos e a teoria da computabilidade, a teoria da prova é um dos chamados quatro pilares dos fundamentos da matemática.^[3] É também importante na lógica filosófica, onde os interesses principais estão na ideia de uma semântica prova-teórica, uma ideia que, para ser viável, depende de ideias técnicas da teoria da prova estrutural.

Algumas das principais áreas da teoria de prova incluem teoria da prova estrutural, análise ordinal, lógica da probabilidade, matemática reversa, mineração de prova, prova automática de teoremas e complexidade de prova. Muitas pesquisas também se concentram em aplicações em ciência da computação, linguística e filosofia.^[2]

Embora a formalização da logica tenha avançado bastante com o trabalho de pessoas como Gottlob Frege, Giuseppe Peano, Bertrand Russell e Richard Dedekind, a história da teoria da prova moderna é muitas vezes vista como estabelecida por David Hilbert, que iniciou o que é chamado de programa de Hilbert nos fundamentos da matemática. O trabalho de Kurt Gödel sobre a teoria da prova primeiro avançou, em seguida, refutou esse programa: o teorema da completude de Gödel, pareceu, inicialmente, anteceder bem o que aconteceria com a intenção de Hilbert de reduzir toda a matemática para um sistema formal finitista;^[4] depois, o teorema da incompletude de Gödel mostrou que isso é inatingível. Todo esse trabalho foi realizado com os cálculos de prova do sistema de Hilbert. Em paralelo, as fundações da teoria da prova estrutural estavam sendo descobertas. 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 forma independente, um sistema chamado de cálculo da dedução natural, com a introdução de Gentzen à ideia de simetria entre os fundamentos para afirmar proposições, expressas em Regras de introdução (dedução natural) e as consequências da aceitação das regras de eliminação, uma ideia que se mostrou muito importante na teoria da prova.^[5] Gentzen além de introduzir a ideia de cálculo sequente, um cálculo avançado que expressa melhor a dualidade dos conectivos lógicos,^[6] também fez avanços fundamentais na formalização da lógica intuicionista e forneceu a primeira prova combinatória da consistência dos axiomas de Peano. Juntos, a apresentação da dedução natural e o cálculo de sequentes, introduziram a ideia fundamental de prova analítica para a teoria da prova.

Artigo principal: Derivação formal

As provas informais da pratica matemática no dia-a-dia são diferentes das provas formais da teoria da prova. Eles são como esboços que permitem que um especialista reconstrua a prova formal pelo menos em princípio, dando tempo e paciência suficiente. Para a maioria dos matemáticos, escrever uma prova totalmente formal é pedante e muito trabalhoso para virar um uso comum. Provas formais são construídas para ajudar computadores na teoria da prova iterativa. Significativamente, essas provas podem ser verificadas automaticamente, também por computador. Normalmente, as verificações de provas formais são simples, enquanto que encontrar as provas (prova automática de teoremas) é geralmente difícil. Uma prova informal na literatura matemática, em contraste, requer semanas de <revisão por pares> para ser verificada, e ainda assim pode conter erros.

Os três mais conhecidos tipos de cálculo de prova são:

• Sistema de Hilbert;
• Dedução natural;
• Cálculo de sequentes.

Cada um desses pode retornar uma formalização completa e axiomática da lógica proposicional ou de predicado, tanto do tipo clássico ou intuicionista, quase qualquer lógica modal e muitas lógicas subestruturais, como a lógica linear por exemplo. Na verdade é raro encontrar uma lógica que resista em ser representado em um desses cálculos.

Como mencionado anteriormente, o estímulo para a investigação matemática de provas em teorias formais foi o programa de Hilbert. A ideia central deste programa era que, se fosse possível dar provas finitárias de consistência^[7] para todas as teorias formais sofisticadas necessárias para matemáticos, então poderíamos basear essas teorias por meio de um argumento matemático, o que mostra que todas as suas afirmações puramente universais, mais tecnicamente suas, demonstráveis, sentenças) são “finitariamente” verdade;^[8] uma vez tão fundamentada que nós não nos preocupamos com o significado não-finitário dos teoremas existenciais, em relação a estas estipulações pseudo-significativas sobre existência de entidades ideais. O fracasso do programa foi induzido pelo teorema da incompletude de Kurt Gödel, que mostrou que qualquer teoria w-consistente, que é suficientemente forte para expressar certas verdades aritméticas, não pode provar sua própria consistência, que na formulação de Gödel é uma sentença .

Muita investigação tem sido realizada sobre esse tema, o qual, em particular, levou a:

• Refinamento do resultado de Gödel, particularmente o refinamento de J. Barkley Rosser, enfraquecendo o requisito acima sobre w-consistência para consistência simples;
• Axiomatização do núcleo do resultado de Gödel em termos de uma linguagem modal, logica de demonstrabilidade;
• Iteração transfinita de teorias, devido a Alan Turing e Solomon Feferman;
• A recente descoberta da teoria da alto-verificação, sistemas fortes o suficiente para falar de si, entretanto, fracos para realizar o argumento diagonal que é a chave para o argumento da indemonstrabilidade de Gödel.

Veja também lógica matemática

Teoria da prova estrutural é a subdisciplina da teoria da prova que estuda o cálculo de prova que dá suporte a noção de prova analítica. A ideia de prova analítica foi introduzida por Gentzen para o cálculo de sequentes; estas são o teorema da eliminação do corte. Seu cálculo de dedução natural também dá suporte para o conceito de prova analítica, como mostrado por Dag Prawitz. A definição é ligeiramente mais complexa: dizemos que provas analíticas são as formas normais que estão relacionadas com o conceito de forma normal no termo reescrito. Cálculos de prova mais exóticos como as redes de prova de Jean-Yves Girard também favorecem o conceito de prova analítica. A teoria da prova estrutural está conectada com a teoria dos tipos, por meio do isomorfismo de Curry-Howard, o qual observa uma analogia estrutural entre o processo de normalização na dedução natural com a redução beta no cálculo tipo lambda. Isso fornece a base para a <teoria dos tipos intuicionista> desenvolvido por Per Martin-Löf, também é muitas vezes estendido a um isomorfismo de três vias, a terceira via sendo as categorias cartesianas fechadas.^[9]

Na linguística, gramática tipo-lógica, gramática categorial e gramática de Montague aplicam formalismos baseados na teoria da prova estrutural para dar uma semântica formal para a linguagem natural.

Artigo principal: Método dos Tableaux

Tableaux analíticos aplica a ideia central da prova analítica da teoria da prova estrutural para fornecer os procedimentos de decisão e semi-decisão para uma vasta gama de lógicas.

• Lógica intermediária
• Teoria dos modelos
• Prova matemática

• 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.
• D. Prawitz (1965). Natural deduction: A proof-theoretical study, Dover Publications, ISBN 978-0-486-44655-4
• 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.
• J.-Y. Girard, P. Taylor, Y. Lafont (1988). "Proofs and types". Cambridge University Press. ISBN 0-521-37181-3
• S. Buss, ed. (1998) Handbook of Proof Theory. Elsevier.
• S.G. Simpson (2010). Subsystems of Second-order Arithmetic, second edition. Cambridge University Press, ISBN 978-0521150149.
• Wang, Hao (1981). Popular Lectures on Mathematical Logic. [S.l.]: Van Nostrand Reinhold Company. ISBN 0442231091 

• Portal da matemática