(Para se ter uma idéia do estado atual da área veja Proof Theory on the eve of Year 2000, por S. Feferman.)
Dedução Natural: Em 1935 Gentzen propõe uma teoria da dedução baseada nas regras de manuseio de suposições em lugar da usual formulação axiomãtica na qual praticamente não há lugar para o raciocínio hipotético. O seu propósito era construir um sistema formal que se aproximasse ao máximo do modo de raciocínio humano. Como resultado desse propósito, Gentzen apresenta um cálculo de dedução para a lógica intuicionística, o cálculo NJ, e um cálculo para a lógica clássica, o cálculo NK. Esses sistemas ficaram conhecidos como sistemas de dedução natural (DN). No sistema de dedução natural as regras de inferência são projetadas num padrão de regras de introdução e eliminação, que seguem o princípio da inversão: a regra de eliminação é o inverso da regra de introdução. A partir desse princípio, Prawitz (1965) analisa as principais propriedades dos sistemas de dedução natural e apresenta uma das suas principais contribuições para a dedução natural: a normalização de provas.
Cálculo de Seqüentes: O cálculo de seqüentes, também proposto por Gentzen, é um sistema dedutivo extremamente rico usado não somente para construir provas mas também para estudar as meta-propriedades dos sistemas lógicos sob a perspectiva da Teoria da Prova. Devido a certas assimetrias inerentes às regras da dedução natural, Gentzen propôs o cálculo de seqüentes com o intuito principal de demonstrar o Hauptsatz, também chamado de Teorema da Eliminação do Corte, para a lógica clássica de forma mais conveniente. O teorema diz que toda prova pode ser transformada em uma prova normal, canônica, padrão.
Lógica Linear: A lógica linear, introduzida por Girard em 1987, se tornou bastante popular na comunidade de ciência da computação. A grande novidade é a existência de novos conectivos que formam um novo sistema lógico com várias características interessantes, como por exemplo a possibilidade de se interpretar um seqüente como um estado de um sistema, assim como o tratamento de uma fórmula como um recurso. Um outro aspecto considerado na literatura como bastante inovativo é a noção de redes-de-prova (do inglês, proof-nets). A idéia é trabalhar com uma representação "grafo-teórica" para as deduções na lógica linear. Girard define estruturas-de-prova, i.e. grafos de prova, chamados por ele de "a dedução natural do cálculo de seqüentes linear", utilizando a noção de links, que são relações entre ocorrências de fórmulas. Aquelas estruturas-de-prova que representam provas logicamente corretas são chamadas de redes-de-prova. Um dos aspectos talvez mais interessantes da teoria de redes-de-prova é a possibilidade de caracterizar dentro da classe de estruturas-de-prova a subclasse de redes-de-prova através de critérios puramente "geométricos/algébricos", i.e. baseados apenas na estrutura dos grafos de prova.
Sabe-se muito bem NP=co-NP se e somente se todas as tautologias proposicionais têm provas "curtas". Mas as conexões entre comprimento de provas e teoria da complexidade vão muito mais além. Limites inferiores em circuitos são intimamente ligados aos limites de comprimento de prova em sistemas formais restritos, e avanços em uma das frentes frequentemente leva a progressos na outra.
Restringindo a complexidade de passos de inferência dentro de uma prova, pode-se obter um fragmento da Aritmética de Peano chamado de Aritmética Limitada (Bounded Arithmetic), que define exatamente os predicados na hierarquia polinomial. Trabalhos recentes e bastante promissores têm mostrado que se certas teorias de aritmética cotada podem provar limites inferiores em teoria da complexidade, então os sistemas criptográficos correspondentes não poderão ser seguros.
Um resultado bastante importante sobre a estrutura das derivações é o teorema da eliminação do corte para o cálculo de seqüentes, dado por Gentzen em 1935. Prawitz em 1965, estendeu esse resultado para o sistema de dedução natural (teorema da normalização). Esses teoremas são de fundamental importância, pois eles garantem que se existe uma prova para uma dada fórmula, essa prova, chamada de normal ou sem cortes, tem uma determinada forma, além de possuir certas propriedades.
Vários estudos estão relacionados à estrutura de provas
formais. Zucker (1974) e Ungar (1992) analisam a relação entre o
teorema da eliminação do corte e o teorema da
normalização.
A. Carbone (1996-9) propõe um modelo
combinatório para estudar a expansão de provas após o
processo de eliminação do corte. Esse modelo se baseia na
noção de logical flow graph, originalmente definida
por S. Buss em 1991.
Girard (1987) propõe o estudo da geometria das
deduções através de um conceito bastante inovativo:
proof-net, grafos de provas do cálculo de seqüentes
linear. O seu traballho no entanto, se aplica à Lógica Linear.
Statman (1974) propõe, em sua tese de doutorado, o estudo da
complexidade estrutural de derivações em dedução
natural através da imersão de grafos de prova em
superfícies. Embora não haja evidências na literatura de que tal linha de pesquisa tenha continuado,
é importante ressaltar o pionerismo de sua abordagem.
Statman foi, aparentemente, quem primeiro observou que para passar do estudo de validade de
provas para o estudo de sua estrutura, a melhor maneira de fazê-lo
é analisar a prova como um objeto geométrico.
Numa abordagem à teoria das redes-de-prova da lógica linear não-comutativa baseada na "teoria das tranças" (do inglês, braids, cf. E. Artin, "Theory of braids", Annals of Mathematics 48:101-126, 1947), A. Fleury (La règle d'échange: logique linéaire multiplicative tressée. PhD thesis, Univ. Paris 7. November 1996) leva a idéia às últimas conseqüências, argumentando que "la géometrisation des preuves est en effet la meilleure garantie de leur pureté mathématique, elle évite de faire preuve de trop mauvais goût logique (il s'agit en effet de fonder la logique sur les mathématiques et non le contraire)" (pág. 4).
Última atualização: 22 de Março de 2005, 09:09:57 GMT-0200.