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

acima: Voltar para o índice de Cálculo Proposicional Clássico
anterior: Axiomática |

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\vdash 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 $\vdash$ 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 $\vdash$ 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 $\#$ possui uma regra de introdução a direita $(\vdash \#)$ e uma a esquerda $(\#\vdash )$:

• $(\vdash \rightarrow ):{\frac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}$
• $(\rightarrow \vdash ):{\frac {\Gamma _{1}\vdash A,\Delta _{1};\Gamma _{2},B\vdash \Delta _{2}}{\Gamma _{1},A\rightarrow B,\Gamma _{2}\vdash \Delta _{1},\Delta _{2}}}$
• $(\vdash \land ):{\frac {\Gamma \vdash A,\Delta ;\Gamma \vdash B,\Delta }{\Gamma \vdash A\land B,\Delta }}$
• $(\land \vdash ):{\frac {\Gamma ,A,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}$
• $(\vdash \lor ):{\frac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}$
• $(\lor \vdash ):{\frac {\Gamma ,A\vdash \Delta ;\Gamma ,B\vdash \Delta }{\Gamma ,A\lor B\vdash \Delta }}$
• $(\vdash \neg ):{\frac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \neg A,\Delta }}$
• $(\vdash \neg ):{\frac {\Gamma \vdash A,\Delta }{\Gamma ,\neg A\vdash \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\vdash A}}$
• (comutatividade): ${\frac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}$
• (monotonicidade): ${\frac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}$
• (contração): ${\frac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}$
• (corte): ${\frac {\Gamma _{1}\vdash \Delta _{1},A;\Gamma _{2},A\vdash \Delta _{2}}{\Gamma _{1},\Gamma _{2}\vdash \Delta _{1},\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\vdash A$ não conseguimos chegar em $\vdash$ e portanto provamos o seguinte teorema:

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