Teorema da eliminação do corte

O teorema da eliminação do corte (ou Hauptsatz de Gentzen) é o resultado central que estabelece a significância do cálculo de sequentes. Foi originalmente provado por Gerhard Gentzen em 1934, no seu definidor artigo "Investigations in Logical Deduction", para os sistemas LJ e LK, formalizando as lógicas intuicionista e clássica, respectivamente. O teorema da eliminação do corte diz que qualquer derivação que possui uma prova no cálculo de sequentes que utiliza a regra do corte também possui uma prova que não a utiliza.

Um sequente é uma expressão lógica que relaciona múltiplas sentenças, na forma "$A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots$", que deve ser lida como "A₁, A₂, A₃, $\ldots$ prova B₁, B₂, B₃, $\ldots$", e (como comentado por Gentzen) deve ser entendida como equivalente à função verdade "Se (A₁ e A₂ e A₃ $\ldots$) então (B₁ ou B₂ ou B₃ $\ldots$)." Note que o lado esquerdo do sequente (LE) é uma conjunção (e) e o lado direito (LD) é uma disjunção (ou).

O LE pode ter uma quantidade arbitrária de fórmulas; quando o LE é vazio, o LD é uma tautologia. No sistema LK, o LD também pode ter qualquer número de fórmulas - se não possui alguma, o LE é uma contradição, enquanto que no sistema LJ o LD pode apenas possuir uma ou nenhuma fórmula: aqui nós vemos que permitir mais de uma fórmula no LD é equivalente, na presença da regra de contração correta, à admissibilidade da lei do terceiro excluído. No entanto, o cálculo de sequentes é uma ferramenta bastante expressiva, e existiram proposições de cálculos de sequente para a lógica intuicionista que permitem muitas fórmulas no LD. Da lógica LC de Jean-Yves Girard é fácil obter uma formalização bastante natural da lógica clássica onde o LD contém no máximo uma fórmula; o diálogo das regras lógicas e estruturais é a chave neste ponto.

O "Corte" é uma regra na formulação normal do cálculo de sequentes, e é equivalente a uma variedade de regras em outras teorias de prova, em que, dados

(1) $\Gamma \vdash A,\Delta$

e

(2) $\Pi ,A\vdash \Lambda$

pode-se inferir

(3) $\Gamma ,\Pi \vdash \Delta ,\Lambda .$

Isto é, ela "corta" as ocorrências da fórmula "A" da relação inferencial. O teorema da eliminação do corte diz que (para um dado sistema) qualquer sequente provável utilizando a regra do corte pode ser provado sem o uso desta regra.

Para os cálculos de sequentes que possuem apenas uma fórmula no LD, a regra do corte é: dados

(1) $\Gamma \vdash A$

e

(2) $\Pi ,A\vdash B$

pode-se inferir

(3) $\Gamma ,\Pi \vdash B.$

Se $B$ é um teorema, então a eliminação do corte neste caso simplesmente diz que um lema $A$ utilizado na prova desse teorema pode ser englobado. Sempre que a prova do teorema menciona o lema $A$, nós podemos substituir as ocorrências pela prova de $A$. Consequentemente, a regra do corte é admissível.

Para sistemas formulados no cálculo de sequentes, provas analíticas são aquelas que não utilizam a regra do corte. Tipicamente, uma prova deste tipo será maior, claro, e não necessariamente de maneira trivial. No seu ensaio "Don't Eliminate Cut!", George Boolos demonstrou que existia uma derivação que podia ser completada em uma página usando a regra do corte, mas cuja prova analítica não poderia ser completada durante toda a existência do universo.

O teorema possui muitas e ricas consequências:

• Um sistema é inconsistente se admite uma prova do absurdo. Se o sistema tem um teorema de eliminação do corte, então, se ele possui uma prova do absurdo, ou do sequente vazio, ele também deve ter uma prova do absurdo (ou do sequente vazio) sem cortes. É tipicamente muito fácil demonstrar que não existem tais provas. Então, uma vez que é provada a posse do teorema da eliminação do corte por um sistema, é geralmente imediato o fato de que o sistema é consistente.
• Normalmente o sistema também tem, ao menos na lógica de primeira ordem, a propriedade da subfórmula, uma propriedade importante em várias abordagens da semântica prova-teórica.

A eliminação do corte é uma das ferramentas mais poderosas para provar o teorema da interpolação. A possibilidade de conduzir busca de prova baseada na resolução, o insight essencial que levou a linguagem de programação Prolog, dependem da admissibilidade do corte no sistema apropriado.

Para sistemas de provas baseados em cálculo lambda tipado de alta ordem através de um isomorfismo de Curry–Howard, algoritmos de eliminação do corte correspondem à propriedade de normalização forte (todo termo de prova é reduzido num número finito de passos em uma forma normal).

Referências

• Gentzen, Gerhard (1934–1935). «Untersuchungen über das logische Schließen». Mathematische Zeitschrift. 39: 405–431. doi:10.1007/BF01201363 
• Gentzen, Gerhard (1964). «Investigations into logical deduction». American Philosophical Quarterly. 1 (4): 249–287 
• Gentzen, Gerhard (1965). «Investigations into logical deduction». American Philosophical Quarterly. 2 (3): 204–218 
• Untersuchungen über das logische Schließen I
• Untersuchungen über das logische Schließen II^{[ligação inativa]}

Ligações externas

• Alex Sakharov. «Cut Elimination Theorem». MathWorld (em inglês)