Lógica: Cálculo Proposicional Clássico: Cálculo de Sequêntes

Introdução

Uma outra, e não menos importante, forma de se calcular a validade de argumentos em lógica proposicional clássica é o chamado cálculo de sequêntes. O cálculo de sequêntes foi proposto por Gentzen na década de trinta como uma tentativa (bem-sucedida) de demostrar a consistência da lógica proposicional clássica.

O estudo do cálculo de sequentes é especialmente importante para a melhor compreensão de algumas lógicas não-clássicas em especial as lógicas sub-estruturais.

Notação

$A1,...,An⊢B1,...,Bm$

Essa expressão deve ser interpretada da seguinte maneira: se $A1,...,An$ forem todos verdadeiros então pelo menos um $Bi$ em $B1,...,Bn$ deve ser verdadeiro.

Por exemplo o sequênte $⊢$ indica que de vazio provamos vazio, ou seja, que a contradição é um teorema e portanto a lógica não é consistente. Em outras palavras: para provar que o cálculo de sequentes é consistente temos que mostrar que o sequente $⊢$ não é válido.

Regras

O calculo de sequêntes, como em todos as outras faces da sintática de qualquer lógica, possui regras de manipulação. Essas regras são divididas em dois tipos: regras lógicas e regras estruturais. As regras lógicas nos mostram como introduzir conectivos lógicos a esquerda e a direita em um sequente enquanto as regras estruturais, como o próprio nome diz são estruturais.

Regras Lógicas

Cada conectivo $\mathrm{\#}$ possui uma regra de introdução a direita $(⊢\mathrm{\#})$ e uma a esquerda $(\mathrm{\#}⊢)$:

• $(⊢\to ):\frac{\mathrm{\Gamma },A⊢B,\mathrm{\Delta }}{\mathrm{\Gamma }⊢A\to B,\mathrm{\Delta }}$
• $(\to ⊢):\frac{{\mathrm{\Gamma }}_1⊢A,{\mathrm{\Delta }}_1;{\mathrm{\Gamma }}_2,B⊢{\mathrm{\Delta }}_2}{{\mathrm{\Gamma }}_1,A\to B,{\mathrm{\Gamma }}_2⊢{\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2}$
• $(⊢\wedge ):\frac{\mathrm{\Gamma }⊢A,\mathrm{\Delta };\mathrm{\Gamma }⊢B,\mathrm{\Delta }}{\mathrm{\Gamma }⊢A\wedge B,\mathrm{\Delta }}$
• $(\wedge ⊢):\frac{\mathrm{\Gamma },A,B⊢\mathrm{\Delta }}{\mathrm{\Gamma },A\wedge B⊢\mathrm{\Delta }}$
• $(⊢\vee ):\frac{\mathrm{\Gamma }⊢A,\mathrm{\Delta }}{\mathrm{\Gamma }⊢A\vee B,\mathrm{\Delta }}$
• $(\vee ⊢):\frac{\mathrm{\Gamma },A⊢\mathrm{\Delta };\mathrm{\Gamma },B⊢\mathrm{\Delta }}{\mathrm{\Gamma },A\vee B⊢\mathrm{\Delta }}$
• $(⊢\mathrm{\neg }):\frac{\mathrm{\Gamma },A⊢\mathrm{\Delta }}{\mathrm{\Gamma }⊢\mathrm{\neg }A,\mathrm{\Delta }}$
• $(⊢\mathrm{\neg }):\frac{\mathrm{\Gamma }⊢A,\mathrm{\Delta }}{\mathrm{\Gamma },\mathrm{\neg }A⊢\mathrm{\Delta }}$

Regras Estruturais

A regra da associatividade é considerada implicitamente. As regras estruturais são idênticas a esquerda e a direita. Vamos mostrar só um dos lados para economizar espaço.

• (axioma): $\frac{}{A⊢A}$
• (comutatividade): $\frac{{\mathrm{\Gamma }}_1,A,B,{\mathrm{\Gamma }}_2⊢\mathrm{\Delta }}{{\mathrm{\Gamma }}_1,B,A,{\mathrm{\Gamma }}_2⊢\mathrm{\Delta }}$
• (monotonicidade): $\frac{\mathrm{\Gamma }⊢\mathrm{\Delta }}{\mathrm{\Gamma },A⊢\mathrm{\Delta }}$
• (contração): $\frac{\mathrm{\Gamma },A,A⊢\mathrm{\Delta }}{\mathrm{\Gamma },A⊢\mathrm{\Delta }}$
• (corte): $\frac{{\mathrm{\Gamma }}_1⊢{\mathrm{\Delta }}_1,A;{\mathrm{\Gamma }}_2,A⊢{\mathrm{\Delta }}_2}{{\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2⊢{\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2}$

Teoremas

Para provar a consistencia do cálculo de seqüêntes vamos primeiro enunciar um (meta)teorema importante no cálculo de seqüêntes:

Teorema da eliminação do corte: Tudo que pode ser provado pelo cálculo de seqüêntes pode ser provado sem usar a regra do corte.

As demais regras do cálculo de seqüêntes são chamadas de analíticas pois preservam os símbolos atômicos. Como a regra do corte não é necessária todos os símbolos atômicos são preservados de algum dos lados e portanto partindo de $A⊢A$ não conseguimos chegar em $⊢$ e portanto provamos o seguinte teorema:

Teorema da Consistencia: O cálculo de seqüêntes é consistênte