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 demonstrar 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,\mathrm{...},An⊢B1,\mathrm{...},Bm$

Essa expressão deve ser interpretada da seguinte maneira: se $A1,\mathrm{...},An$ forem todos verdadeiros então pelo menos um $Bi$ em $B1,\mathrm{...},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{\#}⊢)$:

• (axioma): $\frac{}{\phi ⊢\phi }$

• (corte): $\frac{\mathrm{\Gamma }⊢\mathrm{\Delta },\phi \mathrm{\Sigma },\phi ⊢\mathrm{\Psi }}{\mathrm{\Gamma },\mathrm{\Sigma }⊢\mathrm{\Delta },\mathrm{\Psi }}$

• $(⊢\to ):\frac{\mathrm{\Gamma },\phi ⊢\psi ,\mathrm{\Delta }}{\mathrm{\Gamma }⊢\phi \to \psi ,\mathrm{\Delta }}$

• $(\to ⊢):\frac{\mathrm{\Gamma }⊢\phi ,\mathrm{\Delta }\mathrm{\Sigma },\psi ⊢\mathrm{\Pi }}{\mathrm{\Gamma },\mathrm{\Sigma },\phi \to \psi ⊢\mathrm{\Delta },\mathrm{\Pi }}$

• $(⊢\wedge ):\frac{\mathrm{\Gamma }⊢\phi ,\mathrm{\Delta }\mathrm{\Gamma }⊢\psi ,\mathrm{\Delta }}{\mathrm{\Gamma }⊢\phi \wedge \psi ,\mathrm{\Delta }}$

• $(\wedge ⊢):\frac{\mathrm{\Gamma },\phi ,\psi ⊢\mathrm{\Delta }}{\mathrm{\Gamma },\phi \wedge \psi ⊢\mathrm{\Delta }}$

• $(⊢\vee ):\frac{\mathrm{\Gamma }⊢\phi ,\psi ,\mathrm{\Delta }}{\mathrm{\Gamma }⊢\phi \vee \psi ,\mathrm{\Delta }}$

• $(\vee ⊢):\frac{\mathrm{\Gamma },\phi ⊢\mathrm{\Delta }\mathrm{\Gamma },\psi ⊢\mathrm{\Delta }}{\mathrm{\Gamma },\phi \vee \psi ⊢\mathrm{\Delta }}$

• $(⊢\mathrm{\neg }):\frac{\mathrm{\Gamma },\phi ⊢\mathrm{\Delta }}{\mathrm{\Gamma }⊢\mathrm{\neg }\phi ,\mathrm{\Delta }}$

• $(⊢\mathrm{\neg }):\frac{\mathrm{\Gamma }⊢\phi ,\mathrm{\Delta }}{\mathrm{\Gamma },\mathrm{\neg }\phi ⊢\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.

• (comutatividade): $\frac{\mathrm{\Gamma },\phi ,\psi ,\mathrm{\Sigma }⊢\mathrm{\Delta }}{\mathrm{\Gamma },\psi ,\phi ,\mathrm{\Sigma }⊢\mathrm{\Delta }}$

• (monotonicidade): $\frac{\mathrm{\Gamma }⊢\mathrm{\Delta }}{\mathrm{\Gamma },\phi ⊢\mathrm{\Delta }}$

• (contração): $\frac{\mathrm{\Gamma },\phi ,\phi ⊢\mathrm{\Delta }}{\mathrm{\Gamma },\phi ⊢\mathrm{\Delta }}$

Metateoremas

Para provar a consistência 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 Consistência: O cálculo de seqüêntes é consistente

Teoremas e Inferências

$⊢A\to A$

$\frac{}{A⊢A}(Ax.)$
$\frac{}{⊢A\to A}(⊢\to )$

$⊢A\vee \mathrm{\neg }A$

$\frac{}{A⊢A}(Ax.)$
$\frac{}{⊢\mathrm{\neg }A,A}(⊢\mathrm{\neg })$
$\frac{}{⊢A,\mathrm{\neg }A}(com.)$
$\frac{}{⊢A\vee \mathrm{\neg }A}(⊢\vee )$

Observação: A partir deste ponto, por questões de economia, omitiremos o uso da regra de comutatividade.

$\{A\vee B,\mathrm{\neg }A\}⊢B$

$\frac{{\overline{A⊢A}}^{(Ax.)}}{A⊢A,B}(mon.)\frac{{\overline{B⊢B}}^{(Ax.)}}{B⊢A,B}(mon.)$
$\frac{}{A\vee B⊢A,B}(\vee ⊢)$
$\frac{}{A\vee B,\mathrm{\neg }A⊢B}(\mathrm{\neg }⊢)$

Exercício: Prove $⊢((A\vee B)\wedge \mathrm{\neg }A)\to B$

$⊢(\mathrm{\neg }A\to A)\to A$

$\frac{{\overline{A⊢A}}^{(Ax.)}}{⊢\mathrm{\neg }A,A}(⊢\mathrm{\neg })\frac{}{A⊢A}(Ax.)$
$\frac{}{\mathrm{\neg }A\to A⊢A}(\to ⊢)$
$\frac{}{⊢(\mathrm{\neg }A\to A)\to A}(⊢\to )$

Exercício: Prove $⊢(A\to \mathrm{\neg }A)\to \mathrm{\neg }A$

$\{A,A\to B\}⊢B\left(MP\right)$

$\frac{{\overline{A⊢A}}^{(Ax.)}}{A⊢A,B}(mon.)\frac{}{B⊢B}(Ax.)$
$\frac{}{A,A\to B⊢B}(\to ⊢)$

Exercício: Prove $\{\mathrm{\neg }B,A\to B\}⊢\mathrm{\neg }A\left(MT\right)$

$⊢(A\to (A\to B))\to (A\to B)$

${\overline{A,A\to B⊢B}}^{\left(MP\right)}\frac{{\overline{A⊢A}}^{(Ax.)}}{A⊢A,B}(mon.)$
 $\frac{}{A\to (A\to B),A⊢B}(\to ⊢)$
$\frac{}{A\to (A\to B)⊢A\to B}(⊢\to )$
$\frac{}{⊢(A\to (A\to B))\to (A\to B)}(⊢\to )$

$\{A\to B,B\to C\}⊢A\to C$

$\frac{{\overline{A,A\to B⊢B}}^{\left(MP\right)}}{A,A\to B,B\to C⊢B,C}(mon.3\times )\frac{{\overline{B,B\to C⊢C}}^{\left(MP\right)}}{A,A\to B,B\to C,B⊢C}(mon.3\times )$
$\frac{}{A\to B,B\to C⊢A\to C}\left(corte\right)$

$\mathrm{\neg }A\vee \mathrm{\neg }B⊢\mathrm{\neg }(A\wedge B)$

$\frac{{\overline{A⊢A}}^{(Ax.)}}{\mathrm{\neg }A,A,B⊢}(mon.,\mathrm{\neg }⊢)\frac{{\overline{B⊢B}}^{(Ax.)}}{\mathrm{\neg }B,A,B⊢}(mon.,\mathrm{\neg }⊢)$
$\frac{}{\mathrm{\neg }A\vee \mathrm{\neg }B,A,B⊢}(\vee ⊢)$
$\frac{}{\mathrm{\neg }A\vee \mathrm{\neg }B,A\wedge B⊢}(\wedge ⊢)$
$\frac{}{\mathrm{\neg }A\vee \mathrm{\neg }B⊢\mathrm{\neg }(A\wedge B)}(⊢\mathrm{\neg })$