Na lógica matemática, teoria da prova estrutural é a especialidade da teoria da prova que estuda cálculos prova que suportam uma noção de prova analítica.
Prova Analítica
A noção de prova analítica foi introduzida na teoria da prova por Gerhard Gentzen para o cálculo de sequentes; as provas analíticas são aquelas que são livres-de-corte. Seu cálculo dedução natural também suporta uma noção de prova analítica, como foi mostrado por Dag Prawitz; a definição é um pouco mais complexa - dizemos que as provas analíticas são as formas normais, que estão relacionados à noção de forma normal em rescrita de termos.
Estruturas e conectivos
O termo estrutura em teoria da prova estrutural vem de uma noção técnica introduzida no cálculo de sequentes: o cálculo de sequentes representa o julgamento feito em qualquer fase de uma inferência usando, operadores extra-lógicos especiais que chamamos de operadores estruturais: em as vírgulas à esquerda da catraca são operadores normalmente interpretados como conjunções, os à direita como disjunções, enquanto o símbolo catraca é interpretado como uma implicação. No entanto, é importante notar que há uma diferença fundamental de comportamento entre estes operadores e os conectivos lógicos pelos quais são interpretados no cálculo de sequentes: os operadores estruturais são utilizados em todas as regras do cálculo, e não são considerados quando se pergunta se a propriedade da subfórmula se aplica. Além disso, as regras lógicas seguem um único caminho: a estrutura lógica é introduzido por regras lógicas, e não podem ser eliminadas uma vez criadas, enquanto que os operadores estruturais podem ser introduzidos e eliminados no decorrer de uma derivação.
A ideia de olhar para as características sintáticas de cálculo de sequentes, como operadores especias não-lógicos não é velha, e foi forçada por inovações na teoria da prova: quando os operadores estruturais são tão simples como no cálculo de sequentes original de Getzen há pouca necessidade de analisá-los, mas cálculos de prova de inferência profunda, como os operadores estruturais exibidos de apoio lógica tão complexos como os conectivos lógicos, exigem um tratamento sofisticado.
