Eliminação de Corte

A eliminação de corte é o teorema de Gentzen de que a regra de corte, que formaliza o uso de lemas, pode ser removida de qualquer prova de cálculo de sequentes, deixando uma prova construída apenas a partir das fórmulas que ela concerne.

Definition

A eliminação de corte é o teorema e o procedimento construtivo que demonstra que qualquer derivação de cálculo de sequentes que utiliza a regra de corte pode ser transformada em uma que não a utiliza, de modo que cada sequente provável tenha uma prova na qual aparecem apenas subfórmulas do sequente final.

Scope

Este tópico aborda a regra de corte e seu papel no cálculo de sequentes, o procedimento de eliminação de corte e sua terminação, a propriedade da subfórmula de provas sem corte, as consequências resultantes de consistência e decidibilidade, e os limites no tamanho da prova que a eliminação pode acarretar.

Core questions

• O que a regra de corte expressa e por que sua remoção é significativa?
• Como o procedimento de eliminação de corte termina?
• O que é a propriedade da subfórmula e o que ela implica para a busca de provas?
• Qual é o custo computacional da eliminação de cortes?

Key theories

Gentzen Hauptsatz

O teorema principal de Gentzen afirma que a regra de corte é admissível no cálculo de sequentes, de modo que qualquer prova que utilize cortes pode ser convertida em uma prova sem cortes do mesmo sequente final.

Propriedade da subfórmula

Cada fórmula que ocorre em uma prova sem cortes é uma subfórmula do sequente final, o que restringe a forma da prova e fundamenta procedimentos de decisão e argumentos de consistência.

Consistência via eliminação de corte

Como uma prova sem cortes do sequente vazio é impossível, a eliminação de corte fornece uma prova direta de que o cálculo, e, portanto, a teoria que ele formaliza, é consistente.

Clinical relevance

A eliminação de corte é um resultado fundamental com amplas consequências: ela produz provas de consistência, a propriedade da subfórmula essencial para a prova automática de teoremas e métodos de tableau, teoremas de interpolação e, através da correspondência provas-como-programas, a normalização de programas tipados.

History

Gentzen provou a eliminação de corte, seu Hauptsatz, em 1934 para a lógica de primeira ordem, e o método tornou-se a pedra angular da teoria da prova estrutural. Tait e Girard estenderam a técnica para sistemas mais fortes e lógica de ordem superior, e os limites no crescimento do tamanho da prova sob eliminação de corte tornaram-se um objeto de estudo por si só.

Key figures

• Gerhard Gentzen
• William Tait
• Jean-Yves Girard
• Gaisi Takeuti

Seminal works

• takeuti1987
• troelstra2000
• negri2001

Frequently asked questions

O que é um corte em uma prova?

A regra de corte permite provar um lema e depois usá-lo: a partir de uma derivação que estabelece uma fórmula e outra que usa essa fórmula como premissa, ela conclui o resultado combinado. A eliminação de corte mostra que tais lemas intermediários podem sempre ser removidos em princípio.

Por que a eliminação de cortes pode tornar as provas muito mais longas?

Remover um corte pode exigir a duplicação de grandes partes de uma derivação, e a iteração disso pode aumentar o tamanho da prova por uma torre de exponenciais. Assim, as provas sem cortes são conceitualmente mais simples, mas podem ser vastamente maiores do que as provas originais com cortes.