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,...,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 )$:

• (axioma): ${\frac {}{\varphi \vdash \varphi }}$

• (corte): ${\frac {\Gamma \vdash \Delta ,\varphi \ \qquad \Sigma ,\varphi \vdash \Psi }{\Gamma ,\Sigma \vdash \Delta ,\Psi }}$

• $(\vdash \rightarrow ):{\frac {\Gamma ,\varphi \vdash \psi ,\Delta }{\Gamma \vdash \varphi \rightarrow \psi ,\Delta }}$

• $(\rightarrow \vdash ):{\frac {\Gamma \vdash \varphi ,\Delta \qquad \Sigma ,\psi \vdash \Pi }{\Gamma ,\Sigma ,\varphi \rightarrow \psi \vdash \Delta ,\Pi }}$

• $(\vdash \land ):{\frac {\Gamma \vdash \varphi ,\Delta \qquad \Gamma \vdash \psi ,\Delta }{\Gamma \vdash \varphi \land \psi ,\Delta }}$

• $(\land \vdash ):{\frac {\Gamma ,\varphi ,\psi \vdash \Delta }{\Gamma ,\varphi \land \psi \vdash \Delta }}$

• $(\vdash \lor ):{\frac {\Gamma \vdash \varphi ,\psi ,\Delta }{\Gamma \vdash \varphi \lor \psi ,\Delta }}$

• $(\lor \vdash ):{\frac {\Gamma ,\varphi \vdash \Delta \qquad \Gamma ,\psi \vdash \Delta }{\Gamma ,\varphi \lor \psi \vdash \Delta }}$

• $(\vdash \neg ):{\frac {\Gamma ,\varphi \vdash \Delta }{\Gamma \vdash \neg \varphi ,\Delta }}$

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

• (comutatividade): ${\frac {\Gamma ,\varphi ,\psi ,\Sigma \vdash \Delta }{\Gamma ,\psi ,\varphi ,\Sigma \vdash \Delta }}$

• (monotonicidade): ${\frac {\Gamma \vdash \Delta }{\Gamma ,\varphi \vdash \Delta }}$

• (contração): ${\frac {\Gamma ,\varphi ,\varphi \vdash \Delta }{\Gamma ,\varphi \vdash \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\vdash A$ não conseguimos chegar em $\vdash$ e portanto provamos o seguinte teorema:

Teorema da Consistência: O cálculo de seqüêntes é consistente

Teoremas e Inferências

$\vdash A\to A$

${\frac {}{A\vdash A}}\left(Ax.\right)$
${\frac {}{\vdash A\to A}}\left(\vdash \to \right)$

$\vdash A\lor \neg A$

${\frac {}{A\vdash A}}\left(Ax.\right)$
${\frac {}{\vdash \neg A,A}}\left(\vdash \neg \right)$
${\frac {}{\vdash A,\neg A}}\left(com.\right)$
${\frac {}{\vdash A\lor \neg A}}\left(\vdash \lor \right)$

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

$\{A\lor B,\neg A\}\vdash B$

${\frac {{\overline {A\vdash A}}^{\left(Ax.\right)}}{A\vdash A,B}}{\left(mon.\right)}\qquad {\frac {{\overline {B\vdash B}}^{\left(Ax.\right)}}{B\vdash A,B}}\left(mon.\right)$
${\frac {\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad }{A\lor B\vdash A,B}}\left(\lor \vdash \right)$
${\frac {}{A\lor B,\neg A\vdash B}}\left(\neg \vdash \right)$

Exercício: Prove $\vdash \left(\left(A\lor B\right)\land \neg A\right)\to B$

$\vdash \left(\neg A\to A\right)\to A$

${\frac {{\overline {A\vdash A}}^{\left(Ax.\right)}}{\vdash \neg A,A}}\left(\vdash \neg \right)\qquad \qquad {\frac {}{A\vdash A}}\left(Ax.\right)$
${\frac {\qquad \qquad \qquad \qquad \qquad \qquad \qquad }{\neg A\to A\vdash A}}\left(\to \vdash \right)$
${\frac {}{\vdash \left(\neg A\to A\right)\to A}}\left(\vdash \to \right)$

Exercício: Prove $\vdash \left(A\to \neg A\right)\to \neg A$

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

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

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

$\vdash \left(A\to \left(A\to B\right)\right)\to \left(A\to B\right)$

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

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

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

$\neg A\lor \neg B\vdash \neg \left(A\land B\right)$

${\frac {{\overline {A\vdash A}}^{\left(Ax.\right)}}{\neg A,A,B\vdash }}{\left(mon.,\neg \vdash \right)}\qquad {\frac {{\overline {B\vdash B}}^{\left(Ax.\right)}}{\neg B,A,B\vdash }}\left(mon.,\neg \vdash \right)$
${\frac {\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad }{\neg A\lor \neg B,A,B\vdash }}\left(\lor \vdash \right)$
${\frac {}{\neg A\lor \neg B,A\land B\vdash }}\left(\land \vdash \right)$
${\frac {}{\neg A\lor \neg B\vdash \neg \left(A\land B\right)}}\left(\vdash \neg \right)$

Esta página é um esboço de matemática. Ampliando-a você ajudará a melhorar o Wikilivros.