# 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$
$\vdash A\lor \neg A$
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$
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$
Exercício: Prove $\vdash \left(A\to \neg A\right)\to \neg A$
$\{A,A\to B\}\vdash B\qquad \left(MP\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)$
$\{A\to B,B\to C\}\vdash A\to C$
$\neg A\lor \neg B\vdash \neg \left(A\land B\right)$