Teorema de eliminação de corte - Cut-elimination theorem

O teorema de eliminação do corte (ou Hauptsatz de Gentzen ) é o resultado central que estabelece a significância do cálculo sequente . Foi provado originalmente por Gerhard Gentzen em seu artigo de 1934 "Investigations in Logical Deduction" para os sistemas LJ e LK formalizando lógica intuicionista e clássica, respectivamente. O teorema da eliminação do corte afirma que qualquer julgamento que possua uma prova no cálculo sequente fazendo uso da regra de corte também possui uma prova livre de corte , ou seja, uma prova que não faz uso da regra de corte.

A regra de corte

Um sequente é uma expressão lógica que relaciona várias fórmulas, na forma " "${\ displaystyle A_ {1}, A_ {2}, A_ {3}, \ ldots \ vdash B_ {1}, B_ {2}, B_ {3}, \ ldots}$ , que deve ser lida como "${\ displaystyle A_ {1}, A_ {2}, A_ {3}, \ ldots}$ prova " e (conforme glosado por Gentzen) deve ser entendido como equivalente à função de verdade "Se ( e e ...) então ( ou ou …). " Observe que o lado esquerdo (LHS) é uma conjunção (e) e o lado direito (RHS) é uma disjunção (ou). ${\ displaystyle B_ {1}, B_ {2}, B_ {3}, \ ldots}$${\ displaystyle A_ {1}}$${\ displaystyle A_ {2}}$${\ displaystyle A_ {3}}$${\ displaystyle B_ {1}}$${\ displaystyle B_ {2}}$${\ displaystyle B_ {3}}$

O LHS pode ter arbitrariamente muitas ou poucas fórmulas; quando o LHS está vazio, o RHS é uma tautologia . Em LK, o RHS também pode ter qualquer número de fórmulas - se não tiver nenhum, o LHS é uma contradição , enquanto em LJ o RHS pode ter apenas uma fórmula ou nenhuma: aqui vemos que permitir mais de uma fórmula no RHS é equivalente, na presença da regra da contração correta, à admissibilidade da lei do terceiro excluído . No entanto, o cálculo sequente é uma estrutura bastante expressiva, e tem havido cálculos sequenciais para a lógica intuicionista proposta que permite muitas fórmulas no RHS. A partir da lógica LC de Jean-Yves Girard , é fácil obter uma formalização bastante natural da lógica clássica, onde a RHS contém no máximo uma fórmula; é a interação das regras lógicas e estruturais que é a chave aqui.

"Corte" é uma regra no enunciado normal do cálculo sequente , e equivalente a uma variedade de regras em outras teorias de prova , que, dado

1. ${\ displaystyle \ Gamma \ vdash A, \ Delta}$

e

2. ${\ displaystyle \ Pi, A \ vdash \ Lambda}$

permite inferir

3. ${\ displaystyle \ Gamma, \ Pi \ vdash \ Delta, \ Lambda}$

Ou seja, ele "corta" as ocorrências da fórmula da relação inferencial. ${\ displaystyle A}$

Eliminação de corte

O teorema de eliminação do corte afirma que (para um determinado sistema) qualquer sequência provável usando a regra Corte pode ser provada sem o uso desta regra.

Para cálculos sequentes que têm apenas uma fórmula no RHS, a regra "Cortar" lê, dado

1. ${\ displaystyle \ Gamma \ vdash A}$

e

2. ${\ displaystyle \ Pi, A \ vdash B}$

permite inferir

3. ${\ displaystyle \ Gamma, \ Pi \ vdash B}$

Se pensarmos em um teorema, então a eliminação de corte neste caso simplesmente diz que um lema usado para provar este teorema pode ser sequencial. Sempre que a prova do teorema menciona o lema , podemos substituir as ocorrências pela prova de . Conseqüentemente, a regra de corte é admissível . ${\ displaystyle B}$${\ displaystyle A}$ ${\ displaystyle A}$${\ displaystyle A}$

Consequências do teorema

Para sistemas formulados no cálculo sequente, as provas analíticas são aquelas que não usam Cut. Normalmente, essa prova será mais longa, é claro, e não necessariamente de maneira trivial. Em seu ensaio "Não elimine o corte!" George Boolos demonstrou que havia uma derivação que poderia ser completada em uma página usando cut, mas cuja prova analítica não poderia ser completada durante a vida do universo.

O teorema tem muitas consequências ricas:

• Um sistema é inconsistente se admite a prova do absurdo. Se o sistema possui um teorema de eliminação do corte, então se ele tem uma prova do absurdo, ou do sequente vazio, ele também deve ter uma prova do absurdo (ou do sequente vazio), sem cortes. Normalmente, é muito fácil verificar se essas provas não existem. Assim, uma vez que um sistema demonstra ter um teorema de eliminação de corte, normalmente é imediato que o sistema seja consistente.
• Normalmente também o sistema tem, pelo menos na lógica de primeira ordem, a propriedade da subfórmula , uma propriedade importante em várias abordagens da semântica da teoria da prova .

A eliminação de corte é uma das ferramentas mais poderosas para provar teoremas de interpolação . A possibilidade de realizar a busca de provas com base na resolução , o insight essencial que conduz à linguagem de programação Prolog , depende da admissibilidade do Cut no sistema adequado.

Para sistemas de prova baseados em cálculo lambda de ordem superior por meio de um isomorfismo de Curry-Howard , algoritmos de eliminação de corte correspondem à propriedade de normalização forte (cada termo de prova reduz em um número finito de etapas em uma forma normal ).

Veja também

• Teorema de dedução
• A prova de consistência de Gentzen para os axiomas de Peano

Notas

Referências

• Gentzen, Gerhard (1934-1935). "Untersuchungen über das logische Schließen". Mathematische Zeitschrift . 39 : 405–431. doi : 10.1007 / BF01201363 .
• Gentzen, Gerhard (1964). "Investigações em dedução lógica". American Philosophical Quarterly . 1 (4): 249–287.
• Gentzen, Gerhard (1965). "Investigações em dedução lógica". American Philosophical Quarterly . 2 (3): 204–218.
• Untersuchungen über das logische Schließen I
• Untersuchungen über das logische Schließen II
• Curry, Haskell Brooks (1977) [1963]. Fundamentos da lógica matemática . Nova York: Dover Publications Inc. ISBN 978-0-486-63462-3.
• Kleene, Stephen Cole (2009) [1952]. Introdução à metamatemática . Ishi Press International. ISBN 978-0-923891-57-2.
• Boolos, George (1984). "Não elimine o corte". Journal of Philosophical Logic . 13 (4): 373–378.

links externos

• Alex Sakharov. “Teorema da Eliminação do Corte” . MathWorld .
• Dragalin, AG (2001) [1994], "Sequent calculus" , Encyclopedia of Mathematics , EMS Press