Teoria da prova estrutural

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 $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ 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.

Eliminação do corte no cálculo de sequentes

Ver artigo principal: Eliminação do corte

Dedução natural deduction e a correspondência fórmulas-como-tipos

Ver artigo principal: Dedução natural

Dualidade lógica e harmonia

Ver artigo principal: Harmonia lógica

Cálculo de estruturas

Ver artigo principal: Cálculo de estruturas

Referências

• Sara Negri; Jan Von Plato (2001). Structural proof theory. [S.l.]: Cambridge University Press. ISBN 978-0-521-79307-0 
• Anne Sjerp Troelstra; Helmut Schwichtenberg (2000). Basic proof theory 2nd ed. [S.l.]: Cambridge University Press. ISBN 978-0-521-77911-1