A teoria da prova , também conhecido sob o nome de teoria da prova (do Inglês teoria da prova ) é um ramo da lógica matemática . Foi fundada por David Hilbert no início do XX ° século .
Hilbert propôs esta nova disciplina matemática em sua famosa declaração no 2 º Congresso Internacional de Matemática em 1900 com o objetivo de demonstrar a consistência da matemática. Este objetivo foi invalidado pelo não menos famoso teorema da incompletude de Gödel em 1931, que no entanto não impediu que a teoria da demonstração se desenvolvesse, em particular graças ao trabalho de Jacques Herbrand e Gerhard Gentzen . Este último demonstrou um dos principais resultados da teoria da prova, conhecido como Hauptsatz (teorema principal) ou teorema da eliminação do corte . Gentzen então usou este teorema para dar a primeira prova puramente sintática da consistência da aritmética .
Depois de um período de calma, que mesmo assim permitiu estabelecer uma série de outros resultados de relativa coerência e esboçar uma classificação das teorias axiomáticas, a teoria da prova sofreu um renascimento espetacular durante os anos 1960. com a descoberta do Curry. -Correspondência de modo que exibia uma nova e profunda ligação estrutural entre lógica e computação: essencialmente, o procedimento de eliminação de cortes definido por Gentzen pode ser visto como um processo computacional, de forma que as provas formais tornam-se programas cujo tipo é a proposição a ser demonstrada. Desde então, a teoria da prova se desenvolveu em simbiose próxima com outros campos da lógica e da ciência da computação teórica, notadamente lambda-cálculo , e deu origem a novos modelos de cálculo, sendo o mais recente a lógica linear de Jean-Yves Girard em 1986. Hoje, parte da teoria da prova se funde com a semântica das linguagens de programação e interage com muitas outras disciplinas da lógica e da informática teórica: