Mostrar código-fonte de Teorema da eliminação do corte

{{Má tradução|data=setembro de 2021}}
{{Reciclagem|data=abril de 2013}}
{{revisão|data=abril de 2013}}

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 [[lógica intuicionista|intuicionista]] e [[lógica clássica|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 "<math>A_1, A_2, A_3, \ldots \vdash B_1, B_2, B_3, \ldots</math>", que deve ser lida como "A<sub>1</sub>, A<sub>2</sub>, A<sub>3</sub>, <math>\ldots</math> prova B<sub>1</sub>, B<sub>2</sub>, B<sub>3</sub>, <math>\ldots</math>", e (como comentado por Gentzen) deve ser entendida como equivalente à função verdade "Se (A<sub>1</sub> e A<sub>2</sub> e A<sub>3</sub> <math>\ldots</math>) então (B<sub>1</sub> ou B<sub>2</sub> ou B<sub>3</sub> <math>\ldots</math>)."<ref>Wilfried Buchholz, [http://www.mathematik.uni-muenchen.de/~buchholz/articles/beweisth.ps Beweistheorie] (aulas universitárias sobre eliminação do corte), German, 2002-2003)</ref> 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 (lógica)|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 [[teoria da prova|teorias de prova]], em que, dados

: (1) <math> \Gamma \vdash A,\Delta</math>

e

: (2) <math> \Pi, A \vdash \Lambda</math>

pode-se inferir

: (3) <math>\Gamma, \Pi \vdash \Delta,\Lambda.</math>

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) <math> \Gamma \vdash A</math>

e

: (2) <math> \Pi, A \vdash B</math>

pode-se inferir

: (3) <math>\Gamma, \Pi \vdash B.</math>

Se <math>B</math> é um teorema, então a eliminação do corte neste caso simplesmente diz que um lema <math>A</math> utilizado na prova desse teorema pode ser englobado. Sempre que a prova do teorema menciona o [[Lema (matemática)|lema]] <math>A</math>, nós podemos substituir as ocorrências pela prova de <math>A</math>. Consequentemente, a regra do corte é [[regra admissível|admissível]].

Para sistemas formulados no cálculo de sequentes, [[prova analítica|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 é [[consistência|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 [[Interpolação de Craig|teorema da interpolação]]. A possibilidade de conduzir busca de prova baseada na [[Princípio da resolução|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|isomorfismo de Curry&ndash;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 ==
* {{citar periódico|primeiro =Gerhard |último =Gentzen |autorlink =Gerhard Gentzen |título=Untersuchungen über das logische Schließen |periódico=Mathematische Zeitschrift | volume=39 |páginas=405–431 |ano=1934–1935 | doi=10.1007/BF01201363}}
* {{citar periódico|primeiro =Gerhard |último =Gentzen |título=Investigations into logical deduction |periódico=American Philosophical Quarterly | volume=1 |número=4 |páginas=249–287 |ano=1964}}
* {{citar periódico|primeiro =Gerhard |último =Gentzen |título=Investigations into logical deduction |periódico=American Philosophical Quarterly | volume=2 |número=3 |páginas=204–218 |ano=1965}}
* [https://web.archive.org/web/20151224194624/http://gdz.sub.uni-goettingen.de/dms/load/img/?IDDOC=17178  Untersuchungen über das logische Schließen I ]
* [http://gdz.sub.uni-goettingen.de/dms/load/img/?IDDOC=17188  Untersuchungen über das logische Schließen II]{{Ligação inativa|1=data=maio de 2019 }}
{{Reflist}}

== Ligações externas ==
* {{MathWorld | urlname=CutEliminationTheorem | title=Cut Elimination Theorem | author=Alex Sakharov}}

[[Categoria:Lógica]]
[[Categoria:Lógica matemática]]